Demonstrations for the theory of proveit.logic.equality¶
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:
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,
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.
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:
g_repl = Lambda.global_repl(expr, d)
We now use this lambda map to replace occurences of $d$ in expr with $y$:
d_eq_y = Equals(d, y)
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".
d_eq_y.substitution(expr, assumptions=[d_eq_y])
Either way, the generated proof is the same:
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:
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:
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):
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:
inner_expr = inner_expr.denominator
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:
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:
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.
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:
y_eq_d = Equals(y, d)
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.
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:
y_eq_d.sub_left_side_into(expr, assumptions=[y_eq_d,expr]).proof()
Concluding an equality via direct substitution¶
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,
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)))))
_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:
_eq = Equals(Function(f, (Function(g, (a, b)), Function(h, (c, d)))),
Function(f, (Function(g, (a, beta)), theta)))
_assumptions = [Equals(b, beta), Equals(d, delta),
Equals(Function(h, (c, delta)), theta)]
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,
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))))
_assumptions = (Forall(n, Equals(Function(h, n), Function(theta, n)), domain=Natural),
Equals(ExprTuple(a, b), ExprTuple(alpha, beta)))
_assumptions[0].instantiate(assumptions=_assumptions+(InSet(n, Natural),))
, 
⊢ 
_eq.conclude_via_direct_substitution(assumptions=_assumptions)
, ⊢
Also note that we were able to substitute operands via equating ExprTuples in this example.
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.
from proveit.logic.equality import equals_reflexivity, equals_symmetry, equals_transitivity
equals_reflexivity
equals_symmetry
equals_transitivity
equals_reversal is a useful theorem for applying the symmetry property of equality:
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:
Equals(a, a).prove()
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)
a_eq_b = Equals(a, b)
Equals(b, a).prove(assumptions=[a_eq_b])
The reversed form may also be derived explicitly via derive_reversed. The proof is the same.
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 Judgments will be small and this search algorithm will have ample efficiency.
# We'll make this interesting by reversing some of the equations in the chain.
c_eq_b = Equals(c, b)
d_eq_c = Equals(d, c)
d_eq_z = Equals(d, z)
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.
a_eq_b.prove(assumptions=[a_eq_b]).apply_transitivity(c_eq_b, assumptions=[c_eq_b])
, ⊢ 
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 Judgment is stored for future reference in Equals.evaluations for making other evaluations.
TRUE ($\top$) and FALSE ($\bot$) are both IrreducibleValues:
from proveit.logic import TRUE, FALSE, IrreducibleValue
isinstance(TRUE, IrreducibleValue)
isinstance(FALSE, IrreducibleValue)
TRUE.evaluation()
An IrreducibleValue should implement the eval_equality and deduce_not_equal methods to prove equality relations with other IrreducibleValues as appropriate.
Equals(Equals(FALSE, TRUE), FALSE).derive_contradiction(
assumptions=[Equals(FALSE, TRUE)])
TRUE.eval_equality(TRUE)
TRUE.eval_equality(FALSE)
TRUE.deduce_not_equal(FALSE)
A proven expression will evaluate to TRUE.
from proveit.logic import evaluate_truth
evaluate_truth(a, assumptions=[a])
a_eq_T = a.evaluation(assumptions=[a])
⊢ 
A disproven expression will evaluate to FALSE.
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.
b_eq_F = b.evaluation(assumptions=[Equals(b, a), Not(a)])
, ⊢ 
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.
from proveit.logic import Or, Not, in_bool
nested_eval = Or(a, Not(a)).evaluation(assumptions=[a])
⊢ 
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.
TRUE
FALSE
Proofs via boolean equality are automatic via Equals.deduce_side_effects:
a.prove(assumptions=[Equals(a, TRUE)])
Not(b).prove(assumptions=[Equals(b, FALSE)])
Going the other direction, boolean equalities are proven automatically via Equals.conclude:
Equals(x, TRUE).prove(assumptions=[x])
Equals(TRUE, y).prove(assumptions=[y])
Equals(c, FALSE).prove(assumptions=[Not(c)])
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:
contradiction = Equals(a, FALSE).derive_contradiction(assumptions=[a, Equals(a, FALSE)])
, ⊢ 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:
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)])
, 
⊢ 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.
not_b__truth = Equals(b, FALSE).deny_via_contradiction(
b, assumptions=[Implies(b, Equals(b, FALSE)), in_bool(b)])
, 
⊢ 
not_b__truth.proof().num_steps()
not_b__truth.proof()
Equality and sets¶
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).
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_singleton_truth = Equals(x, c).derive_is_in_singleton(assumptions=[Equals(x, c)])
⊢ 
Not equals¶
The NotEquals operation is a more way of expressing that two mathematical objects are not equal to each other.
from proveit.logic import NotEquals
a_neq_b = NotEquals(a, b)
a_neq_b.definition()
From $\lnot (a = b)$ one can derive $a \neq b$ and vice-versa, folding and unfolding the NotEquals.
a_neq_b.prove(assumptions=[Not(a_eq_b)])
a_neq_b.prove(assumptions=[Not(a_eq_b)]).proof()
Not(a_eq_b).prove(assumptions=[a_neq_b])
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.
NotEquals(b, a).prove(assumptions=[a_neq_b])
Or explicitly via derive_reversed
a_neq_b.prove(assumptions=[a_neq_b]).derive_reversed()
If two objects are both equal and not equal, there is a contradiction.
neq_contradiction = a_neq_b.derive_contradiction(assumptions=[a_neq_b, a_eq_b])
, ⊢ a_neq_a = NotEquals(a, a)
b_from_contradiction = a_neq_a.affirm_via_contradiction(
b, assumptions=[Implies(Not(b), a_neq_a), in_bool(b)])
, 
⊢ 
%end demonstrations