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.2-pl2 (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 patch to compile with Coq
trunk r13847
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.
Older versions
- Version 0.1 (16th of June, 2010): tar.gz. Distributed under LGPL 3. Compiles
with the Coq v8.3 `beta' (-r 13027, -r 13060 and hopefully the
following ones until -r 13243).
- Version 0.1-pl1 (5th of July, 2010) tar.gz. Distributed under LGPL 3. Compiles
with the Coq v8.3 `beta' (at least -r 13244, -r 13422, and hopefully
the following ones).
- Version 0.2-pl1 (5th of July, 2010) tar.gz. Distributed under LGPL 3. Compiles
with the Coq v8.3 `beta' (at least -r 13244, -r 13422, and hopefully
the following ones).
Authors
Thomas Braibant and
Damien Pous
Last modified: Tue Feb 22 13:21:03 CET 2011