# 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.

## 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