Canonical ordering for aac_normalise tactic

.gitignore

@@ -20,6 +20,7 @@
 
 src/aac.ml
 .lia.cache
+.nia.cache
 .merlin
 Makefile.coq
 Makefile.coq.conf

CHANGELOG.md

@@ -0,0 +1,20 @@
+# Changelog
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
+
+## [Unreleased]
+
+## [8.19.1] - 2024-06-01
+
+### Added
+
+- `aac_normalise in H` tactic.
+- `gcd` and `lcm` instances for `Nat`, `N`, and `Z`.
+
+### Fixed
+
+- Make the order of sums produced by `aac_normalise` tactic consistent across calls.
+
+[Unreleased]: https://github.com/coq-community/chapar/compare/v8.19.1...master
+[8.19.1]: https://github.com/coq-community/chapar/releases/tag/v8.19.1

src/matcher.ml

@@ -108,6 +108,9 @@ module Terms : sig
   val equal_aac : units -> t -> t -> bool
   val size: t -> int
 
+  (* permute symbols according to p *)
+  val map_syms: (symbol -> symbol) -> t -> t
+
   (** {1 Terms in normal form}
 
       A term in normal form is the canonical representative of the
@@ -162,6 +165,13 @@ end
       | Sym (_,v)-> Array.fold_left (fun acc x -> size x + acc) 1 v
       | _ -> 1
 
+    (* permute symbols according to p *)
+    let rec map_syms p = function
+      | Dot(s,u,v) -> Dot(p s, map_syms p u, map_syms p v)
+      | Plus(s,u,v) -> Plus(p s, map_syms p u, map_syms p v)
+      | Sym(s,u) -> Sym(p s, Array.map (map_syms p) u)
+      | Unit s -> Unit(p s)
+      | u -> u
 
     type nf_term =
       | TAC of  symbol * nf_term mset

src/matcher.mli

@@ -118,6 +118,8 @@ sig
       units of a same operator are not considered equal.  *)
   val equal_aac : units ->  t -> t -> bool
 
+  (* permute symbols according to p *)
+  val map_syms: (symbol -> symbol) -> t -> t
 
   (** {2 Normalised terms (canonical representation) }
 

src/theory.ml

@@ -724,6 +724,24 @@ module Trans = struct
     let sigma = Gather.gather env sigma rlt envs (EConstr.of_constr (Constr.mkApp (l, [| Constr.mkRel 0;Constr.mkRel 0|]))) in
     sigma
 
+  (* reorder the environment to make it (more) canonical *)
+  let reorder envs =
+    let rec insert k v = function
+      | [] -> [k,v]
+      | ((h,_)::_) as l when Constr.compare k h = -1 -> (k,v)::l
+      | y::q -> y::insert k v q
+    in
+    let insert k v l =
+      match v with Some v -> insert k v l | None -> l
+    in
+    let l = HMap.fold insert envs.discr [] in
+    let old = Hashtbl.copy envs.bloom_back in
+    PackTable.clear envs.bloom;
+    Hashtbl.clear envs.bloom_back;
+    envs.bloom_next := 1;
+    List.iter (fun (c,pack) -> add_bloom envs pack) l;
+    (fun s -> PackTable.find envs.bloom (Hashtbl.find old s))
+
   (* [t_of_constr] buils a the abstract syntax tree of a constr,
      updating in place the environment. Doing so, we infer all the
      morphisms and the AC/A operators. It is mandatory to do so both
@@ -734,7 +752,8 @@ module Trans = struct
     let sigma = Gather.gather env sigma rlt envs r in
     let l,sigma = Parse.t_of_constr env sigma rlt envs l in
     let r, sigma = Parse.t_of_constr env sigma rlt envs r in
-    l, r, sigma
+    let p = reorder envs in
+    Matcher.Terms.map_syms p l, Matcher.Terms.map_syms p r, sigma
 
   (* An intermediate representation of the environment, with association lists for AC/A operators, and also the raw [packer] information *)
 
@@ -967,25 +986,6 @@ module Trans = struct
     in
       sigma,record
 
-  (* We want to lift down the indexes of symbols. *)
-  let renumber (l: (int * 'a) list ) =
-    let _, l = List.fold_left (fun (next,acc) (glob,x) ->
-				 (next+1, (next,glob,x)::acc)
-			      ) (1,[]) l
-    in
-    let rec to_global loc = function
-      | [] -> assert false
-      | (local, global,x)::q when  local = loc -> global
-      | _::q -> to_global loc q
-    in
-    let rec to_local glob = function
-      | [] -> assert false
-      | (local, global,x)::q when  global = glob -> local
-      | _::q -> to_local glob q
-    in
-    let locals = List.map (fun (local,global,x) -> local,x) l in
-      locals, (fun x -> to_local x l) , (fun x -> to_global x l)
-
   (** [build_sigma_maps] given a envs and some reif_params, we are
       able to build the sigmas *)
   let build_sigma_maps (rlt : Coq.Relation.t) zero ir : (sigmas * sigma_maps) Proofview.tactic =
@@ -996,11 +996,10 @@ module Trans = struct
         let env = Proofview.Goal.env goal in
         let sigma,rp = build_reif_params env sigma rlt zero in
         Unsafe.tclEVARS sigma
-        <*> let renumbered_sym, to_local, to_global = renumber ir.sym  in
-            let env_sym = Sigma.of_list
+        <*> let env_sym = Sigma.of_list
                             rp.sym_ty
                             (rp.sym_null)
-                            renumbered_sym
+                            ir.sym
             in 
             Coq.mk_letin "env_sym" env_sym >>= fun env_sym ->
             let bin = (List.map ( fun (n,s) -> n, Bin.mk_pack rlt s) ir.bin) in
@@ -1029,8 +1028,8 @@ module Trans = struct
             let f = List.map (fun (x,_) -> (x,Coq.Pos.of_int x)) in
             let sigma_maps =
               {
-	        sym_to_pos = (let sym = f renumbered_sym in fun x ->  (List.assoc (to_local x) sym));
-	        bin_to_pos = (let bin = f bin in fun x ->  (List.assoc  x bin));
+	        sym_to_pos = (let sym = f ir.sym in fun x ->  (List.assoc x sym));
+	        bin_to_pos = (let bin = f bin in fun x ->  (List.assoc x bin));
 	        units_to_pos = (let units = f units in fun x ->  (List.assoc  x units));
               }
             in

theories/AAC.v

@@ -281,14 +281,14 @@ Section s.
   (** 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
+      | sum i l, sum j vs => lex (Pos.compare i j) (mset_compare compare l vs)
+      | prd i l, prd j vs => lex (Pos.compare i j) (list_compare compare l vs)
+      | sym i l, sym j vs => lex (Pos.compare i j) (vcompare l vs)
+      | unit i , unit j => Pos.compare i j
       | unit _ , _        => Lt
-      | _      , unit _  => Gt
-      | sum _ _, _        => Lt
-      | _      , sum _ _  => Gt
+      | _      , unit _   => Gt
+      | sym _ _,  _       => Lt
+      | _      , sym _ _  => Gt
       | prd _ _, _        => Lt
       | _      , prd _ _  => Gt
 
@@ -335,14 +335,14 @@ Section s.
       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.
+      case_eq (Pos.compare i i0); intro Hi; try constructor.
       (* the [symmetry] is required *)
-      apply idx_compare_reflect_eq in Hi. symmetry in Hi. subst.       
+      apply pos_compare_reflect_eq in Hi. symmetry in Hi. subst.
       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.
+      case_eq (Pos.compare p p0); intro Hi; try constructor.
+      apply pos_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.
@@ -961,3 +961,15 @@ Section t.
 End t.
 
 Declare ML Module "aac_plugin:coq-aac-tactics.plugin".
+
+Lemma transitivity4 {A R} {H: @Equivalence A R} a b a' b': R a a' -> R b b' -> R a b -> R a' b'.
+Proof. now intros -> ->. Qed.
+Tactic Notation "aac_normalise" "in" hyp(H) :=
+  eapply transitivity4 in H; [| aac_normalise; reflexivity | aac_normalise; reflexivity].
+
+Ltac aac_normalise_all :=
+    aac_normalise;
+    repeat match goal with
+      | H: _ |- _ => aac_normalise in H
+      end.
+Tactic Notation "aac_normalise" "in" "*" := aac_normalise_all.

theories/Instances.v

@@ -34,13 +34,25 @@ Module Peano.
   #[export] Instance aac_Nat_max_Comm : Commutative eq Nat.max := Nat.max_comm.
   #[export] Instance aac_Nat_max_Assoc : Associative eq Nat.max := Nat.max_assoc.
   #[export] Instance aac_Nat_max_Idem : Idempotent eq Nat.max := Nat.max_idempotent.
-
+
+  #[export] Instance aac_Nat_gcd_Comm : Commutative eq Nat.gcd := Nat.gcd_comm.
+  #[export] Instance aac_Nat_gcd_Assoc : Associative eq Nat.gcd := Nat.gcd_assoc.
+  #[export] Instance aac_Nat_gcd_Idem : Idempotent eq Nat.gcd := Nat.gcd_diag.
+
+  #[export] Instance aac_Nat_lcm_Comm : Commutative eq Nat.lcm := Nat.lcm_comm.
+  #[export] Instance aac_Nat_lcm_Assoc : Associative eq Nat.lcm := Nat.lcm_assoc.
+  #[export] Instance aac_Nat_lcm_Idem : Idempotent eq Nat.lcm := Nat.lcm_diag.
+
   #[export] Instance aac_Nat_mul_1_Unit : Unit eq Nat.mul 1 :=
     Build_Unit eq Nat.mul 1 Nat.mul_1_l Nat.mul_1_r.
+  #[export] Instance aac_Nat_lcm_1_Unit : Unit eq Nat.lcm 1 :=
+    Build_Unit eq Nat.lcm 1 Nat.lcm_1_l Nat.lcm_1_r.
   #[export] Instance aac_Nat_add_0_Unit : Unit eq Nat.add 0 :=
     Build_Unit eq Nat.add (0) Nat.add_0_l Nat.add_0_r.
   #[export] Instance aac_Nat_max_0_Unit : Unit eq Nat.max 0 :=
     Build_Unit eq Nat.max 0 Nat.max_0_l Nat.max_0_r.
+  #[export] Instance aac_Nat_gcd_0_Unit : Unit eq Nat.gcd 0 :=
+    Build_Unit eq Nat.gcd 0 Nat.gcd_0_l Nat.gcd_0_r.
 
   (** We also provide liftings from  [Nat.le] to [eq] *)
   #[export] Instance Nat_le_PreOrder : PreOrder Nat.le :=
@@ -68,7 +80,13 @@ Module Z.
   #[export] Instance aac_Z_max_Comm : Commutative eq Z.max := Z.max_comm.
   #[export] Instance aac_Z_max_Assoc : Associative eq Z.max := Z.max_assoc.
   #[export] Instance aac_Z_max_Idem : Idempotent eq Z.max := Z.max_idempotent.
-
+
+  #[export] Instance aac_Z_gcd_Comm : Commutative eq Z.gcd := Z.gcd_comm.
+  #[export] Instance aac_Z_gcd_Assoc : Associative eq Z.gcd := Z.gcd_assoc.
+
+  #[export] Instance aac_Z_lcm_Comm : Commutative eq Z.lcm := Z.lcm_comm.
+  #[export] Instance aac_Z_lcm_Assoc : Associative eq Z.lcm := Z.lcm_assoc.
+
   #[export] Instance aac_Z_mul_1_Unit : Unit eq Z.mul 1 :=
     Build_Unit eq Z.mul 1 Z.mul_1_l Z.mul_1_r.
   #[export] Instance aac_Z_add_0_Unit : Unit eq Z.add 0 :=
@@ -123,13 +141,25 @@ Module N.
   #[export] Instance aac_N_max_Comm : Commutative eq N.max := N.max_comm.
   #[export] Instance aac_N_max_Assoc : Associative eq N.max := N.max_assoc.
   #[export] Instance aac_N_max_Idem : Idempotent eq N.max := N.max_idempotent.
+
+  #[export] Instance aac_N_gcd_Comm : Commutative eq N.gcd := N.gcd_comm.
+  #[export] Instance aac_N_gcd_Assoc : Associative eq N.gcd := N.gcd_assoc.
+  #[export] Instance aac_N_gcd_Idem : Idempotent eq N.gcd := N.gcd_diag.
+
+  #[export] Instance aac_N_lcm_Comm : Commutative eq N.lcm := N.lcm_comm.
+  #[export] Instance aac_N_lcm_Assoc : Associative eq N.lcm := N.lcm_assoc.
+  #[export] Instance aac_N_lcm_Idem : Idempotent eq N.lcm := N.lcm_diag.
 
   #[export] Instance aac_N_mul_1_Unit : Unit eq N.mul (1)%N :=
-    Build_Unit eq N.mul (1)%N N.mul_1_l N.mul_1_r.
+    Build_Unit eq N.mul 1 N.mul_1_l N.mul_1_r.
+  #[export] Instance aac_N_lcm_1_Unit : Unit eq N.lcm (1)%N :=
+    Build_Unit eq N.lcm 1 N.lcm_1_l N.lcm_1_r.
   #[export] Instance aac_N_add_0_Unit : Unit eq N.add (0)%N :=
-    Build_Unit eq N.add (0)%N N.add_0_l N.add_0_r.
+    Build_Unit eq N.add 0 N.add_0_l N.add_0_r.
   #[export] Instance aac_N_max_0_Unit : Unit eq N.max 0 :=
     Build_Unit eq N.max 0 N.max_0_l N.max_0_r.
+  #[export] Instance aac_N_gcd_0_Unit : Unit eq N.gcd 0 :=
+    Build_Unit eq N.gcd 0 N.gcd_0_l N.gcd_0_r.
 
   (* We also provide liftings from [N.le] to [eq] *)
   #[export] Instance N_le_PreOrder : PreOrder N.le :=

theories/Tutorial.v

@@ -356,19 +356,39 @@ End Peano.
 
 Section AAC_normalise.
   Import Instances.Z.
-  Import ZArith.
+  Import ZArith Lia.
   Open Scope Z_scope.
 
   Variable a b c d : Z.
   Goal a + (b + c*c*d) + a + 0 + d*1 = a.
     aac_normalise.
   Abort.
 
+  Goal b + 0 + a = c*1 -> a+b = c.
+    intro H.
+    aac_normalise in H.
+    assumption.
+  Qed.
+
+  Goal b + 0 + a = c*1+d -> a+b = d*(1+0)+c.
+    intro.
+    aac_normalise in *.
+    assumption.
+  Qed.
+
   Goal Z.max (a+b) (b+a) = a+b.
     aac_reflexivity.
-    Show Proof.
   Abort.
 
+  (** Example by Abhishek Anand extracted from verification of a C++ gcd function *)
+  Goal forall a b a' b' : Z,
+    0 < b' -> Z.gcd a' b' = Z.gcd a b -> Z.gcd b' (a' mod b') = Z.gcd a b.
+  Proof.
+    intros.
+    aac_rewrite Z.gcd_mod; try lia.
+    aac_normalise_all.
+    lia.
+  Qed.
 End AAC_normalise.
 
 (** ** Examples from previous website *)