# Demonstrations for the theory of proveit.logic.booleans.disjunction¶

In [1]:
import proveit
from proveit import defaults, ProofFailure
from proveit import A, B, C, D, E,F,G,H,I,J,K,L, m
from proveit.numbers import num, NaturalPos
from proveit.logic import Boolean, in_bool, InSet, Or, And, TRUE, FALSE, Not, Implies, Equals
from proveit.logic.booleans.disjunction import closure, each_is_bool
%begin demonstrations

In [2]:
closure

In [3]:
closure_spec = closure.instantiate({m:m}, assumptions=[InSet(m, NaturalPos)])

closure_spec:
In [4]:
closure.instantiate({m:num(4), A:C}, num_forall_eliminations=1)

In [5]:
demo1 = closure.instantiate({m:num(4), A:[A, B, C, D]}, assumptions=[in_bool(A), in_bool(B), in_bool(C), in_bool(D)])

demo1: , , ,  ⊢
In [6]:
demo1.element.deduce_part_in_bool(1, assumptions=[demo1.expr])

In [7]:
each_is_bool

In [ ]:


In [8]:
Or(TRUE, TRUE).prove()

In [9]:
Or(TRUE, FALSE).prove()

In [10]:
Or(FALSE, TRUE).prove()

In [11]:
Not(Or(FALSE, FALSE)).prove()

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

In [13]:
Or(A, B).prove(assumptions=[A, Not(B)])

In [14]:
Or(A, B).prove(assumptions=[B, Not(A)])

In [15]:
Not(Or(A, B)).prove(assumptions=[Not(A), Not(B)])

In [16]:
Or(A, B).derive_contradiction(assumptions=[Not(A), Not(B), Or(A, B)])

, ,  ⊢
In [17]:
Or(A, B).derive_left_if_not_right(assumptions=[in_bool(A), in_bool(B), Not(B), Or(A, B)])

, , ,  ⊢
In [18]:
Or(A, B).derive_right_if_not_left(assumptions=[*in_bool(A, B), Not(A), Or(A, B)])

, , ,  ⊢
In [19]:
Or(A, B).derive_via_dilemma(C, assumptions=[Or(A, B), in_bool(B), Implies(A, C), Implies(B, C), in_bool(A), Implies(A, Or(C, D)), Implies(B, Or(C, D))])

, , , ,  ⊢
In [20]:
Or(A, B, C, D).derive_via_dilemma(E, assumptions=[Or(A, B, C, D), Implies(A, E), Implies(B, E), Implies(C, E), Implies(D, E), in_bool(A), in_bool(B), in_bool(C), in_bool(D)])

, , , , , , , ,  ⊢
In [21]:
Or(A, B).prove(assumptions=[in_bool(B), A, in_bool(A)])

, ,  ⊢
In [22]:
Or(A, B).prove(assumptions=[in_bool(A), in_bool(B), B])

, ,  ⊢
In [23]:
Or(C, D).derive_via_dilemma(Or(C, D), assumptions=[Or(A, B), Or(C, D), Implies(A, C), Implies(A, C), Implies(B, D), in_bool(A), in_bool(B), in_bool(C), in_bool(D)])

, ,  ⊢
In [24]:
Or(A, B, C, D).derive_via_multi_dilemma(Or(H, I, J, K), assumptions=[Or(A, B, C, D), Implies(A, H), Implies(B, I), Implies(C, J), Implies(D, K), in_bool(A), in_bool(B), in_bool(C), in_bool(D), in_bool(H), in_bool(I), in_bool(J), in_bool(K)])

, , , , , , , , , , , ,  ⊢
In [25]:
Or(A, B, C, D).derive_via_dilemma(Or(H, I, J, K), assumptions=[Or(A, B, C, D), Implies(A, H), Implies(B, I), Implies(C, J), Implies(D, K),in_bool(A), in_bool(B), in_bool(C), in_bool(D), in_bool(H), in_bool(I), in_bool(J), in_bool(K)])

, , , , , , , , , , , ,  ⊢
In [26]:
Or(H, I, J, K).deduce_part_in_bool(2, assumptions=[Or(H, I, J, K)])


destructive_dilemma

In [27]:
Or(Not(C), Not(D)).derive_via_dilemma(Or(Not(A), Not(B)), assumptions=[Or(Not(C), Not(D)), Implies(A, C), Implies(B, D), in_bool(A), in_bool(B), in_bool(C), in_bool(D)])

, , , , , ,  ⊢
In [28]:
Or(Not(A), Not(B), Not(C), Not(D)).derive_via_dilemma(Or(Not(H), Not(I), Not(J), Not(K)), assumptions=[Or(Not(A), Not(B), Not(C), Not(D)),Implies(A,H), Implies(B,I), Implies(C,J), Implies(D,K),in_bool(A), in_bool(B), in_bool(C), in_bool(D), in_bool(H), in_bool(I), in_bool(J), in_bool(K)])

, , , , , , , , , , , ,  ⊢
In [29]:
Not(A).prove(assumptions=[Not(Or(A, B))])

In [30]:
Not(B).prove(assumptions=[Not(Or(A, B))])

In [31]:
reduction = Or(A).unary_reduction(assumptions=[in_bool(A)])

reduction:
In [32]:
in_bool(B).prove(assumptions=[in_bool(Or(A, B, C))])

In [33]:
Or(A, B, C).prove(assumptions=[A, in_bool(A), in_bool(B), in_bool(C)])

, , ,  ⊢
In [34]:
Not(Or(A, B, C)).prove(assumptions=[Not(A), Not(B), Not(C)])

, ,  ⊢
In [35]:
Or(A,B,C).derive_contradiction(assumptions=[Or(A,B,C), Not(A), Not(B), Not(C)])

, , ,  ⊢
In [36]:
group_c_d = Or(A,B,C,D,E,F,G).associate(2,length=2,assumptions=[Or(A,B,Or(C,D),E,F,G),Or(A,B,C,D,E,F,G),in_bool(A), in_bool(B),in_bool(C),in_bool(D),in_bool(E),in_bool(F),in_bool(G)])

group_c_d:
In [37]:
group_c_d.disassociate(2, assumptions=[group_c_d.expr])

In [38]:
Or(A,B,C,D,E).commutation(1,3, assumptions=in_bool(A,B,C,D,E))

, , , ,  ⊢
In [39]:
Or(A,B,C,D,E).commutation(-1,0, assumptions=in_bool(A,B,C,D,E))

, , , ,  ⊢
In [40]:
Or(A,B,C,D,E,F,G,H,I).commute(3, 5, assumptions=[Or(A,B,C,D,E,F,G,H,I), *in_bool(A,B,C,D,E,F,G,H,I)])

In [41]:
Or(A,B,C,D,E,F,G,H,I).commute(6, 3, assumptions=[Or(A,B,C,D,E,F,G,H,I), *in_bool(A,B,C,D,E,F,G,H,I)])

In [42]:
Or(A,B,C,D,E,F,G,H,I).group_commute(0, 3, length=2, assumptions=[Or(A,B,C,D,E,F,G,H,I), *in_bool(A,B,C,D,E,F,G,H,I)])

In [43]:
Or(A,B,C,D).group_commute(0, 1, length=2, assumptions=[Or(A,B,C,D)])

In [44]:
Or(A,B,C,D).group_commutation(1, 0, length=2, assumptions=in_bool(A,B,C,D))

, , ,  ⊢
In [45]:
And(A, B, Or(A,B,C,D)).inner_expr().operands[2].group_commutation(0, 1, length=2, assumptions=in_bool(A,B,C,D))

, , ,  ⊢
In [46]:
And(A, B, Or(A,B,C,D)).operands[2].group_commutation(0, 1, length=2, assumptions=[And(A, B, Or(A,B,C,D))], auto_simplify=False)

In [47]:
And(A, B, Or(A,B,C,D)).inner_expr().operands[2].group_commute(0, 1, length=2, assumptions=[And(A, B, Or(A,B,C,D))], auto_simplify=False)

In [48]:
Or(A,B,C,D,E,F,G,H).deduce_in_bool(assumptions=in_bool(A,B,C,D,E,F,G,H))

, , , , , , ,  ⊢

true_eval

In [49]:
Or(FALSE,FALSE,TRUE,FALSE,FALSE).evaluation()

In [50]:
Or(A,B,TRUE,C,D).evaluation(assumptions=[in_bool(A), in_bool(B), in_bool(C), in_bool(D)])

, , ,  ⊢

false_eval

In [51]:
Equals(Or(A,B,C,D),FALSE).prove(assumptions=[Equals(A,FALSE), Equals(B,FALSE),Equals(C,FALSE),Equals(D,FALSE)])

, , ,  ⊢
In [52]:
in_bool(Or(A,B)).prove(assumptions=[in_bool(A), in_bool(B)])

In [53]:
in_bool(Or(A,B,C,D)).prove(assumptions=[in_bool(A), in_bool(B), in_bool(C), in_bool(D)])

, , ,  ⊢
In [54]:
Or(A,B).prove(assumptions=[Not(And(Not(A), Not(B)))])

In [55]:
Or(A, B, C).prove(assumptions=[Not(And(Not(A),Not(B),Not(C)))])

In [56]:
# testing a simple Or.conclude() failure
try:
Or(A, B).conclude()
assert False, "Expecting a ProofFailure; should not get this far!"
except ProofFailure as the_error:
print("ProofFailure: {}".format(the_error))

ProofFailure: Unable to prove A or B:
Or.conclude() has failed to find a proof for the disjunction: (A or B)


### Automatically proving conjunctions are equal via permutation¶

In [57]:
defaults.assumptions = [Or(D, B, A, C)]

False
In [58]:
A.readily_provable(assumptions=[Or(D, B, A, C)])

False
In [59]:
Implies(Or(D, B, A, C), Or(A, C, B, D)).readily_provable()

False
In [60]:
eq = Equals(Or(D, B, A, C), Or(A, B, C, D))

eq:
In [61]:
Equals(Or(D, B, A, C), Or(A, B, C, D)).prove(assumptions=in_bool(A, B, C, D))

, , ,  ⊢
In [62]:
Equals(Or(D, B, C, A), Or(A, C, B, D)).prove(assumptions=in_bool(A, B, C, D))

, , ,  ⊢
In [63]:
Equals(Or(B, D, C, A), Or(D, C, B, A)).prove(assumptions=in_bool(A, B, C, D))

, , ,  ⊢

This even works in a nested manner

In [64]:
Equals(Or(And(B, A), D, C, A), Or(D, C, And(A, B), A)).prove(assumptions=in_bool(A, B, C, D))

, , ,  ⊢
In [65]:
%end demonstrations