Theorems (or conjectures) for the theory of proveit.core_expr_types.conditionals

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 Conditional
from proveit import a, b, f, g, m, n, A, Q, R
from proveit.core_expr_types import (x_1_to_n, y_1_to_n, f__x_1_to_n, f__y_1_to_n, 
                                     g__x_1_to_n, g__y_1_to_n, Q__x_1_to_n, Q__y_1_to_n,
                                     Q_1_to_m, R_1_to_n)
from proveit.logic import TRUE, FALSE, And, Implies, Forall, Equals, Not, NotEquals
from proveit.numbers import Natural, NaturalPos

%begin theorems

Defining theorems for theory 'proveit.core_expr_types.conditionals'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

satisfied_condition_reduction = Forall((a, Q), Equals(Conditional(a, Q), a),
                                      condition=Q)

satisfied_condition_reduction (conjecture without proof):

dissatisfied_condition_reduction = Forall((a, Q), Equals(Conditional(a, Q), Conditional(a, FALSE)),
                                          condition=Not(Q))

dissatisfied_condition_reduction (conjecture without proof):

condition_substitution = \
    Forall((a, Q, R), Equals(Conditional(a, Q),
                             Conditional(a, R)).with_wrap_before_operator(),
          conditions=[Equals(Q, R)])

condition_substitution (conjecture without proof):

redundant_condition_reduction = Forall((a, Q), Equals(Conditional(Conditional(a, Q), Q),
                                                      Conditional(a, Q)))

redundant_condition_reduction (conjecture without proof):

implication_from_conditional =  Forall((A, Q), Implies(Q, A), 
                                      condition=Conditional(A, Q))

implication_from_conditional (established theorem):

Note: to prove the following, we will need to use the fact that a condition of $Q$ is the same as having a condition of $Q=\top$ in order to avoid requiring that $Q$ is boolean.

singular_conjunction_condition_reduction = \
    Forall((a, Q), Equals(Conditional(a, And(Q)), 
                          Conditional(a, Q)).with_wrap_before_operator())

singular_conjunction_condition_reduction (conjecture without proof):

Note: to prove the following, we will need to use the fact that a condition of $Q$ is the same as having a condition of $Q=\top$ in order to avoid requiring that the $Q$ and $R$ variables be booleans.

condition_merger_reduction = \
    Forall((m, n), Forall((a, Q_1_to_m, R_1_to_n), 
                          Equals(Conditional(a, (And(Q_1_to_m), And(R_1_to_n))), 
                                 Conditional(a, (Q_1_to_m, R_1_to_n))).with_wrap_before_operator()),
           domain=Natural)

condition_merger_reduction (conjecture without proof):

condition_append_reduction = \
    Forall(m, Forall((a, Q_1_to_m, R), 
                     Equals(Conditional(a, (And(Q_1_to_m), R)), 
                            Conditional(a, (Q_1_to_m, R))).with_wrap_before_operator()),
           domain=Natural)

condition_append_reduction (conjecture without proof):

condition_prepend_reduction = \
    Forall(n, Forall((a, Q, R_1_to_n), 
                     Equals(Conditional(a, (Q, And(R_1_to_n))), 
                            Conditional(a, (Q, R_1_to_n))).with_wrap_before_operator()),
           domain=Natural)

condition_prepend_reduction (conjecture without proof):

true_condition_elimination = (
    Forall((m, n), Forall((a, Q_1_to_m, R_1_to_n), 
                          Equals(Conditional(a, (And(Q_1_to_m, TRUE, R_1_to_n))), 
                                 Conditional(a, (Q_1_to_m, R_1_to_n)))
                          .with_wrap_before_operator()),
           domain=Natural))

true_condition_elimination (conjecture without proof):

condition_with_true_on_left_reduction = \
    Forall(m, Forall((a, Q_1_to_m), 
                     Equals(Conditional(a, (TRUE, And(Q_1_to_m))), 
                            Conditional(a, (Q_1_to_m))).with_wrap_before_operator()),
           domain=Natural)

condition_with_true_on_left_reduction (conjecture without proof):

condition_with_true_on_right_reduction = \
    Forall(m, Forall((a, Q_1_to_m), 
                          Equals(Conditional(a, (And(Q_1_to_m), TRUE)), 
                                 Conditional(a, (Q_1_to_m))).with_wrap_before_operator()),
           domain=Natural)

condition_with_true_on_right_reduction (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.core_expr_types.conditionals