# Demonstrations for the theory of proveit.core_expr_types.conditionals¶

In [1]:
import proveit
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)

Out[2]:
x_if_A:
In [3]:
requirements = []
x_if_A.replaced({A:TRUE}, requirements=requirements)

Out[3]:
In [4]:
requirements

Out[4]:

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 [5]:
requirements = []
x_if_A.replaced({A:And(B)}, requirements=requirements)

Out[5]:
In [6]:
requirements

Out[6]:

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 [7]:
x_if_A_and_B = Conditional(x, (A, B))

Out[7]:
x_if_A_and_B:
In [8]:
assumptions = (InSet(n, Natural), InSet(m, Natural))

Out[8]:
assumptions:
In [9]:
x_if_A_and_B.replaced({A:A_1_to_m, B:B_1_to_n})

Out[9]:
In [10]:
requirements = []
x_if_A_and_B.replaced({A:And(A_1_to_m), B:And(B_1_to_n)},
assumptions=assumptions,
requirements=requirements)

Out[10]:
In [11]:
requirements

Out[11]:
In [12]:
requirements = []
x_if_A_and_B.replaced({A:And(A_1_to_m), B:And()},
assumptions=assumptions,
requirements=requirements)

Out[12]:
In [13]:
requirements

Out[13]:
In [14]:
requirements = []
x_if_A_and_B.replaced({A:And(), B:And(B_1_to_n)},
assumptions=assumptions,
requirements=requirements)

Out[14]:
In [15]:
requirements

Out[15]:
In [16]:
requirements = []
x_if_A_and_B.replaced({A:A, B:And(B_1_to_n)},
assumptions=assumptions,
requirements=requirements)

Out[16]:
In [17]:
requirements

Out[17]:
In [18]:
requirements = []
x_if_A_and_B.replaced({A:And(A_1_to_m), B:B},
assumptions=assumptions,
requirements=requirements)

Out[18]:
In [19]:
requirements

Out[19]:

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

In [20]:
# ConditionalSet(Conditional(A, FALSE), Conditional(A, FALSE), Conditional(B, TRUE)).reduce_to_truth()


### Test value substitution¶

In [21]:
x_eq_y = Equals(x, y)

Out[21]:
x_eq_y:
In [22]:
eq_if_Q = Implies(Q, x_eq_y)

Out[22]:
eq_if_Q:

Two ways to accomplish the same thing:

In [23]:
Conditional(x, Q).value_substitution(x_eq_y, assumptions=[eq_if_Q])

Out[23]:
In [24]:
x_eq_y.substitution(Conditional(x, Q), [eq_if_Q])

Out[24]:

We can also use a universally quantified equality.

In [25]:
quantified_eq = Forall(x, Equals(fx, gx), condition=Qx)

Out[25]:
quantified_eq:
In [26]:
Conditional(fx, Qx).value_substitution(quantified_eq, assumptions=[quantified_eq])

Out[26]:
In [27]:
%end demonstrations