# Demonstrations for context proveit.logic.equality¶

In [1]:
import proveit
%begin demonstrations


## Substitution¶

Equality is a fundamental concept of logic. When two mathematical operations are equal, then one may be substituted for the other. This is rule is defined by the substitution axiom:

In [2]:
from proveit.logic.equality._axioms_ import substitution
from proveit._common_ import a, b, c, d, x, y, z, fx # we'll use these later
substitution

Out[2]:
⊢

The English translation of this axiom is: for any function $f$ and any $x, y$ such that $x=y$, $f(x) = f(y)$. In other words, we may substitute $y$ for $x$ in any function whenever $x=y$. The equality of $x$ and $y$ transfers to an equality between $f(x)$ and $f(y)$. This is fundamental to the meaning of equality regardless of what $f$ does (as long as it can act on a single argument). We may specialize this axiom using any operation for $f$. For example,

In [3]:
from proveit.logic import Not, Equals
substitution.specialize({fx:Not(x), x:a, y:b}, assumptions=[Equals(a, b)])

Out[3]:
⊢

There are more convenient ways to apply this substitution rule than manual specialization that was demonstrated in the previous input. The Equals class has the substitution, subLeftSideInto and subRightSideInto methods for conveniently applying substitution and its variants, as we will demonstrate below. Each of these methods takes a lambdaMap argument to provide a context for the substitution -- what is being substituted and where. A lambdaMap can be an actual Lambda expression, an InnerExpr object, or if it is neither of these, it can be any other Expression for which the default will be to performa a global replacement.

In [4]:
from proveit import Lambda
from proveit.number import Add, Frac, Exp
expr = Equals(a, Add(b, Frac(c, d), Exp(c, d)))

Out[4]:
expr:

The globalRepl static method of Lambda is useful for creating a global replacement lambda map. Below, we create a map for replacing every occurence of $d$ in expr with anything else:

In [5]:
gRepl = Lambda.globalRepl(expr, d)

Out[5]:
gRepl:

We now use this lambda map to replace occurences of $d$ in expr with $y$:

In [6]:
d_eq_y = Equals(d, y)

Out[6]:
d_eq_y:
In [7]:
d_eq_y.substitution(gRepl, assumptions=[d_eq_y])

Out[7]:
⊢

Or we can take advantage of that a global replacement is performed by default when a non-Lambda expression is provided as the "lambdaMap".

In [8]:
d_eq_y.substitution(expr, assumptions=[d_eq_y])

Out[8]:
⊢

Either way, the generated proof is the same:

In [9]:
d_eq_y.substitution(expr, assumptions=[d_eq_y]).proof()

Out[9]:
step typerequirementsstatement
0specialization1, 2 ⊢
: , : , :
1axiom ⊢
proveit.logic.equality.substitution
2assumption ⊢

If we want to perform substitution for a specific inner expression, and not necessarily a global replacement, the proveit._core_.expression.InnerExpr class (aliased as proveit.InnerExpr) is extremely convenient. It uses some Python tricks via implementing the __getitem__ and __getattr__ methods. First, you create the InnerExpr object by calling the innerExpr() method on the top-level expression:

In [10]:
innerExpr = expr.innerExpr()

Out[10]:
innerExpr:

The InnerExpr object displays itself with two important pieces of information: the lambda map that it represents and the inner expression of the top-level expression that would be replaced by this lambda map. The point is that we will be able to "dig" in to inner expressions of the top-level expression via accessing sub-expression attributes. For example, we next will "dig" into the "right hand side" (rhs) of the master expression:

In [11]:
innerExpr = innerExpr.rhs

Out[11]:
innerExpr:

By accessing the rhs attribute, we created a new InnerExpr object that has the same top-level expression as the original but has a new current inner expression. Note that the InnerExpr class does not know anything about the rhs attribute itself; it is relying on the fact that the previous sub-expression has this attribute. The InnerExpr class also has tricks for getting an sub-expression with an index (or key):

In [12]:
innerExpr = innerExpr.operands[1]

Out[12]:
innerExpr:

Now will "dig" down to the denominator of $\frac{c}{d}$ and show how we use the InnerExpr class to replace a particular occurence of $d$ rather than a global replacement:

In [13]:
innerExpr = innerExpr.denominator

Out[13]:
innerExpr:
In [14]:
d_eq_y.substitution(innerExpr, assumptions=[d_eq_y])

Out[14]:
⊢

Let us demonstrate this technique again, replacing the other occurrence of $d$. This time we do this more succinctly, without the extra pedogogial steps:

In [15]:
d_eq_y.substitution(expr.innerExpr().rhs.operands[2].exponent, assumptions=[d_eq_y])

Out[15]:
⊢

The substition method, that we demonstrated above, is a direct application of the substitution axiom. It proves the equality between some $f(x)$ and some $f(y)$. We often will want to take a shortcut to perform a statement substitution in which we prove some $P(y)$ is true assuming that $P(x)$ is true and $P(x) = P(y)$. For this, we have the subRightSideInto and subLeftSideInto methods.

If the expression that we want to substitute in is on the right hand side of the Equals object playing the role of $x=y$, then we use subRightSideInto:

In [16]:
d_eq_y.subRightSideInto(gRepl, assumptions=[d_eq_y,expr])

Out[16]:
⊢

We can also take advantage of the global replacement default and provide a non-Lambda Expression.

In [17]:
d_eq_y.subRightSideInto(expr, assumptions=[d_eq_y,expr])

Out[17]:
⊢

If the expression that we want to substitute in is on the left hand side of the Equals object playing the role of $x=y$, then we use subLeftSideInto:

In [18]:
y_eq_d = Equals(y, d)

Out[18]:
y_eq_d:
In [19]:
y_eq_d.subLeftSideInto(gRepl, assumptions=[y_eq_d,expr])

Out[19]:
⊢

Again, we can provide a non-Lambda Expression to do a simple global replacement.

In [20]:
y_eq_d.subLeftSideInto(expr, assumptions=[y_eq_d,expr])

Out[20]:
⊢

The proof uses a theorem the relies upon the substitution axiom, rather than using the substition axiom directly:

In [21]:
y_eq_d.subLeftSideInto(expr, assumptions=[y_eq_d,expr]).proof()

Out[21]:
step typerequirementsstatement
0specialization1, 2, 3 ⊢
: , : , :
1theorem ⊢
proveit.logic.equality.subLeftSideInto
2assumption ⊢
3assumption ⊢

## Reflexivity, symmetry, and transitivity¶

Reflexivity, symmetry, and transitivity are also fundamental properties of equality, in addition to the ability to perform substitution. Reflexivity is the fact that any mathematical object is equal to itself. Symmetry is the fact that $x = y$ and $y = x$ are equivalent (either both of these are true or both of these false). Transitivity is the ability to derive $x=z$ from $x=y$ and $y=z$. These are all axioms.

In [22]:
from proveit.logic.equality._axioms_ import equalsReflexivity, equalsSymmetry, equalsTransitivity

In [23]:
equalsReflexivity

Out[23]:
⊢
In [24]:
equalsSymmetry

Out[24]:
⊢
In [25]:
equalsTransitivity

Out[25]:
⊢

equalsReversal is a useful theorem for applying the symmetry property of equality:

In [26]:
from proveit.logic.equality._theorems_ import equalsReversal
equalsReversal # y=x derives from x=y

Out[26]:
⊢

These three properties are applied automatically for Equals objects

Reflexivity is concluded automatically:

In [27]:
Equals(a, a).prove()

Out[27]:
⊢
In [28]:
Equals(a, a).prove().proof()

Out[28]:
step typerequirementsstatement
0specialization1 ⊢
:
1axiom ⊢
proveit.logic.equality.equalsReflexivity

Symmetric statements are derived as side-effects. Note that the KnownTruth.deriveSideEffects method employs a mechanism to prevent infinite recursion or this would not be possible (it would continually go back and forth, proving $y=x$ from $x=y$ then $x=y$ from $y=x$, ad infinitum)

In [29]:
a_eq_b = Equals(a, b)

Out[29]:
a_eq_b:
In [30]:
Equals(b, a).prove([a_eq_b])

Out[30]:
⊢

The reversed form may also be derived explicitly via deriveReversed. The proof is the same.

In [31]:
a_eq_b.prove([a_eq_b]).deriveReversed().proof()

Out[31]:
step typerequirementsstatement
0specialization1, 2 ⊢
: , :
1theorem ⊢
proveit.logic.equality.equalsReversal
2assumption ⊢

Transitivity derivations are attempted with automation via the conclude method using the trensitivitySearch function in proveit.logic.equality.transitivity_search. This performs a breadth-first, bidirectional search (meeting in the middle from both ends) over the space of KnownTruth objects representing equality and using appropriate assumptions. This is therefore reasonably efficient. Efficiency should not really be an issue, anyways, as long as proofs for each theorem are relatively small. A long proof should be broken up into several smaller proofs for lemma-like theorems. In that case (in the setting of small proofs), the space of KnownTruths will be small and this search algorithm will have ample efficiency.

In [32]:
# We'll make this interesting by reversing some of the equations in the chain.
c_eq_b = Equals(c, b)

Out[32]:
c_eq_b:
In [33]:
d_eq_c = Equals(d, c)

Out[33]:
d_eq_c:
In [34]:
d_eq_z = Equals(d, z)

Out[34]:
d_eq_z:
In [35]:
a_eq_z = Equals(a, z).prove(assumptions=[a_eq_b, c_eq_b, d_eq_c, d_eq_z])

Out[35]:
a_eq_z: ⊢
In [36]:
a_eq_z.proof()

Out[36]:
step typerequirementsstatement
0specialization5, 1, 2 ⊢
: , : , :
1specialization5, 3, 4 ⊢
: , : , :
2assumption ⊢
3specialization5, 6, 7 ⊢
: , : , :
4specialization9, 8 ⊢
: , :
5axiom ⊢
proveit.logic.equality.equalsTransitivity
6assumption ⊢
7specialization9, 10 ⊢
: , :
8assumption ⊢
9theorem ⊢
proveit.logic.equality.equalsReversal
10assumption ⊢

The applyTransivity method applies the transitivity relation explicity.

In [37]:
a_eq_b.prove([a_eq_b]).applyTransitivity(c_eq_b, assumptions=[c_eq_b])

Out[37]:
⊢

## Evaluation¶

An evaluation is an equality in which the right hand side is an irreducible value (specifically, an instance of proveit.logic.irreducible_value.IrreducibleValue, aliased as proveit.logic.IrreducibleValue). An irreducible value represents a mathematical object in its simplest form. It cannot be reduced. The evaluation of an IrreducibleValue is itself. When an evaluation is proven, the associated KnownTruth is stored for future reference in Equals.evaluations for making other evaluations.

TRUE ($\top$) and FALSE ($\bot$) are both IrreducibleValues:

In [38]:
from proveit.logic import TRUE, FALSE, IrreducibleValue

In [39]:
isinstance(TRUE, IrreducibleValue)

Out[39]:
True
In [40]:
isinstance(FALSE, IrreducibleValue)

Out[40]:
True
In [41]:
TRUE.evaluation()

Out[41]:
⊢

An IrreducibleValue should implement the evalEquality and notEqual methods to prove equality relations with other IrreducibleValues as appropriate.

In [42]:
Equals(Equals(FALSE, TRUE), FALSE).deriveContradiction([Equals(FALSE, TRUE)])

Out[42]:
⊢
In [43]:
TRUE.evalEquality(TRUE)

Out[43]:
⊢
In [44]:
TRUE.evalEquality(FALSE)

Out[44]:
⊢
In [45]:
TRUE.notEqual(FALSE)

Out[45]:
⊢

A proven expression will evaluate to TRUE.

In [46]:
a_eq_T = a.evaluation([a])

Out[46]:
a_eq_T: ⊢
In [47]:
a_eq_T.proof()

Out[47]:
step typerequirementsstatement
0specialization1, 2 ⊢
:
1axiom ⊢
proveit.logic.boolean.eqTrueIntro
2assumption ⊢

A disproven expression will evaluate to FALSE.

In [48]:
a_eq_F = a.evaluation([Not(a)])

Out[48]:
a_eq_F: ⊢
In [49]:
a_eq_F.proof()

Out[49]:
step typerequirementsstatement
0specialization1, 2 ⊢
:
1axiom ⊢
proveit.logic.boolean.negation.negationElim
2assumption ⊢

If the expression to be evaluated is known to be equal to an expression that has already been evaluated, transitivity will automatically be applied.

In [50]:
b_eq_F = b.evaluation([Equals(b, a), Not(a)])

Out[50]:
b_eq_F: ⊢
In [51]:
b_eq_F.proof()

Out[51]:
step typerequirementsstatement
0specialization1, 2, 3 ⊢
: , : , :
1axiom ⊢
proveit.logic.equality.equalsTransitivity
2assumption ⊢
3specialization4, 5 ⊢
:
4axiom ⊢
proveit.logic.boolean.negation.negationElim
5assumption ⊢

When evaluating an expression, an evaluation of the operands will be attempted. The operation class is responsible for overridding the evaluate method in order to properly treat the operation applied to irreducible values or generate a more efficient proof as appropriate.

In [52]:
from proveit.logic import Or, Not, inBool

In [53]:
nested_eval = Or(a, Not(a)).evaluation([a])

Out[53]:
nested_eval: ⊢
In [54]:
nested_eval.proof()

Out[54]:
step typerequirementsstatement
0specialization1, 2 ⊢
:
1axiom ⊢
proveit.logic.boolean.eqTrueIntro
2specialization3, 4 ⊢
:
3theorem ⊢
proveit.logic.boolean.unfoldInBool
4specialization5, 6 ⊢
:
5theorem ⊢
proveit.logic.boolean.inBoolIfTrue
6assumption ⊢

## Boolean equality¶

Equality with TRUE ($\top$) or FALSE ($\bot$) has special logical consequences. The Equals object has automation capabilities to treat these special kinds of equations.

In [55]:
TRUE

Out[55]:
In [56]:
FALSE

Out[56]:

Proofs via boolean equality are automatic via Equals.deduceSideEffects:

In [57]:
a.prove([Equals(a, TRUE)])

Out[57]:
⊢
In [58]:
a.prove([Equals(a, TRUE)]).proof()

Out[58]:
step typerequirementsstatement
0specialization1, 2 ⊢
:
1axiom ⊢
proveit.logic.boolean.eqTrueElim
2assumption ⊢
In [59]:
Not(b).prove([Equals(b, FALSE)])

Out[59]:
⊢
In [60]:
Not(b).prove([Equals(b, FALSE)]).proof()

Out[60]:
step typerequirementsstatement
0specialization1, 2 ⊢
:
1axiom ⊢
proveit.logic.boolean.negation.negationIntro
2assumption ⊢

Going the other direction, boolean equalities are proven automatically via Equals.conclude:

In [61]:
Equals(x, TRUE).prove([x])

Out[61]:
⊢
In [62]:
Equals(TRUE, y).prove([y])

Out[62]:
⊢
In [63]:
Equals(c, FALSE).prove([Not(c)])

Out[63]:
⊢
In [64]:
Equals(FALSE, c).prove([Not(c)])

Out[64]:
⊢

When something is equal to FALSE and known to be true, there is a contradiction. That is, FALSE is a consequence. The deriveContradiction method of Equals can be used to prove such a contradiction:

In [65]:
contradiction = Equals(a, FALSE).deriveContradiction([a, Equals(a, FALSE)])

Out[65]:
In [66]:
contradiction.proof()

Out[66]:
step typerequirementsstatement
0specialization1, 2, 3 ⊢
:
1theorem ⊢
2assumption ⊢
3assumption ⊢

Contradictions are useful in making contradiction proofs (reductio ad absurdum). The affirmViaContradiction and denyViaContradiction methods are useful in making such a proof. They both use deriveContradiction. For example:

In [67]:
from proveit.logic import Implies, inBool
not_a__truth = Equals(a, FALSE).affirmViaContradiction(Not(a), [Implies(a, Equals(a, FALSE)), inBool(a)])

Out[67]:
not_a__truth: ⊢
In [68]:
not_a__truth.proof().numSteps()

Out[68]:
13

It is more efficient to use denyViaContradiction when proving the negation of something. Here we prove the same as above but in fewer steps.

In [69]:
not_b__truth = Equals(b, FALSE).denyViaContradiction(b, [Implies(b, Equals(b, FALSE)), inBool(b)])

Out[69]:
not_b__truth: ⊢
In [70]:
not_b__truth.proof().numSteps()

Out[70]:
9
In [71]:
not_b__truth.proof()

Out[71]:
step typerequirementsstatement
0specialization1, 2, 3 ⊢
:
1theorem ⊢
2assumption ⊢
3hypothetical reasoning4 ⊢
4specialization5, 8, 6 ⊢
:
5theorem ⊢
6modus ponens7, 8 ⊢
7assumption ⊢
8assumption ⊢

## Equality and sets¶

All equality expressions are in the boolean set by the equalityInBool axiom. That is, given any two mathematical objects, they are either equal or not (even nonsense is either the same nonsense or different nonsense).

In [72]:
eq_in_bool = Equals(a, b).deduceInBool()

Out[72]:
eq_in_bool: ⊢
In [73]:
eq_in_bool.proof()

Out[73]:
step typerequirementsstatement
0specialization1 ⊢
: , :
1axiom ⊢
proveit.logic.equality.equalityInBool

A singleton is a set with one element. If $x=c$, then $x$ is in the singleton set of $\{c\}$:

In [74]:
in_singleton_truth = Equals(x, c).deriveIsInSingleton([Equals(x, c)])

Out[74]:
in_singleton_truth: ⊢
In [75]:
in_singleton_truth.proof()

Out[75]:
step typerequirementsstatement
0specialization1, 2 ⊢
: , :
1theorem ⊢
proveit.logic.set_theory.enumeration.foldSingleton
2assumption ⊢

## Not equals¶

The NotEquals operation is a more way of expressing that two mathematical objects are not equal to each other.

In [76]:
from proveit.logic import NotEquals

In [77]:
a_neq_b = NotEquals(a, b)

Out[77]:
a_neq_b:
In [78]:
a_neq_b.definition()

Out[78]:
⊢
In [79]:
a_neq_b.definition().proof()

Out[79]:
step typerequirementsstatement
0specialization1 ⊢
: , :
1axiom ⊢
proveit.logic.equality.notEqualsDef

From $\lnot (a = b)$ one can derive $a \neq b$ and vice-versa, folding and unfolding the NotEquals.

In [80]:
a_neq_b.prove([Not(a_eq_b)])

Out[80]:
⊢
In [81]:
a_neq_b.prove([Not(a_eq_b)]).proof()

Out[81]:
step typerequirementsstatement
0specialization1, 2 ⊢
: , :
1theorem ⊢
proveit.logic.equality.foldNotEquals
2assumption ⊢
In [82]:
Not(a_eq_b).prove([a_neq_b])

Out[82]:
⊢
In [83]:
Not(a_eq_b).prove([a_neq_b]).proof()

Out[83]:
step typerequirementsstatement
0specialization1, 2 ⊢
: , :
1theorem ⊢
proveit.logic.equality.unfoldNotEquals
2assumption ⊢

NotEquals also has a symmetry property which can be applied directly. It can be proven through automation.

In [84]:
NotEquals(b, a).prove([a_neq_b])

Out[84]:
⊢

Or explicitly via deriveReversed

In [85]:
a_neq_b.prove([a_neq_b]).deriveReversed().proof()

Out[85]:
step typerequirementsstatement
0specialization1, 2 ⊢
: , :
1theorem ⊢
proveit.logic.equality.notEqualsSymmetry
2assumption ⊢

If two objects are both equal and not equal, there is a contradiction.

In [86]:
neq_contradiction = a_neq_b.deriveContradiction([a_neq_b, a_eq_b])

Out[86]:
In [87]:
neq_contradiction.proof()

Out[87]:
step typerequirementsstatement
0specialization1, 2, 3 ⊢
: , :
1theorem ⊢
2assumption ⊢
3assumption ⊢
In [88]:
a_neq_a = NotEquals(a, a)

Out[88]:
a_neq_a:
In [89]:
b_from_contradiction = a_neq_a.affirmViaContradiction(b, [Implies(Not(b), a_neq_a), inBool(b)])

Out[89]:
In [90]:
b_from_contradiction.proof()

Out[90]:
step typerequirementsstatement
0specialization1, 2, 3 ⊢
:
1theorem ⊢
2assumption ⊢
3hypothetical reasoning4 ⊢
4specialization5, 6, 7 ⊢
: , :
5theorem ⊢
%end demonstrations