From 03d6a8934e305e979d3f931ea27baf2600e722dc Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 3 Jan 2024 01:29:35 +0100 Subject: [PATCH 1/3] Automatic weakening of constants --- elpi/param-class.elpi | 52 ++++++++++++++++++++++++++++++++++++---- elpi/util.elpi | 11 +++++++++ examples/Vector_tuple.v | 16 +++---------- examples/int_to_Zp.v | 17 ++----------- examples/peano_bin_nat.v | 8 +------ theories/Database.v | 1 + theories/Hierarchy.v | 2 ++ theories/Param.v | 6 ++--- theories/Param_Type.v | 4 ++++ theories/Param_arrow.v | 2 ++ theories/Param_forall.v | 2 ++ theories/Param_option.v | 6 ++--- theories/Vernac.v | 19 +++++++++++++-- 13 files changed, 99 insertions(+), 47 deletions(-) diff --git a/elpi/param-class.elpi b/elpi/param-class.elpi index 17968a9..9c6f13c 100644 --- a/elpi/param-class.elpi +++ b/elpi/param-class.elpi @@ -102,6 +102,15 @@ weakenings-to map2b [map3]. weakenings-to map3 [map4]. weakenings-to map4 []. +% lower/higher levels at distance 1 from a given level +pred all-weakenings-from i:map-class, o:list map-class. +all-weakenings-from map0 []. +all-weakenings-from map1 [map0]. +all-weakenings-from map2a [map1, map0]. +all-weakenings-from map2b [map1, map0]. +all-weakenings-from map3 [map2a, map2b, map1, map0]. +all-weakenings-from map4 [map3, map2a, map2b, map1, map0]. + % all possible parametricity classes that can be created by combinations of 2 lists of map classes pred product i:list map-class, i:list map-class, o:list param-class. product Ms Ns Classes :- @@ -176,10 +185,6 @@ dep-arrow map4 (pc map0 map4) (pc map4 map0). } % map-class -pred do-not-fail. -:before "term->gref:fail" -coq.term->gref _ _ :- do-not-fail, !, false. - namespace param-class { % extensions of functions over map classes to parametricity classes @@ -196,6 +201,15 @@ weakenings-to (pc M N) Classes :- map-class.weakenings-to N Ns, map-class.product Ms Ns Classes. +pred all-weakenings-from i:param-class, o:list param-class. +all-weakenings-from (pc M N) Classes :- + map-class.all-weakenings-from M Ms, + map-class.all-weakenings-from N Ns, + map-class.product Ms Ns StrictClasses, + map-class.product [M] Ns MClasses, + map-class.product Ms [N] NClasses, + std.flatten [StrictClasses, MClasses, NClasses] Classes. + pred negate i:param-class, o:param-class. negate (pc M N) (pc N M). @@ -229,6 +243,13 @@ dep-arrow (pc M N) ClassA ClassB :- union ClassAM {param-class.negate ClassAN} ClassA, union ClassBM {param-class.negate ClassBN} ClassB. +pred to-string i:param-class, o:string. +to-string (pc M N) String :- std.do! [ + map-class->string M MStr, + map-class->string N NStr, + String is MStr ^ NStr +]. + % generate a weakening function from a parametricity class to another, by forgetting fields 1 by 1 pred forget i:param-class, i:param-class, o:univ-instance -> term -> term -> term -> term. forget (pc M N) (pc M N) (_\ _\ _\ r\ r) :- !. @@ -247,6 +268,29 @@ forget (pc M N) (pc M' N') ForgetF :- {calc ("forget_" ^ {map-class->string M} ^ NStr ^ "_" ^ {map-class->string M1} ^ NStr)} Forget1, ForgetF = (ui\ a\ b\ r\ ForgetF' ui a b (app [pglobal Forget1 ui, a, b, r])). +% weaking of the out class of a gref. +% e.g. if GR has type `forall A B, R A B -> Param21 X Y` +% then `weaken-out (pc map1 map0) GR T` +% where `T` has type `forall A B, R A B -> Param10 X Y` +pred weaken-out i:param-class, i:gref, o:term. +weaken-out OutC GR WT :- std.do! [ + coq.env.global GR T, + coq.env.typeof GR Ty, + replace-out-ty OutC Ty WTy, + std.assert-ok! (coq.elaborate-skeleton T WTy WT) + "weaken-out: failed to weaken" +]. + +pred replace-out-ty i:param-class, i:term, o:term. +replace-out-ty OutC (prod N A B) (prod N A B') :- !, + pi x\ replace-out-ty OutC (B x) (B' x). +replace-out-ty OutC InT OutT :- std.do! [ + coq.safe-dest-app InT HD Ts, + trocq.db.gref->class OutGRClass OutC, + util.subst-gref HD OutGRClass HD', + coq.mk-app HD' Ts OutT + ]. + % succeed if the parametricity class contains a map class over 2b % this means that a translation of a sort at this class will require univalence, % and the translation of a dependent product will require funext diff --git a/elpi/util.elpi b/elpi/util.elpi index 45e664e..eb48043 100644 --- a/elpi/util.elpi +++ b/elpi/util.elpi @@ -14,6 +14,10 @@ % utility predicates % ----------------------------------------------------------------------------- +pred do-not-fail. +:before "term->gref:fail" +coq.term->gref _ _ :- do-not-fail, !, false. + kind or type -> type -> type. type inl A -> or A B. type inr B -> or A B. @@ -79,4 +83,11 @@ delete A [A|Xs] Xs :- !. delete A [X|Xs] [X|Xs'] :- delete A Xs Xs'. delete _ [] []. +% subst-gref T GR' T' +% substitutes GR for GR' in T if T = (global GR) or (pglobal GR I) +pred subst-gref i:term, i:gref, o:term. +subst-gref (global _) GR' (global GR'). +subst-gref (pglobal _ I) GR' (pglobal GR' I). +subst-gref T _ _ :- coq.error T "is not a gref". + } % util diff --git a/examples/Vector_tuple.v b/examples/Vector_tuple.v index 20fed4a..60e43b2 100644 --- a/examples/Vector_tuple.v +++ b/examples/Vector_tuple.v @@ -209,7 +209,6 @@ Defined. Module AppendConst. -Trocq Use Param00_nat. Trocq Use Param2a0_nat. Trocq Use Param_add. Trocq Use Param02b_tuple_vector. @@ -240,19 +239,14 @@ Axiom Param_head : forall Module HeadConst. Axiom (int : Type) (Zp : Type) (Rp42b : Param42b.Rel Zp int). -Definition Rp00 : Param00.Rel Zp int := Rp42b. -Definition Rp2a0 : Param2a0.Rel Zp int := Rp42b. -Definition Rp02b : Param02b.Rel Zp int := Rp42b. +Definition Rp2a2b : Param2a2b.Rel Zp int := Rp42b. Lemma head_const {n : nat} : forall (i : int), Vector.hd (Vector.const i (S n)) = i. Proof. destruct n; simpl; reflexivity. Qed. -Trocq Use Param00_nat. Trocq Use Param2a0_nat. Trocq Use SR. -Trocq Use Rp00. -Trocq Use Rp2a0. -Trocq Use Rp02b. +Trocq Use Rp2a2b. Trocq Use Param_head. Trocq Use Param_const. Trocq Use Param01_paths. @@ -464,13 +458,9 @@ Axiom setBitThenGetSame : forall {k : nat} (bv : bitvector k) (i : nat) (b : Bool), (i < k)%nat -> getBit_bv (setBit_bv bv i b) i = b. -Definition Param2a0_Bool : Param2a0.Rel Bool Bool := Param44_Bool. -Definition Param02b_Bool : Param02b.Rel Bool Bool := Param44_Bool. -Trocq Use Param00_nat. Trocq Use Param2a0_nat. -Trocq Use Param2a0_Bool. -Trocq Use Param02b_Bool. +Trocq Use Param44_Bool. Trocq Use Param2a0_bnat_bv. Trocq Use getBitR. Trocq Use setBitR. diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index 71964eb..f8538c4 100644 --- a/examples/int_to_Zp.v +++ b/examples/int_to_Zp.v @@ -76,12 +76,7 @@ Axiom Rzero : Rp zerop zero. Variable Radd : binop_param Rp Rp Rp addp add. Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. -Trocq Use Rp00. -Trocq Use Rp01. -Trocq Use Rp10. -Trocq Use Rp02b. -Trocq Use Rp2a0. - +Trocq Use Rp2a2b. Trocq Use Param01_paths. Trocq Use Param10_paths. Trocq Use Radd. @@ -109,13 +104,6 @@ Module IntToZmodp. Definition Rp n x := modp n = x. Definition Rp42a@{i} : Param42a.Rel int@{i} Zmodp@{i} := SplitSurj.toParam (SplitSurj.Build_type modp reprp reprpK). -Definition Rp00 : Param00.Rel int Zmodp := Rp42a. -Definition Rp01 : Param01.Rel int Zmodp := Rp42a. -Definition Rp40 : Param40.Rel int Zmodp := Rp42a. -Definition Rp10 : Param10.Rel int Zmodp := Rp42a. -Definition Rp02a : Param02a.Rel int Zmodp := Rp42a. -Definition Rp2a0 : Param2a0.Rel int Zmodp := Rp42a. -Definition Rp2b0 : Param2b0.Rel int Zmodp := Rp42a. Axiom Rzero' : Rp zero zerop. Variable Radd' : binop_param Rp Rp Rp add addp. @@ -124,8 +112,7 @@ Variable Rmul' : binop_param Rp Rp Rp mul mulp. Trocq Use Rmul'. Trocq Use Rzero'. Trocq Use Param10_paths. -Trocq Use Rp2a0. -Trocq Use Rp2b0. +Trocq Use Rp42a. Definition eq_Zmodp (x y : Zmodp) := (x = y). (* Bug if we inline the previous def in the following axiom *) diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v index b421095..9cfb091 100644 --- a/examples/peano_bin_nat.v +++ b/examples/peano_bin_nat.v @@ -141,10 +141,6 @@ Definition RN2a3 : Param2a3.Rel@{Set} N nat := SplitSurj.toParamSym@{Set} {| that do not need this field, so that it is not imported before forgetting, and the lower instances can be declared without the axiom *) -Definition RN02b : Param02b.Rel N nat := RN2a3. -Definition RN02a : Param02a.Rel N nat := RN2a3. -Definition RN2a0 : Param2a0.Rel N nat := RN2a3. - (* as 0 and Nsucc appear in the goal, we need to link them with nat constructors *) (* NB: as these are not type formers, only class (0,0) is required, so these proofs amount to what would be done in the context of raw parametricity *) @@ -153,9 +149,7 @@ Definition RN0 : RN N0 0. Proof. done. Qed. Definition RNS : forall m n, RN m n -> RN (Nsucc m) (S n). Proof. by move=> _ + <-; case=> //=. Qed. -Trocq Use RN02b. -Trocq Use RN02a. -Trocq Use RN2a0. +Trocq Use RN2a3. Trocq Use RN0. Trocq Use RNS. diff --git a/theories/Database.v b/theories/Database.v index 038e3a7..1840c5d 100644 --- a/theories/Database.v +++ b/theories/Database.v @@ -64,5 +64,6 @@ Elpi Db trocq.db lp:{{ pred trocq.db.gref o:gref, o:param-class, o:list param-class, o:gref, o:gref. :name "default-gref" + trocq.db.gref _ _ _ _ _ :- do-not-fail, !, false. trocq.db.gref GR Out _ _ _ :- coq.error "cannot find" GR "at out class" Out. }}. diff --git a/theories/Hierarchy.v b/theories/Hierarchy.v index fde29ec..efdf1fb 100644 --- a/theories/Hierarchy.v +++ b/theories/Hierarchy.v @@ -17,6 +17,7 @@ Require Import HoTT_additions Database. From elpi Require Import elpi. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. +From Trocq.Elpi Extra Dependency "util.elpi" as util. Set Universe Polymorphism. Unset Universe Minimization ToSet. @@ -75,6 +76,7 @@ End Map4. (********************) Elpi Command genhierarchy. +Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. Elpi Accumulate lp:{{ diff --git a/theories/Param.v b/theories/Param.v index 68fa77d..8a4ca07 100644 --- a/theories/Param.v +++ b/theories/Param.v @@ -35,8 +35,8 @@ Inductive map_class : Set := map0 | map1 | map2a | map2b | map3 | map4. Elpi Command genpparam. Elpi Accumulate File util. -Elpi Accumulate File param_class. Elpi Accumulate Db trocq.db. +Elpi Accumulate File param_class. Definition PType@{i} (m n : map_class) (* : Type@{i+1} *) := Type@{i}. Definition weaken@{i} (m n m' n' : map_class) {A : Type@{i}} (a : A) : A := a. @@ -55,8 +55,8 @@ Elpi Query lp:{{ Elpi Command genpparamtype. Elpi Accumulate File util. -Elpi Accumulate File param_class. Elpi Accumulate Db trocq.db. +Elpi Accumulate File param_class. Elpi Accumulate lp:{{ pred generate-branch i:univ-instance, i:param-class, i:param-class, o:term. generate-branch UI2 Class RClass (pglobal ParamType UI2) :- @@ -141,9 +141,9 @@ Elpi Query lp:{{ }}. Elpi Tactic trocq. +Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File annot. -Elpi Accumulate File util. Elpi Accumulate File param_class. Elpi Accumulate File simple_graph. Elpi Accumulate File constraint_graph. diff --git a/theories/Param_Type.v b/theories/Param_Type.v index bcc091c..fbec6c4 100644 --- a/theories/Param_Type.v +++ b/theories/Param_Type.v @@ -15,6 +15,7 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Database. +From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. Set Universe Polymorphism. @@ -28,6 +29,8 @@ Local Open Scope param_scope. + symmetry MapM_Type_symNP *) Elpi Command genmaptype. +Elpi Accumulate File util. +Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. Elpi Accumulate lp:{{ pred generate-fields @@ -166,6 +169,7 @@ Defined. (for M or N in [2b, 3, 4] PQ is always 44) *) Elpi Command genparamtype. +Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. Elpi Accumulate lp:{{ diff --git a/theories/Param_arrow.v b/theories/Param_arrow.v index eff3688..d5bb3b9 100644 --- a/theories/Param_arrow.v +++ b/theories/Param_arrow.v @@ -15,6 +15,7 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Database. +From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. Set Universe Polymorphism. @@ -23,6 +24,7 @@ Unset Universe Minimization ToSet. Local Open Scope param_scope. Elpi Command genparamarrow. +Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. diff --git a/theories/Param_forall.v b/theories/Param_forall.v index 3b4f660..1178286 100644 --- a/theories/Param_forall.v +++ b/theories/Param_forall.v @@ -15,6 +15,7 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Database. +From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. Set Universe Polymorphism. @@ -23,6 +24,7 @@ Unset Universe Minimization ToSet. Local Open Scope param_scope. Elpi Command genparamforall. +Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. diff --git a/theories/Param_option.v b/theories/Param_option.v index 190114d..d63ed4d 100644 --- a/theories/Param_option.v +++ b/theories/Param_option.v @@ -83,18 +83,18 @@ Definition option_map_in_R : | Some a' => fun e => someR A A' AR a a' (map_in_R AR a a' (some_inj1 A' (map AR a) a' e)) - | none => + | None => fun e => exfalso_option_some_none (optionR A A' AR (Some a) (None)) A' (map AR a) e end - | none => + | None => match oa' with | Some a' => fun e => exfalso_option_none_some (optionR A A' AR (None) (Some a')) A' a' e - | none => fun e => noneR A A' AR + | None => fun e => noneR A A' AR end end. diff --git a/theories/Vernac.v b/theories/Vernac.v index e2e2f90..f2c19dd 100644 --- a/theories/Vernac.v +++ b/theories/Vernac.v @@ -27,8 +27,8 @@ From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. Elpi Command Trocq. -Elpi Accumulate Db trocq.db. Elpi Accumulate File util. +Elpi Accumulate Db trocq.db. Elpi Accumulate File annot. Elpi Accumulate File param_class. Elpi Accumulate File simple_graph. @@ -86,7 +86,22 @@ Elpi Accumulate lp:{{ coq.say "accumultating" GR "@" Class "(" CList ") ~" GR' ":." GRR, coq.elpi.accumulate _ "trocq.db" (clause _ (before "default-gref") - (trocq.db.gref GR Class CList GR' GRR)) + (trocq.db.gref GR Class CList GR' GRR)), + std.forall {param-class.all-weakenings-from Class} subclass\ + sigma WTRR BaseName Suffix WName WCRR \ + if (do-not-fail => trocq.db.gref GR subclass _ _ _) true (std.do! [ + param-class.weaken-out subclass GRR WTRR, + coq.gref->id GRR BaseName, + param-class.to-string subclass Suffix, + WName is BaseName ^ "_weakened_to_" ^ Suffix, + @udecl! [] tt [] tt => + coq.env.add-const WName WTRR _ @transparent! WCRR, + coq.elpi.accumulate _ "trocq.db" + (clause _ (before "default-gref") + (trocq.db.gref GR subclass CList GR' (const WCRR))), + coq.say "accumultating" GR "@" subclass "(" CList ") ~" GR' + ":." (const WCRR), + ]) ]. % coq.elpi.accumulate _ "trocq.db" % (clause _ (before "default-gref") From 9d9748e295a242b9a6268779808327445b500040 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 3 Jan 2024 01:41:04 +0100 Subject: [PATCH 2/3] code simplifications --- examples/int_to_Zp.v | 79 ++++++++++++++++++---------------------- examples/peano_bin_nat.v | 8 ++-- 2 files changed, 39 insertions(+), 48 deletions(-) diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index f8538c4..3c30d1a 100644 --- a/examples/int_to_Zp.v +++ b/examples/int_to_Zp.v @@ -50,6 +50,42 @@ Notation "x + y" := (addp x%Zmodp y%Zmodp) : Zmodp_scope. Notation "x * y" := (mul x%int y%int) : int_scope. Notation "x * y" := (mulp x%Zmodp y%Zmodp) : Zmodp_scope. +Module IntToZmodp. + +Definition Rp := SplitSurj.toParam + (SplitSurj.Build_type modp reprp reprpK). + +Axiom Rzero' : Rp zero zerop. +Variable Radd' : binop_param Rp Rp Rp add addp. +Variable Rmul' : binop_param Rp Rp Rp mul mulp. + +Trocq Use Rmul'. +Trocq Use Rzero'. +Trocq Use Param10_paths. +Trocq Use Rp. + +Definition eq_Zmodp (x y : Zmodp) := (x = y). +(* Bug if we inline the previous def in the following axiom *) +Axiom Reqmodp01 : forall (m : int) (x : Zmodp), Rp m x -> + forall n y, Rp n y -> Param01.Rel (eqmodp m n) (eq_Zmodp x y). +Trocq Use Reqmodp01. +Arguments eq_Zmodp /. + +Hypothesis RedZmodpEq0 : + (forall (m n p : Zmodp), (m = n * n)%Zmodp -> m = (p * p * p)%Zmodp -> + m = zerop). + +Lemma IntRedModZp : forall (m n p : int), + (m = n * n)%int -> m = (p * p * p)%int -> eqmodp m zero. +Proof. +trocq; simpl. +exact @RedZmodpEq0. +Qed. + +(* Print Assumptions IntRedModZp. (* No Univalence *) *) + +End IntToZmodp. + Module ZmodpToInt. Definition Rp x n := eqmodp (reprp x) n. @@ -66,12 +102,6 @@ unshelve econstructor. + by move=> a b; rewrite /Rp/sym_rel/eqmodp reprpK => <-. Defined. -Definition Rp00 : Param00.Rel Zmodp int := Rp2a2b. -Definition Rp01 : Param01.Rel Zmodp int := Rp2a2b. -Definition Rp10 : Param10.Rel Zmodp int := Rp2a2b. -Definition Rp02b : Param02b.Rel Zmodp int := Rp2a2b. -Definition Rp2a0 : Param2a0.Rel Zmodp int := Rp2a2b. - Axiom Rzero : Rp zerop zero. Variable Radd : binop_param Rp Rp Rp addp add. Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. @@ -98,40 +128,3 @@ Proof. Qed. End ZmodpToInt. - -Module IntToZmodp. - -Definition Rp n x := modp n = x. -Definition Rp42a@{i} : Param42a.Rel int@{i} Zmodp@{i} := - SplitSurj.toParam (SplitSurj.Build_type modp reprp reprpK). - -Axiom Rzero' : Rp zero zerop. -Variable Radd' : binop_param Rp Rp Rp add addp. -Variable Rmul' : binop_param Rp Rp Rp mul mulp. - -Trocq Use Rmul'. -Trocq Use Rzero'. -Trocq Use Param10_paths. -Trocq Use Rp42a. - -Definition eq_Zmodp (x y : Zmodp) := (x = y). -(* Bug if we inline the previous def in the following axiom *) -Axiom Reqmodp01 : forall (m : int) (x : Zmodp), Rp m x -> - forall n y, Rp n y -> Param01.Rel (eqmodp m n) (eq_Zmodp x y). -Trocq Use Reqmodp01. -Arguments eq_Zmodp /. - -Hypothesis RedZmodpEq0 : - (forall (m n p : Zmodp), (m = n * n)%Zmodp -> m = (p * p * p)%Zmodp -> - m = zerop). - -Lemma IntRedModZp : forall (m n p : int), - (m = n * n)%int -> m = (p * p * p)%int -> eqmodp m zero. -Proof. -trocq; simpl. -exact @RedZmodpEq0. -Qed. - -(* Print Assumptions IntRedModZp. (* No Univalence *) *) - -End IntToZmodp. diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v index 9cfb091..947060e 100644 --- a/examples/peano_bin_nat.v +++ b/examples/peano_bin_nat.v @@ -107,8 +107,6 @@ Definition Nmap (n : N) : nat := Fixpoint Ncomap (n : nat) : N := match n with O => 0 | S n => Nsucc (Ncomap n) end. -Definition RN@{} := sym_rel@{Set} (graph@{Set} Ncomap). - Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0. Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Qed. @@ -129,7 +127,7 @@ Proof. by case: n => //= ; elim=> //= p /NcomapNpos/= ->. Qed. (* the best we can do to link these types is (4,4), but we only need (2a,3) which is morally that Nmap is a split injection *) -Definition RN2a3 : Param2a3.Rel@{Set} N nat := SplitSurj.toParamSym@{Set} {| +Definition RN := SplitSurj.toParamSym@{Set} {| SplitSurj.retract := Ncomap; SplitSurj.section := Nmap; SplitSurj.sectionK := NmapK |}. @@ -145,11 +143,11 @@ Definition RN2a3 : Param2a3.Rel@{Set} N nat := SplitSurj.toParamSym@{Set} {| (* NB: as these are not type formers, only class (0,0) is required, so these proofs amount to what would be done in the context of raw parametricity *) -Definition RN0 : RN N0 0. Proof. done. Qed. +Definition RN0 : RN N0 0%nat. Proof. done. Qed. Definition RNS : forall m n, RN m n -> RN (Nsucc m) (S n). Proof. by move=> _ + <-; case=> //=. Qed. -Trocq Use RN2a3. +Trocq Use RN. Trocq Use RN0. Trocq Use RNS. From 0744669f3721f81e09cbba728d40d3d0e3d3ddcb Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 3 Jan 2024 02:18:04 +0100 Subject: [PATCH 3/3] code refactoring: isolating example of artifact paper --- _CoqProject | 5 +- examples/N.v | 134 ++++++++++++++++++++++++++++++ examples/artifact_paper_example.v | 46 ++++++++++ examples/int_to_Zp.v | 19 +---- examples/{Example.v => misc.v} | 0 examples/peano_bin_nat.v | 109 +----------------------- theories/Common.v | 9 +- 7 files changed, 194 insertions(+), 128 deletions(-) create mode 100644 examples/N.v create mode 100644 examples/artifact_paper_example.v rename examples/{Example.v => misc.v} (100%) diff --git a/_CoqProject b/_CoqProject index 616b59e..12de94b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -3,6 +3,7 @@ -R theories/ Trocq -R elpi/ Trocq.Elpi +-R examples/ Trocq_examples theories/HoTT_additions.v theories/Hierarchy.v @@ -23,10 +24,12 @@ theories/Param_prod.v theories/Param_option.v theories/Param_vector.v -examples/Example.v +examples/artifact_paper_example.v +examples/N.v examples/int_to_Zp.v examples/peano_bin_nat.v examples/setoid_rewrite.v examples/summable.v examples/trocq_setoid_rewrite.v examples/Vector_tuple.v +examples/misc.v diff --git a/examples/N.v b/examples/N.v new file mode 100644 index 0000000..52cde81 --- /dev/null +++ b/examples/N.v @@ -0,0 +1,134 @@ +(*****************************************************************************) +(* * Trocq *) +(* _______ * Copyright (C) 2023 Inria & MERCE *) +(* |__ __| * (Mitsubishi Electric R&D Centre Europe) *) +(* | |_ __ ___ ___ __ _ * Cyril Cohen *) +(* | | '__/ _ \ / __/ _` | * Enzo Crance *) +(* | | | | (_) | (_| (_| | * Assia Mahboubi *) +(* |_|_| \___/ \___\__, | ************************************************) +(* | | * This file is distributed under the terms of *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * see LICENSE file for the text of the license *) +(*****************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +From Trocq Require Import Common. + +Set Universe Polymorphism. + +(* definition of binary natural numbers *) + +Inductive positive : Set := + | xI : positive -> positive + | xO : positive -> positive + | xH : positive. + +Declare Scope positive_scope. +Delimit Scope positive_scope with positive. +Bind Scope positive_scope with positive. + +Notation "1" := xH : positive_scope. +Notation "p ~ 1" := (xI p) + (at level 7, left associativity, format "p '~' '1'") : positive_scope. +Notation "p ~ 0" := (xO p) + (at level 7, left associativity, format "p '~' '0'") : positive_scope. + +Module Pos. +Local Open Scope positive_scope. +Fixpoint succ x := + match x with + | p~1 => (succ p)~0 + | p~0 => p~1 + | 1 => 1~0 + end. + +Fixpoint map (x : positive) : nat := + match x with + | p~1 => 1 + (map p + map p) + | p~0 => map p + map p + | 1 => 1 + end. + +Fixpoint add (x y : positive) : positive := + match x, y with + | 1, p | p, 1 => succ p + | p~0, q~0 => (add p q)~0 + | p~0, q~1 | p~1, q~0 => (add p q)~1 + | p~1, q~1 => succ (add p q)~1 + end. +Infix "+" := add : positive_scope. +Notation "p .+1" := (succ p) : positive_scope. + +Lemma addpp x : x + x = x~0. Proof. by elim: x => //= ? ->. Defined. +Lemma addp1 x : x + 1 = x.+1. Proof. by elim: x. Defined. +Lemma addpS x y : x + y.+1 = (x + y).+1. +Proof. by elim: x y => // p IHp [q|q|]//=; rewrite ?IHp ?addp1//. Defined. +Lemma addSp x y : x.+1 + y = (x + y).+1. +Proof. by elim: x y => [p IHp|p IHp|]// [q|q|]//=; rewrite ?IHp//. Defined. + +End Pos. +Infix "+" := Pos.add : positive_scope. +Notation "p .+1" := (Pos.succ p) : positive_scope. + +Inductive N : Set := + | N0 : N + | Npos : positive -> N. + +Declare Scope N_scope. +Delimit Scope N_scope with N. +Bind Scope N_scope with N. + +Notation "0" := N0 : N_scope. + +Definition succ_pos (n : N) : positive := + match n with + | N0 => 1%positive + | Npos p => Pos.succ p + end. + +Definition Nsucc (n : N) := Npos (succ_pos n). + +Definition Nadd (m n : N) := match m, n with +| N0, x | x, N0 => x +| Npos p, Npos q => Npos (Pos.add p q) +end. +Infix "+" := Nadd : N_scope. +Notation "n .+1" := (Nsucc n) : N_scope. + +(* various possible proofs to fill the fields of a parametricity witness between N and nat *) + +Definition Nmap (n : N) : nat := + match n with + | N0 => 0 + | Npos p => Pos.map p + end. + +Fixpoint Ncomap (n : nat) : N := + match n with O => 0 | S n => Nsucc (Ncomap n) end. + +Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0. +Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Defined. + +Lemma NcomapD i j : Ncomap (i + j) = (Ncomap i + Ncomap j)%N. +Proof. +elim: i j => [|i IHi] [|j]//=; first by rewrite -nat_add_n_O//. +rewrite -nat_add_n_Sm/= IHi. +case: (Ncomap i) => // p; case: (Ncomap j) => //=. +- by rewrite /Nsucc/= Pos.addp1. +- by move=> q; rewrite /Nsucc/= Pos.addpS Pos.addSp. +Defined. + +Let NcomapNpos p k : Ncomap k = Npos p -> Ncomap (k + k) = Npos p~0. +Proof. by move=> kp; rewrite NcomapD kp Naddpp. Defined. + +Lemma NmapK (n : N) : Ncomap (Nmap n) = n. +Proof. by case: n => //= ; elim=> //= p /NcomapNpos/= ->. Defined. + +Lemma NcomapK (n : nat) : Nmap (Ncomap n) = n. +Proof. +elim: n => //= n IHn; rewrite -[in X in _ = X]IHn. +by case: (Ncomap n)=> //; elim=> //= p ->; rewrite /= !add_n_Sm. +Defined. + +Definition Niso := Iso.Build NcomapK NmapK. \ No newline at end of file diff --git a/examples/artifact_paper_example.v b/examples/artifact_paper_example.v new file mode 100644 index 0000000..13f860a --- /dev/null +++ b/examples/artifact_paper_example.v @@ -0,0 +1,46 @@ +(*****************************************************************************) +(* * Trocq *) +(* _______ * Copyright (C) 2023 Inria & MERCE *) +(* |__ __| * (Mitsubishi Electric R&D Centre Europe) *) +(* | |_ __ ___ ___ __ _ * Cyril Cohen *) +(* | | '__/ _ \ / __/ _` | * Enzo Crance *) +(* | | | | (_) | (_| (_| | * Assia Mahboubi *) +(* |_|_| \___/ \___\__, | ************************************************) +(* | | * This file is distributed under the terms of *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * see LICENSE file for the text of the license *) +(*****************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +From Trocq Require Import Trocq. +From Trocq_examples Require Import N. + +Set Universe Polymorphism. + +(* Let us first prove that type nat , of unary natural numbers, and type N , of +binary ones, are equivalent *) +Definition RN44 : (N <=> nat)%P := Iso.toParamSym Niso. + +(* This equivalence proof coerces to a relation of type N -> nat -> Type , which +relates the respective zero and successor constants of these types: *) +Definition RN0 : RN44 0%N 0%nat. Proof. done. Defined. +Definition RNS m n : RN44 m n -> RN44 (Nsucc m) (S n). +Proof. by move: m n => _ + <-; case=> //=. Defined. + +(* We now register all these informations in a database known to the tactic: *) +Trocq Use RN0. Trocq Use RNS. +Trocq Use RN44. + +(* We can now make use of the tactic to prove a recurrence principle on N *) +Lemma N_Srec : forall (P : N -> Type), P N0 -> + (forall n, P n -> P (Nsucc n)) -> forall n, P n. +Proof. trocq. (* N replaces nat in the goal *) exact nat_rect. Defined. + +(* Inspecting the proof term atually reveals that univalence was not needed +in the proof of N_Srec. *) +Print N_Srec. +Print Assumptions N_Srec. + +(* Indeed this computes *) +Eval compute in N_Srec (fun n => N) (0%N) Nadd (Npos 1~0~1~1~1~0). diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index 3c30d1a..6b74cf7 100644 --- a/examples/int_to_Zp.v +++ b/examples/int_to_Zp.v @@ -52,8 +52,7 @@ Notation "x * y" := (mulp x%Zmodp y%Zmodp) : Zmodp_scope. Module IntToZmodp. -Definition Rp := SplitSurj.toParam - (SplitSurj.Build_type modp reprp reprpK). +Definition Rp := SplitSurj.toParam (SplitSurj.Build reprpK). Axiom Rzero' : Rp zero zerop. Variable Radd' : binop_param Rp Rp Rp add addp. @@ -88,25 +87,13 @@ End IntToZmodp. Module ZmodpToInt. -Definition Rp x n := eqmodp (reprp x) n. - -Definition Rp2a2b@{i} : Param2a2b.Rel Zmodp@{i} int@{i}. -Proof. -unshelve econstructor. -- exact Rp. -- unshelve econstructor. - + exact reprp. - + move=> a b; move=> /(ap modp); exact. -- unshelve econstructor. - + exact modp. - + by move=> a b; rewrite /Rp/sym_rel/eqmodp reprpK => <-. -Defined. +Definition Rp := SplitSurj.toParamSym (SplitSurj.Build reprpK). Axiom Rzero : Rp zerop zero. Variable Radd : binop_param Rp Rp Rp addp add. Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. -Trocq Use Rp2a2b. +Trocq Use Rp. Trocq Use Param01_paths. Trocq Use Param10_paths. Trocq Use Radd. diff --git a/examples/Example.v b/examples/misc.v similarity index 100% rename from examples/Example.v rename to examples/misc.v diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v index 947060e..6cddc28 100644 --- a/examples/peano_bin_nat.v +++ b/examples/peano_bin_nat.v @@ -14,117 +14,10 @@ From Coq Require Import ssreflect. From HoTT Require Import HoTT. From Trocq Require Import Trocq. +From Trocq_examples Require Import N. Set Universe Polymorphism. -(* definition of binary natural numbers *) - -Inductive positive : Set := - | xI : positive -> positive - | xO : positive -> positive - | xH : positive. - -Declare Scope positive_scope. -Delimit Scope positive_scope with positive. -Bind Scope positive_scope with positive. - -Notation "1" := xH : positive_scope. -Notation "p ~ 1" := (xI p) - (at level 7, left associativity, format "p '~' '1'") : positive_scope. -Notation "p ~ 0" := (xO p) - (at level 7, left associativity, format "p '~' '0'") : positive_scope. - -Module Pos. -Local Open Scope positive_scope. -Fixpoint succ x := - match x with - | p~1 => (succ p)~0 - | p~0 => p~1 - | 1 => 1~0 - end. - -Fixpoint map (x : positive) : nat := - match x with - | p~1 => 1 + (map p + map p) - | p~0 => map p + map p - | 1 => 1 - end. - -Fixpoint add (x y : positive) : positive := - match x, y with - | 1, p | p, 1 => succ p - | p~0, q~0 => (add p q)~0 - | p~0, q~1 | p~1, q~0 => (add p q)~1 - | p~1, q~1 => succ (add p q)~1 - end. -Infix "+" := add : positive_scope. -Notation "p .+1" := (succ p) : positive_scope. - -Lemma addpp x : x + x = x~0. Proof. by elim: x => //= ? ->. Qed. -Lemma addp1 x : x + 1 = x.+1. Proof. by elim: x. Qed. -Lemma addpS x y : x + y.+1 = (x + y).+1. -Proof. by elim: x y => // p IHp [q|q|]//=; rewrite ?IHp ?addp1//. Qed. -Lemma addSp x y : x.+1 + y = (x + y).+1. -Proof. by elim: x y => [p IHp|p IHp|]// [q|q|]//=; rewrite ?IHp//. Qed. - -End Pos. -Infix "+" := Pos.add : positive_scope. -Notation "p .+1" := (Pos.succ p) : positive_scope. - -Inductive N : Set := - | N0 : N - | Npos : positive -> N. - -Declare Scope N_scope. -Delimit Scope N_scope with N. -Bind Scope N_scope with N. - -Notation "0" := N0 : N_scope. - -Definition succ_pos (n : N) : positive := - match n with - | N0 => 1%positive - | Npos p => Pos.succ p - end. - -Definition Nsucc (n : N) := Npos (succ_pos n). - -Definition Nadd (m n : N) := match m, n with -| N0, x | x, N0 => x -| Npos p, Npos q => Npos (Pos.add p q) -end. -Infix "+" := Nadd : N_scope. -Notation "n .+1" := (Nsucc n) : N_scope. - -(* various possible proofs to fill the fields of a parametricity witness between N and nat *) - -Definition Nmap (n : N) : nat := - match n with - | N0 => 0 - | Npos p => Pos.map p - end. - -Fixpoint Ncomap (n : nat) : N := - match n with O => 0 | S n => Nsucc (Ncomap n) end. - -Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0. -Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Qed. - -Lemma NcomapD i j : Ncomap (i + j) = (Ncomap i + Ncomap j)%N. -Proof. -elim: i j => [|i IHi] [|j]//=; first by rewrite -nat_add_n_O//. -rewrite -nat_add_n_Sm/= IHi. -case: (Ncomap i) => // p; case: (Ncomap j) => //=. -- by rewrite /Nsucc/= Pos.addp1. -- by move=> q; rewrite /Nsucc/= Pos.addpS Pos.addSp. -Qed. - -Let NcomapNpos p k : Ncomap k = Npos p -> Ncomap (k + k) = Npos p~0. -Proof. by move=> kp; rewrite NcomapD kp Naddpp. Qed. - -Lemma NmapK (n : N) : Ncomap (Nmap n) = n. -Proof. by case: n => //= ; elim=> //= p /NcomapNpos/= ->. Qed. - (* the best we can do to link these types is (4,4), but we only need (2a,3) which is morally that Nmap is a split injection *) Definition RN := SplitSurj.toParamSym@{Set} {| diff --git a/theories/Common.v b/theories/Common.v index d9c60c6..5b5b0d9 100644 --- a/theories/Common.v +++ b/theories/Common.v @@ -44,7 +44,7 @@ Module SplitInj. Section SplitInj. Universe i. Context {A B : Type@{i}}. -Record type@{} := { +Record type@{} := Build { section :> A -> B; retract : B -> A; sectionK : forall x, retract (section x) = x @@ -78,12 +78,13 @@ End to. End SplitInj. End SplitInj. +Arguments SplitInj.Build {A B section retract}. Module SplitSurj. Section SplitSurj. Universe i. Context {A B : Type@{i}}. -Record type := { +Record type := Build { retract :> A -> B; section : B -> A; sectionK : forall x, retract (section x) = x @@ -117,6 +118,7 @@ End to. End SplitSurj. End SplitSurj. +Arguments SplitSurj.Build {A B retract section}. Module Equiv. (* This is exactly adjointify *) @@ -134,7 +136,7 @@ Module Iso. Section Iso. Universe i. Context {A B : Type@{i}}. -Record type@{} := { +Record type@{} := Build { map :> A -> B; comap : B -> A; mapK : forall x, comap (map x) = x; @@ -184,3 +186,4 @@ End to. End Iso. End Iso. +Arguments Iso.Build {A B map comap}. \ No newline at end of file