Proof of proveit.logic.booleans.disjunction.or_if_left theorem

import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic import in_bool, Or
theory = proveit.Theory() # the theorem's theory

%proving or_if_left

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

We will prove this using unfold_is_bool_explicit, proving $(B = \top) \lor (B = \bot)$, rather than unfold_is_bool to prove $B \lor (\lnot B)$. The latter would make this proof shorter, but requires constructive_dilemma which will use this theorem for convenience.

defaults.assumptions = or_if_left.all_conditions()

defaults.assumptions:

BeqT_or_BeqF = in_bool(B).unfold(assumptions=[in_bool(B)])

BeqT_or_BeqF:  ⊢  

BeqT = BeqT_or_BeqF.operands[0]

BeqT:

BeqF = BeqT_or_BeqF.operands[1]

BeqF:

By proving $\vdash (B = \top) \in \mathbb{B}$ and $\vdash (B = \bot) \in \mathbb{B}$ (under no assumptions) we can force the proof to be shorter than otherwise (since it automatically deduces these assuming $B \in \mathbb{B}$ in a convoluted manner).

in_bool(BeqT).prove(assumptions=[])

 ⊢  

in_bool(BeqF).prove(assumptions=[])

 ⊢  

Or(A, B).prove(assumptions=[A, BeqT])

,  ⊢  

Or(A, B).prove(assumptions=[A, BeqF])

,  ⊢  

BeqT_or_BeqF.derive_via_singular_dilemma(Or(A, B), assumptions=[in_bool(B), A])

,  ⊢  

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

%qed

proveit.logic.booleans.disjunction.or_if_left has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4, 5, 6, 7	,  ⊢
	: , : , :
2	theorem		⊢
	proveit.logic.booleans.disjunction.singular_constructive_dilemma
3	instantiation	8	⊢
	: , :
4	instantiation	8	⊢
	: , :
5	instantiation	9, 10	⊢
	:
6	deduction	11	⊢
7	deduction	12	⊢
8	axiom		⊢
	proveit.logic.equality.equality_in_bool
9	conjecture		⊢
	proveit.logic.booleans.unfold_is_bool_explicit
10	assumption		⊢
11	instantiation	13, 16, 14	,  ⊢
	: , :
12	instantiation	15, 16, 17	,  ⊢
	: , :
13	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_both
14	instantiation	18, 19	⊢
	:
15	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_only_left
16	assumption		⊢
17	instantiation	20, 21	⊢
	:
18	axiom		⊢
	proveit.logic.booleans.eq_true_elim
19	assumption		⊢
20	theorem		⊢
	proveit.logic.booleans.negation.negation_intro
21	assumption		⊢