New upstream version 8.8.0+1.gbp069dc3bupstream/8.8.0+1.gbp069dc3bupstream

5 files changed, 2196 insertions, 0 deletions

diff --git a/theories/AAC.v b/theories/AAC.v
new file mode 100644
index 0000000..d7cc7a2
--- /dev/null
+++ b/theories/AAC.v
@@ -0,0 +1,901 @@
+(***************************************************************************)
+(*  This is part of aac_tactics, it is distributed under the terms of the  *)
+(*         GNU Lesser General Public License version 3                     *)
+(*              (see file LICENSE for more details)                        *)
+(*                                                                         *)
+(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
+(***************************************************************************)
+
+(** * Theory file for the aac_rewrite tactic
+
+   We define several base classes to package associative and possibly
+   commutative operators, and define a data-type for reified (or
+   quoted) expressions (with morphisms).
+
+   We then define a reflexive decision procedure to decide the
+   equality of reified terms: first normalise reified terms, then
+   compare them. This allows us to close transitivity steps
+   automatically, in the [aac_rewrite] tactic.
+  
+   We restrict ourselves to the case where all symbols operate on a
+   single fixed type. In particular, this means that we cannot handle
+   situations like  
+
+   [H: forall x y, nat_of_pos (pos_of_nat (x) + y) + x = ....]
+
+   where one occurrence of [+] operates on nat while the other one
+   operates on positive. *)
+
+Require Import Arith NArith.
+Require Import List.
+Require Import FMapPositive FMapFacts.
+Require Import RelationClasses Equality.
+Require Export Morphisms.
+
+From AAC_tactics
+Require Import Utils.
+
+Set Implicit Arguments.
+Set Asymmetric Patterns.
+
+Local Open Scope signature_scope.
+
+(** * Environments for the reification process: we use positive maps to index elements *)
+
+Section sigma.
+  Definition sigma := PositiveMap.t.
+  Definition sigma_get A (null : A) (map : sigma A) (n : positive) : A :=
+    match PositiveMap.find n map with
+      | None => null
+      | Some x => x
+    end.
+  Definition sigma_add := @PositiveMap.add.
+  Definition sigma_empty := @PositiveMap.empty.
+End sigma.
+
+
+(** * Classes for properties of operators *)
+
+Class Associative (X:Type) (R:relation X) (dot: X -> X -> X) :=
+  law_assoc : forall x y z, R (dot x (dot y z)) (dot (dot x y) z).
+Class Commutative (X:Type) (R: relation X) (plus: X -> X -> X) :=
+  law_comm: forall x y, R (plus x y) (plus y x).
+Class Unit (X:Type) (R:relation X) (op : X -> X -> X) (unit:X) := {
+  law_neutral_left: forall x, R (op unit x) x;
+  law_neutral_right: forall x, R (op x unit) x
+}.
+
+
+(** Class used to find the equivalence relation on which operations
+   are A or AC, starting from the relation appearing in the goal *)
+
+Class AAC_lift X (R: relation X) (E : relation X) := {
+  aac_lift_equivalence : Equivalence E;
+  aac_list_proper : Proper (E ==> E ==> iff) R
+}.
+
+(** simple instances, when we have a subrelation, or an equivalence *)
+
+Instance aac_lift_subrelation {X} {R} {E} {HE: Equivalence E}
+  {HR: @Transitive X R} {HER: subrelation E R}: AAC_lift  R E | 3.
+Proof.
+  constructor; trivial.
+  intros ? ? H ? ? H'. split; intro G.
+   rewrite <- H, G. apply HER, H'.
+   rewrite H, G. apply HER. symmetry. apply H'.
+Qed.
+
+Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E}
+  {HR: Proper (E==>E==>iff) R}: AAC_lift  R E | 4 := {}.
+
+
+
+Module Internal.
+(** * Utilities for the evaluation function *)
+
+Section copy.
+
+  Context {X} {R} {HR: @Equivalence X R} {plus}
+   (op: Associative R plus) (op': Commutative R plus) (po: Proper (R ==> R ==> R) plus).
+
+  (* copy n x = x+...+x (n times) *)
+  Fixpoint copy' n x := match n with
+                         | xH => x
+                         | xI n => let xn := copy' n x in plus (plus xn xn) x
+                         | xO n => let xn := copy' n x in (plus xn xn)
+                       end.
+  Definition copy n x :=  Prect (fun _ => X) x (fun _ xn => plus x xn) n.
+     
+  Lemma copy_plus : forall n m x, R (copy (n+m) x) (plus (copy n x) (copy m x)).
+  Proof.
+    unfold copy.
+    induction n using Pind; intros m x.
+     rewrite Prect_base. rewrite <- Pplus_one_succ_l. rewrite Prect_succ. reflexivity. 
+     rewrite Pplus_succ_permute_l. rewrite 2Prect_succ. rewrite IHn. apply op.
+  Qed.
+  Lemma copy_xH : forall x, R (copy 1 x) x.
+  Proof. intros; unfold copy; rewrite Prect_base. reflexivity. Qed.
+  Lemma copy_Psucc : forall n x, R (copy (Pos.succ n) x) (plus x (copy n x)).
+  Proof. intros; unfold copy; rewrite Prect_succ. reflexivity. Qed.
+
+  Global Instance copy_compat n: Proper (R ==> R) (copy n).
+  Proof.
+    unfold copy.
+    induction n using Pind; intros x y H.
+     rewrite 2Prect_base. assumption.
+     rewrite 2Prect_succ. apply po; auto.
+  Qed.
+
+End copy.
+
+(** * Packaging structures *)
+
+(** ** free symbols  *)
+
+Module Sym.
+  Section t.
+    Context {X} {R : relation X} .
+   
+    (** type of an arity  *)
+    Fixpoint type_of  (n: nat) :=
+      match n with
+        | O => X
+        | S n => X -> type_of  n
+      end.
+
+    (** relation to be preserved at an arity  *)
+    Fixpoint rel_of n : relation (type_of n) :=
+      match n with
+        | O => R
+      | S n => respectful R (rel_of n)
+      end.
+   
+  (** a symbol package contains an arity,
+     a value of the corresponding type,
+     and a proof that the value is a proper morphism *)
+  Record pack  : Type := mkPack {
+    ar : nat;
+    value :> type_of  ar;
+    morph : Proper (rel_of ar) value
+  }.
+
+  (** helper to build default values, when filling reification environments *)
+  Definition null: pack := mkPack 1 (fun x => x) (fun _ _ H => H).
+   
+  End t.
+
+End Sym.
+  
+(** ** binary operations *)
+
+Module Bin.
+  Section t.
+    Context {X} {R: relation X}.
+
+    Record pack := mk_pack {
+      value:> X -> X -> X;
+      compat: Proper (R ==> R ==> R) value;
+      assoc: Associative R value;
+      comm: option (Commutative R value)
+    }.
+  End t.
+  (*    See #<a href="Instances.html">Instances.v</a># for concrete instances of these classes. *)
+
+End Bin.
+
+
+(** * Reification, normalisation, and decision  *)
+
+Section s.
+  Context {X} {R: relation X} {E: @Equivalence X R}.
+  Infix "==" := R (at level 80).
+
+  (* We use environments to store the various operators and the
+     morphisms.*)
+ 
+  Variable e_sym: idx -> @Sym.pack X R.
+  Variable e_bin: idx -> @Bin.pack X R.
+
+ 
+  (** packaging units (depends on e_bin) *)
+
+  Record unit_of u := mk_unit_for {
+    uf_idx: idx;
+    uf_desc: Unit R (Bin.value (e_bin uf_idx)) u
+  }.
+
+  Record unit_pack := mk_unit_pack {
+    u_value:> X;
+    u_desc: list (unit_of u_value)
+  }.
+  Variable e_unit: positive -> unit_pack.
+ 
+  Hint Resolve e_bin e_unit: typeclass_instances.
+
+  (** ** Almost normalised syntax
+     a term in [T] is in normal form if:
+     - sums do not contain sums
+     - products do not contain products
+     - there are no unary sums or products
+     - lists and msets are lexicographically sorted according to the order we define below
+    
+     [vT n] denotes the set of term vectors of size [n] (the mutual dependency could be removed),
+
+     Note that [T] and [vT] depend on the [e_sym] environment (which
+     contains, among other things, the arity of symbols)
+     *)
+
+  Inductive T: Type :=
+  | sum: idx -> mset T -> T
+  | prd: idx -> nelist T -> T
+  | sym: forall i, vT (Sym.ar (e_sym i)) -> T
+  | unit : idx -> T
+  with vT: nat -> Type :=
+  | vnil: vT O
+  | vcons: forall n, T -> vT n -> vT (S n).
+
+
+  (** lexicographic rpo over the normalised syntax *)
+  Fixpoint compare (u v: T) :=
+    match u,v with
+      | sum i l, sum j vs => lex (idx_compare i j) (mset_compare compare l vs)
+      | prd i l, prd j vs => lex (idx_compare i j) (list_compare compare l vs)
+      | sym i l, sym j vs => lex (idx_compare i j) (vcompare l vs)
+      | unit i , unit j => idx_compare i j
+      | unit _ , _        => Lt
+      | _      , unit _  => Gt
+      | sum _ _, _        => Lt
+      | _      , sum _ _  => Gt
+      | prd _ _, _        => Lt
+      | _      , prd _ _  => Gt
+
+    end
+  with vcompare i j (us: vT i) (vs: vT j) :=
+    match us,vs with
+      | vnil, vnil => Eq
+      | vnil, _    => Lt
+      | _,    vnil => Gt
+      | vcons _ u us, vcons _ v vs => lex (compare u v) (vcompare us vs)
+    end.
+ 
+
+
+  (** ** Evaluation from syntax to the abstract domain *)
+
+  Fixpoint eval u: X :=
+    match u with
+      | sum i l => let o := Bin.value (e_bin i) in
+        fold_map (fun un => let '(u,n):=un in @copy _ o n (eval u)) o l
+      | prd i l => fold_map eval (Bin.value (e_bin i)) l
+      | sym i v => eval_aux v (Sym.value (e_sym i))
+      | unit i  => e_unit i
+    end
+  with eval_aux i (v: vT i): Sym.type_of i -> X :=
+    match v with
+      | vnil => fun f => f
+      | vcons _ u v => fun f => eval_aux v (f (eval u))
+    end.
+
+  (** we need to show that compare reflects equality (this is because
+     we work with msets rather than lists with arities) *)
+  Lemma tcompare_weak_spec: forall (u v : T), compare_weak_spec u v (compare u v)
+  with vcompare_reflect_eqdep: forall i us j vs (H: i=j), vcompare us vs = Eq -> cast vT H us = vs.
+  Proof.
+    induction u.
+     destruct v; simpl; try constructor.
+      case (pos_compare_weak_spec p p0); intros; try constructor.
+      case (mset_compare_weak_spec compare tcompare_weak_spec m m0); intros; try constructor.
+     destruct v; simpl; try constructor.
+      case (pos_compare_weak_spec p p0); intros; try constructor.
+      case (list_compare_weak_spec compare tcompare_weak_spec n n0); intros; try constructor.
+     destruct v0; simpl; try constructor.
+      case_eq (idx_compare i i0); intro Hi; try constructor.
+      apply idx_compare_reflect_eq in Hi. symmetry in Hi. subst. (* the [symmetry] is required ! *)
+      case_eq (vcompare v v0); intro Hv; try constructor.
+      rewrite <- (vcompare_reflect_eqdep _ _ _ _ eq_refl Hv). constructor.
+     destruct v; simpl; try constructor.
+      case_eq (idx_compare p p0); intro Hi; try constructor.
+      apply idx_compare_reflect_eq in Hi. symmetry in Hi. subst.  constructor.
+
+    induction us; destruct vs; simpl; intros H Huv; try discriminate.
+     apply cast_eq, eq_nat_dec.
+     injection H; intro Hn.
+     revert Huv; case (tcompare_weak_spec t t0); intros; try discriminate.
+     symmetry in Hn. subst.   (* symmetry required *)
+     rewrite <- (IHus _ _ eq_refl Huv).
+     apply cast_eq, eq_nat_dec.
+  Qed.
+
+  Instance eval_aux_compat i (l: vT i): Proper (@Sym.rel_of X R i ==> R) (eval_aux l).
+  Proof.
+    induction l; simpl; repeat intro.
+     assumption.
+     apply IHl, H. reflexivity.
+  Qed.
+
+ 
+  (* is [i] a unit for [j] ? *)
+  Definition is_unit_of j i :=
+    List.existsb (fun p => eq_idx_bool j (uf_idx p)) (u_desc (e_unit i)).
+
+  (* is [i] commutative ? *)
+  Definition is_commutative i :=
+    match Bin.comm (e_bin i) with Some _ => true | None => false end.
+
+
+  (** ** Normalisation *)
+
+  Inductive discr {A} : Type :=
+  | Is_op : A -> discr
+  | Is_unit : idx -> discr
+  | Is_nothing : discr .
+ 
+  (* This is called sum in the std lib *)
+  Inductive m {A} {B} :=
+  | left : A -> m
+  | right : B -> m.
+
+  Definition comp A B (merge : B -> B -> B) (l : B) (l' : @m A B) : @m A B :=
+    match l' with
+      | left _ => right l
+      | right l' => right (merge l l')
+    end.
+ 
+  (** auxiliary functions, to clean up sums  *)
+
+  Section sums.
+    Variable i : idx.
+    Variable is_unit : idx -> bool.
+
+    Definition sum' (u: mset T): T :=
+      match u with
+        | nil (u,xH) => u
+        | _ => sum i u
+      end.
+
+    Definition is_sum  (u: T) : @discr (mset T) :=
+    match u with
+      | sum j l => if eq_idx_bool j i then Is_op l else Is_nothing
+      | unit j => if is_unit j   then Is_unit j else Is_nothing
+      | u => Is_nothing
+    end.
+
+    Definition copy_mset n (l: mset T): mset T :=
+      match n with
+        | xH => l
+        | _ => nelist_map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l
+      end.
+   
+    Definition return_sum  u n :=
+      match is_sum  u with
+        | Is_nothing => right (nil (u,n))
+        | Is_op l' =>  right (copy_mset n l')
+        | Is_unit j => left j
+      end.
+   
+    Definition add_to_sum u n (l : @m idx (mset T))  :=
+      match is_sum  u with
+        | Is_nothing => comp (merge_msets compare) (nil (u,n)) l
+        | Is_op l' => comp (merge_msets compare) (copy_mset n l') l
+        | Is_unit _ => l
+    end.
+
+
+    Definition norm_msets_ norm  (l: mset T) :=
+    fold_map'
+    (fun un => let '(u,n) := un in  return_sum  (norm u) n)
+    (fun un l => let '(u,n) := un in  add_to_sum  (norm u) n l) l.
+
+
+  End sums.
+ 
+  (** similar functions for products *)
+
+  Section prds.
+
+    Variable i : idx.
+    Variable is_unit : idx -> bool.
+    Definition prd'  (u: nelist T): T :=
+    match u with
+      | nil u => u
+      | _ => prd i u
+    end.
+
+    Definition is_prd (u: T) : @discr (nelist T) :=
+    match u with
+      | prd j l => if eq_idx_bool j i then Is_op l else Is_nothing
+      | unit j => if is_unit j  then Is_unit j else Is_nothing
+      | u => Is_nothing
+    end.
+ 
+   
+    Definition return_prd u :=
+      match is_prd u with
+        | Is_nothing => right (nil (u))
+        | Is_op l' =>  right (l')
+        | Is_unit j => left j
+      end.
+   
+    Definition add_to_prd  u  (l : @m idx (nelist T))  :=
+      match is_prd  u with
+        | Is_nothing => comp (@appne T) (nil (u)) l
+        | Is_op l' => comp (@appne T) (l') l
+        | Is_unit _ => l
+      end.
+
+    Definition norm_lists_ norm (l : nelist T) :=
+    fold_map'
+    (fun u => return_prd  (norm u))
+    (fun u l => add_to_prd (norm u) l) l.
+
+
+  End prds.
+
+
+  Definition run_list x := match x with
+                        | left n => nil (unit n)
+                        | right l => l
+                      end.
+ 
+  Definition norm_lists norm i l :=
+    let is_unit := is_unit_of i in
+      run_list (norm_lists_ i is_unit norm l).
+
+  Definition run_msets x := match x with
+                        | left n => nil (unit n, xH)
+                        | right l => l
+                      end.
+ 
+  Definition norm_msets norm i l :=
+    let is_unit := is_unit_of i in
+      run_msets (norm_msets_ i is_unit norm l).
+ 
+  Fixpoint norm u {struct u}:=
+    match u with
+      | sum i l => if is_commutative i then sum' i (norm_msets norm i l)  else u
+      | prd i l => prd' i (norm_lists norm i l)
+      | sym i l => sym i (vnorm l)
+      | unit i => unit i
+    end
+  with vnorm i (l: vT i): vT i :=
+    match l with
+      | vnil => vnil
+      | vcons _ u l => vcons (norm u) (vnorm l)
+    end.
+
+  (** ** Correctness *)
+
+  Lemma is_unit_of_Unit  : forall i j : idx,
+   is_unit_of i j = true -> Unit R (Bin.value (e_bin i)) (eval (unit j)).
+  Proof.
+    intros. unfold is_unit_of in H.
+    rewrite existsb_exists in H.
+    destruct H as [x [H H']].
+    revert H' ; case (eq_idx_spec); [intros H' _ ; subst| intros _ H'; discriminate].
+    simpl. destruct x. simpl. auto.
+  Qed.
+ 
+  Instance Binvalue_Commutative i (H :  is_commutative i = true) : Commutative R  (@Bin.value _ _ (e_bin i) ).
+  Proof.
+    unfold is_commutative in H.
+    destruct (Bin.comm (e_bin i)); auto.
+    discriminate.
+  Qed.
+
+  Instance Binvalue_Associative i :Associative R (@Bin.value _ _ (e_bin i) ).
+  Proof.
+    destruct ((e_bin i)); auto.
+  Qed.
+ 
+  Instance Binvalue_Proper i : Proper (R ==> R ==> R) (@Bin.value _ _ (e_bin i) ).
+  Proof.
+    destruct ((e_bin i)); auto.
+  Qed.
+  Hint Resolve Binvalue_Proper Binvalue_Associative Binvalue_Commutative.
+
+  (** auxiliary lemmas about sums  *)
+
+  Hint Resolve is_unit_of_Unit.
+  Section sum_correctness.
+    Variable i : idx.
+    Variable is_unit : idx -> bool.
+    Hypothesis is_unit_sum_Unit : forall j, is_unit j = true->  @Unit X R (Bin.value (e_bin i)) (eval (unit j)).
+
+    Inductive is_sum_spec_ind : T ->  @discr (mset T) -> Prop :=
+    | is_sum_spec_op : forall j l, j = i -> is_sum_spec_ind (sum j l) (Is_op l)
+    | is_sum_spec_unit : forall j, is_unit j = true ->  is_sum_spec_ind (unit j) (Is_unit j)
+    | is_sum_spec_nothing : forall u, is_sum_spec_ind  u (Is_nothing).
+ 
+    Lemma is_sum_spec u : is_sum_spec_ind u (is_sum i is_unit u).
+    Proof.
+      unfold is_sum; case u; intros; try constructor.
+      case_eq (eq_idx_bool p i); intros; subst;  try constructor; auto.
+      revert H. case eq_idx_spec; try discriminate. auto.
+      case_eq (is_unit p); intros; try constructor. auto.
+    Qed.
+
+    Instance assoc :   @Associative X R (Bin.value (e_bin i)).
+    Proof.
+      destruct (e_bin i). simpl. assumption.
+    Qed.
+    Instance proper :   Proper (R ==> R ==> R)(Bin.value (e_bin i)).
+    Proof.
+      destruct (e_bin i). simpl. assumption.
+    Qed.
+    Hypothesis comm : @Commutative X R (Bin.value (e_bin i)).
+
+    Lemma sum'_sum : forall  (l: mset T),  eval (sum' i l) ==eval (sum i l) .
+    Proof.
+      intros [[a n] | [a n] l]; destruct n;  simpl; reflexivity.
+    Qed.
+
+    Lemma eval_sum_nil x:
+      eval (sum i (nil (x,xH))) == (eval x).
+    Proof. rewrite <- sum'_sum. reflexivity.   Qed.
+     
+    Lemma eval_sum_cons : forall n a (l: mset T),
+      (eval (sum i ((a,n)::l))) == (@Bin.value _ _ (e_bin i) (@copy _ (@Bin.value _ _ (e_bin i)) n (eval a)) (eval (sum i l))).
+    Proof.
+      intros n a [[? ? ]|[b m] l]; simpl; reflexivity.
+    Qed.
+   
+    Inductive compat_sum_unit : @m idx (mset T) -> Prop :=
+    | csu_left : forall x,  is_unit x = true->  compat_sum_unit  (left x)
+    | csu_right : forall m, compat_sum_unit (right m)
+    .
+
+    Lemma compat_sum_unit_return x n : compat_sum_unit  (return_sum i is_unit x n).
+    Proof.
+      unfold return_sum.
+      case is_sum_spec; intros; try constructor; auto.
+    Qed.
+   
+    Lemma compat_sum_unit_add : forall x n h,
+      compat_sum_unit  h
+      ->
+     compat_sum_unit
+     (add_to_sum i (is_unit_of i) x n
+       h).
+    Proof.
+      unfold add_to_sum;intros; inversion H;
+        case_eq  (is_sum i (is_unit_of i) x);
+        intros; simpl; try constructor || eauto. apply H0.
+    Qed.
+
+    (* Hint Resolve copy_plus. : this lags because of  the inference of the implicit arguments *)
+    Hint Extern 5 (copy (?n + ?m) (eval ?a) == Bin.value (copy ?n (eval ?a)) (copy ?m (eval ?a))) => apply copy_plus.
+    Hint Extern 5 (?x == ?x) => reflexivity.
+    Hint Extern 5 ( Bin.value ?x ?y == Bin.value ?y ?x) => apply Bin.comm.
+   
+    Lemma eval_merge_bin : forall (h k: mset T),
+      eval (sum i (merge_msets compare h k)) == @Bin.value _ _ (e_bin i) (eval (sum i h)) (eval (sum i k)).
+    Proof.
+      induction h as [[a n]|[a n] h IHh]; intro k.
+      simpl.
+      induction k as [[b m]|[b m] k IHk]; simpl.
+      destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto. apply copy_plus; auto.
+     
+      destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto.
+      rewrite copy_plus,law_assoc; auto. 
+      rewrite IHk;  clear IHk. rewrite 2 law_assoc. apply proper. apply law_comm. reflexivity.
+     
+      induction k as [[b m]|[b m] k IHk]; simpl;  simpl in IHh.
+      destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl.
+      rewrite  (law_comm _ (copy m (eval a))), law_assoc, <- copy_plus,  Pplus_comm; auto. 
+      rewrite <- law_assoc, IHh.  reflexivity.
+      rewrite law_comm. reflexivity.
+     
+      simpl in IHk.
+      destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl.
+      rewrite IHh; clear IHh. rewrite 2 law_assoc. rewrite (law_comm _ (copy m (eval a))). rewrite law_assoc, <- copy_plus,  Pplus_comm; auto. 
+      rewrite IHh; clear IHh. simpl.  rewrite law_assoc. reflexivity. 
+      rewrite 2 (law_comm  (copy m (eval b))). rewrite law_assoc.  apply proper; [ | reflexivity]. 
+      rewrite <- IHk. reflexivity.
+    Qed.
+
+ 
+    Lemma copy_mset' n (l: mset T):  copy_mset n l = nelist_map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l.
+    Proof.
+      unfold copy_mset.  destruct n; try reflexivity.
+     
+      simpl. induction l as [|[a l] IHl]; simpl; try congruence.  destruct a.  reflexivity.
+    Qed.
+   
+   
+    Lemma copy_mset_succ  n (l: mset T):  eval (sum i (copy_mset (Pos.succ n) l)) == @Bin.value _ _ (e_bin i) (eval (sum i l)) (eval (sum i (copy_mset n l))).
+    Proof.
+      rewrite 2 copy_mset'.
+     
+      induction l as [[a m]|[a m] l IHl].
+      simpl eval.   rewrite <- copy_plus; auto. rewrite Pmult_Sn_m. reflexivity.
+     
+      simpl nelist_map.  rewrite ! eval_sum_cons. rewrite IHl.  clear IHl.
+      rewrite Pmult_Sn_m. rewrite copy_plus; auto. rewrite <- !law_assoc.
+      apply Binvalue_Proper; try reflexivity.
+      rewrite law_comm . rewrite <- !law_assoc. apply proper; try reflexivity.
+      apply law_comm.
+    Qed.
+
+    Lemma copy_mset_copy : forall n  (m : mset T), eval (sum i (copy_mset n m)) == @copy _ (@Bin.value _ _ (e_bin i)) n (eval (sum i m)).
+    Proof.
+      induction n using Pind; intros.
+     
+      unfold copy_mset. rewrite copy_xH. reflexivity.
+      rewrite copy_mset_succ. rewrite copy_Psucc. rewrite IHn. reflexivity.
+    Qed.
+   
+    Instance compat_sum_unit_Unit : forall p, compat_sum_unit (left p) ->
+      @Unit X R (Bin.value (e_bin i)) (eval (unit p)).
+    Proof.
+      intros.
+      inversion H. subst.  auto.
+    Qed.
+  
+    Lemma copy_n_unit : forall j n, is_unit j = true ->
+      eval (unit j) == @copy _ (Bin.value (e_bin i)) n (eval (unit j)).
+    Proof.
+      intros.
+      induction n using Prect.
+      rewrite copy_xH. reflexivity.
+      rewrite copy_Psucc. rewrite <- IHn. apply is_unit_sum_Unit in H. rewrite law_neutral_left. reflexivity.
+    Qed.
+
+   
+    Lemma z0  l r (H : compat_sum_unit  r):
+      eval (sum i (run_msets (comp (merge_msets compare) l r))) == eval (sum i ((merge_msets compare) (l) (run_msets r))).
+    Proof.
+      unfold comp. unfold run_msets.
+      case_eq r; intros; subst.
+      rewrite eval_merge_bin; auto.
+      rewrite eval_sum_nil.
+      apply compat_sum_unit_Unit in H. rewrite law_neutral_right.  reflexivity.
+      reflexivity.
+    Qed.
+
+    Lemma z1 : forall n x,
+      eval (sum i (run_msets (return_sum i (is_unit) x n )))
+      == @copy _ (@Bin.value _ _ (e_bin i)) n (eval x).
+    Proof.
+      intros. unfold return_sum.  unfold run_msets.
+      case (is_sum_spec); intros; subst.
+      rewrite copy_mset_copy.
+      reflexivity.
+     
+      rewrite eval_sum_nil. apply copy_n_unit. auto.
+      reflexivity.
+    Qed.
+    Lemma z2 : forall  u n x, compat_sum_unit  x ->
+      eval (sum i ( run_msets
+        (add_to_sum i (is_unit) u n x)))
+      == 
+      @Bin.value _ _ (e_bin i) (@copy _ (@Bin.value _ _ (e_bin i))  n (eval u)) (eval (sum i (run_msets x))).
+    Proof.
+      intros u n x Hix .
+      unfold add_to_sum.
+      case is_sum_spec; intros; subst.
+   
+      rewrite z0 by auto.  rewrite eval_merge_bin.  rewrite copy_mset_copy. reflexivity.
+      rewrite <- copy_n_unit by assumption.
+      apply is_unit_sum_Unit in H.
+      rewrite law_neutral_left. reflexivity.
+     
+     
+      rewrite z0 by auto.  rewrite eval_merge_bin. reflexivity.
+    Qed.
+  End sum_correctness.
+  Lemma eval_norm_msets i norm
+    (Comm : Commutative R (Bin.value (e_bin i)))
+    (Hnorm: forall u, eval (norm u) == eval u) : forall h, eval (sum i (norm_msets norm i h)) == eval (sum i h).
+  Proof.
+    unfold norm_msets.
+    assert (H :
+      forall h : mset T,
+        eval (sum i (run_msets (norm_msets_ i (is_unit_of i) norm h))) ==  eval (sum i h) /\ compat_sum_unit (is_unit_of i) (norm_msets_ i (is_unit_of i) norm h)).
+      
+    induction h as [[a n] | [a n] h [IHh IHh']]; simpl norm_msets_; split.
+    rewrite z1 by auto. rewrite Hnorm . reflexivity. auto.
+    apply compat_sum_unit_return.
+      
+    rewrite z2 by auto. rewrite IHh. 
+    rewrite eval_sum_cons.  rewrite Hnorm. reflexivity. apply compat_sum_unit_add, IHh'.
+   
+    apply H.
+  Defined.
+ 
+  (** auxiliary lemmas about products  *)
+
+  Section prd_correctness.
+    Variable i : idx.
+    Variable is_unit : idx -> bool.
+    Hypothesis is_unit_prd_Unit : forall j, is_unit j = true->  @Unit X R (Bin.value (e_bin i)) (eval (unit j)).
+
+    Inductive is_prd_spec_ind  : T ->  @discr (nelist T) -> Prop :=
+    | is_prd_spec_op :
+      forall j l, j = i -> is_prd_spec_ind (prd j l) (Is_op l)
+    | is_prd_spec_unit :
+      forall j, is_unit j = true ->  is_prd_spec_ind (unit j) (Is_unit j)
+    | is_prd_spec_nothing :
+      forall u, is_prd_spec_ind u (Is_nothing).
+   
+    Lemma is_prd_spec u : is_prd_spec_ind u (is_prd i is_unit u).
+    Proof.
+      unfold is_prd; case u; intros; try constructor.
+      case (eq_idx_spec); intros; subst;  try constructor; auto.
+      case_eq (is_unit p); intros; try constructor; auto.  
+    Qed.
+
+    Lemma prd'_prd : forall (l: nelist T), eval (prd' i l) == eval (prd i l).
+    Proof.
+      intros  [?|? [|? ?]]; simpl; reflexivity.
+    Qed.
+   
+   
+    Lemma eval_prd_nil x:  eval (prd i (nil x)) == eval x. 
+    Proof.
+      rewrite <- prd'_prd. simpl. reflexivity.
+    Qed.
+    Lemma eval_prd_cons a : forall (l: nelist T), eval (prd i (a::l)) == @Bin.value _ _ (e_bin i) (eval a) (eval (prd i l)).
+    Proof.
+      intros  [|b l]; simpl; reflexivity.
+    Qed.       
+    Lemma eval_prd_app : forall (h k: nelist T), eval (prd i (h++k)) == @Bin.value _ _ (e_bin i) (eval (prd i h)) (eval (prd i k)).
+    Proof.
+      induction h; intro k. simpl; try reflexivity.
+      simpl appne.  rewrite  2 eval_prd_cons, IHh, law_assoc. reflexivity.
+    Qed.       
+
+    Inductive compat_prd_unit : @m idx (nelist T) -> Prop :=
+    | cpu_left : forall x,  is_unit  x = true -> compat_prd_unit  (left x)
+    | cpu_right : forall m, compat_prd_unit (right m)
+    .
+ 
+    Lemma compat_prd_unit_return  x: compat_prd_unit (return_prd i is_unit x).
+    Proof.
+      unfold return_prd.
+      case (is_prd_spec); intros; try constructor; auto.
+    Qed.
+
+    Lemma compat_prd_unit_add  : forall x  h,
+      compat_prd_unit  h
+      ->
+      compat_prd_unit
+      (add_to_prd i is_unit x
+        h).
+    Proof.
+      intros.
+      unfold add_to_prd.
+      unfold comp.
+      case (is_prd_spec); intros; try constructor; auto.
+      unfold comp; case h; try constructor.
+      unfold comp; case h; try constructor.
+    Qed.
+
+   
+    Instance compat_prd_Unit : forall p, compat_prd_unit (left p) ->
+      @Unit X R (Bin.value (e_bin i)) (eval (unit p)).
+    Proof.
+      intros.
+      inversion H; subst. apply is_unit_prd_Unit. assumption.
+    Qed.
+
+    Lemma z0' : forall l (r: @m idx (nelist T)), compat_prd_unit r ->
+      eval (prd i (run_list (comp (@appne T) l r))) == eval (prd i ((appne (l) (run_list r)))).
+    Proof.
+      intros.
+      unfold comp. unfold run_list. case_eq r; intros; auto; subst.
+      rewrite eval_prd_app.
+      rewrite eval_prd_nil.
+      apply compat_prd_Unit in H. rewrite law_neutral_right. reflexivity.
+      reflexivity.
+    Qed.
+ 
+    Lemma z1' a :  eval (prd i (run_list (return_prd i is_unit a))) ==  eval (prd i (nil a)).
+    Proof.
+      intros. unfold return_prd.  unfold run_list.
+      case (is_prd_spec); intros; subst; reflexivity.
+    Qed.
+    Lemma z2' : forall  u  x, compat_prd_unit  x -> 
+      eval (prd i ( run_list
+        (add_to_prd i is_unit u x))) ==  @Bin.value _ _ (e_bin i) (eval u) (eval (prd i (run_list x))).
+    Proof.
+      intros u x Hix.
+      unfold add_to_prd.
+      case (is_prd_spec); intros; subst.
+      rewrite z0' by auto.  rewrite eval_prd_app.  reflexivity.
+      apply is_unit_prd_Unit in H. rewrite law_neutral_left. reflexivity.
+      rewrite z0' by auto.  rewrite eval_prd_app. reflexivity.
+    Qed.
+ 
+  End prd_correctness.
+
+
+
+
+  Lemma eval_norm_lists i (Hnorm: forall u, eval (norm u) == eval u) : forall h, eval (prd i (norm_lists norm i h)) == eval (prd i h).
+  Proof.
+    unfold norm_lists.
+    assert (H :  forall h : nelist T,
+      eval (prd i (run_list (norm_lists_ i (is_unit_of i) norm h))) ==
+      eval (prd i h)
+      /\ compat_prd_unit (is_unit_of i) (norm_lists_ i (is_unit_of i) norm h)).
+  
+   
+      induction h as [a | a h [IHh IHh']]; simpl norm_lists_; split.
+      rewrite z1'. simpl.  apply Hnorm.
+   
+      apply compat_prd_unit_return.
+   
+      rewrite z2'. rewrite IHh.  rewrite eval_prd_cons.  rewrite Hnorm. reflexivity. apply is_unit_of_Unit.
+      auto.
+
+      apply compat_prd_unit_add. auto.
+      apply H.
+    Defined.
+
+  (** correctness of the normalisation function *)
+
+  Theorem eval_norm: forall u, eval (norm u) == eval u
+    with eval_norm_aux: forall i (l: vT i) (f: Sym.type_of i),
+      Proper (@Sym.rel_of X R i) f -> eval_aux (vnorm l) f == eval_aux l f.
+  Proof.
+    induction u as [ p m | p l | ? | ?];  simpl norm.
+    case_eq (is_commutative p); intros.
+    rewrite sum'_sum.
+    apply eval_norm_msets; auto.
+    reflexivity.
+
+    rewrite prd'_prd.
+    apply eval_norm_lists; auto.
+
+    apply eval_norm_aux, Sym.morph.
+
+    reflexivity.
+
+    induction l; simpl; intros f Hf. reflexivity.
+    rewrite eval_norm. apply IHl, Hf; reflexivity.
+  Qed.
+
+
+  (** corollaries, for goal normalisation or decision *)
+
+  Lemma normalise : forall (u v: T), eval (norm u) == eval (norm v) -> eval u == eval v.
+  Proof. intros u v. rewrite 2 eval_norm. trivial. Qed.
+   
+  Lemma compare_reflect_eq: forall u v, compare u v = Eq -> eval u == eval v.
+  Proof. intros u v. case (tcompare_weak_spec u v); intros; try congruence. reflexivity. Qed.
+
+  Lemma decide: forall (u v: T), compare (norm u) (norm v) = Eq -> eval u == eval v.
+  Proof. intros u v H. apply normalise. apply compare_reflect_eq. apply H. Qed.
+
+  Lemma lift_normalise {S} {H : AAC_lift S R}:
+    forall (u v: T), (let x := norm u in let y := norm v in
+      S (eval x) (eval y)) -> S (eval u) (eval v).
+  Proof. destruct H. intros u v; simpl; rewrite 2 eval_norm. trivial. Qed.
+
+End s.
+End Internal.
+
+Local Ltac internal_normalize :=
+  let x := fresh in let y := fresh in
+  intro x; intro y; vm_compute in x; vm_compute in y; unfold x; unfold y;
+  compute [Internal.eval Utils.fold_map Internal.copy Prect]; simpl.
+
+
+(** * Lemmas for performing transitivity steps
+   given an instance of AAC_lift *)
+
+Section t.
+  Context `{AAC_lift}.
+
+  Lemma lift_transitivity_left  (y x z : X): E x y -> R y z -> R x z.
+  Proof. destruct H as [Hequiv Hproper]; intros G;rewrite G. trivial. Qed.
+ 
+  Lemma lift_transitivity_right (y x z : X): E y z -> R x y -> R x z.
+  Proof.  destruct H as [Hequiv Hproper]; intros G. rewrite G. trivial. Qed.
+
+  Lemma lift_reflexivity {HR :Reflexive R}: forall x y, E x y -> R x y.
+  Proof. destruct H. intros ? ? G. rewrite G. reflexivity. Qed.
+
+End t.
+       
+Declare ML Module "aac_plugin".
diff --git a/theories/Caveats.v b/theories/Caveats.v
new file mode 100644
index 0000000..d7824cd
--- /dev/null
+++ b/theories/Caveats.v
@@ -0,0 +1,376 @@
+(***************************************************************************)
+(*  This is part of aac_tactics, it is distributed under the terms of the  *)
+(*         GNU Lesser General Public License version 3                     *)
+(*              (see file LICENSE for more details)                        *)
+(*                                                                         *)
+(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
+(***************************************************************************)
+
+(** * Currently known caveats and limitations of the [aac_tactics] library.
+
+   Depending on your installation, either uncomment the following two
+   lines, or add them to your .coqrc files, replacing "."
+   with the path to the [aac_tactics] library
+*)
+
+Require NArith Minus.
+
+From AAC_tactics
+Require Import AAC.
+From AAC_tactics
+Require Instances.
+
+(** ** Limitations *)
+
+(** *** 1. Dependent parameters
+   The type of the rewriting hypothesis must be of the form
+
+   [forall (x_1: T_1) ... (x_n: T_n), R l r],
+
+   where [R] is a relation over some type [T] and such that for all
+   variable [x_i] appearing in the left-hand side ([l]), we actually
+   have [T_i]=[T]. The goal should be of the form [S g d], where [S]
+   is a relation on [T].
+
+   In other words, we cannot instantiate arguments of an exogeneous
+   type. *)
+
+Section parameters.
+
+  Context {X} {R} {E: @Equivalence X R}
+  {plus} {plus_A: Associative R plus} {plus_C: Commutative R plus}
+         {plus_Proper: Proper (R ==> R ==> R) plus}
+  {zero} {Zero: Unit R plus zero}.
+
+  Notation "x == y"  := (R x y) (at level 70).
+  Notation "x + y"   := (plus x y) (at level 50, left associativity).
+  Notation "0"       := (zero).
+
+  Variable f: nat -> X -> X.
+
+  (** in [Hf], the parameter [n] has type [nat], it cannot be instantiated automatically *)
+  Hypothesis Hf: forall n x, f n x + x == x.
+  Hypothesis Hf': forall n, Proper (R ==> R) (f n).
+
+  Goal forall a b k, a + f k (b+a) + b == a+b.
+    intros.
+    Fail aac_rewrite Hf. (** [aac_rewrite] does not instantiate [n] automatically *)
+    aac_rewrite (Hf k).         (** of course, this argument can be given explicitly *)
+    aac_reflexivity.
+  Qed. 
+
+  (** for the same reason, we cannot handle higher-order parameters (here, [g])*)
+  Hypothesis H : forall g x y, g x + g y == g (x + y).
+  Variable g : X -> X.
+  Hypothesis Hg : Proper (R ==> R) g.
+  Goal forall a b c, g a + g b + g c == g (a + b + c).
+    intros.
+    Fail aac_rewrite H.
+    do 2 aac_rewrite (H g). aac_reflexivity.
+  Qed.
+
+End parameters.
+
+
+(** *** 2. Exogeneous morphisms
+
+   We do not handle `exogeneous' morphisms: morphisms that move from
+   type [T] to some other type [T']. *)
+
+Section morphism.
+  Import NArith Minus.
+  Open Scope nat_scope.
+
+  (** Typically, although [N_of_nat] is a proper morphism from
+     [@eq nat] to [@eq N], we cannot rewrite under [N_of_nat] *)
+  Goal forall a b: nat, N_of_nat (a+b-(b+a)) = 0%N.
+    intros.
+    Fail aac_rewrite minus_diag.
+  Abort.
+
+
+  (* More generally, this prevents us from rewriting under
+     propositional contexts *)
+  Context {P} {HP : Proper (@eq nat ==> iff) P}.
+  Hypothesis H : P 0.
+
+  Goal forall a b, P (a + b - (b + a)).
+    intros a b.
+    Fail aac_rewrite minus_diag.
+    (** a solution is to introduce an evar to replace the part to be
+       rewritten. This tiresome process should be improved in the
+       future. Here, it can be done using eapply and the morphism. *)
+    eapply HP.
+    aac_rewrite minus_diag.
+     reflexivity.
+     exact H.
+  Qed.
+
+  Goal forall a b, a+b-(b+a) = 0 /\ b-b = 0.
+    intros.
+    (** similarly, we need to bring equations to the toplevel before
+    being able to rewrite *)
+    Fail aac_rewrite minus_diag.
+    split; aac_rewrite minus_diag; reflexivity.
+  Qed.
+   
+End morphism.
+
+
+(** *** 3. Treatment of variance with inequations.
+
+   We do not take variance into account when we compute the set of
+   solutions to a matching problem modulo AC. As a consequence,
+   [aac_instances] may propose solutions for which [aac_rewrite] will
+   fail, due to the lack of adequate morphisms *)
+
+Section ineq. 
+
+  Import ZArith.
+  Import Instances.Z.
+  Open Scope Z_scope.
+
+  Instance Zplus_incr: Proper (Z.le ==> Z.le ==> Z.le) Zplus.
+  Proof. intros ? ? H ? ? H'. apply Zplus_le_compat; assumption. Qed. 
+
+  Hypothesis H: forall x, x+x <= x.
+  Goal forall a b c, c + - (a + a) + b + b <= c.
+    intros.
+    (** this fails because the first solution is not valid ([Zopp] is not increasing), *)
+    Fail aac_rewrite H.
+    aac_instances H.       
+    (** on the contrary, the second solution is valid: *) 
+    aac_rewrite H at 1.
+    (** Currently, we cannot filter out such invalid solutions in an easy way;
+       this should be fixed in the future  *)
+  Abort.
+
+End ineq. 
+
+
+
+(** ** Caveats  *)
+
+(** *** 1. Special treatment for units.
+   [S O] is considered as a unit for multiplication whenever a [Peano.mult]
+   appears in the goal. The downside is that [S x] does not match [1],
+   and [1] does not match [S(0+0)] whenever [Peano.mult] appears in
+   the goal. *)
+
+Section Peano.
+  Import Instances.Peano.
+
+  Hypothesis H : forall x, x + S x = S (x+x).
+
+  Goal 1 = 1.
+  (** ok (no multiplication around), [x] is instantiated with [O] *)
+    aacu_rewrite H.
+  Abort.
+
+  Goal 1*1 = 1.
+  (** fails since 1 is seen as a unit, not the application of the
+     morphism [S] to the constant [O] *)
+    Fail aacu_rewrite H.
+  Abort.
+
+  Hypothesis H': forall x, x+1 = 1+x.
+
+  Goal forall a, a+S(0+0) = 1+a.
+  (** ok (no multiplication around), [x] is instantiated with [a]*)
+    intro. aac_rewrite H'.
+  Abort.
+
+  Goal forall a, a*a+S(0+0) = 1+a*a.
+  (** fails: although [S(0+0)] is understood as the application of
+     the morphism [S] to the constant [O], it is not recognised
+     as the unit [S O] of multiplication *)
+    intro. Fail aac_rewrite H'.
+  Abort.
+
+  (** More generally, similar counter-intuitive behaviours can appear
+     when declaring an applied morphism as an unit. *)
+
+End Peano.
+
+
+
+(** *** 2. Existential variables.
+We implemented an algorithm for _matching_ modulo AC, not for
+_unifying_ modulo AC. As a consequence, existential variables
+appearing in a goal are considered as constants, they will not be
+instantiated. *)
+
+Section evars.
+  Import ZArith.
+  Import Instances.Z.
+
+  Variable P: Prop.
+  Hypothesis H: forall x y, x+y+x = x -> P.
+  Hypothesis idem: forall x, x+x = x.
+  Goal P.
+    eapply H.
+    aac_rewrite idem. (** this works: [x] is instantiated with an evar *)
+    instantiate (2 := 0).
+    symmetry. aac_reflexivity. (** this does work but there are remaining evars in the end *)
+  Abort.
+
+  Hypothesis H': forall x, 3+x = x -> P.
+  Goal P.
+    eapply H'.
+    Fail aac_rewrite idem. (** this fails since we do not instantiate evars *)
+  Abort.
+End evars.
+
+
+(** *** 3. Distinction between [aac_rewrite] and [aacu_rewrite] *)
+
+Section U.
+  Context {X} {R} {E: @Equivalence X R}
+  {dot}  {dot_A: Associative R dot} {dot_Proper: Proper (R ==> R ==> R) dot}
+  {one}  {One: Unit R dot one}.
+
+  Infix "=="   := R (at level 70).
+  Infix "*"    := dot.
+  Notation "1" := one.
+
+  (** In some situations, the [aac_rewrite] tactic allows
+  instantiations of a variable with a unit, when the variable occurs
+  directly under a function symbol: *)
+
+  Variable f : X -> X.
+  Hypothesis Hf : Proper (R ==> R) f.
+  Hypothesis dot_inv_left : forall x, f x*x  == x.
+  Goal f 1 == 1.
+    aac_rewrite dot_inv_left. reflexivity.
+  Qed.
+
+  (** This behaviour seems desirable in most situations: these
+  solutions with units are less peculiar than the other ones, since
+  the unit comes from the goal. However, this policy is not properly
+  enforced for now (hard to do with the current algorithm): *)
+
+  Hypothesis dot_inv_right : forall x, x*f x  == x.
+  Goal f 1 == 1.
+    Fail aac_rewrite dot_inv_right.
+    aacu_rewrite dot_inv_right. reflexivity.
+  Qed.
+
+End U.
+
+(** *** 4. Rewriting units *)
+Section V.
+  Context {X} {R} {E: @Equivalence X R}
+  {dot}  {dot_A: Associative R dot} {dot_Proper: Proper (R ==> R ==> R) dot}
+  {one}  {One: Unit R dot one}.
+
+  Infix "=="   := R (at level 70).
+  Infix "*"    := dot.
+  Notation "1" := one.
+ 
+  (** [aac_rewrite] uses the symbols appearing in the goal and the
+     hypothesis to infer the AC and A operations. In the following
+     example, [dot] appears neither in the left-hand-side of the goal,
+     nor in the right-hand side of the hypothesis. Hence, 1 is not
+     recognised as a unit. To circumvent this problem, we can force
+     [aac_rewrite] to take into account a given operation, by giving
+     it an extra argument. This extra argument seems useful only in
+     this peculiar case. *)
+
+  Lemma inv_unique: forall x y y', x*y == 1 -> y'*x == 1 -> y==y'.
+  Proof.
+    intros x y y' Hxy Hy'x.
+    aac_instances <- Hy'x [dot].
+    aac_rewrite <- Hy'x at 1 [dot].
+    aac_rewrite Hxy. aac_reflexivity.
+  Qed.
+End V.
+
+(** *** 5. Rewriting too much things.  *)
+Section W.
+  Variables a b c: nat.
+  Hypothesis H: 0 = c.
+
+  Goal  b*(a+a) <= b*(c+a+a+1).
+   
+  (** [aac_rewrite] finds a pattern modulo AC that matches a given
+     hypothesis, and then makes a call to [setoid_rewrite]. This
+     [setoid_rewrite] can unfortunately make several rewrites (in a
+     non-intuitive way: below, the [1] in the right-hand side is
+     rewritten into [S c]) *)
+    aac_rewrite H.
+
+    (** To this end, we provide a companion tactic to [aac_rewrite]
+    and [aacu_rewrite], that makes the transitivity step, but not the
+    setoid_rewrite:
+   
+    This allows the user to select the relevant occurrences in which
+    to rewrite. *)
+    aac_pattern H at 2. setoid_rewrite H at 1.
+  Abort.
+
+End W.
+
+(** *** 6. Rewriting nullifiable patterns.  *)
+Section Z.
+
+(** If the pattern of the rewritten hypothesis does not contain "hard"
+symbols (like constants, function symbols, AC or A symbols without
+units), there can be infinitely many subterms such that the pattern
+matches: it is possible to build "subterms" modulo ACU that make the
+size of the term increase (by making neutral elements appear in a
+layered fashion). Hence, we settled with heuristics to propose only
+"some" of these solutions. In such cases, the tactic displays a
+(conservative) warning.  *)
+
+Variables a b c: nat.
+Variable f: nat -> nat.
+Hypothesis H0: forall x, 0 = x - x.
+Hypothesis H1: forall x, 1 = x * x.
+
+Goal a+b*c = c.
+  aac_instances H0.
+  (** In this case, only three solutions are proposed, while there are
+  infinitely many solutions. E.g.
+     - a+b*c*(1+[])
+     - a+b*c*(1+0*(1+ []))
+     - ...
+     *)
+Abort.
+
+(** **** If the pattern is a unit or can be instantiated to be equal
+   to a unit:
+  
+   The heuristic is to make the unit appear at each possible position
+   in the term, e.g. transforming [a] into [1*a] and [a*1], but this
+   process is not recursive (we will not transform [1*a]) into
+   [(1+0*1)*a] *)
+
+Goal a+b+c = c.
+ 
+  aac_instances H0 [mult].            
+  (** 1 solution, we miss solutions like [(a+b+c*(1+0*(1+[])))] and so on  *)
+ 
+  aac_instances H1 [mult].     
+  (** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*)
+Abort.
+
+(** *** Another example of the former case is the following, where the hypothesis can be instantiated to be equal to [1] *)
+Hypothesis H : forall x y, (x+y)*x = x*x + y *x.
+Goal a*a+b*a + c = c.
+  (** Here, only one solution if we use the aac_instance tactic  *)
+  aac_instances <- H.
+
+  (** There are 8 solutions using aacu_instances (but, here,
+     there are infinitely many different solutions). We miss e.g. [a*a +b*a
+     + (x*x + y*x)*c], which seems to be more peculiar. *)
+  aacu_instances <- H.
+
+  (** The 7 last solutions are the same as if we were matching [1] *)
+  aacu_instances H1.  Abort.
+
+(** The behavior of the tactic is not satisfying in this case. It is
+still unclear how to handle properly this kind of situation : we plan
+to investigate on this in the future *)
+
+End Z.
+
diff --git a/theories/Instances.v b/theories/Instances.v
new file mode 100644
index 0000000..d007ceb
--- /dev/null
+++ b/theories/Instances.v
@@ -0,0 +1,261 @@
+(***************************************************************************)
+(*  This is part of aac_tactics, it is distributed under the terms of the  *)
+(*         GNU Lesser General Public License version 3                     *)
+(*              (see file LICENSE for more details)                        *)
+(*                                                                         *)
+(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
+(***************************************************************************)
+
+Require List.
+Require Arith NArith Max Min.
+Require ZArith Zminmax.
+Require QArith Qminmax.
+Require Relations.
+
+From AAC_tactics
+Require Export AAC.
+
+(** Instances for aac_rewrite.*)
+
+
+(* This one is not declared as an instance: this interferes badly with setoid_rewrite *)
+Lemma eq_subr {X} {R} `{@Reflexive X R}: subrelation eq R.
+Proof. intros x y ->. reflexivity. Qed.
+
+(* At the moment, all the instances are exported even if they are packaged into modules. Even using LocalInstances in fact*)
+
+Module Peano.
+  Import Arith NArith Max Min.
+  Instance aac_plus_Assoc : Associative eq plus := plus_assoc.
+  Instance aac_plus_Comm : Commutative eq plus :=  plus_comm.
+ 
+  Instance aac_mult_Comm : Commutative eq mult :=  mult_comm.
+  Instance aac_mult_Assoc : Associative eq mult :=  mult_assoc.
+ 
+  Instance aac_min_Comm : Commutative eq min :=  min_comm.
+  Instance aac_min_Assoc : Associative eq min :=  min_assoc.
+
+  Instance aac_max_Comm : Commutative eq max :=  max_comm.
+  Instance aac_max_Assoc : Associative eq max :=  max_assoc.
+ 
+  Instance aac_one : Unit eq mult 1 :=  Build_Unit eq mult 1 mult_1_l mult_1_r. 
+  Instance aac_zero_plus  : Unit eq plus O := Build_Unit eq plus (O) plus_0_l plus_0_r.
+  Instance aac_zero_max  :  Unit eq max  O := Build_Unit eq max 0 max_0_l max_0_r. 
+
+
+  (* We also provide liftings from le to eq *)
+  Instance preorder_le : PreOrder le := Build_PreOrder _ le_refl le_trans.
+  Instance lift_le_eq : AAC_lift le eq := Build_AAC_lift eq_equivalence _.
+
+End Peano.
+
+
+Module Z.
+  Import ZArith Zminmax.
+  Open Scope Z_scope.
+  Instance aac_Zplus_Assoc : Associative eq Zplus :=  Zplus_assoc.
+  Instance aac_Zplus_Comm : Commutative eq Zplus :=  Zplus_comm.
+ 
+  Instance aac_Zmult_Comm : Commutative eq Zmult :=  Zmult_comm.
+  Instance aac_Zmult_Assoc : Associative eq Zmult :=  Zmult_assoc.
+ 
+  Instance aac_Zmin_Comm : Commutative eq Z.min :=  Z.min_comm.
+  Instance aac_Zmin_Assoc : Associative eq Z.min :=  Z.min_assoc.
+
+  Instance aac_Zmax_Comm : Commutative eq Z.max :=  Z.max_comm.
+  Instance aac_Zmax_Assoc : Associative eq Z.max :=  Z.max_assoc.
+ 
+  Instance aac_one : Unit eq Zmult 1 :=  Build_Unit eq Zmult 1 Zmult_1_l Zmult_1_r. 
+  Instance aac_zero_Zplus  : Unit eq Zplus 0 := Build_Unit eq Zplus 0 Zplus_0_l Zplus_0_r.
+
+  (* We also provide liftings from le to eq *)
+  Instance preorder_Zle : PreOrder Z.le := Build_PreOrder _ Z.le_refl Z.le_trans.
+  Instance lift_le_eq : AAC_lift Z.le eq := Build_AAC_lift eq_equivalence _.
+
+End Z.
+
+Module Lists.
+   Import List.
+   Instance aac_append_Assoc {A} : Associative eq (@app A) := @app_assoc A.
+   Instance aac_nil_append  {A} : @Unit (list A) eq (@app A) (@nil A) := Build_Unit _ (@app A) (@nil A) (@app_nil_l A) (@app_nil_r A).
+   Instance aac_append_Proper {A} : Proper (eq ==> eq ==> eq) (@app A).
+   Proof.
+     repeat intro.
+     subst.
+     reflexivity.
+   Qed.
+End Lists.
+
+
+Module N.
+  Import NArith.
+  Open Scope N_scope.
+  Instance aac_Nplus_Assoc : Associative eq Nplus :=  Nplus_assoc.
+  Instance aac_Nplus_Comm : Commutative eq Nplus :=  Nplus_comm.
+ 
+  Instance aac_Nmult_Comm : Commutative eq Nmult :=  Nmult_comm.
+  Instance aac_Nmult_Assoc : Associative eq Nmult :=  Nmult_assoc.
+ 
+  Instance aac_Nmin_Comm : Commutative eq N.min :=  N.min_comm.
+  Instance aac_Nmin_Assoc : Associative eq N.min :=  N.min_assoc.
+
+  Instance aac_Nmax_Comm : Commutative eq N.max :=  N.max_comm.
+  Instance aac_Nmax_Assoc : Associative eq N.max :=  N.max_assoc.
+ 
+  Instance aac_one  : Unit eq Nmult (1)%N := Build_Unit eq Nmult (1)%N Nmult_1_l Nmult_1_r. 
+  Instance aac_zero  : Unit eq Nplus (0)%N := Build_Unit eq Nplus (0)%N Nplus_0_l Nplus_0_r.
+  Instance aac_zero_max  :  Unit eq N.max 0 := Build_Unit eq N.max 0 N.max_0_l N.max_0_r. 
+   
+  (* We also provide liftings from le to eq *)
+  Instance preorder_le : PreOrder N.le := Build_PreOrder N.le N.le_refl N.le_trans.
+  Instance lift_le_eq : AAC_lift N.le eq := Build_AAC_lift eq_equivalence _.
+
+End N.
+
+Module P.
+  Import NArith.
+  Open Scope positive_scope.
+  Instance aac_Pplus_Assoc : Associative eq Pplus :=  Pplus_assoc.
+  Instance aac_Pplus_Comm : Commutative eq Pplus :=  Pplus_comm.
+ 
+  Instance aac_Pmult_Comm : Commutative eq Pmult :=  Pmult_comm.
+  Instance aac_Pmult_Assoc : Associative eq Pmult :=  Pmult_assoc.
+ 
+  Instance aac_Pmin_Comm : Commutative eq Pos.min :=  Pos.min_comm.
+  Instance aac_Pmin_Assoc : Associative eq Pos.min :=  Pos.min_assoc.
+
+  Instance aac_Pmax_Comm : Commutative eq Pos.max :=  Pos.max_comm.
+  Instance aac_Pmax_Assoc : Associative eq Pos.max :=  Pos.max_assoc.
+ 
+  Instance aac_one  : Unit eq Pmult 1 := Build_Unit eq Pmult 1 _ Pmult_1_r. 
+  intros; reflexivity. Qed.          (*  TODO : add this lemma in the stdlib *)
+  Instance aac_one_max  :  Unit eq Pos.max 1 := Build_Unit eq Pos.max 1 Pos.max_1_l Pos.max_1_r. 
+
+  (* We also provide liftings from le to eq *)
+  Instance preorder_le : PreOrder Pos.le := Build_PreOrder Pos.le Pos.le_refl Pos.le_trans.
+  Instance lift_le_eq : AAC_lift Pos.le eq := Build_AAC_lift eq_equivalence _.
+End P.
+
+Module Q.
+  Import QArith Qminmax.
+  Instance aac_Qplus_Assoc : Associative Qeq Qplus :=  Qplus_assoc.
+  Instance aac_Qplus_Comm : Commutative Qeq Qplus :=  Qplus_comm.
+ 
+  Instance aac_Qmult_Comm : Commutative Qeq Qmult :=  Qmult_comm.
+  Instance aac_Qmult_Assoc : Associative Qeq Qmult :=  Qmult_assoc.
+ 
+  Instance aac_Qmin_Comm : Commutative Qeq Qmin :=  Q.min_comm.
+  Instance aac_Qmin_Assoc : Associative Qeq Qmin :=  Q.min_assoc.
+
+  Instance aac_Qmax_Comm : Commutative Qeq Qmax :=  Q.max_comm.
+  Instance aac_Qmax_Assoc : Associative Qeq Qmax :=  Q.max_assoc.
+ 
+  Instance aac_one : Unit Qeq Qmult 1 :=  Build_Unit Qeq Qmult 1 Qmult_1_l Qmult_1_r. 
+  Instance aac_zero_Qplus  : Unit Qeq Qplus 0 := Build_Unit Qeq Qplus 0 Qplus_0_l Qplus_0_r.
+
+  (* We also provide liftings from le to eq *)
+  Instance preorder_le : PreOrder Qle := Build_PreOrder Qle Qle_refl Qle_trans.
+  Instance lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _.
+
+End Q.
+
+Module Prop_ops.
+  Instance aac_or_Assoc : Associative iff or. Proof.  unfold Associative; tauto.  Qed.
+  Instance aac_or_Comm : Commutative iff or. Proof.  unfold Commutative; tauto.  Qed.
+  Instance aac_and_Assoc : Associative iff and. Proof.  unfold Associative; tauto.  Qed.
+  Instance aac_and_Comm : Commutative iff and. Proof.  unfold Commutative; tauto.  Qed.
+  Instance aac_True : Unit iff or False.  Proof.  constructor; firstorder.  Qed.
+  Instance aac_False : Unit iff and True.  Proof.  constructor; firstorder.  Qed.
+ 
+  Program Instance aac_not_compat : Proper (iff ==> iff) not.
+  Solve All Obligations with firstorder.
+
+  Instance lift_impl_iff : AAC_lift Basics.impl iff := Build_AAC_lift _  _.
+End Prop_ops.
+
+Module Bool.
+  Instance aac_orb_Assoc : Associative eq orb. Proof.  unfold Associative; firstorder.  Qed.
+  Instance aac_orb_Comm : Commutative eq orb. Proof.  unfold Commutative; firstorder.  Qed.
+  Instance aac_andb_Assoc : Associative eq andb. Proof.  unfold Associative; firstorder.  Qed.
+  Instance aac_andb_Comm : Commutative eq andb. Proof.  unfold Commutative; firstorder.  Qed.
+  Instance aac_true : Unit eq orb false.  Proof.  constructor; firstorder.  Qed.
+  Instance aac_false : Unit eq andb true.  Proof.  constructor; intros [|];firstorder.  Qed.
+ 
+  Instance negb_compat : Proper (eq ==> eq) negb.  Proof. intros [|] [|]; auto. Qed.
+End Bool.
+
+Module Relations.
+  Import Relations.Relations.
+  Section defs.
+    Variable T : Type.
+    Variables R S: relation T.
+    Definition inter : relation T := fun x y => R x y /\ S x y.
+    Definition compo : relation T := fun x y => exists z : T, R x z /\ S z y.
+    Definition negr : relation T := fun x y => ~ R x y.
+    (* union and converse are already defined in the standard library *)
+
+    Definition bot : relation T := fun _ _ => False.
+    Definition top : relation T := fun _ _ => True.
+  End defs.
+ 
+  Instance eq_same_relation T : Equivalence (same_relation T). Proof. firstorder. Qed.
+ 
+  Instance aac_union_Comm T : Commutative (same_relation T) (union T). Proof. unfold Commutative; compute; intuition.  Qed.
+  Instance aac_union_Assoc T : Associative (same_relation T) (union T). Proof. unfold Associative; compute; intuition.  Qed.
+  Instance aac_bot T : Unit (same_relation T) (union T) (bot T). Proof. constructor; compute; intuition. Qed.
+
+  Instance aac_inter_Comm T : Commutative (same_relation T) (inter T). Proof. unfold Commutative; compute; intuition.  Qed.
+  Instance aac_inter_Assoc T : Associative (same_relation T) (inter T). Proof. unfold Associative; compute; intuition.  Qed.
+  Instance aac_top T : Unit (same_relation T) (inter T) (top T). Proof. constructor; compute; intuition. Qed.
+ 
+  (* note that we use [eq] directly as a neutral element for composition *)
+  Instance aac_compo T : Associative (same_relation T) (compo T). Proof. unfold Associative; compute; firstorder. Qed.
+  Instance aac_eq T : Unit (same_relation T) (compo T) (eq). Proof.  compute; firstorder subst; trivial. Qed.
+
+  Instance negr_compat T : Proper (same_relation T ==> same_relation T) (negr T).
+  Proof. compute. firstorder. Qed.
+
+  Instance transp_compat T : Proper (same_relation T ==> same_relation T) (transp T).
+  Proof. compute. firstorder. Qed.
+
+  Instance clos_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_trans T).
+  Proof.
+    intros  R S H x y Hxy. induction Hxy.
+      constructor 1. apply H. assumption.
+      econstructor 2; eauto 3.
+  Qed.
+  Instance clos_trans_compat T: Proper (same_relation T ==> same_relation T) (clos_trans T).
+  Proof. intros R S H; split; apply clos_trans_incr, H. Qed.
+
+  Instance clos_refl_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_refl_trans T).
+  Proof.
+    intros R S H x y Hxy. induction Hxy.
+      constructor 1. apply H. assumption.
+      constructor 2.
+      econstructor 3; eauto 3.
+  Qed.
+  Instance clos_refl_trans_compat T : Proper (same_relation T ==> same_relation T) (clos_refl_trans T).
+  Proof. intros R S H; split; apply clos_refl_trans_incr, H. Qed.
+
+  Instance preorder_inclusion T : PreOrder (inclusion T).
+  Proof. constructor; unfold Reflexive, Transitive, inclusion; intuition.   Qed.
+
+  Instance lift_inclusion_same_relation T: AAC_lift (inclusion T) (same_relation T) :=
+    Build_AAC_lift (eq_same_relation T) _.
+  Proof.  firstorder. Qed.
+
+End Relations.
+
+Module All.
+  Export Peano.
+  Export Z.
+  Export P.
+  Export N.
+  Export Prop_ops.
+  Export Bool.
+  Export Relations.
+End All.
+ 
+(* Here, we should not see any instance of our classes.
+   Print HintDb typeclass_instances.
+*)
diff --git a/theories/Tutorial.v b/theories/Tutorial.v
new file mode 100644
index 0000000..e403d92
--- /dev/null
+++ b/theories/Tutorial.v
@@ -0,0 +1,401 @@
+(***************************************************************************)
+(*  This is part of aac_tactics, it is distributed under the terms of the  *)
+(*         GNU Lesser General Public License version 3                     *)
+(*              (see file LICENSE for more details)                        *)
+(*                                                                         *)
+(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
+(***************************************************************************)
+
+(** * Tutorial for using the [aac_tactics] library.
+
+   Depending on your installation, either modify the following two
+   lines, or add them to your .coqrc files, replacing "."  with the
+   path to the [aac_tactics] library. *)
+
+Require Arith ZArith.
+
+From AAC_tactics
+Require Import AAC.
+From AAC_tactics
+Require Instances.
+
+(** ** Introductory example 
+
+   Here is a first example with relative numbers ([Z]): one can
+   rewrite an universally quantified hypothesis modulo the
+   associativity and commutativity of [Zplus]. *)
+
+Section introduction.
+
+  Import ZArith.
+  Import Instances.Z.
+
+  Variables a b c : Z.
+  Hypothesis H: forall x, x + Z.opp x = 0.
+  Goal a + b + c + Z.opp (c + a) = b.
+    aac_rewrite H.
+    aac_reflexivity.
+  Qed.
+  Goal a + c + Z.opp (b + a + Z.opp b) = c.
+    do 2 aac_rewrite H.
+    reflexivity.
+  Qed.
+
+  (** Notes:
+     - the tactic handles arbitrary function symbols like [Zopp] (as
+       long as they are proper morphisms w.r.t. the considered
+       equivalence relation);
+     - here, ring would have done the job.
+     *)
+
+End introduction. 
+
+
+(** ** Usage
+
+   One can also work in an abstract context, with arbitrary
+   associative and commutative operators. (Note that one can declare
+   several operations of each kind.) *)
+
+Section base.
+  Context {X} {R} {E: Equivalence R}
+  {plus}
+  {dot}
+  {zero}
+  {one}
+  {dot_A:  @Associative X R dot }       
+  {plus_A: @Associative X R plus }
+  {plus_C: @Commutative X R plus }
+  {dot_Proper :Proper (R ==> R ==> R) dot}
+  {plus_Proper :Proper (R ==> R ==> R) plus}
+  {Zero : Unit R plus zero}
+  {One : Unit R dot one}
+  .     
+
+  Notation "x == y"  := (R x y) (at level 70).
+  Notation "x * y"   := (dot x y) (at level 40, left associativity).
+  Notation "1"       := (one).
+  Notation "x + y"   := (plus x y) (at level 50, left associativity).
+  Notation "0"       := (zero).
+
+  (** In the very first example, [ring] would have solved the
+  goal. Here, since [dot] does not necessarily distribute over [plus],
+  it is not possible to rely on it. *)
+
+  Section reminder.
+    Hypothesis H : forall x, x * x == x.
+    Variables a b c : X.
+   
+    Goal (a+b+c)*(c+a+b) == a+b+c.
+      aac_rewrite H.
+      aac_reflexivity.
+    Qed.
+
+    (** The tactic starts by normalising terms, so that trailing units
+    are always eliminated. *)
+
+    Goal ((a+b)+0+c)*((c+a)+b*1) == a+b+c.
+      aac_rewrite H.
+      aac_reflexivity.
+    Qed.
+  End reminder.
+ 
+  (** The tactic can deal with "proper" morphisms of arbitrary arity
+     (here [f] and [g], or [Zopp] earlier): it rewrites under such
+     morphisms ([g]), and, more importantly, it is able to reorder
+     terms modulo AC under these morphisms ([f]). *)
+
+  Section morphisms.
+    Variable f : X -> X -> X.
+    Hypothesis Hf : Proper (R ==> R ==> R) f.
+    Variable g : X -> X.
+    Hypothesis Hg : Proper (R ==> R) g.
+   
+    Variable a b: X.
+    Hypothesis H : forall x y, x+f (b+y) x == y+x.
+    Goal g ((f (a+b) a) + a) == g (a+a).
+      aac_rewrite H.
+      reflexivity.
+    Qed.
+  End morphisms.
+
+  (** *** Selecting what and where to rewrite 
+
+     There are sometimes several solutions to the matching problem. We
+     now show how to interact with the tactic to select the desired
+     one. *)
+
+  Section occurrence.
+    Variable f : X -> X.
+    Variable a : X.
+    Hypothesis Hf : Proper (R ==> R) f.
+    Hypothesis H : forall x, x + x == x.
+
+    Goal f(a+a)+f(a+a) == f a.
+      (** In case there are several possible solutions, one can print
+         the different solutions using the [aac_instances] tactic (in
+         proof-general, look at buffer *coq* ): *)
+      aac_instances H.
+      (** the default choice is the occurrence with the smallest
+      possible context (number 0), but one can choose the desired
+      one; *)
+      aac_rewrite H at 1.           
+      (** now the goal is [f a + f a  == f a], there is only one solution. *)     
+      aac_rewrite H.
+      reflexivity.
+    Qed.
+ 
+  End occurrence.
+
+  Section subst.
+    Variables a b c d : X.
+    Hypothesis H: forall x y, a*x*y*b == a*(x+y)*b.
+    Hypothesis H': forall x, x + x == x.
+   
+    Goal a*c*d*c*d*b  == a*c*d*b.
+    (** Here, there is only one possible occurrence, but several substitutions; *)
+      aac_instances H.
+      (** one can select them with the proper keyword.  *)
+      aac_rewrite H subst 1.
+      aac_rewrite H'.
+      aac_reflexivity.
+    Qed.
+  End subst.
+ 
+  (** As expected, one can use both keywords together to select the
+     occurrence and the substitution. We also provide a keyword to
+     specify that the rewrite should be done in the right-hand side of
+     the equation. *)
+
+  Section both.
+    Variables a b c d : X.
+    Hypothesis H: forall x y, a*x*y*b == a*(x+y)*b.
+    Hypothesis H': forall x, x + x == x.
+   
+    Goal a*c*d*c*d*b*b == a*(c*d*b)*b.
+      aac_instances H.
+      aac_rewrite H at 1 subst 1.
+      aac_instances H.
+      aac_rewrite H.
+      aac_rewrite H'.
+      aac_rewrite H at 0 subst 1 in_right.
+      aac_reflexivity.
+    Qed.
+     
+  End both.
+
+  (** *** Distinction between [aac_rewrite] and [aacu_rewrite]:
+
+  [aac_rewrite] rejects solutions in which variables are instantiated
+  by units, while the companion tactic, [aacu_rewrite] allows such
+  solutions.  *)
+
+  Section dealing_with_units.
+    Variables a b c: X.
+    Hypothesis H: forall x, a*x*a == x.
+    Goal a*a == 1.
+      (** Here, [x] must be instantiated with [1], so that the [aac_*]
+         tactics give no solutions; *)
+      try aac_instances H.           
+      (** while we get solutions with the [aacu_*] tactics. *)     
+      aacu_instances H.
+      aacu_rewrite H.
+      reflexivity.
+    Qed.
+     
+    (** We introduced this distinction because it allows us to rule
+    out dummy cases in common situations: *)
+
+    Hypothesis H': forall x y z,  x*y + x*z == x*(y+z).
+    Goal a*b*c + a*c + a*b == a*(c+b*(1+c)).
+    (** 6 solutions without units,  *)
+      aac_instances H'.        
+      aac_rewrite H' at 0.
+    (** more than 52 with units. *)
+      aacu_instances H'.
+    Abort.
+
+  End dealing_with_units. 
+End base.
+
+(** *** Declaring instances
+
+   To use one's own operations: it suffices to declare them as
+   instances of our classes. (Note that the following instances are
+   already declared in file [Instances.v].) *)
+
+Section Peano.
+  Import Arith.
+    
+  Instance aac_plus_Assoc : Associative eq plus := plus_assoc.
+  Instance aac_plus_Comm : Commutative eq plus :=  plus_comm.
+ 
+  Instance aac_one : Unit eq mult 1 :=
+    Build_Unit eq mult 1 mult_1_l mult_1_r. 
+  Instance aac_zero_plus : Unit eq plus O :=
+    Build_Unit eq plus (O) plus_0_l plus_0_r.
+ 
+
+  (** Two (or more) operations may share the same units: in the
+  following example, [0] is understood as the unit of [max] as well as
+  the unit of [plus]. *)
+
+  Instance aac_max_Comm : Commutative eq Max.max :=  Max.max_comm.
+  Instance aac_max_Assoc : Associative eq Max.max := Max.max_assoc.
+
+  Instance aac_zero_max : Unit eq Max.max  O :=
+    Build_Unit eq Max.max 0 Max.max_0_l Max.max_0_r. 
+
+  Variable a b c : nat.
+  Goal Max.max (a + 0) 0 = a.
+    aac_reflexivity.
+  Qed.
+   
+  (** Furthermore, several operators can be mixed: *)
+
+  Hypothesis H : forall x y z, Max.max (x + y) (x + z) = x+ Max.max y z.
+ 
+  Goal Max.max (a + b) (c + (a * 1)) = Max.max c b + a.
+    aac_instances H. aac_rewrite H. aac_reflexivity.
+  Qed. 
+  Goal Max.max (a + b) (c + Max.max (a*1+0) 0) = a + Max.max b c.
+    aac_instances H. aac_rewrite H. aac_reflexivity.
+  Qed.
+
+ 
+  (** *** Working with inequations
+
+     To be able to use the tactics, the goal must be a relation [R]
+     applied to two arguments, and the rewritten hypothesis must end
+     with a relation [Q] applied to two arguments. These relations are
+     not necessarily equivalences, but they should be related
+     according to the occurrence where the rewrite takes place; we
+     leave this check to the underlying call to [setoid_rewrite].  *)
+
+  (** One can rewrite equations in the left member of inequations, *)
+  Goal (forall x, x + x = x) -> a + b + b + a <= a + b.
+    intro Hx.
+    aac_rewrite Hx.
+    reflexivity.
+  Qed.
+
+  (** or in the right member of inequations, using the [in_right] keyword  *)
+  Goal (forall x, x + x = x) -> a + b  <= a + b + b + a.
+    intro Hx.
+    aac_rewrite Hx in_right.
+    reflexivity.
+  Qed.
+ 
+  (** Similarly, one can rewrite inequations in inequations, *)
+  Goal (forall x, x + x <= x) -> a + b + b + a <= a + b.
+    intro Hx.
+    aac_rewrite Hx.
+    reflexivity.
+  Qed. 
+
+  (** possibly in the right-hand side. *)
+  Goal (forall x, x <= x + x) -> a + b <= a + b + b + a.
+    intro Hx.
+    aac_rewrite <- Hx in_right.
+    reflexivity.
+  Qed.
+
+  (** [aac_reflexivity] deals with "trivial" inequations too *)
+  Goal Max.max (a + b) (c + a) <= Max.max (b + a) (c + 1*a).
+    aac_reflexivity.
+  Qed.
+
+  (** In the last three examples, there were no equivalence relation
+     involved in the goal. However, we actually had to guess the
+     equivalence relation with respect to which the operators
+     ([plus,max,0]) were AC.  In this case, it was Leibniz equality
+     [eq] so that it was automatically inferred; more generally, one
+     can specify which equivalence relation to use by declaring
+     instances of the [AAC_lift] type class: *)
+
+  Instance lift_le_eq : AAC_lift le eq := {}.
+  (** (This instance is automatically inferred because [eq] is always a
+     valid candidate, here for [le].) *)
+
+
+End Peano.
+
+
+(** *** Normalising goals
+
+   We also provide a tactic to normalise terms modulo AC. This
+   normalisation is the one we use internally.  *)
+
+Section AAC_normalise.
+
+  Import Instances.Z.
+  Import ZArith.
+  Open Scope Z_scope.
+ 
+  Variable a b c d : Z.
+  Goal a + (b + c*c*d) + a + 0 + d*1 = a.
+    aac_normalise.
+  Abort.
+
+End AAC_normalise.
+
+
+
+
+(** ** Examples from the web page *)
+Section Examples.
+
+  Import Instances.Z.
+  Import ZArith.
+  Open Scope Z_scope.
+
+  (** *** Reverse triangle inequality *)
+
+  Lemma Zabs_triangle : forall x y,  Z.abs (x + y) <= Z.abs x + Z.abs y .
+  Proof Z.abs_triangle.
+
+  Lemma Zplus_opp_r : forall x, x + -x = 0.
+  Proof Zplus_opp_r.
+
+  (** The following morphisms are required to perform the required rewrites *)
+  Instance Zminus_compat : Proper (Z.ge ==> Z.le) Z.opp.
+  Proof. intros x y. omega. Qed.
+ 
+  Instance Proper_Zplus : Proper (Z.le ==> Z.le ==> Z.le) Zplus.
+  Proof. firstorder. Qed.
+
+  Goal forall a b, Z.abs a - Z.abs b <= Z.abs (a - b).
+    intros. unfold Zminus.
+    aac_instances <- (Zminus_diag b).
+    aac_rewrite <- (Zminus_diag b) at 3.
+    unfold Zminus.
+    aac_rewrite Z.abs_triangle.
+    aac_rewrite Zplus_opp_r.
+    aac_reflexivity.
+  Qed.
+
+
+  (** *** Pythagorean triples *)
+
+  Notation "x ^2" := (x*x) (at level 40).
+  Notation "2 ⋅ x" := (x+x) (at level 41).
+
+  Lemma Hbin1: forall x y, (x+y)^2   = x^2 + y^2 +  2⋅x*y. Proof. intros; ring. Qed.
+  Lemma Hbin2: forall x y, x^2 + y^2 = (x+y)^2   + -(2⋅x*y). Proof. intros; ring.  Qed.
+  Lemma Hopp : forall x, x + -x = 0. Proof Zplus_opp_r. 
+ 
+  Variables a b c : Z.
+  Hypothesis H : c^2 + 2⋅(a+1)*b  = (a+1+b)^2.
+  Goal a^2 + b^2 + 2⋅a + 1 = c^2.
+    aacu_rewrite <- Hbin1.
+    rewrite Hbin2.
+    aac_rewrite <- H.
+    aac_rewrite Hopp.
+    aac_reflexivity.
+  Qed.
+
+  (** Note: after the [aac_rewrite <- H], one could use [ring] to close the proof.*)
+
+End Examples.
+
+
diff --git a/theories/Utils.v b/theories/Utils.v
new file mode 100644
index 0000000..0f37ae1
--- /dev/null
+++ b/theories/Utils.v
@@ -0,0 +1,257 @@
+(***************************************************************************)
+(*  This is part of aac_tactics, it is distributed under the terms of the  *)
+(*         GNU Lesser General Public License version 3                     *)
+(*              (see file LICENSE for more details)                        *)
+(*                                                                         *)
+(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
+(***************************************************************************)
+
+
+Require Import Arith NArith.
+Require Import List.
+Require Import FMapPositive FMapFacts.
+Require Import RelationClasses Equality.
+
+Set Implicit Arguments.
+Set Asymmetric Patterns.
+
+(** * Utilities for positive numbers
+   which we use as:
+     - indices for morphisms and symbols
+     - multiplicity of terms in sums *)
+
+Notation idx := positive.
+
+Fixpoint eq_idx_bool i j :=
+  match i,j with
+    | xH, xH => true
+    | xO i, xO j => eq_idx_bool i j
+    | xI i, xI j => eq_idx_bool i j
+    | _, _ => false
+  end.
+
+Fixpoint idx_compare i j :=
+  match i,j with
+    | xH, xH => Eq
+    | xH, _ => Lt
+    | _, xH => Gt
+    | xO i, xO j => idx_compare i j
+    | xI i, xI j => idx_compare i j
+    | xI _, xO _ => Gt
+    | xO _, xI _ => Lt
+  end.
+
+Notation pos_compare := idx_compare (only parsing).
+
+(** Specification predicate for boolean binary functions *)
+Inductive decide_spec {A} {B} (R : A -> B -> Prop) (x : A) (y : B) : bool -> Prop :=
+| decide_true : R x y -> decide_spec R x y true
+| decide_false : ~(R x y) -> decide_spec R x y false.
+
+Lemma eq_idx_spec : forall i j, decide_spec (@eq _) i j (eq_idx_bool i j).
+Proof.
+  induction i; destruct j; simpl; try (constructor; congruence).
+   case (IHi j); constructor; congruence.
+   case (IHi j); constructor; congruence.
+Qed.
+
+(** weak specification predicate for comparison functions: only the 'Eq' case is specified *)
+Inductive compare_weak_spec A: A -> A -> comparison -> Prop :=
+| pcws_eq: forall i, compare_weak_spec i i Eq
+| pcws_lt: forall i j, compare_weak_spec i j Lt
+| pcws_gt: forall i j, compare_weak_spec i j Gt.
+
+Lemma pos_compare_weak_spec: forall i j, compare_weak_spec i j (pos_compare i j).
+Proof. induction i; destruct j; simpl; try constructor; case (IHi j); intros; constructor. Qed.
+
+Lemma idx_compare_reflect_eq: forall i j, idx_compare i j = Eq -> i=j.
+Proof. intros i j. case (pos_compare_weak_spec i j); intros; congruence. Qed.
+
+(** * Dependent types utilities *)
+
+Notation cast T H u := (eq_rect _ T u _ H).
+
+Section dep.
+  Variable U: Type.
+  Variable T: U -> Type.
+
+  Lemma cast_eq: (forall u v: U, {u=v}+{u<>v}) ->
+    forall A (H: A=A) (u: T A), cast T H u = u.
+  Proof. intros. rewrite <- Eqdep_dec.eq_rect_eq_dec; trivial. Qed.
+
+  Variable f: forall A B, T A -> T B -> comparison.
+  Definition reflect_eqdep := forall A u B v (H: A=B), @f A B u v = Eq -> cast T H u = v.
+
+  (* these lemmas have to remain transparent to get structural recursion
+     in the lemma [tcompare_weak_spec] below *)
+  Lemma reflect_eqdep_eq: reflect_eqdep ->
+    forall A u v, @f A A u v = Eq -> u = v.
+  Proof. intros H A u v He. apply (H _ _ _ _ eq_refl He). Defined.
+
+  Lemma reflect_eqdep_weak_spec: reflect_eqdep ->
+    forall A u v, compare_weak_spec u v (@f A A u v).
+  Proof.
+    intros. case_eq (f u v); try constructor.
+    intro H'. apply reflect_eqdep_eq in H'. subst. constructor. assumption.
+  Defined.
+End dep.
+
+
+(** * Utilities about (non-empty) lists and multisets  *)
+
+Inductive nelist (A : Type) : Type :=
+| nil : A -> nelist A
+| cons : A -> nelist A -> nelist A.
+
+Notation "x :: y" := (cons x y).
+
+Fixpoint nelist_map (A B: Type) (f: A -> B) l :=
+  match l with
+    | nil x => nil ( f x)
+    | cons x l => cons ( f x) (nelist_map  f l)
+  end.
+
+Fixpoint appne  A l l' : nelist A :=
+  match l with
+    nil x => cons x l'
+    | cons t q => cons t (appne A q l')
+  end.
+
+Notation "x ++ y" := (appne x y).
+
+(** finite multisets are represented with ordered lists with multiplicities *)
+Definition mset A := nelist (A*positive).
+
+(** lexicographic composition of comparisons (this is a notation to keep it lazy) *)
+Notation lex e f := (match e with Eq => f | _ => e end).  
+
+
+Section lists.
+
+  (** comparison functions *)
+
+  Section c.
+    Variables A B: Type.
+    Variable compare: A -> B -> comparison.
+    Fixpoint list_compare h k :=
+      match h,k with
+        | nil x, nil y => compare x y
+        | nil x, _   => Lt
+        | _,   nil x => Gt
+        | u::h, v::k => lex (compare u v) (list_compare h k)
+      end. 
+  End c.
+  Definition mset_compare A B compare: mset A -> mset B -> comparison :=
+    list_compare (fun un vm =>
+      let '(u,n) := un in
+        let '(v,m) := vm in
+        lex (compare u v) (pos_compare n m)).
+
+  Section list_compare_weak_spec.
+    Variable A: Type.
+    Variable compare: A -> A -> comparison.
+    Hypothesis Hcompare: forall u v, compare_weak_spec u v (compare u v).
+    (* this lemma has to remain transparent to get structural recursion
+       in the lemma [tcompare_weak_spec] below *)
+    Lemma list_compare_weak_spec: forall h k,
+      compare_weak_spec h k (list_compare compare h k).
+    Proof.
+      induction h as [|u h IHh]; destruct k as [|v k]; simpl; try constructor.
+
+      case (Hcompare a a0 ); try constructor.
+      case (Hcompare u v ); try constructor.
+      case (IHh k); intros; constructor.
+    Defined.
+  End list_compare_weak_spec.
+
+  Section mset_compare_weak_spec.
+    Variable A: Type.
+    Variable compare: A -> A -> comparison.
+    Hypothesis Hcompare: forall u v, compare_weak_spec u v (compare u v).
+    (* this lemma has to remain transparent to get structural recursion
+       in the lemma [tcompare_weak_spec] below *)
+    Lemma mset_compare_weak_spec: forall h k,
+      compare_weak_spec h k (mset_compare compare h k).
+    Proof.
+      apply list_compare_weak_spec.
+      intros [u n] [v m].
+       case (Hcompare u v); try constructor.
+       case (pos_compare_weak_spec n m); try constructor.
+    Defined.
+  End mset_compare_weak_spec.
+
+  (** (sorted) merging functions  *)
+
+  Section m.
+    Variable A: Type.
+    Variable compare: A -> A -> comparison.
+    Definition insert n1 h1 :=
+      let fix insert_aux l2 :=
+      match l2 with
+        | nil (h2,n2) =>
+          match compare h1 h2 with
+            | Eq => nil (h1,Pplus n1 n2)
+            | Lt => (h1,n1):: nil (h2,n2)
+            | Gt => (h2,n2):: nil (h1,n1)
+          end
+        | (h2,n2)::t2 =>
+          match compare h1 h2 with
+            | Eq => (h1,Pplus n1 n2):: t2
+            | Lt => (h1,n1)::l2
+            | Gt => (h2,n2)::insert_aux t2
+          end
+      end
+      in insert_aux.
+   
+    Fixpoint merge_msets l1 :=
+      match l1 with
+        | nil (h1,n1) => fun l2 => insert n1 h1 l2
+        | (h1,n1)::t1 =>
+          let fix merge_aux l2 :=
+            match l2 with
+               | nil (h2,n2) =>
+                match compare h1 h2 with
+                  | Eq => (h1,Pplus n1 n2) :: t1
+                  | Lt => (h1,n1):: merge_msets t1 l2
+                  | Gt => (h2,n2)::  l1
+                end
+              | (h2,n2)::t2 =>
+                match compare h1 h2 with
+                  | Eq => (h1,Pplus n1 n2)::merge_msets t1 t2
+                  | Lt => (h1,n1)::merge_msets t1 l2
+                  | Gt => (h2,n2)::merge_aux t2
+                end
+            end
+            in merge_aux
+      end.
+
+    (** interpretation of a list with a constant and a binary operation *)
+
+    Variable B: Type.
+    Variable map: A -> B.
+    Variable b2: B -> B -> B.
+    Fixpoint fold_map l :=
+      match l with
+        | nil x => map x
+        | u::l => b2 (map u) (fold_map l)
+      end.
+
+    (** mapping and merging *)
+
+    Variable merge: A -> nelist B -> nelist B.
+    Fixpoint merge_map (l: nelist A): nelist B :=
+      match l with
+        | nil x => nil (map x)
+        | u::l => merge u (merge_map l)
+      end.
+
+    Variable ret : A -> B.
+    Variable bind : A -> B -> B.
+    Fixpoint fold_map' (l : nelist A) : B :=
+      match l with
+        | nil x => ret x
+        | u::l => bind u (fold_map' l)
+      end.
+
+  End m.
+End lists.