logo

Demonstrations for the theory of proveit.core_expr_types.conditionals

In [1]:
import proveit
from proveit import defaults
from proveit import Conditional, ConditionalSet
from proveit import A, B, m, n, Q, x, y, fx, gx, Qx
from proveit.logic import Implies, And, TRUE, FALSE, Forall, Equals, InSet
from proveit.core_expr_types import A_1_to_m, B_1_to_n
from proveit.numbers import Natural
%begin demonstrations

Conditional reductions

A conditional with a TRUE condition reduces to its value.

In [2]:
x_if_A = Conditional(x, A)
x_if_A:
In [3]:
requirements = []
x_if_A.complete_replaced({A:TRUE}, requirements=requirements)
In [4]:
requirements

A redundant condition can be dropped via simplification.

In [5]:
Conditional(Conditional(x, A), A).shallow_simplification()
 ⊢  

A conditional with a condition that is a singular conjunction can drop the conjunction regardless of whether or not we know the contents to be boolean.

In [6]:
requirements = []
x_if_A.complete_replaced({A:And(B)}, requirements=requirements)
In [7]:
requirements

A conditional with a conjunction of a pair of conjunctions as its condition is reduced to a flattened single conjunction for its conjunction which is displayed as a comma-delimited list.

In [8]:
x_if_A_and_B = Conditional(x, (A, B))
x_if_A_and_B:
In [9]:
defaults.assumptions = (InSet(n, Natural), InSet(m, Natural))
defaults.assumptions:
In [10]:
x_if_A_and_B.complete_replaced({A:A_1_to_m, B:B_1_to_n})
In [11]:
requirements = []
x_if_A_and_B.complete_replaced({A:And(A_1_to_m), B:And(B_1_to_n)},
                      requirements=requirements)
In [12]:
requirements
In [13]:
requirements = []
x_if_A_and_B.complete_replaced({A:And(A_1_to_m), B:And()}, 
                      requirements=requirements)
In [14]:
requirements
In [15]:
requirements = []
x_if_A_and_B.complete_replaced({A:And(), B:And(B_1_to_n)}, 
                      requirements=requirements)
In [16]:
requirements
In [17]:
requirements = []
x_if_A_and_B.complete_replaced({A:A, B:And(B_1_to_n)}, 
                      requirements=requirements)
In [18]:
requirements
In [19]:
requirements = []
x_if_A_and_B.complete_replaced({A:And(A_1_to_m), B:B}, 
                      requirements=requirements)
In [20]:
requirements

A ConditionalSet with a single TRUE conditional reduces to its value.

In [21]:
 ConditionalSet(Conditional(A, FALSE), Conditional(A, FALSE), B).single_case_via_elimination()
Out[21]:
 ⊢  
In [22]:
ConditionalSet(Conditional(A, FALSE), Conditional(A, FALSE), Conditional(B, FALSE), 
               Conditional(A, FALSE), B).single_case_via_elimination()
 ⊢  

Test value substitution

In [23]:
x_eq_y = Equals(x, y)
x_eq_y:
In [24]:
eq_if_Q = Implies(Q, x_eq_y)
eq_if_Q:

Two ways to accomplish the same thing:

In [25]:
Conditional(x, Q).value_substitution(x_eq_y, assumptions=[eq_if_Q])
 ⊢  
In [26]:
x_eq_y.substitution(Conditional(x, Q), assumptions=[eq_if_Q])
 ⊢  

We can also use a universally quantified equality.

In [27]:
quantified_eq = Forall(x, Equals(fx, gx), condition=Qx)
quantified_eq:
In [28]:
Conditional(fx, Qx).value_substitution(quantified_eq, assumptions=[quantified_eq])
 ⊢  
In [29]:
%end demonstrations