# Theorems (or conjectures) for the theory of proveit.logic.equality¶

In [1]:
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 ExprRange, IndexedVar
from proveit.logic import Equals, NotEquals, Implies, Not, And, Forall, FALSE, in_bool
from proveit import A, a, b, c, d, i, n, x, y, z, f, P, fa, fab, fx, fxy, Px, Py, Q
from proveit.core_expr_types import (x_1_to_n, x_1_to_np1, x_i, y_1_to_n, x_eq_y__1_to_n,
f__x_1_to_n, f__y_1_to_n, P__x_1_to_n, P__y_1_to_n)
from proveit.logic import PofTrue, PofFalse
from proveit.logic.equality import elementwise_equality
from proveit.numbers import one, Natural, NaturalPos, Add
%begin theorems

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


### Extending transitivity¶

In [2]:
four_chain_transitivity = Forall((a, b, c, d), Equals(a, d), conditions=[Equals(a, b), Equals(b, c), Equals(c, d)])

four_chain_transitivity (conjecture without proof):

In [3]:
transitivity_chain = Forall(
n, Forall(x_1_to_np1, Equals(IndexedVar(x, one), IndexedVar(x, Add(n, one))),
one, n)]),
domain=NaturalPos)

transitivity_chain (conjecture without proof):

### Substitution or equivalence with a statement that is known to be true (left-hand side)¶

In [4]:
sub_left_side_into = Forall((P, x, y), Px, conditions=[Py, Equals(x, y)])

sub_left_side_into (established theorem):

In [5]:
lhs_via_equality = Forall((P, Q), P, conditions=[Q, Equals(P, Q)])

lhs_via_equality (established theorem):

### Applying symmetry, we can reverse any known equality:¶

In [6]:
equals_reversal = Forall((x, y), Equals(y, x), conditions=[Equals(x, y)])

equals_reversal (established theorem):

### Substitution or equivalence with a statement that is known to be true (right-hand side)¶

In [7]:
sub_right_side_into = Forall((P, x, y), Py, conditions=[Px, Equals(x, y)])

sub_right_side_into (established theorem):

In [8]:
rhs_via_equality = Forall((P, Q), Q, conditions=[P, Equals(P, Q)])

rhs_via_equality (established theorem):

### Special substitution involving Boolean values¶

In [9]:
substitute_in_true = Forall((P, x), PofTrue, conditions=[Px, x])

substitute_in_true (established theorem):

In [10]:
substitute_truth = Forall((P, x), Px, conditions=[PofTrue, x])

substitute_truth (established theorem):

In [11]:
substitute_in_false = Forall((P, x), PofFalse, conditions=[Px, Not(x)])

substitute_in_false (established theorem):

In [12]:
substitute_falsehood = Forall((P, x), Px, conditions=[PofFalse, Not(x)])

substitute_falsehood (established theorem):

### Folding and unfolding $\neq$¶

In [13]:
unfold_not_equals = Forall((x, y), Not(Equals(x, y)), conditions=[NotEquals(x, y)])

unfold_not_equals (established theorem):

In [14]:
fold_not_equals = Forall((x, y), NotEquals(x, y), conditions=[Not(Equals(x, y))])

fold_not_equals (established theorem):

$\neq$ is also symmetric:

In [15]:
not_equals_symmetry = Forall((x, y), NotEquals(y, x), conditions=[NotEquals(x, y)])

not_equals_symmetry (established theorem):

If two things are both equal and not equal, there is a contradiction:

In [16]:
not_equals_contradiction = Forall((x, y), FALSE, conditions=[Equals(x, y), NotEquals(x, y)])


In [17]:
sub_in_left_operands = Forall(n, Forall((P, x_1_to_n, y_1_to_n), P__x_1_to_n,
conditions=[P__y_1_to_n, x_eq_y__1_to_n]),
domain=Natural)

sub_in_left_operands (established theorem):

In [18]:
sub_in_right_operands = Forall(n, Forall((P, x_1_to_n, y_1_to_n), P__y_1_to_n,
conditions=[P__x_1_to_n, x_eq_y__1_to_n]),
domain=Natural)

sub_in_right_operands (established theorem):

In [19]:
sub_in_left_operands_via_tuple = Forall(n, Forall((P, x_1_to_n, y_1_to_n), P__x_1_to_n,
conditions=[P__y_1_to_n, Equals([x_1_to_n], [y_1_to_n])]),
domain=Natural)

sub_in_left_operands_via_tuple (conjecture with conjecture-based proof):

In [20]:
sub_in_right_operands_via_tuple = Forall(n, Forall((P, x_1_to_n, y_1_to_n), P__y_1_to_n,
conditions=[P__x_1_to_n, Equals([x_1_to_n], [y_1_to_n])]),
domain=Natural)

sub_in_right_operands_via_tuple (conjecture with conjecture-based proof):

In [21]:
multi_substitution = Forall(n, Forall((f, x_1_to_n, y_1_to_n),
Equals(f__x_1_to_n, f__y_1_to_n),
conditions=[elementwise_equality]),
domain=NaturalPos)

multi_substitution (conjecture with conjecture-based proof):

In [22]:
mult_sub_left_into = Forall(n, Forall((P, x_1_to_n, y_1_to_n), P__x_1_to_n,
conditions=[P__y_1_to_n, elementwise_equality]),
domain=Natural)

mult_sub_left_into (conjecture without proof):

(alternate proof for sub_in_left_operands)
In [23]:
mult_sub_right_into = Forall(n, Forall((P, x_1_to_n, y_1_to_n), P__y_1_to_n,
conditions=[P__x_1_to_n, elementwise_equality]),
domain=Natural)

mult_sub_right_into (conjecture without proof):

(alternate proof for sub_in_right_operands)
In [ ]:


In [24]:
unary_evaluation = Forall((f, x, a, c), Implies(Equals(x, a), Implies(Equals(fa, c), Equals(fx, c))))

unary_evaluation (established theorem):

In [25]:
binary_substitution = Forall((f, x, y, a, b), Implies(And(Equals(x, a), Equals(y, b)), Equals(fxy, fab)))

binary_substitution (conjecture without proof):

In [26]:
binary_evaluation = Forall((f, x, y, a, b, c), Implies(And(Equals(x, a), Equals(y, b)), Implies(Equals(fab, c), Equals(fxy, c))))

binary_evaluation (conjecture without proof):

In [27]:
# Proven
not_equals_is_bool = Forall((x, y), in_bool(NotEquals(x, y)))

not_equals_is_bool (conjecture with conjecture-based proof):

In [28]:
contradiction_via_falsification = Forall(A, FALSE, conditions=[A, Equals(A, FALSE)])

%end theorems

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