Automatic weakening of constants

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

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

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.

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

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.
 

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

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:{{

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.

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:{{

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.
 

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.
 

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.
 

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