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 pen-and-paper 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.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:
- a simple tutorial, and corresponding .v source file.
- some caveats and limitations, and corresponding .v source file.

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 inner-working 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