Merge pull request #91 from damien-pous/v8.14

support for idempotent operations, v8.14

README.md

@@ -37,6 +37,10 @@ operators and their properties as type class instances. Many common
 operator instances, such as for Z binary arithmetic and booleans, are
 provided with the plugin.
 
+An additional tactic makes it possible to prove equations between
+expressions involving associative/commutative/idempotent operations
+and their potential units.
+
 ## Meta
 
 - Author(s):
@@ -90,6 +94,12 @@ Section ZOpp.
     aac_rewrite H.
     aac_reflexivity.
   Qed.
+
+  Goal Z.max (b + c) (c + b) + a + Z.opp (c + b) = a.
+    aac_normalise.
+    aac_rewrite H.
+    aac_reflexivity.
+  Qed.
 End ZOpp.
 ```
 

src/theory.ml

@@ -77,6 +77,16 @@ module Classes = struct
 
   end
 
+  module Idempotent = struct
+    let typ = Coq.find_global "classes.Idempotent"
+    let ty (rlt : Coq.Relation.t) (value : constr) =
+      mkApp (Coq.get_efresh typ, [| rlt.Coq.Relation.carrier;
+				rlt.Coq.Relation.r;
+				value
+			     |] )
+
+  end
+
   module Proper = struct
     let typeof =  Coq.find_global "internal.sym.type_of"
     let relof = Coq.find_global "internal.sym.rel_of"
@@ -190,6 +200,7 @@ module Bin =struct
 	       compat : Constr.t;
 	       assoc : Constr.t;
 	       comm : Constr.t option;
+	       idem : Constr.t option;
 	      }
 
   let typ = Coq.find_global "bin.pack"
@@ -198,11 +209,13 @@ module Bin =struct
   let mk_pack: Coq.Relation.t -> pack -> constr = fun (rlt) s ->
     let (x,r) = Coq.Relation.split rlt in
     let comm_ty = Classes.Commutative.ty rlt (EConstr.of_constr s.value) in
+    let idem_ty = Classes.Idempotent.ty rlt (EConstr.of_constr s.value) in
     mkApp (Coq.get_efresh mkPack , [| x ; r;
 				  EConstr.of_constr s.value;
 				  EConstr.of_constr s.compat ;
 				  EConstr.of_constr s.assoc;
-				  Coq.Option.of_option comm_ty (Option.map EConstr.of_constr s.comm)
+				  Coq.Option.of_option comm_ty (Option.map EConstr.of_constr s.comm);
+				  Coq.Option.of_option idem_ty (Option.map EConstr.of_constr s.idem)
 			       |])
   let mk_ty : Coq.Relation.t -> constr = fun rlt ->
    let (x,r) = Coq.Relation.split rlt in
@@ -319,12 +332,14 @@ module Trans = struct
       Constr.equal p1.value p2.value &&
       Constr.equal p1.compat p2.compat &&
       Constr.equal p1.assoc p2.assoc &&
-      Option.equal Constr.equal p1.comm p2.comm
+      Option.equal Constr.equal p1.comm p2.comm &&
+      Option.equal Constr.equal p1.idem p2.idem
+
 
     let hash_bin_pack p =
       let open Bin in
-      combine4 (Constr.hash p.value) (Constr.hash p.compat)
-        (Constr.hash p.assoc) (Option.hash Constr.hash p.comm)
+      combine5 (Constr.hash p.value) (Constr.hash p.compat)
+        (Constr.hash p.assoc) (Option.hash Constr.hash p.comm) (Option.hash Constr.hash p.idem)
 
     let eq_unit_of u1 u2 =
       let open Unit in
@@ -455,6 +470,7 @@ module Trans = struct
 	  : (Evd.evar_map * Bin.pack) option =
 	let assoc_ty = Classes.Associative.ty rlt op in
 	let comm_ty = Classes.Commutative.ty rlt op in
+	let idem_ty = Classes.Idempotent.ty rlt op in
 	let proper_ty  = Classes.Proper.ty rlt op 2 in
 	try
 	  let sigma, proper = Typeclasses.resolve_one_typeclass env sigma proper_ty in
@@ -466,11 +482,19 @@ module Trans = struct
 	    with Not_found ->
 	      sigma, None
 	  in
+	  let sigma, idem  =
+	    try
+	      let sigma,idem = Typeclasses.resolve_one_typeclass env sigma idem_ty in
+	      sigma, Some idem
+	    with Not_found ->
+	      sigma, None
+	  in
 	  let bin =
 	    {Bin.value = EConstr.to_constr sigma op;
 	     Bin.compat = EConstr.to_constr sigma proper;
 	     Bin.assoc = EConstr.to_constr sigma assoc;
-	     Bin.comm = Option.map (EConstr.to_constr sigma) comm }
+	     Bin.comm = Option.map (EConstr.to_constr sigma) comm;
+	     Bin.idem = Option.map (EConstr.to_constr sigma) idem }
 	  in
 	  Some (sigma,bin)
 	with |Not_found -> None
@@ -917,7 +941,8 @@ module Trans = struct
 	    Bin.value = EConstr.to_constr sigma op;
 	    Bin.compat = EConstr.to_constr sigma compat;
 	    Bin.assoc = EConstr.to_constr sigma assoc;
-	    Bin.comm = None
+	    Bin.comm = None;
+	    Bin.idem = None
 	  }
       with Not_found -> user_error @@ Pp.strbrk "Cannot infer a default A operator (required at least to be Proper and Associative)"
     in

theories/AAC.v

@@ -9,7 +9,7 @@
 (** * 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
+   commutative/idempotent operators, and define a data-type for reified (or
    quoted) expressions (with morphisms).
 
    We then define a reflexive decision procedure to decide the
@@ -64,12 +64,15 @@ 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 Idempotent (X:Type) (R: relation X) (plus: X -> X -> X) :=
+  law_idem: forall x, R (plus x x) 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
                                                                }.
 Register Associative as aac_tactics.classes.Associative.
 Register Commutative as aac_tactics.classes.Commutative.
+Register Idempotent as aac_tactics.classes.Idempotent.
 Register Unit as aac_tactics.classes.Unit.
 
 
@@ -196,7 +199,8 @@ Module Bin.
       value:> X -> X -> X;
       compat: Proper (R ==> R ==> R) value;
       assoc: Associative R value;
-      comm: option (Commutative R value)
+      comm: option (Commutative R value);
+      idem: option (Idempotent R value)
                      }.
 
     Register pack as aac_tactics.bin.pack.
@@ -364,6 +368,10 @@ Section s.
   Definition is_commutative i :=
     match Bin.comm (e_bin i) with Some _ => true | None => false end.
 
+  (* is [i] idempotent ? *)
+  Definition is_idempotent i :=
+    match Bin.idem (e_bin i) with Some _ => true | None => false end.
+
 
   (** ** Normalisation *)
 
@@ -496,7 +504,11 @@ Section s.
 
   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
+      | sum i l => if is_commutative i then
+                     if is_idempotent i then
+                        sum' i (reduce_mset (norm_msets norm i l))
+                     else 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
@@ -526,6 +538,13 @@ Section s.
     discriminate.
   Qed.
 
+  Instance Binvalue_Idempotent i (H :  is_idempotent i = true) : Idempotent R  (@Bin.value _ _ (e_bin i) ).
+  Proof.
+    unfold is_idempotent in H.
+    destruct (Bin.idem (e_bin i)); auto.
+    discriminate.
+  Qed.
+
   Instance Binvalue_Associative i :Associative R (@Bin.value _ _ (e_bin i) ).
   Proof.
     destruct ((e_bin i)); auto.
@@ -732,6 +751,7 @@ Section s.
       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).
@@ -750,6 +770,22 @@ Section s.
 
     apply H.
   Defined.
+
+  Lemma copy_idem i (Idem : Idempotent R (Bin.value (e_bin i))) n x:
+    copy (plus:=(Bin.value (e_bin i))) n x == x.
+  Proof.
+    induction n using Pos.peano_ind; simpl.
+    apply copy_xH.
+    rewrite copy_Psucc, IHn. apply law_idem.
+  Qed.
+
+  Lemma eval_reduce_msets i (Idem : Idempotent R (Bin.value (e_bin i))) m:
+    eval (sum i (reduce_mset m)) == eval (sum i m).
+  Proof.
+    induction m as [[a n]|[a n] m IH].
+    - simpl. now rewrite 2copy_idem.
+    - simpl. rewrite IH. now rewrite 2copy_idem.
+  Qed.
 
   (** auxiliary lemmas about products  *)
 
@@ -889,8 +925,14 @@ Section s.
   Proof.
     induction u as [ p m | p l | ? | ?];  simpl norm.
     case_eq (is_commutative p); intros.
+    case_eq (is_idempotent p); intros.
     rewrite sum'_sum.
+    rewrite eval_reduce_msets. 2: eauto with typeclass_instances. 
     apply eval_norm_msets; auto.
+
+    rewrite sum'_sum.
+    apply eval_norm_msets; auto.
+
     reflexivity.
 
     rewrite prd'_prd.

theories/Instances.v

@@ -40,11 +40,15 @@ Module Peano.
   Instance aac_min_Comm : Commutative eq min :=  min_comm.
   #[global]
   Instance aac_min_Assoc : Associative eq min :=  min_assoc.
+  #[global]
+  Instance aac_min_Idem : Idempotent eq min :=  min_idempotent.
 
   #[global]
   Instance aac_max_Comm : Commutative eq max :=  max_comm.
   #[global]
   Instance aac_max_Assoc : Associative eq max :=  max_assoc.
+  #[global]
+  Instance aac_max_Idem : Idempotent eq max :=  max_idempotent.
 
   #[global]
   Instance aac_one : Unit eq mult 1 :=  Build_Unit eq mult 1 mult_1_l mult_1_r. 
@@ -80,11 +84,15 @@ Module Z.
   Instance aac_Zmin_Comm : Commutative eq Z.min :=  Z.min_comm.
   #[global]
   Instance aac_Zmin_Assoc : Associative eq Z.min :=  Z.min_assoc.
+  #[global]
+  Instance aac_Zmin_Idem : Idempotent eq Z.min :=  Z.min_idempotent.
 
   #[global]
   Instance aac_Zmax_Comm : Commutative eq Z.max :=  Z.max_comm.
   #[global]
   Instance aac_Zmax_Assoc : Associative eq Z.max :=  Z.max_assoc.
+  #[global]
+  Instance aac_Zmax_Idem : Idempotent eq Z.max :=  Z.max_idempotent.
 
   #[global]
   Instance aac_one : Unit eq Zmult 1 :=  Build_Unit eq Zmult 1 Zmult_1_l Zmult_1_r. 
@@ -132,11 +140,15 @@ Module N.
   Instance aac_Nmin_Comm : Commutative eq N.min :=  N.min_comm.
   #[global]
   Instance aac_Nmin_Assoc : Associative eq N.min :=  N.min_assoc.
+  #[global]
+  Instance aac_Nmin_Idem : Idempotent eq N.min :=  N.min_idempotent.
 
   #[global]
   Instance aac_Nmax_Comm : Commutative eq N.max :=  N.max_comm.
   #[global]
   Instance aac_Nmax_Assoc : Associative eq N.max :=  N.max_assoc.
+  #[global]
+  Instance aac_Nmax_Idem : Idempotent eq N.max :=  N.max_idempotent.
 
   #[global]
   Instance aac_one  : Unit eq Nmult (1)%N := Build_Unit eq Nmult (1)%N Nmult_1_l Nmult_1_r. 
@@ -170,11 +182,15 @@ Module P.
   Instance aac_Pmin_Comm : Commutative eq Pos.min :=  Pos.min_comm.
   #[global]
   Instance aac_Pmin_Assoc : Associative eq Pos.min :=  Pos.min_assoc.
+  #[global]
+  Instance aac_Pmin_Idem : Idempotent eq Pos.min :=  Pos.min_idempotent.
 
   #[global]
   Instance aac_Pmax_Comm : Commutative eq Pos.max :=  Pos.max_comm.
   #[global]
   Instance aac_Pmax_Assoc : Associative eq Pos.max :=  Pos.max_assoc.
+  #[global]
+  Instance aac_Pmax_Idem : Idempotent eq Pos.max :=  Pos.max_idempotent.
 
   (*  TODO : add this lemma in the stdlib *)
   Lemma Pmult_1_l (x : positive) : 1 * x = x.
@@ -208,11 +224,15 @@ Module Q.
   Instance aac_Qmin_Comm : Commutative Qeq Qmin :=  Q.min_comm.
   #[global]
   Instance aac_Qmin_Assoc : Associative Qeq Qmin :=  Q.min_assoc.
+  #[global]
+  Instance aac_Qmin_Idem : Idempotent Qeq Qmin :=  Q.min_idempotent.
 
   #[global]
   Instance aac_Qmax_Comm : Commutative Qeq Qmax :=  Q.max_comm.
   #[global]
   Instance aac_Qmax_Assoc : Associative Qeq Qmax :=  Q.max_assoc.
+  #[global]
+  Instance aac_Qmax_Idem : Idempotent Qeq Qmax :=  Q.max_idempotent.
 
   #[global]
   Instance aac_one : Unit Qeq Qmult 1 :=  Build_Unit Qeq Qmult 1 Qmult_1_l Qmult_1_r. 
@@ -233,9 +253,9 @@ Module Prop_ops.
   #[global]
   Instance aac_or_Comm : Commutative iff or. Proof.  unfold Commutative; tauto.  Qed.
   #[global]
-  Instance aac_and_Assoc : Associative iff and. Proof.  unfold Associative; tauto.  Qed.
+  Instance aac_or_Idem : Idempotent iff or. Proof.  unfold Idempotent; tauto.  Qed.
   #[global]
-  Instance aac_and_Comm : Commutative iff and. Proof.  unfold Commutative; tauto.  Qed.
+  Instance aac_and_Idem : Idempotent iff and. Proof.  unfold Idempotent; tauto.  Qed.
   #[global]
   Instance aac_True : Unit iff or False.  Proof.  constructor; firstorder.  Qed.
   #[global]
@@ -255,10 +275,14 @@ Module Bool.
   #[global]
   Instance aac_orb_Comm : Commutative eq orb. Proof.  unfold Commutative; firstorder with bool.  Qed.
   #[global]
+  Instance aac_orb_Idem : Idempotent eq orb. Proof.  intro; apply Bool.orb_diag.  Qed.
+  #[global]
   Instance aac_andb_Assoc : Associative eq andb. Proof.  unfold Associative; firstorder with bool.  Qed.
   #[global]
   Instance aac_andb_Comm : Commutative eq andb. Proof.  unfold Commutative; firstorder with bool.  Qed.
   #[global]
+  Instance aac_andb_Idem : Idempotent eq andb. Proof.  intro; apply Bool.andb_diag.  Qed.
+  #[global]
   Instance aac_true : Unit eq orb false.  Proof.  constructor; firstorder with bool.  Qed.
   #[global]
   Instance aac_false : Unit eq andb true.  Proof.  constructor; intros [|];firstorder.  Qed.
@@ -289,13 +313,17 @@ Module Relations.
   #[global]
   Instance aac_union_Assoc T : Associative (same_relation T) (union T). Proof. unfold Associative; compute; intuition.  Qed.
   #[global]
+  Instance aac_union_Idem T : Idempotent (same_relation T) (union T). Proof. unfold Idempotent; compute; intuition.  Qed.
+  #[global]
   Instance aac_bot T : Unit (same_relation T) (union T) (bot T). Proof. constructor; compute; intuition. Qed.
 
   #[global]
   Instance aac_inter_Comm T : Commutative (same_relation T) (inter T). Proof. unfold Commutative; compute; intuition.  Qed.
   #[global]
   Instance aac_inter_Assoc T : Associative (same_relation T) (inter T). Proof. unfold Associative; compute; intuition.  Qed.
   #[global]
+  Instance aac_inter_Idem T : Idempotent (same_relation T) (inter T). Proof. unfold Idempotent; compute; intuition.  Qed.
+  #[global]
   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 *)