Theorems (or conjectures) for the theory of proveit.logic.booleans.disjunction

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import Lambda, ExprRange, IndexedVar
from proveit import i, j, k, l, m, n, A, B, C, D, E, P, Pk
from proveit.logic import (Or, TRUE, FALSE, Forall, Exists, Implies, Not, in_bool, 
                           And, Boolean, Equals, Set)
from proveit.core_expr_types import A_1_to_l, A_1_to_m, B_1_to_m, C_1_to_m, C_1_to_n, D_1_to_n
from proveit.numbers import Natural, NaturalPos, Add, Exp, one, LessEq, Integer, Interval
%begin theorems

Defining theorems for theory 'proveit.logic.booleans.disjunction'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

true_or_true = Or(TRUE, TRUE)

true_or_true (established theorem):

true_or_false = Or(TRUE, FALSE)

true_or_false (established theorem):

false_or_true = Or(FALSE, TRUE)

false_or_true (established theorem):

false_or_false_negated = Not(Or(FALSE, FALSE))

false_or_false_negated (established theorem):

or_if_both = Forall((A, B), Or(A, B), conditions=[A, B])

or_if_both (established theorem):

or_if_only_left = Forall((A, B), Or(A, B), conditions=[A, Not(B)])

or_if_only_left (established theorem):

or_if_only_right = Forall((A, B), Or(A, B), conditions=[Not(A), B])

or_if_only_right (established theorem):

neither_intro = Forall((A, B), Not(Or(A, B)), conditions=[Not(A), Not(B)])

neither_intro (established theorem):

binary_or_contradiction = Forall((A, B), FALSE, conditions=(Or(A, B), Not(A), Not(B)))

binary_or_contradiction (established theorem):

left_if_not_right = Forall((A, B), A, domain=Boolean, conditions=(Or(A, B), Not(B)))

left_if_not_right (established theorem):

right_if_not_left = Forall((A, B), B, domain=Boolean, conditions=(Or(A, B), Not(A)))

right_if_not_left (established theorem):

This singular constructive dilemma lemma will require a single provable $C$ be designated as a Boolean. The main (non-lemma) version will drop this constraint. This will all culminate to the constructive dilemma, below, that can prove some $C \lor D$ given $A \lor B$, $A \Rightarrow C$ and $B \Rightarrow D$.

singular_constructive_dilemma_lemma = Forall((A, B, C), C, conditions=[Or(A, B), Implies(A, C), Implies(B, C)],
                                                domain=Boolean)

singular_constructive_dilemma_lemma (established theorem):

singular_constructive_dilemma = Forall((A, B), Forall(C, C, conditions=[Implies(A, C), Implies(B, C)]), 
                                     domain=Boolean, conditions=[Or(A, B)])

singular_constructive_dilemma (established theorem):

singular_constructive_multi_dilemma = \
    Forall(m, 
           Forall(A_1_to_m,
                  Forall(C, C,
                         conditions=[ExprRange(i, Implies(IndexedVar(A,i),
                                                          C), 
                                          one, m)]),
                  domain=Boolean,
                  conditions=[Or(A_1_to_m)]),
           domain = Natural)

singular_constructive_multi_dilemma (conjecture without proof):

or_if_left = Forall((A, B), Or(A, B), domain=Boolean, conditions=[A])

or_if_left (conjecture with conjecture-based proof):

or_if_right = Forall((A, B), Or(A, B), domain=Boolean, conditions=[B])

or_if_right (conjecture with conjecture-based proof):

constructive_dilemma = Forall((A, B, C, D), Or(C, D), domain=Boolean, 
                             conditions=[Or(A, B), Implies(A, C), Implies(B, D)])

constructive_dilemma (conjecture with conjecture-based proof):

constructive_multi_dilemma = \
    Forall(m, 
           Forall((A_1_to_m, B_1_to_m), 
                  Or(B_1_to_m),
                  domain=Boolean,
                  conditions=[Or(A_1_to_m), 
                              ExprRange(i,Implies(IndexedVar(A,i), 
                                                  IndexedVar(B,i)),
                                   one, m)]),
           domain = Natural)

constructive_multi_dilemma (conjecture without proof):

destructive_dilemma = Forall((A, B, C, D), Or(Not(A), Not(B)), domain=Boolean, 
                            conditions=[Or(Not(C), Not(D)), Implies(A, C), Implies(B, D)])

destructive_dilemma (conjecture with conjecture-based proof):

destructive_multi_dilemma = \
    Forall(m,
           Forall((A_1_to_m, B_1_to_m), 
                  Or(ExprRange(i, Not(IndexedVar(B,i)), one, m)), 
                  domain=Boolean, 
                  conditions=[Or(ExprRange(i, Not(IndexedVar(A,i)), 
                                           one, m)), 
                              ExprRange(i,Implies(IndexedVar(A, i), 
                                                  IndexedVar(B, i)),
                                   one,m)]), 
           domain=Natural)

destructive_multi_dilemma (conjecture without proof):

not_left_if_neither = Forall((A, B), Not(A), conditions=(Not(Or(A, B))))

not_left_if_neither (conjecture with conjecture-based proof):

not_right_if_neither = Forall((A, B), Not(B), conditions=(Not(Or(A, B))))

not_right_if_neither (conjecture with conjecture-based proof):

empty_disjunction_eval = Equals(Or(), FALSE)

empty_disjunction_eval (established theorem):

unary_or_lemma = Forall(A, (Equals(Or(A), Or(FALSE, A))), domain = Boolean)

unary_or_lemma (conjecture with conjecture-based proof):

unary_or_reduction = Forall(A, Equals(Or(A), A), domain = Boolean)

unary_or_reduction (conjecture with conjecture-based proof):

each_is_bool = \
    Forall((m, n), 
           Forall((A_1_to_m, B, C_1_to_n), 
                  in_bool(B), 
                  conditions=in_bool(Or(A_1_to_m, B, C_1_to_n))),
           domain=Natural)

each_is_bool (conjecture without proof):

or_if_any = Forall((m, n), 
                 Forall((A_1_to_m, B, C_1_to_n),
                        Or(A_1_to_m, B, C_1_to_n),
                        domain=Boolean, 
                        conditions=[B]),
                 domain=Natural)

or_if_any (conjecture without proof):

not_or_if_not_any = \
    Forall(m, Forall(A_1_to_m, Not(Or(A_1_to_m)),
                     conditions=[ExprRange(i, Not(IndexedVar(A, i)),
                                           one, m)]),
           domain=Natural)

not_or_if_not_any (conjecture without proof):

# As long as there is at least one operand then "if all then any."
any_if_all = \
    Forall(m, Forall(A_1_to_m, Or(A_1_to_m),
                     conditions=[A_1_to_m]),
           domain=NaturalPos)

any_if_all (conjecture without proof):

or_contradiction = \
    Forall(m, Forall(A_1_to_m, FALSE, 
                     conditions=(Or(A_1_to_m), 
                                 ExprRange(i, Not(IndexedVar(A, i)),
                                           one, m))),
           domain=Natural)

or_contradiction (conjecture without proof):

true_eval = Forall((m, n), 
                  Forall((A_1_to_m, C_1_to_n), 
                         Equals(Or(A_1_to_m, TRUE, C_1_to_n), TRUE),
                         domain=Boolean),
                  domain=Natural)

true_eval (conjecture without proof):

false_eval = Forall(m, Forall(A_1_to_m, 
                             Equals(Or(A_1_to_m), FALSE), 
                             domain=Set(FALSE)),
                   domain=Natural)

false_eval (conjecture without proof):

binary_closure = Forall((A, B), in_bool(Or(A, B)), domain=Boolean)

binary_closure (conjecture with conjecture-based proof):

closure = Forall(m, Forall(A_1_to_m, 
                           in_bool(Or(A_1_to_m)), 
                           domain=Boolean),
                 domain=NaturalPos)

closure (conjecture with conjecture-based proof):

demorgans_law_and_to_or_bin_explicit = \
    Forall((A,B), Or(A,B), 
           conditions=[Not(And(Not(A), Not(B)))], 
           domain=Boolean)

demorgans_law_and_to_or_bin_explicit (conjecture with conjecture-based proof):

demorgans_law_and_to_or_bin = Forall((A,B), Or(A,B), 
                                conditions=[Not(And(Not(A), Not(B)))])

demorgans_law_and_to_or_bin (conjecture with conjecture-based proof):

demorgans_law_and_to_or = \
    Forall(m, Forall(A_1_to_m, Or(A_1_to_m), 
                     condition=Not(And(ExprRange(i, Not(IndexedVar(A,i)), one, m)))),
           domain=Natural)

demorgans_law_and_to_or (conjecture without proof):

commutation = Forall((A, B), Equals(Or(A, B), Or(B, A)), 
                     domain=Boolean)

commutation (conjecture without proof):

leftward_commutation = \
    Forall((l, m, n),
           Forall((A_1_to_l,B_1_to_m,C,D_1_to_n), 
                  Equals(Or(A_1_to_l, B_1_to_m, C, D_1_to_n), 
                         Or(A_1_to_l, C, B_1_to_m, D_1_to_n)) \
                  .with_wrapping_at(2),
                  domain=Boolean), 
           domain=Natural)

leftward_commutation (conjecture without proof):

rightward_commutation = \
    Forall((l, m, n),
           Forall((A_1_to_l,B,C_1_to_m,D_1_to_n), 
                  Equals(Or(A_1_to_l, B, C_1_to_m, D_1_to_n), 
                         Or(A_1_to_l, C_1_to_m, B, D_1_to_n)) \
                  .with_wrapping_at(2),
                  domain=Boolean),
           domain = Natural)

rightward_commutation (conjecture without proof):

commute = Forall((A, B), Or(B, A), conditions=[Or(A, B)])

commute (conjecture without proof):

rightward_commute = \
    Forall((l, m, n), 
           Forall((A_1_to_l,B,C_1_to_m,D_1_to_n), 
                  Or(A_1_to_l, C_1_to_m, B, D_1_to_n),
                  conditions=[Or(A_1_to_l, B, C_1_to_m, D_1_to_n)]),
           domain=Natural)

rightward_commute (conjecture without proof):

leftward_commute = \
    Forall((l, m, n), 
           Forall((A_1_to_l,B_1_to_m,C,D_1_to_n), 
                  Or(A_1_to_l, C, B_1_to_m,D_1_to_n),
                  conditions=[Or(A_1_to_l, B_1_to_m, C, D_1_to_n)]),
           domain=Natural)

leftward_commute (conjecture without proof):

association = \
    Forall((l,m,n), 
           Forall((A_1_to_l,B_1_to_m,C_1_to_n), 
                  Equals(Or(A_1_to_l, B_1_to_m, C_1_to_n),
                         Or(A_1_to_l, Or(B_1_to_m), C_1_to_n)) \
                  .with_wrapping_at(2),
                  domain=Boolean),
           domain=Natural)

association (conjecture without proof):

disassociation = \
    Forall((l,m,n), 
           Forall((A_1_to_l,B_1_to_m,C_1_to_n), 
                  Equals(Or(A_1_to_l, Or(B_1_to_m), C_1_to_n),
                         Or(A_1_to_l, B_1_to_m, C_1_to_n)) \
                  .with_wrapping_at(2),
                  domain=Boolean),
           domain=Natural)

disassociation (conjecture without proof):

associate = \
    Forall((l,m,n), 
           Forall((A_1_to_l,B_1_to_m,C_1_to_n), 
                  Or(A_1_to_l, Or(B_1_to_m), C_1_to_n),
                  conditions=[Or(A_1_to_l, B_1_to_m, C_1_to_n)]),
           domain=Natural)

associate (conjecture without proof):

disassociate = \
    Forall((l,m,n), 
           Forall((A_1_to_l,B_1_to_m,C_1_to_n), 
                  Or(A_1_to_l, B_1_to_m, C_1_to_n),
                  conditions=[Or(A_1_to_l, Or(B_1_to_m), C_1_to_n)]),
           domain=Natural)

disassociate (conjecture without proof):

disjunction_eq_quantification = Forall(
    (i, j), Forall(P, Equals(Or(ExprRange(k, Pk, i, j)),
                             Exists(k, Pk, domain=Interval(i,j))),
                   conditions=[LessEq(i, Add(j, one))]),
    domain=Integer)

disjunction_eq_quantification (conjecture without proof):

disjunction_from_quantification = Forall(
    (i, j), Forall(P, Implies(Exists(k, Pk, domain=Interval(i,j)), 
                              Or(ExprRange(k, Pk, i, j))),
                   conditions=[LessEq(i, Add(j, one))]),
    domain=Integer)

disjunction_from_quantification (conjecture without proof):

quantification_from_disjunction = Forall(
    (i, j), Forall(P, Implies(Or(ExprRange(k, Pk, i, j)),
                              Exists(k, Pk, domain=Interval(i,j)))),
    domain=Integer)

quantification_from_disjunction (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.logic.booleans.disjunction