From f2e58befb2e8df5dd1948e9b07191130b416bcca Mon Sep 17 00:00:00 2001 From: Damien Pous Date: Sat, 9 Oct 2021 16:47:38 +0200 Subject: [PATCH 1/2] adding support for (commutative) idempotent operations --- src/theory.ml | 37 ++++++++++++++++++++++++++++------ theories/AAC.v | 48 +++++++++++++++++++++++++++++++++++++++++--- theories/Instances.v | 32 +++++++++++++++++++++++++++-- theories/Tutorial.v | 17 ++++++++++++++++ theories/Utils.v | 3 +++ 5 files changed, 126 insertions(+), 11 deletions(-) diff --git a/src/theory.ml b/src/theory.ml index ada7fe4..7d64738 100644 --- a/src/theory.ml +++ b/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 diff --git a/theories/AAC.v b/theories/AAC.v index 622165b..62ca07a 100644 --- a/theories/AAC.v +++ b/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. diff --git a/theories/Instances.v b/theories/Instances.v index 4b08fcc..eeeece2 100644 --- a/theories/Instances.v +++ b/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,6 +313,8 @@ 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] @@ -296,6 +322,8 @@ Module Relations. #[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 *) diff --git a/theories/Tutorial.v b/theories/Tutorial.v index b3254e0..74342f8 100644 --- a/theories/Tutorial.v +++ b/theories/Tutorial.v @@ -243,6 +243,12 @@ Section Peano. Instance aac_max_Comm : Commutative eq Max.max := Max.max_comm. Instance aac_max_Assoc : Associative eq Max.max := Max.max_assoc. + (** Commutative operations may additionally be declared as idempotent + this does not change the behaviour of [aac_rewrite], but this enables more simplifications in + [aac_normalise] and [aac_reflexivity] + *) + Instance aac_max_Idem : Idempotent eq Max.max := Max.max_idempotent. + Instance aac_zero_max : Unit eq Max.max O := Build_Unit eq Max.max 0 Max.max_0_l Max.max_0_r. @@ -250,6 +256,11 @@ Section Peano. Goal Max.max (a + 0) 0 = a. aac_reflexivity. Qed. + + (* here we use idempotency *) + Goal Max.max (a + 0) a = a. + aac_reflexivity. + Qed. (** Furthermore, several operators can be mixed: *) @@ -337,6 +348,12 @@ Section AAC_normalise. aac_normalise. Abort. + Print HintDb typeclass_instances. + Goal Z.max (a+b) (b+a) = a+b. + aac_reflexivity. + Show Proof. + Abort. + End AAC_normalise. diff --git a/theories/Utils.v b/theories/Utils.v index fc34317..54452f1 100644 --- a/theories/Utils.v +++ b/theories/Utils.v @@ -230,6 +230,9 @@ Section lists. in merge_aux end. + (* setting all multiplicities to one, in order to implement idempotency *) + Definition reduce_mset: mset A -> mset A := nelist_map (fun x => (fst x,xH)). + (** interpretation of a list with a constant and a binary operation *) Variable B: Type. From ee5f49ba978266515f96fdf311cf8a91c4909bf8 Mon Sep 17 00:00:00 2001 From: Damien Pous Date: Sun, 10 Oct 2021 09:51:22 +0200 Subject: [PATCH 2/2] more doc on idempotent operations --- README.md | 10 ++++++++++ theories/Tutorial.v | 24 ++++++++++++++++++++++++ 2 files changed, 34 insertions(+) diff --git a/README.md b/README.md index ba536a4..66c9f21 100644 --- a/README.md +++ b/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. ``` diff --git a/theories/Tutorial.v b/theories/Tutorial.v index 74342f8..c893799 100644 --- a/theories/Tutorial.v +++ b/theories/Tutorial.v @@ -48,6 +48,30 @@ Section introduction. - here, ring would have done the job. *) + (** several associative/commutative operations can be used at the same time. + here, [Zmult] and [Zplus], which are both associative and commutative (AC) + *) + Goal (b + c) * (c + b) + a + Z.opp ((c + b) * (b + c)) = a. + aac_rewrite H. + aac_reflexivity. + Qed. + + (** some commutative operations can be declared as idempotent, here [Z.max] + which is taken into account by the [aac_normalise] and [aac_reflexivity] tactics. + Note however that [aac_rewrite] does not match modulo idempotency. + *) + Goal Z.max (b + c) (c + b) + a + Z.opp (c + b) = a. + aac_normalise. + aac_rewrite H. + aac_reflexivity. + Qed. + + Goal Z.max c (Z.max b c) + a + Z.opp (Z.max c b) = a. + aac_normalise. + aac_rewrite H. + aac_reflexivity. + Qed. + End introduction.