WIP: decorrelates knowing translations from using translations

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,23 +234,26 @@ 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
+    ]
   ).
 }
 
 % reduce the graph by instantiating variables in the precedence order and updating the graph
 % 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.

elpi/trocq.elpi

@@ -0,0 +1,38 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                            %                     Trocq                      %
+%  _______                   %        Copyright (C) 2023 Inria & MERCE        %
+% |__   __|                  %     (Mitsubishi Electric R&D Centre Europe)    %
+%    | |_ __ ___   ___ __ _  %        Cyril Cohen <cyril.cohen@inria.fr>      %
+%    | | '__/ _ \ / __/ _` | %        Enzo Crance <enzo.crance@inria.fr>      %
+%    | | | | (_) | (_| (_| | %    Assia Mahboubi <assia.mahboubi@inria.fr>    %
+%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                        | | %   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
+  ].
+}

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.

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.
 

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. *)

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.

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.
+
 }}.

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).

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.

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}]}.
 
@@ -124,7 +148,8 @@ Elpi Accumulate lp:{{
       "usage:",
       "- Trocq Register Univalence <u>",
       "- Trocq Register Funext <f>",
-      "- Trocq Use <RTrocq>",
+      "- Trocq Use <RTrocq>*",
+      "- Trocq Knows <Relation> <RTrocq>*",
       "", "",
     ] U.
 }}.