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
49 lines
535 B
Text
49 lines
535 B
Text
-- BEGINWAIT
|
||
-- ENDWAIT
|
||
-- BEGININFO
|
||
-- SYMBOL|7|15
|
||
=
|
||
-- ACK
|
||
-- TYPE|7|17
|
||
ℕ
|
||
-- ACK
|
||
-- IDENTIFIER|7|17
|
||
a
|
||
-- ACK
|
||
-- TYPE|7|19
|
||
ℕ → ℕ → ℕ
|
||
-- ACK
|
||
-- SYMBOL|7|19
|
||
+
|
||
-- ACK
|
||
-- TYPE|7|21
|
||
ℕ
|
||
-- ACK
|
||
-- IDENTIFIER|7|21
|
||
c
|
||
-- ACK
|
||
-- TYPE|7|23
|
||
ℕ → ℕ → ℕ
|
||
-- ACK
|
||
-- SYMBOL|7|23
|
||
+
|
||
-- ACK
|
||
-- TYPE|7|25
|
||
ℕ
|
||
-- ACK
|
||
-- IDENTIFIER|7|25
|
||
b
|
||
-- ACK
|
||
-- SYMBOL|7|31
|
||
by
|
||
-- ACK
|
||
-- SYMBOL|7|34
|
||
rewrite
|
||
-- ACK
|
||
-- TYPE|7|42
|
||
∀ (a_1 b_1 c_1 : ?A), (:a_1 + b_1 + c_1:) = (:a_1 + (b_1 + c_1):)
|
||
-- ACK
|
||
-- IDENTIFIER|7|42
|
||
add.assoc
|
||
-- ACK
|
||
-- ENDINFO
|