Applies "obvious" simplifications to each hypothesis, using each of the other hypotheses in turn. For instance, if the other hypothesis is of the form P and the current hypothesis is of the form P|Q, it gets simplified to Q. Then, simplify the goal using all the other hypotheses. If, in the course of doing so, a hypothesis turns into false, or the goal turns into true, complete the goal.
"Expensive" simplifications that require linear algebra or SAT solving are not implemented in this tactic. If use_sympy is set to true, sympy's native simplifier simplify is invoked; as a consequence, sometimes this tactic will perform simplification even in the presence of an irrelevant hypothesis.
Some examples of supported simplifications:
| Statement | Hypothesis | Simplification |
|---|---|---|
P |
P |
true |
P |
Not(P) |
false |
x >= y |
x <= y |
Eq(x,y) |
x >= y |
Ne(x,y) |
x > y |
Max(x,y) |
x <= y |
y |
Min(x,y) |
x <= y |
x |
The set of simplifications performed is currently far from complete. If you discover that a situation where an "obvious" simplification should have occurred, but didn't, please inform me (e.g., via a github issue) to see if it can be added to the simplification routine.
Note: setting use_sympy = True can cause additional issues due to various unwanted simplifications generated by this tool (most notably involving subtraction, which is not fully defined for orders of magnitude). Also it does not guard against issues such as division by zero. For instance, x/x will simplify to 1 even if x is not proven to be non-zero.
In some cases, SimpAll() may need to be iterated to apply later simplifications again; setting repeat to True will automatically perform such iteration until no further changes to the proof state occur. Due to (unfortunate) non-determinism in the ordering of Python core classes such as set and dict, it can occur that the effect of SimpAll() may also be non-deterministic, particularly if repeat is False.
Example:
>>> from estimates.main import *
>>> p = case_split_exercise()
Starting proof. Current proof state:
P: bool
Q: bool
R: bool
S: bool
h1: P | Q
h2: R | S
|- (P & R) | (P & S) | (Q & R) | (Q & S)
>>> p.use(Cases("h1"))
Splitting h1: P | Q into cases.
2 goals remaining.
>>> p.use(SimpAll())
Simplified (P & R) | (P & S) | (Q & R) | (Q & S) to R | S using Q.
Simplified R | S to True using R | S.
Goal solved!
1 goal remaining.
>>> p.use(SimpAll(repeat=True))
Simplified (P & R) | (P & S) | (Q & R) | (Q & S) to R | S | (P & R) | (P & S) using {Type((S,)), Type((Q,)), R | S, Q, Type((P,)), Type((R,))}.
Simplified R | S | (P & R) | (P & S) to True using {Type((S,)), Type((Q,)), R | S, Q, Type((P,)), Type((R,))}.
Goal solved!
Proof complete!
Example:
>>> from estimates.main import *
>>> p = sympy_simplify_exercise()
Starting proof. Current proof state:
x: real
y: real
|- Eq((x - y)*(x + y), x**2 - y**2)
>>> p.use(SimpAll(use_sympy=True))
Simplified Eq((x - y)*(x + y), x**2 - y**2) to True using None.
Goal solved!
Proof complete!
Breaks up a relational inequality goal into a chain of relational inequality subgoals, where the relation operators and intermediate terms are passed as alternating arguments to Calc. For instance, if the goal is x < y, and Calc( "<", z, "<=", w, "==") is called, then the goal is split into three subgoals x < z, z <= w, w == y. Of course, the relations have to be compatible in the sense that the subgoals imply the original goal.
>>> from estimates.main import *
>>> p = calc_example()
Starting proof. Current proof state:
x: real
y: real
hx: x < 4
hy: y >= 4
|- x < y
>>> p.use(Calc("<", 4, "<="))
Split into goals x < 4, 4 <= y.
2 goals remaining.
>>> print(p)
Proof Assistant is in tactic mode. Current proof state:
x: real
y: real
hx: x < 4
hy: y >= 4
|- x < 4
This is goal 1 of 2.
>>> p.next_goal()
Moved to goal 2 of 2.
>>> print(p)
Proof Assistant is in tactic mode. Current proof state:
x: real
y: real
hx: x < 4
hy: y >= 4
|- 4 <= y
This is goal 2 of 2.