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

In [1]:
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

In [2]:
%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.

In [3]:
defaults.assumptions = or_if_left.all_conditions()

defaults.assumptions:
In [4]:
BeqT_or_BeqF = in_bool(B).unfold(assumptions=[in_bool(B)])

BeqT_or_BeqF:
In [5]:
BeqT = BeqT_or_BeqF.operands[0]

BeqT:
In [6]:
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 [7]:
in_bool(BeqT).prove(assumptions=[])

In [8]:
in_bool(BeqF).prove(assumptions=[])

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

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

In [11]:
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".

In [12]:
%qed

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

Out[12]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, 4, 5, 6, 7,  ⊢
: , : , :
2theorem
proveit.logic.booleans.disjunction.singular_constructive_dilemma
3instantiation8
: , :
4instantiation8
: , :
5instantiation9, 10
:
6deduction11
7deduction12
8axiom
proveit.logic.equality.equality_in_bool
9conjecture
proveit.logic.booleans.unfold_is_bool_explicit
10assumption
11instantiation13, 16, 14,  ⊢
: , :
12instantiation15, 16, 17,  ⊢
: , :
13theorem
proveit.logic.booleans.disjunction.or_if_both
14instantiation18, 19
:
15theorem
proveit.logic.booleans.disjunction.or_if_only_left
16assumption
17instantiation20, 21
:
18axiom
proveit.logic.booleans.eq_true_elim
19assumption
20theorem
proveit.logic.booleans.negation.negation_intro
21assumption