Proof of proveit.logic.booleans.implication.not_true_via_contradiction theorem

import proveit
from proveit import defaults
from proveit.logic import Equals, NotEquals, Implies, Not, And, Forall, TRUE, FALSE, in_bool
from proveit import A
from proveit.logic.equality import not_equals_contradiction
theory = proveit.Theory() # the theorem's theory

%proving not_true_via_contradiction

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
not_true_via_contradiction:
(see dependencies)

AeqT = Equals(A, TRUE)

AeqT:

defaults.assumptions = not_true_via_contradiction.all_conditions() + [AeqT]

defaults.assumptions:

AeqT.deduce_in_bool()

 ⊢  

AeqT_impl_F = FALSE.prove().as_implication(AeqT)

AeqT_impl_F:  ⊢  

not_true_via_contradiction may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

AeqT_impl_F.derive_via_contradiction()

 ⊢  

We'll now by able to generate a proof-by-contradiction via automation.

%qed

proveit.logic.booleans.implication.not_true_via_contradiction has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , :
2	theorem		⊢
	proveit.logic.equality.fold_not_equals
3	instantiation	4, 5, 6	⊢
	:
4	axiom		⊢
	proveit.logic.booleans.implication.denial_via_contradiction
5	instantiation	7	⊢
	: , :
6	deduction	8	⊢
7	axiom		⊢
	proveit.logic.equality.equality_in_bool
8	modus ponens	9, 10	,  ⊢
9	assumption		⊢
10	instantiation	11, 12	⊢
	:
11	axiom		⊢
	proveit.logic.booleans.eq_true_elim
12	assumption		⊢