From c7e8b2f0edb5ddef6a7d94f108949d3cc8d452b3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Jan 2024 17:06:09 +0100 Subject: [PATCH 1/4] WIP: decorrelates knowing translations from using translations --- elpi/constraints/constraints.elpi | 23 +++++++++++----- elpi/util.elpi | 4 +++ examples/int_to_Zp.v | 11 ++++---- examples/misc.v | 4 +-- examples/summable.v | 14 ++++------ theories/Database.v | 10 +++++++ theories/Param.v | 19 +++++++++---- theories/Trocq.v | 3 ++ theories/Vernac.v | 46 +++++++++++++++++++++++-------- 9 files changed, 94 insertions(+), 40 deletions(-) diff --git a/elpi/constraints/constraints.elpi b/elpi/constraints/constraints.elpi index 41f3d0f..7849785 100644 --- a/elpi/constraints/constraints.elpi +++ b/elpi/constraints/constraints.elpi @@ -103,6 +103,9 @@ pred reduce-graph. reduce-graph :- declare_constraint internal.c.reduce-graph [_]. +pred local-db i:list prop. +local-db DB :- declare_constraint (internal.c.db DB) [_]. + % ================================================================================================== namespace internal { @@ -185,6 +188,9 @@ constraint c.univ-link c.univ-link? c.univ-link- { % store the constraint graph in the Elpi constraint store pred c.graph o:constraint-graph. +% stores the local db +pred c.db o:list prop. + % constraints to trigger addition of information to the constraint graph pred c.dep-pi o:class-id, o:class-id, o:class-id. pred c.dep-arrow o:class-id, o:class-id, o:class-id. @@ -195,7 +201,7 @@ pred c.geq o:or class-id param-class, o:or class-id param-class. % trigger reduction of the graph pred c.reduce-graph. -constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-graph { +constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-graph c.db { rule \ (c.graph G) (c.dep-pi ID IDA IDB) <=> ( cstr-graph.add-dep-pi ID IDA IDB G G', declare_constraint (c.graph G') [_] @@ -216,7 +222,7 @@ constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-gra cstr-graph.add-geq IDorC1 IDorC2 G G', declare_constraint (c.graph G') [_] ). - rule \ (c.graph G) (c.reduce-graph) <=> ( + rule (c.db DB) \ (c.graph G) (c.reduce-graph) <=> ( vars? IDs, util.when-debug dbg.steps ( coq.say "final constraint graph:", @@ -228,9 +234,11 @@ constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-gra coq.say "order:" SortedIDs, coq.say "***********************************************************************************" ), - reduce SortedIDs G FinalValues, - util.when-debug dbg.steps (coq.say "final values:" FinalValues), - std.forall FinalValues instantiate-coq + DB => std.do! [ + reduce SortedIDs G FinalValues, + util.when-debug dbg.steps (coq.say "final values:" FinalValues), + std.forall FinalValues instantiate-coq + ] ). } @@ -238,13 +246,14 @@ constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-gra % return a list of associations of a variable and its constant class pred reduce i:list class-id, i:constraint-graph, o:list (pair class-id param-class). reduce [] _ []. -reduce [ID|IDs] ConstraintGraph [pr ID MinClass|FinalValues] :- +reduce [ID|IDs] ConstraintGraph [pr ID MinClass|FinalValues] :- std.do![ cstr-graph.minimal-class ID ConstraintGraph MinClass, util.when-debug dbg.full (coq.say "min value" MinClass "for" ID), cstr-graph.maximal-class ID ConstraintGraph MaxClass, util.when-debug dbg.full (coq.say "max value" MaxClass "for" ID), util.unless (param-class.geq MaxClass MinClass) (coq.error "no solution for variable" ID), - reduce IDs {cstr-graph.instantiate ID MinClass ConstraintGraph} FinalValues. + reduce IDs {cstr-graph.instantiate ID MinClass ConstraintGraph} FinalValues +]. % now instantiate for real pred instantiate-coq i:pair class-id param-class. diff --git a/elpi/util.elpi b/elpi/util.elpi index 8dc57d2..4565806 100644 --- a/elpi/util.elpi +++ b/elpi/util.elpi @@ -84,6 +84,10 @@ delete A [A|Xs] Xs :- !. delete A [X|Xs] [X|Xs'] :- delete A Xs Xs'. delete _ [] []. +pred argument->gref i:argument, o:gref. +argument->gref (str S) GR :- coq.locate S GR. +argument->gref (trm T) GR :- coq.term->gref T GR. + % 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. diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index a98f461..25efc1d 100644 --- a/examples/int_to_Zp.v +++ b/examples/int_to_Zp.v @@ -23,6 +23,7 @@ Declare Scope Zmodp_scope. Delimit Scope Zmodp_scope with Zmodp. Local Open Scope Zmodp_scope. + Definition binop_param {X X'} RX {Y Y'} RY {Z Z'} RZ (f : X -> Y -> Z) (g : X' -> Y' -> Z') := forall x x', RX x x' -> forall y y', RY y y' -> RZ (f x y) (g x' y'). @@ -64,14 +65,14 @@ Variable Rmul : binop_param Rp Rp Rp mul mulp. Variable 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 Rp Rmul Rzero Param10_paths Reqmodp01. +Trocq RelatedWith Rp Rp Rmul Rzero Reqmodp01. Lemma IntRedModZp : (forall (m n p : Zmodp), (m = n * n)%Zmodp -> m = 0) -> forall (m n p : int), (m = n * n)%int -> (m == 0)%int. Proof. move=> Hyp. -trocq; simpl. +trocq Rp; simpl. exact: Hyp. Qed. @@ -87,11 +88,11 @@ 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 Rp Param01_paths Param10_paths Radd Rzero. +Trocq RelatedWith Rp Rp Radd Rzero. Goal (forall x y, x + y = y + x)%Zmodp. Proof. - trocq. + trocq Rp. exact addC. Qed. @@ -100,7 +101,7 @@ Proof. intros x y z. suff addpC: forall x y, (x + y = y + x)%Zmodp. { by rewrite (addpC x y). } - trocq. + trocq Rp. exact addC. Qed. diff --git a/examples/misc.v b/examples/misc.v index ec979e1..4f12abe 100644 --- a/examples/misc.v +++ b/examples/misc.v @@ -30,12 +30,12 @@ Trocq Register Funext f. Goal (* Type@{i}. *) - (* Type@{i} -> Type@{i}. *) + forall A (P : Type@{i} -> Type@{i}), P A. (* forall (A : Type@{i}), A. *) (* forall (A : Type@{i}), A -> A. *) (* forall (A B : Type@{i}), A -> B. *) (* forall (F : Type@{i} -> Type@{i}) (A : Type@{i}), F A. *) - forall (F : Type@{i} -> Type@{i}) (A B : Type@{i}), F A -> F B. + (* forall (F : Type@{i} -> Type@{i}) (A B : Type@{i}), F A -> F B. *) (* forall (F : Type@{i} -> Type@{i} -> Type@{i}) (A B : Type@{i}), F A B. *) (* forall (F : Type@{i} -> Type@{i} -> Type@{i}) (A B : Type@{i}), F A B -> F B A. *) (* forall (F : Type@{i} -> Type@{i}) (A : Type@{i}), F A -> forall (B : Type@{i}), F B. *) diff --git a/examples/summable.v b/examples/summable.v index 1891128..ada58b8 100644 --- a/examples/summable.v +++ b/examples/summable.v @@ -139,9 +139,7 @@ Proof. + exact truncate. + exact R_in_truncate_nnR. Defined. - -(* the only level we will need to pre-process the distributivity goal is (0,2b) *) -Definition Param02b_nnR : Param02b.Rel nnR xnnR := Param42b_nnR. +Trocq RelatedWith R_nnR Param42b_nnR. (* as sequences are encoded with constants, we need to relate them *) @@ -169,9 +167,7 @@ Proof. + exact R_in_extendK_rseq. - unshelve econstructor. Defined. - -(* we will only need (2a,0) on sequences to pre-process the distributivity goal *) -Definition Param2a0_rseq : Param2a0.Rel _ _ := Param40_rseq. +Trocq RelatedWith Rrseq Param40_rseq. (* now we need to relate the various constants at level (0,0) *) @@ -203,12 +199,12 @@ move=> u _ <-; rewrite extend_truncate//. by apply isSummableP. Qed. -Trocq Use Param01_paths Param02b_nnR Param2a0_rseq. -Trocq Use R_sum_xnnR R_add_xnnR seq_nnR_add. +Trocq RelatedWith R_nnR R_sum_xnnR R_sum_xnnR R_add_xnnR. +Trocq RelatedWith Rrseq seq_nnR_add. (* we get a proof over non negative reals for free, from the analogous proof over the extended ones *) Lemma sum_nnR_add : forall (u v : summable), (Σ (u + v) = Σ u + Σ v)%nnR. -Proof. trocq; exact: sum_xnnR_add. Qed. +Proof. trocq R_nnR Rrseq; exact: sum_xnnR_add. Qed. Print Assumptions sum_nnR_add. diff --git a/theories/Database.v b/theories/Database.v index ab66b95..e2e76ae 100644 --- a/theories/Database.v +++ b/theories/Database.v @@ -92,4 +92,14 @@ Elpi Db trocq.db lp:{{ :name "default-gref" trocq.db.gref _ _ _ _ _ :- do-not-fail, !, false. trocq.db.gref GR Out _ _ _ :- coq.error "cannot find" GR "at out class" Out. + + % The predicate known-gref is similar to the last one with one extra arguments: + % known-gref Rel GR ω [α_1, ..., α_n] GR' GRR + % BundleRel is the underlying relation in use + % it is used to find all translations associated to a given relation + % so that `trocq.use Rel`, all the associated translations + % of the form `gref Rel GR ω [α_1, ..., α_n] GR' GRR` will be used, i.e. + % added to the above database gref. + pred trocq.db.known-gref o:gref, o:gref, o:param-class, o:list param-class, o:gref, o:gref. + }}. diff --git a/theories/Param.v b/theories/Param.v index e13ee65..4f8dc9b 100644 --- a/theories/Param.v +++ b/theories/Param.v @@ -22,6 +22,7 @@ From Trocq.Elpi Extra Dependency "annot.elpi" as annot. From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. From Trocq.Elpi Extra Dependency "param.elpi" as param. +From Trocq.Elpi Extra Dependency "trocq.elpi" as trocq. From Trocq.Elpi.constraints Extra Dependency "simple-graph.elpi" as simple_graph. From Trocq.Elpi.constraints Extra Dependency "constraint-graph.elpi" as constraint_graph. From Trocq.Elpi.constraints Extra Dependency "constraints.elpi" as constraints. @@ -135,6 +136,7 @@ Elpi Accumulate File simple_graph. Elpi Accumulate File constraint_graph. Elpi Accumulate File constraints. Elpi Accumulate File param. +Elpi Accumulate File trocq. Elpi Typecheck. Elpi Accumulate lp:{{ @@ -144,21 +146,25 @@ Elpi Accumulate lp:{{ Elpi Accumulate lp:{{ solve InitialGoal NewGoals :- debug dbg.none => std.do! [ - InitialGoal = goal _Context _ G _ [], + InitialGoal = goal _Context _ G _ Args, + util.when-debug dbg.full (coq.say "translating args" Args), + std.map Args util.argument->gref GRArgs, + util.when-debug dbg.full (coq.say "loading rels" GRArgs), + trocq.load-rels GRArgs DB, + util.when-debug dbg.full (coq.say "local DB" DB), util.when-debug dbg.full (coq.say "goal" G), - translate-goal G (pc map0 map1) G' GR, + translate-goal DB G (pc map0 map1) G' GR, util.when-debug dbg.full (coq.say "trocq:" G "~" G' "by" GR), FinalProof = {{ @comap lp:G lp:G' lp:GR (_ : lp:G') }}, util.when-debug dbg.full (coq.say FinalProof), - std.assert-ok! (coq.elaborate-skeleton FinalProof G EFinalProof) "proof elaboration error", std.assert-ok! (coq.typecheck EFinalProof G2) "proof typechecking error", std.assert-ok! (coq.unify-leq G2 G) "goal unification error", refine.no_check EFinalProof InitialGoal NewGoals ]. - pred translate-goal i:term, i:param-class, o:term, o:term. - translate-goal G (pc M N) G' GR' :- std.do! [ + pred translate-goal i:list prop, i:term, i:param-class, o:term, o:term. + translate-goal DB G (pc M N) G' GR' :- DB => std.do! [ cstr.init, T = (app [pglobal (const {trocq.db.ptype}) _, {map-class->term M}, {map-class->term N}]), % first annotate the initial goal with fresh parametricity class variables @@ -177,6 +183,7 @@ Elpi Accumulate lp:{{ coq.say "***********************************************************************************" ), % reduce the graph, so the variables all become ground in the terms + cstr.local-db DB, cstr.reduce-graph, % now we can remove the weaken placeholders and replace them with real weakening functions % or nothing if it is weaken α α @@ -193,4 +200,4 @@ Elpi Accumulate lp:{{ }}. Elpi Typecheck. -Tactic Notation "trocq" := elpi trocq. +Tactic Notation "trocq" ident_list(l) := elpi trocq ltac_string_list:(l). \ No newline at end of file diff --git a/theories/Trocq.v b/theories/Trocq.v index 207d601..7fa7421 100644 --- a/theories/Trocq.v +++ b/theories/Trocq.v @@ -16,3 +16,6 @@ From HoTT Require Export HoTT. From Trocq Require Export HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param Param_paths Vernac Common Param_nat Param_trans Param_bool. + +Trocq Use Param10_paths. +Trocq Use Param01_paths. diff --git a/theories/Vernac.v b/theories/Vernac.v index f1a7544..619ffac 100644 --- a/theories/Vernac.v +++ b/theories/Vernac.v @@ -79,15 +79,12 @@ Elpi Accumulate lp:{{ ]. % command to add custom witnesses to the database - - main [str "Use", str X] :- !, - coq.locate X GR, main [str "Use", trm (global GR)]. - - main [str "Use", trm X] :- !, std.do! [ - coq.term->gref X GRR, + % and tells trocq to use it immediately + main [str "Use", X] :- !, std.do! [ + util.argument->gref X GRR, coq.env.typeof GRR XTy, param-class.type->classes XTy Class CList GR GR', - coq.say "accumultating" GR "@" Class "(" CList ") ~" GR' ":." GRR, + coq.info "accumulating" GR "@" Class "(" CList ") ~" GR' ":." GRR, coq.elpi.accumulate _ "trocq.db" (clause _ (before "default-gref") (trocq.db.gref GR Class CList GR' GRR)), @@ -103,18 +100,45 @@ Elpi Accumulate lp:{{ 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' + coq.info "accumulating" GR "@" subclass "(" CList ") ~" GR' ":." (const WCRR), ]) ]. - % coq.elpi.accumulate _ "trocq.db" - % (clause _ (before "default-gref") - % (trocq.db.gref GR (pc map4 map2b) [] {{:gref int}} {{:gref Rp42b}})), % serveral use in one go! main [str "Use", X, Y | Rest] :- !, std.do![ main [str "Use", X], main [str "Use", Y | Rest]]. + main [str "RelatedWith", Rel, X] :- !, std.do! [ + util.argument->gref Rel GRRel, + util.argument->gref X GRR, + coq.env.typeof GRR XTy, + param-class.type->classes XTy Class CList GR GR', + coq.info "accumulating" GR "@" Class "(" CList ") ~" GR' ":." GRR + "attached to relation" GRRel, + coq.elpi.accumulate _ "trocq.db" + (clause _ _ + (trocq.db.known-gref GRRel 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.known-gref GRRel 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 _ _ + (trocq.db.known-gref GRRel GR subclass CList GR' (const WCRR))), + coq.info "accumulating" GR "@" subclass "(" CList ") ~" GR' + ":." (const WCRR) "attached to relation" GRRel, + ]) + ]. + % serveral use in one go! + main [str "RelatedWith", Rel, X, Y | Rest] :- !, std.do![ + main [str "RelatedWith", Rel, X], main [str "RelatedWith", Rel, Y | Rest]]. + main [str "Usage"] :- !, coq.say {usage-msg}. main _ :- coq.error {std.string.concat "\n" ["command syntax error", {usage-msg}]}. From cbb1f544d13fdd41b0ccc2b8875e248e30194ebd Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Jan 2024 17:10:24 +0100 Subject: [PATCH 2/4] rudimentary doc --- theories/Vernac.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theories/Vernac.v b/theories/Vernac.v index 619ffac..ad539d2 100644 --- a/theories/Vernac.v +++ b/theories/Vernac.v @@ -148,7 +148,8 @@ Elpi Accumulate lp:{{ "usage:", "- Trocq Register Univalence ", "- Trocq Register Funext ", - "- Trocq Use ", + "- Trocq Use *", + "- Trocq Knows *" "", "", ] U. }}. From 73e12d728f477002c81249d1bcc18e6df5fcb33a Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Jan 2024 18:54:33 +0100 Subject: [PATCH 3/4] forgotten file --- elpi/trocq.elpi | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 elpi/trocq.elpi diff --git a/elpi/trocq.elpi b/elpi/trocq.elpi new file mode 100644 index 0000000..974a845 --- /dev/null +++ b/elpi/trocq.elpi @@ -0,0 +1,38 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % 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) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% ----------------------------------------------------------------------------- +% main code for trocq tactics +% ----------------------------------------------------------------------------- + + +namespace trocq { + +pred known->gref i:prop, o:prop. +known->gref + (trocq.db.known-gref _Rel GR OutCl Classes GR' GRR) + (trocq.db.gref GR OutCl Classes GR' GRR :- !). + +pred load-rel i:gref, o:list prop. +load-rel GRRel DB :- std.do! [ + std.findall + (trocq.db.known-gref GRRel _GR _OutCl _Classes _GR' _GRR) + AllRel, + std.map AllRel known->gref DB + ]. + +pred load-rels i:list gref, o:list prop. +load-rels GRRels DB :- std.do! [ + std.map GRRels load-rel DBs, + std.flatten DBs DB + ]. +} \ No newline at end of file From 5614e355dd467557d1ec297d20c0a2a24b970255 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Jan 2024 19:18:40 +0100 Subject: [PATCH 4/4] typo --- theories/Vernac.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Vernac.v b/theories/Vernac.v index ad539d2..f7056d1 100644 --- a/theories/Vernac.v +++ b/theories/Vernac.v @@ -149,7 +149,7 @@ Elpi Accumulate lp:{{ "- Trocq Register Univalence ", "- Trocq Register Funext ", "- Trocq Use *", - "- Trocq Knows *" + "- Trocq Knows *", "", "", ] U. }}.