54f2c0f254
The motivation is to reduce the number of instances generated by ematching. For example, given inv_inv: forall a, (a⁻¹)⁻¹ = a the new heuristic uses ((a⁻¹)⁻¹) as the pattern. This matches the intuition that inv_inv should be used a simplification rule. The default pattern inference procedure would use (a⁻¹). This is bad because it generates an infinite chain of instances whenever there is a term (a⁻¹) in the proof state. By using (a⁻¹), we get (a⁻¹)⁻¹ = a Now that we have (a⁻¹)⁻¹, we can match again and generate ((a⁻¹)⁻¹)⁻¹ = a⁻¹ and so on
11 lines
No EOL
309 B
Text
11 lines
No EOL
309 B
Text
VISIT consume_args.lean
|
|
SYNC 7
|
|
import logic data.nat.basic
|
|
open nat eq.ops algebra
|
|
|
|
theorem tst (a b c : nat) : a + b + c = a + c + b :=
|
|
calc a + b + c = a + (b + c) : by rewrite add.assoc
|
|
... = a + (c + b) : by rewrite (add.comm b c)
|
|
... = a + c + b : by rewrite add.assoc
|
|
WAIT
|
|
INFO 7 |