In [1]:

```
import proveit
%begin demonstrations
```

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 import substitution
from proveit import a, b, c, d, x, y, z, fx # we'll use these later
substitution
```

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 instantiate this axiom using any operation for $f$. For example,

In [3]:

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

There are more convenient ways to apply this substitution rule than manual instantiation that was demonstrated in the previous input. The `Equals`

class has the `substitution`

, `sub_left_side_into`

and `sub_right_side_into`

methods for conveniently applying substitution and its variants, as we will demonstrate below. Each of these methods takes a `lambda_map`

argument to provide a theory for the substitution -- what is being substituted and where. A `lambda_map`

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.numbers import Add, frac, Exp
expr = Equals(a, Add(b, frac(c, d), Exp(c, d)))
```

The `global_repl`

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]:

```
g_repl = Lambda.global_repl(expr, d)
```

We now use this lambda map to replace occurences of $d$ in `expr`

with $y$:

In [6]:

```
d_eq_y = Equals(d, y)
```

In [7]:

```
d_eq_y.substitution(g_repl, assumptions=[d_eq_y])
```

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

".

In [8]:

```
d_eq_y.substitution(expr, assumptions=[d_eq_y])
```

Either way, the generated proof is the same:

In [9]:

```
d_eq_y.substitution(expr, assumptions=[d_eq_y]).proof()
```

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 `inner_expr()`

method on the top-level expression:

In [10]:

```
inner_expr = expr.inner_expr()
```

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]:

```
inner_expr = inner_expr.rhs
```

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]:

```
inner_expr = inner_expr.operands[1]
```

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]:

```
inner_expr = inner_expr.denominator
```

In [14]:

```
d_eq_y.substitution(inner_expr, assumptions=[d_eq_y])
```

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.inner_expr().rhs.operands[2].exponent, assumptions=[d_eq_y])
```

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 `sub_right_side_into`

and `sub_left_side_into`

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 `sub_right_side_into`

:

In [16]:

```
d_eq_y.sub_right_side_into(g_repl, assumptions=[d_eq_y,expr])
```

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

In [17]:

```
d_eq_y.sub_right_side_into(expr, assumptions=[d_eq_y,expr])
```

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 `sub_left_side_into`

:

In [18]:

```
y_eq_d = Equals(y, d)
```

In [19]:

```
y_eq_d.sub_left_side_into(g_repl, assumptions=[y_eq_d,expr])
```

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

In [20]:

```
y_eq_d.sub_left_side_into(expr, assumptions=[y_eq_d,expr])
```

The proof uses a theorem the relies upon the `substitution`

axiom, rather than using the `substition`

axiom directly:

In [21]:

```
y_eq_d.sub_left_side_into(expr, assumptions=[y_eq_d,expr]).proof()
```

The `conclude_via_direct_substitution`

allows us to conclude the equality between two expressions that have the same structure apart from sub-expressions that are known to be equal. For example,

In [22]:

```
from proveit import Function
from proveit import f, g, h, n, alpha, beta, delta, theta
_eq = Equals(Function(f, (Function(g, (a, b)), Function(h, (c, d)))),
Function(f, (Function(g, (a, beta)), Function(h, (c, delta)))))
```

In [23]:

```
_eq.conclude_via_direct_substitution(
assumptions=[Equals(b, beta), Equals(d, delta)])
```

This method is limited, however, and does not resolve cascading substitutions such as the following example:

In [24]:

```
_eq = Equals(Function(f, (Function(g, (a, b)), Function(h, (c, d)))),
Function(f, (Function(g, (a, beta)), theta)))
```

In [25]:

```
_assumptions = [Equals(b, beta), Equals(d, delta),
Equals(Function(h, (c, delta)), theta)]
```

In [26]:

```
try:
_eq.conclude_via_direct_substitution(assumptions=_assumptions)
assert False, "An error was expected but didn't occur."
except ValueError as e:
print("Expected Error: %s"%e)
```

But it can handle inner scopes with conditions if the proper equalities are explicitly known (proven) under appropriate assumptions. For example,

In [27]:

```
from proveit import ExprTuple
from proveit.logic import Forall, Exists, InSet
from proveit.numbers import Natural
_eq = Equals(Function(f, (Function(g, (a, b)), Exists(n, Function(h, n), domain=Natural))),
Function(f, (Function(g, (alpha, beta)), Exists(n, Function(theta, n), domain=Natural))))
```

In [28]:

```
_assumptions = (Forall(n, Equals(Function(h, n), Function(theta, n)), domain=Natural),
Equals(ExprTuple(a, b), ExprTuple(alpha, beta)))
```

In [29]:

```
_assumptions[0].instantiate(assumptions=_assumptions+(InSet(n, Natural),))
```

In [30]:

```
_eq.conclude_via_direct_substitution(assumptions=_assumptions)
```

Also note that we were able to substitute operands via equating `ExprTuple`

s in this example.

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 [31]:

```
from proveit.logic.equality import equals_reflexivity, equals_symmetry, equals_transitivity
```

In [32]:

```
equals_reflexivity
```

In [33]:

```
equals_symmetry
```

In [34]:

```
equals_transitivity
```

`equals_reversal`

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

In [35]:

```
from proveit.logic.equality import equals_reversal
equals_reversal # y=x derives from x=y
```

These three properties are applied automatically for `Equals`

objects

Reflexivity is concluded automatically:

In [36]:

```
Equals(a, a).prove()
```

In [37]:

```
Equals(a, a).prove().proof()
```

Symmetric statements are derived as side-effects. Note that the `Judgment.derive_side_effects`

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 [38]:

```
a_eq_b = Equals(a, b)
```

In [39]:

```
Equals(b, a).prove(assumptions=[a_eq_b])
```

The reversed form may also be derived explicitly via `derive_reversed`

. The proof is the same.

In [40]:

```
a_eq_b.prove(assumptions=[a_eq_b]).derive_reversed()
```

Transitivity derivations are attempted with automation via the `conclude_via_transitivity`

method from the `TransitiveRelation`

superclass of `Equals`

. This performs a breadth-first, bidirectional search (meeting in the middle from both ends) over the space of **Judgment** 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 **Judgment**s will be small and this search algorithm will have ample efficiency.

In [41]:

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

In [42]:

```
d_eq_c = Equals(d, c)
```

In [43]:

```
d_eq_z = Equals(d, z)
```

In [44]:

```
a_eq_z = Equals(a, z).conclude_via_transitivity(assumptions=[a_eq_b, c_eq_b, d_eq_c, d_eq_z])
```

The `apply_transivity`

method applies the transitivity relation explicity.

In [45]:

```
a_eq_b.prove(assumptions=[a_eq_b]).apply_transitivity(c_eq_b, assumptions=[c_eq_b])
```

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 **Judgment** is stored for future reference in `Equals.evaluations`

for making other evaluations.

`TRUE`

($\top$) and `FALSE`

($\bot$) are both `IrreducibleValue`

s:

In [46]:

```
from proveit.logic import TRUE, FALSE, IrreducibleValue
```

In [47]:

```
isinstance(TRUE, IrreducibleValue)
```

In [48]:

```
isinstance(FALSE, IrreducibleValue)
```

In [49]:

```
TRUE.evaluation()
```

An `IrreducibleValue`

should implement the `eval_equality`

and `deduce_not_equal`

methods to prove equality relations with other `IrreducibleValue`

s as appropriate.

In [50]:

```
Equals(Equals(FALSE, TRUE), FALSE).derive_contradiction(
assumptions=[Equals(FALSE, TRUE)])
```

In [51]:

```
TRUE.eval_equality(TRUE)
```

In [52]:

```
TRUE.eval_equality(FALSE)
```

In [53]:

```
TRUE.deduce_not_equal(FALSE)
```

A proven expression will evaluate to `TRUE`

.

In [54]:

```
from proveit.logic import evaluate_truth
evaluate_truth(a, assumptions=[a])
```

In [55]:

```
a_eq_T = a.evaluation(assumptions=[a])
```

A disproven expression will evaluate to `FALSE`

.

In [56]:

```
a_eq_F = a.evaluation(assumptions=[Not(a)])
```

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 [57]:

```
b_eq_F = b.evaluation(assumptions=[Equals(b, a), Not(a)])
```

In [58]:

```
b_eq_F.proof()
```

When evaluating an expression, an evaluation of the operands will be attempted. The operation class is responsible for overridding the `evaluation`

method, or `do_reduced_evaluation`

(called by the default `Expression.evaluation`

method that first reduces the operation by evaluating its operands) in order to properly treat the operation applied to irreducible values or generate a more efficient proof as appropriate.

In [59]:

```
from proveit.logic import Or, Not, in_bool
```

In [60]:

```
nested_eval = Or(a, Not(a)).evaluation(assumptions=[a])
```

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 [61]:

```
TRUE
```

In [62]:

```
FALSE
```

Proofs via boolean equality are automatic via `Equals.deduce_side_effects`

:

In [63]:

```
a.prove(assumptions=[Equals(a, TRUE)])
```

In [64]:

```
Not(b).prove(assumptions=[Equals(b, FALSE)])
```

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

:

In [65]:

```
Equals(x, TRUE).prove(assumptions=[x])
```

In [66]:

```
Equals(TRUE, y).prove(assumptions=[y])
```

In [67]:

```
Equals(c, FALSE).prove(assumptions=[Not(c)])
```

In [68]:

```
Equals(FALSE, c).prove(assumptions=[Not(c)])
```

When something is equal to `FALSE`

and known to be true, there is a contradiction. That is, `FALSE`

is a consequence. The `derive_contradiction`

method of `Equals`

can be used to prove such a contradiction:

In [69]:

```
contradiction = Equals(a, FALSE).derive_contradiction(assumptions=[a, Equals(a, FALSE)])
```

In [70]:

```
contradiction.proof()
```

Contradictions are useful in making contradiction proofs (reductio ad absurdum). The `affirm_via_contradiction`

and `deny_via_contradiction`

methods are useful in making such a proof. They both use `derive_contradiction`

. For example:

In [71]:

```
from proveit.logic import Implies, in_bool
not_a__truth = Equals(a, FALSE).affirm_via_contradiction(
Not(a), assumptions=[Implies(a, Equals(a, FALSE)), in_bool(a)])
```

In [72]:

```
not_a__truth.proof().num_steps()
```

It is more efficient to use `deny_via_contradiction`

when proving the negation of something. Here we prove the same as above but in fewer steps.

In [73]:

```
not_b__truth = Equals(b, FALSE).deny_via_contradiction(
b, assumptions=[Implies(b, Equals(b, FALSE)), in_bool(b)])
```

In [74]:

```
not_b__truth.proof().num_steps()
```

In [75]:

```
not_b__truth.proof()
```

All equality expressions are in the boolean set by the `equality_in_bool`

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 [76]:

```
eq_in_bool = Equals(a, b).deduce_in_bool()
```

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

In [77]:

```
in_singleton_truth = Equals(x, c).derive_is_in_singleton(assumptions=[Equals(x, c)])
```

The `NotEquals`

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

In [78]:

```
from proveit.logic import NotEquals
```

In [79]:

```
a_neq_b = NotEquals(a, b)
```

In [80]:

```
a_neq_b.definition()
```

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

.

In [81]:

```
a_neq_b.prove(assumptions=[Not(a_eq_b)])
```

In [82]:

```
a_neq_b.prove(assumptions=[Not(a_eq_b)]).proof()
```

In [83]:

```
Not(a_eq_b).prove(assumptions=[a_neq_b])
```

In [84]:

```
Not(a_eq_b).prove(assumptions=[a_neq_b]).proof()
```

`NotEquals`

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

In [85]:

```
NotEquals(b, a).prove(assumptions=[a_neq_b])
```

Or explicitly via `derive_reversed`

In [86]:

```
a_neq_b.prove(assumptions=[a_neq_b]).derive_reversed()
```

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

In [87]:

```
neq_contradiction = a_neq_b.derive_contradiction(assumptions=[a_neq_b, a_eq_b])
```

In [88]:

```
a_neq_a = NotEquals(a, a)
```

In [89]:

```
b_from_contradiction = a_neq_a.affirm_via_contradiction(
b, assumptions=[Implies(Not(b), a_neq_a), in_bool(b)])
```

In [90]:

```
%end demonstrations
```