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

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

closure

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

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

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.element.deduce_part_in_bool(1, assumptions=[demo1.expr])

each_is_bool

Or(TRUE, TRUE).prove()

Or(TRUE, FALSE).prove()

Or(FALSE, TRUE).prove()

Not(Or(FALSE, FALSE)).prove()

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

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

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

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

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

Or(A, B).derive_left_if_not_right(assumptions=[in_bool(A), in_bool(B), Not(B), Or(A, B)])

Or(A, B).derive_right_if_not_left(assumptions=[*in_bool(A, B), Not(A), Or(A, B)])

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))])

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)])

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

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

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)])

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)])

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)])

Or(H, I, J, K).deduce_part_in_bool(2, assumptions=[Or(H, I, J, K)])

destructive_dilemma

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)])

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)])

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

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

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

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

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

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

Or(A,B,C).derive_contradiction(assumptions=[Or(A,B,C), Not(A), Not(B), Not(C)])

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.disassociate(2, assumptions=[group_c_d.expr])

Or(A,B,C,D,E).commutation(1,3, assumptions=in_bool(A,B,C,D,E))

Or(A,B,C,D,E).commutation(-1,0, assumptions=in_bool(A,B,C,D,E))

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)])

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)])

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)])

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

Or(A,B,C,D).group_commutation(1, 0, length=2, assumptions=in_bool(A,B,C,D))

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))

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)

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)

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

Or(FALSE,FALSE,TRUE,FALSE,FALSE).evaluation()

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

false_eval

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

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

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

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

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

# 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¶

defaults.assumptions = [Or(D, B, A, C)]
Or(A, C, B, D).readily_provable()

False

A.readily_provable(assumptions=[Or(D, B, A, C)])

False

Implies(Or(D, B, A, C), Or(A, C, B, D)).readily_provable()

False

eq = Equals(Or(D, B, A, C), Or(A, B, C, D))

Equals(Or(D, B, A, C), Or(A, B, C, D)).prove(assumptions=in_bool(A, B, C, D))

Equals(Or(D, B, C, A), Or(A, C, B, D)).prove(assumptions=in_bool(A, B, C, D))

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

Equals(Or(And(B, A), D, C, A), Or(D, C, And(A, B), A)).prove(assumptions=in_bool(A, B, C, D))

%end demonstrations

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

Automatically proving conjunctions are equal via permutation¶

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