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_rewriteHbin1.   
(* (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_rewriteH.
(* 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

What's new

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