From 51f3dd8096102f420ca354e11e20cce8ea02aa46 Mon Sep 17 00:00:00 2001 From: Damien Pous Date: Fri, 31 May 2024 15:05:28 +0200 Subject: [PATCH 01/10] canonical ordering --- src/matcher.ml | 10 ++++++++++ src/matcher.mli | 2 ++ src/theory.ml | 49 ++++++++++++++++++++++++------------------------ theories/AAC.v | 22 +++++++++++----------- theories/Utils.v | 27 +++++++------------------- 5 files changed, 54 insertions(+), 56 deletions(-) diff --git a/src/matcher.ml b/src/matcher.ml index 787e02e..2e154f9 100644 --- a/src/matcher.ml +++ b/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 diff --git a/src/matcher.mli b/src/matcher.mli index a6b6f46..0894528 100644 --- a/src/matcher.mli +++ b/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) } diff --git a/src/theory.ml b/src/theory.ml index aaa9864..e4a7705 100644 --- a/src/theory.ml +++ b/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 diff --git a/theories/AAC.v b/theories/AAC.v index 7298663..35557c6 100644 --- a/theories/AAC.v +++ b/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. diff --git a/theories/Utils.v b/theories/Utils.v index 2ba81e2..d290a48 100644 --- a/theories/Utils.v +++ b/theories/Utils.v @@ -30,19 +30,6 @@ Fixpoint 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 @@ -64,16 +51,16 @@ Inductive compare_weak_spec A: A -> A -> comparison -> Prop := | 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). +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. + intros. case Pos.compare_spec; try constructor. + intros <-; constructor. Qed. -Lemma idx_compare_reflect_eq: forall i j, idx_compare i j = Eq -> i=j. +Lemma pos_compare_reflect_eq: forall i j, Pos.compare i j = Eq -> i=j. Proof. - intros i j. - case (pos_compare_weak_spec i j); intros; congruence. + intros ??. + case pos_compare_weak_spec; intros; congruence. Qed. (** ** Dependent types utilities *) @@ -161,7 +148,7 @@ Section lists. list_compare (fun un vm => let '(u,n) := un in let '(v,m) := vm in - lex (compare u v) (pos_compare n m)). + lex (compare u v) (Pos.compare n m)). Section list_compare_weak_spec. Variable A: Type. From 2c15c23893146ed62aea25555ad4ee1b26bddd73 Mon Sep 17 00:00:00 2001 From: Damien Pous Date: Fri, 31 May 2024 15:56:19 +0200 Subject: [PATCH 02/10] aac_normalise in H --- theories/AAC.v | 5 +++++ theories/Tutorial.v | 6 ++++++ 2 files changed, 11 insertions(+) diff --git a/theories/AAC.v b/theories/AAC.v index 35557c6..5c6235d 100644 --- a/theories/AAC.v +++ b/theories/AAC.v @@ -961,3 +961,8 @@ 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]. diff --git a/theories/Tutorial.v b/theories/Tutorial.v index 9eba645..b7a25cf 100644 --- a/theories/Tutorial.v +++ b/theories/Tutorial.v @@ -364,6 +364,12 @@ Section AAC_normalise. aac_normalise. Abort. + Goal b + 0 + a = c*1 -> a+b = c. + intro H. + aac_normalise in H. + assumption. + Qed. + Goal Z.max (a+b) (b+a) = a+b. aac_reflexivity. Show Proof. From bf4e295d8edea5f27c2a532faa760effbff989c2 Mon Sep 17 00:00:00 2001 From: Damien Pous Date: Fri, 31 May 2024 16:00:59 +0200 Subject: [PATCH 03/10] changelog --- CHANGELOG | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 CHANGELOG diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 index 0000000..9531bf8 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,6 @@ +* 31 May 2024: v8.19.1 + +- [aac_normalise in H] tactic +- make the order of sums produced by [aac_normalise] consistent across calls + +* were not tracked before From c6f396579c6ee60e2296737752085d4ce662b493 Mon Sep 17 00:00:00 2001 From: Damien Pous Date: Fri, 31 May 2024 16:46:48 +0200 Subject: [PATCH 04/10] gcd instances for Nat, N, Z --- CHANGELOG | 1 + theories/Instances.v | 19 +++++++++++++++++-- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 9531bf8..19330c6 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,5 +2,6 @@ - [aac_normalise in H] tactic - make the order of sums produced by [aac_normalise] consistent across calls +- gcd instances for Nat, N, Z * were not tracked before diff --git a/theories/Instances.v b/theories/Instances.v index 87b3c9c..3cb3161 100644 --- a/theories/Instances.v +++ b/theories/Instances.v @@ -34,13 +34,19 @@ 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_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_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 +74,10 @@ 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_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,6 +132,10 @@ 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_mul_1_Unit : Unit eq N.mul (1)%N := Build_Unit eq N.mul (1)%N N.mul_1_l N.mul_1_r. @@ -130,6 +143,8 @@ Module N. Build_Unit eq N.add (0)%N 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 := From 2c7f1cddd077b23cdaa3debfbad87894ed047b52 Mon Sep 17 00:00:00 2001 From: Damien Pous Date: Fri, 31 May 2024 17:03:48 +0200 Subject: [PATCH 05/10] lcm instances for Nat, N, Z --- CHANGELOG | 2 +- theories/Instances.v | 19 +++++++++++++++++-- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 19330c6..8148113 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,6 +2,6 @@ - [aac_normalise in H] tactic - make the order of sums produced by [aac_normalise] consistent across calls -- gcd instances for Nat, N, Z +- gcd/lcm instances for Nat, N, Z * were not tracked before diff --git a/theories/Instances.v b/theories/Instances.v index 3cb3161..b199351 100644 --- a/theories/Instances.v +++ b/theories/Instances.v @@ -39,8 +39,14 @@ Module Peano. #[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 := @@ -77,6 +83,9 @@ Module Z. #[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. @@ -137,10 +146,16 @@ Module N. #[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 := From 3276712998d87d87018f3495b24b54ee4e575727 Mon Sep 17 00:00:00 2001 From: Damien Pous Date: Fri, 31 May 2024 17:04:02 +0200 Subject: [PATCH 06/10] gitignore --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 52070c8..9064803 100644 --- a/.gitignore +++ b/.gitignore @@ -20,6 +20,7 @@ src/aac.ml .lia.cache +.nia.cache .merlin Makefile.coq Makefile.coq.conf From cbbba634e7d392cdc701c97e6f0f6166df95ae6a Mon Sep 17 00:00:00 2001 From: Damien Pous Date: Fri, 31 May 2024 17:09:07 +0200 Subject: [PATCH 07/10] aac_normalise in * --- theories/AAC.v | 7 +++++++ theories/Tutorial.v | 7 ++++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/theories/AAC.v b/theories/AAC.v index 5c6235d..febd1e5 100644 --- a/theories/AAC.v +++ b/theories/AAC.v @@ -966,3 +966,10 @@ Lemma transitivity4 {A R} {H: @Equivalence A R} a b a' b': R a a' -> R b b' -> R 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. diff --git a/theories/Tutorial.v b/theories/Tutorial.v index b7a25cf..7309d85 100644 --- a/theories/Tutorial.v +++ b/theories/Tutorial.v @@ -369,10 +369,15 @@ Section AAC_normalise. 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. End AAC_normalise. From 1b7a4109cc23842f1fcd4d14f34eab8f4f835c69 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 1 Jun 2024 13:22:33 +0200 Subject: [PATCH 08/10] add example by Abhishek Anand using aac_normalise_all tactic --- theories/Tutorial.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/theories/Tutorial.v b/theories/Tutorial.v index 7309d85..290ef65 100644 --- a/theories/Tutorial.v +++ b/theories/Tutorial.v @@ -356,7 +356,7 @@ End Peano. Section AAC_normalise. Import Instances.Z. - Import ZArith. + Import ZArith Lia. Open Scope Z_scope. Variable a b c d : Z. @@ -380,6 +380,15 @@ Section AAC_normalise. aac_reflexivity. 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 *) From 48ae1978c8c38c9a41832c257f8f0e6b3eb22333 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 1 Jun 2024 14:10:01 +0200 Subject: [PATCH 09/10] use more standard format CHANGELOG --- CHANGELOG | 7 ------- CHANGELOG.md | 20 ++++++++++++++++++++ 2 files changed, 20 insertions(+), 7 deletions(-) delete mode 100644 CHANGELOG create mode 100644 CHANGELOG.md diff --git a/CHANGELOG b/CHANGELOG deleted file mode 100644 index 8148113..0000000 --- a/CHANGELOG +++ /dev/null @@ -1,7 +0,0 @@ -* 31 May 2024: v8.19.1 - -- [aac_normalise in H] tactic -- make the order of sums produced by [aac_normalise] consistent across calls -- gcd/lcm instances for Nat, N, Z - -* were not tracked before diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..9e2bd80 --- /dev/null +++ b/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 From eae486780a4725559e63471f682c7138d226a005 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 1 Jun 2024 14:14:20 +0200 Subject: [PATCH 10/10] fix deployment boilerplate --- .github/workflows/deploy-docs.yml | 59 ------------------------------- 1 file changed, 59 deletions(-) delete mode 100644 .github/workflows/deploy-docs.yml diff --git a/.github/workflows/deploy-docs.yml b/.github/workflows/deploy-docs.yml deleted file mode 100644 index c5243c3..0000000 --- a/.github/workflows/deploy-docs.yml +++ /dev/null @@ -1,59 +0,0 @@ -name: Build and Deploy documentation - -on: - push: - branches: - - master - pull_request: - branches: - - '**' - -jobs: - build-coqdoc: - runs-on: ubuntu-latest - steps: - - name: Set up Git repository - uses: actions/checkout@v2 - - - name: Build coqdoc - uses: coq-community/docker-coq-action@v1 - with: - custom_image: 'coqorg/coq:dev' - custom_script: | - {{before_install}} - startGroup "Build aac-tactics dependencies" - opam pin add -n -y -k path coq-aac-tactics . - opam update -y - opam install -y -j "$(nproc)" coq-aac-tactics --deps-only - endGroup - startGroup "Add permissions" - sudo chown -R coq:coq . - endGroup - startGroup "Build aac-tactics" - make -j "$(nproc)" - endGroup - startGroup "Build coqdoc" - make coqdoc - endGroup - startGroup "Build ocamldoc" - make ocamldoc - endGroup - - - name: Revert Coq user permissions - # to avoid a warning at cleanup time - if: ${{ always() }} - run: sudo chown -R 1001:116 . - - - name: Copy HTML and CSS and JavaScript - run: | - mkdir public - cp -r resources/index.html docs/ public/ - - - name: Deploy to GitHub pages - if: github.event_name == 'push' && github.ref == 'refs/heads/master' - uses: crazy-max/ghaction-github-pages@v2 - with: - build_dir: public - jekyll: false - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}