logo

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))), 
              conditions=[ExprRange(i, Equals(x_i, IndexedVar(x, Add(i, 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)])
not_equals_contradiction (established theorem):
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)])
contradiction_via_falsification (established theorem):
In [29]:
%end theorems

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