Rewriting modulo associativity and commutativity
plugin provides tactics for
rewriting universally quantified equations, modulo associative and
possibly commutative operators, and modulo neutral elements (units):
Proving the reverse triangle inequality
Using aac_rewrite, we obtain a proof of the reverse triangle
inequality which is similar to the pen-and-paper proof.
x y, Zabs (x+y) ≤ Zabs x + Zabs y.
x, x + - x = 0.
a b : Z
Zabs a + - Zabs b ≤ Zabs (a - b).
(Zminus_diag b) at 3.
|| (* Zabs (a + (b - b)) + - Zabs b ≤ Zabs (a - b) || *)
|| (* Zabs (a + (b + - b)) + - Zabs b ≤ Zabs (a + - b) || *)
|| (* Zabs (- b + a) + Zabs b + - Zabs b ≤ Zabs (a + - b) || *)
|| (* 0 + Zabs (- b + a) ≤ Zabs (a + - b) || *)
Exploiting binomial identities
Here is an example where we show how to exploit binomial identities to
prove a goal about Pythagorean triples, without breaking a sweat. By
comparison, making the rewrites using standard tools is difficult
since this requires to manage parentheses and term reorderings
"x ² " := (x*x).
"2 ⋅ x" := (x+x).
x y, (x+y)² = x² +y² +2⋅x*y.
x y, x² + y² = (x+y)² - 2⋅x*y .
x, x - x = 0.
a b c : Z
: c² + 2⋅(a+1)*b = (a+1+b)².
a² + b² + 2⋅a + 1 =
| (* (1 + a)² + b² = c² || *)
|| (* substitution [x → a; y → 1] || *)
| (* (b + (1 + a))² - (2 ⋅ b * (1 + a)) = c² || *)
|| (* substitution [x → 1+a; y → b] || *)
| (* c² + 2 ⋅ (a + 1) * b - (2 ⋅ (1 + a) * b) = c² || *)
|| (* no substitution || *)
| (* 0 + c² = c² || *)
|| (* substitution [x → 2 ⋅ (a + 1) * b] || *)
- Version 0.3-pl1 (April 2013) tar.gz. Distributed under LGPL 3. Compiles
with the Coq v8.4-pl2.
- Version 0.2-pl3 (February 2011) tar.gz. Distributed under LGPL 3. Compiles
with the Coq v8.3.
- Documented Coq file that illustrates how to use the library:
- Several operators can share a given unit (like max and plus
sharing zero on nat)
- Added some support to rewrite inequations (using inequations)
- Better printing functions for aac_instances
- Overhauled inference of morphisms and operators :
- Lift the previous requirement to have at least one AC and one A
operator for each setting
- Binary operators can start with universal quantifications
(e.g., List.app is recognised as being associative)
- Should now be able to handle goal with evars (but this is not unification modulo AC)
- Added several instances of associative and commutative operators
- The tactics do not abstract the proofs they build (was troublesome if evars appeared)
Please refer to the tutorial
succinct introduction on how to use these tactics, and to the README
file from the archive for explanations
about how to install the plugin.
To understand the inner-working of the plugin, here is the
coqdoc generated documentation
of the Coq
theory file, and here is the ocamldoc
of the OCaml files of the plugin.
Last modified: Tue Feb 22 13:21:03 CET 2011