Rewriting modulo associativity and commutativity
This
Coq plugin provides tactics for
rewriting universally quantified equations, modulo associative and
possibly commutative operators, and modulo neutral elements (units):
Examples
Proving the reverse triangle inequality
Using aac_rewrite, we obtain a proof of the reverse triangle
inequality which is similar to the penandpaper proof.
Lemma Zabs_triangle:
forall x y, Zabs (x+y) ≤ Zabs x + Zabs y.
Lemma Zplus_opp_r :
forall x, x +  x = 0.
Variables a b :
Z.
Goal
Zabs a +  Zabs b ≤ Zabs (a  b).
aac_rewrite ←
(Zminus_diag b) at 3.

(* Zabs (a + (b  b)) +  Zabs b ≤ Zabs (a  b)  *) 

unfold
Zminus.

(* Zabs (a + (b +  b)) +  Zabs b ≤ Zabs (a +  b)  *) 

aac_rewrite Zabs_triangle.

(* Zabs ( b + a) + Zabs b +  Zabs b ≤ Zabs (a +  b)  *) 

aac_rewrite Zplus_opp_r.

(* 0 + Zabs ( b + a) ≤ Zabs (a +  b)  *) 

aac_reflexivity.

 

Qed.
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
explicitly.
Notation "x ² " := (x*x).
Notation "2 ⋅ x" := (x+x).
Lemma Hbin1:
forall x y, (x+y)² = x² +y² +2⋅x*y.
Lemma Hbin2:
forall x y, x² + y² = (x+y)²  2⋅x*y .
Lemma Hopp :
forall x, x  x = 0.
Variables a b c :
Z.
Hypothesis H: c² + 2⋅(a+1)*b = (a+1+b)².
Goal a² + b² + 2⋅a + 1 =
c².
aacu_rewrite
← Hbin1.

(* (1 + a)² + b² = c²  *) 
(* substitution [x → a; y → 1]  *) 
rewrite Hbin2.

(* (b + (1 + a))²  (2 ⋅ b * (1 + a)) = c²  *) 
(* substitution [x → 1+a; y → b]  *) 
aac_rewrite
← H.

(* c² + 2 ⋅ (a + 1) * b  (2 ⋅ (1 + a) * b) = c²  *) 
(* no substitution  *) 
aac_rewrite Hopp.

(* 0 + c² = c²  *) 
(* substitution [x → 2 ⋅ (a + 1) * b]  *) 
aac_reflexivity.


Qed.
Downloads
 Version 0.3pl1 (April 2013) tar.gz. Distributed under LGPL 3. Compiles
with the Coq v8.4pl2.
 Version 0.2pl3 (February 2011) tar.gz. Distributed under LGPL 3. Compiles
with the Coq v8.3.
 Documented Coq file that illustrates how to use the library:
What's new
 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)
Documentation
Please refer to
the tutorial for a
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 innerworking of the plugin, here is the
coqdoc generated documentation of the Coq
theory file, and here is the
ocamldoc
generated documentation of the OCaml files of the plugin.
Authors
Thomas Braibant and
Damien Pous
Last modified: Tue Feb 22 13:21:03 CET 2011