wip

_CoqProject

@@ -1,4 +1,5 @@
 -arg -indices-matter
+-arg -w -arg +elpi.typechecker
 
 -R theories/ Trocq
 -R elpi/ Trocq.Elpi

elpi/annot.elpi

@@ -22,6 +22,10 @@ coq.subst-fun Args F FArgs :- !, coq.mk-app F Args FArgs.
 % NB: the output type is term because the annotations are encoded directly in Coq
 % see PType in Param.v
 pred term->annot-term i:term, o:term.
+term->annot-term (sort prop) (app [PProp , M, N]) :-
+  trocq.db.pprop PPropGR, !,
+  coq.env.global (const PPropGR) PProp, !,
+  cstr.univ-link _ M N.
 term->annot-term (sort (typ U)) (app [pglobal (const PType) UI, M, N]) :- trocq.db.ptype PType, !,
   coq.univ-instance UI [{coq.univ.variable U}],
   cstr.univ-link _ M N.
@@ -60,6 +64,11 @@ sub-type (app [pglobal (const PType) _, M1, N1]) (app [pglobal (const PType) _,
   cstr.univ-link C1 M1 N1,
   cstr.univ-link C2 M2 N2,
   cstr.geq C1 C2.
+sub-type (app [pglobal (const PProp) _, M1, N1]) (app [pglobal (const PProp) _, M2, N2]) :-
+  trocq.db.pprop PProp, !,
+  cstr.univ-link C1 M1 N1,
+  cstr.univ-link C2 M2 N2,
+  cstr.geq C1 C2.
 % SubPi
 sub-type (prod N T F) (prod _ T' F') :- !,
   sub-type T' T, !,
@@ -83,6 +92,11 @@ eq (app [pglobal (const PType) UI, M1, N1]) (app [pglobal (const PType) UI, M2,
   cstr.univ-link C1 M1 N1,
   cstr.univ-link C2 M2 N2,
   cstr.eq C1 C2.
+eq (app [pglobal (const PProp) UI, M1, N1]) (app [pglobal (const PProp) UI, M2, N2]) :-
+  trocq.db.pprop PProp, !,
+  cstr.univ-link C1 M1 N1,
+  cstr.univ-link C2 M2 N2,
+  cstr.eq C1 C2.
 eq (prod _ T F) (prod _ T' F') :- !,
   eq T T', !,
   pi x\ eq (F x) (F' x).
@@ -111,6 +125,8 @@ classes T Cs' Out :-
 pred all-classes i:term, o:list param-class.
 all-classes (app [pglobal (const PType) _, M, N]) [C] :- trocq.db.ptype PType, !,
   cstr.univ-link C M N.
+all-classes (app [pglobal (const PProp) _, M, N]) [C] :- trocq.db.pprop PProp, !,
+  cstr.univ-link C M N.
 all-classes X Cs :- (X = prod _ T F ; X = fun _ T F), !,
   pi x\ std.append {all-classes T} {all-classes (F x)} Cs.
 all-classes (app L) Cs :- !,
@@ -122,6 +138,8 @@ all-classes X _ :- coq.error "all-classes:" X.
 pred out-class i:term, o:option param-class.
 out-class (app [pglobal (const PType) _, M, N]) (some C) :- trocq.db.ptype PType, !,
   cstr.univ-link C M N.
+out-class (app [pglobal (const PProp) _, M, N]) (some C) :- trocq.db.pprop PProp, !,
+  cstr.univ-link C M N.
 out-class (prod _ _ F) Out :- !, pi x\ out-class (F x) Out.
 out-class (fun _ _ _) none :- !.
 out-class (app [F|Xs]) Out :- !,

elpi/constraints/constraints.elpi

@@ -118,9 +118,9 @@ pred c.vars? o:list class-id.
 pred c.vars! o:list class-id.
 
 pred vars? o:list class-id.
-vars? IDs :- declare_constraint (c.vars? IDs) [_].
+vars? IDs :- !, declare_constraint (c.vars? IDs) [_].
 pred vars! i:list class-id.
-vars! IDs :- declare_constraint (c.vars! IDs) [_].
+vars! IDs :- !, declare_constraint (c.vars! IDs) [_].
 
 constraint c.vars c.vars? c.vars! {
   rule (c.vars IDs) \ (c.vars? IDs') <=> (IDs' = IDs).
@@ -216,21 +216,23 @@ 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.graph G) (c.reduce-graph) <=> (std.spy-do! [
+    coq.say "final constraint graph START:",
     vars? IDs,
-    util.when-debug dbg.steps (
+    util.when-debug dbg.full (
       coq.say "final constraint graph:",
       cstr-graph.pp G,
       coq.say "***********************************************************************************"
     ),
     cstr-graph.instantiation-order IDs G SortedIDs,
-    util.when-debug dbg.steps (
+    util.when-debug dbg.full (
       coq.say "order:" SortedIDs,
       coq.say "***********************************************************************************"
     ),
     reduce SortedIDs G FinalValues,
-    util.when-debug dbg.steps (coq.say "final values:" FinalValues),
+    util.when-debug dbg.full (coq.say "final values:" FinalValues),
     std.forall FinalValues instantiate-coq
+  ]
   ).
 }
 
@@ -248,13 +250,14 @@ reduce [ID|IDs] ConstraintGraph [pr ID MinClass|FinalValues] :-
 
 % now instantiate for real
 pred instantiate-coq i:pair class-id param-class.
-instantiate-coq (pr ID (pc M0 N0)) :-
+instantiate-coq (pr ID (pc M0 N0)) :- std.spy-do! [
   util.when-debug dbg.full (coq.say "instantiating" ID "with" (pc M0 N0)),
   link- C ID,
   univ-link- C M N,
   map-class->term M0 M,
   map-class->term N0 N,
-  C = pc M0 N0.
+  C = pc M0 N0
+].
 
 } % internal
 

examples/int_to_Zp.v

@@ -96,10 +96,18 @@ Definition Rp := SplitSurj.toParam (SplitSurj.Build reprK).
 Lemma Rzero : Rp 0%R 0%R. Proof. done. Qed.
 
 Arguments graph /.
-Lemma Radd : binop_param Rp Rp Rp (@GRing.add _) (@GRing.add _).
+
+
+Definition int_add (x y : int) : int := (x + y)%R.
+Definition int_mul (x y : int) : int := (x * y)%R.
+
+Definition Zp_add (x y : 'Z_p) : 'Z_p := (x + y)%R.
+Definition Zp_mul (x y : 'Z_p) : 'Z_p := (x * y)%R.
+
+Lemma Radd : binop_param Rp Rp Rp (int_add) (Zp_add).
 Proof. by move=> /= m _ <- n _ <- /=; rewrite rmorphD. Qed.
 
-Lemma Rmul : binop_param Rp Rp Rp (@GRing.mul _) (@GRing.mul _).
+Lemma Rmul : binop_param Rp Rp Rp (int_mul) (Zp_mul).
 Proof. by move=> /= m _ <- n _ <- /=; rewrite rmorphM. Qed.
 
 Definition Reqmodp01 : forall (m : int) (x : 'Z_p), Rp m x ->
@@ -115,10 +123,11 @@ Trocq Use Rp Rmul Rzero Param10_paths Reqmodp01.
 Local Open Scope ring_scope.
 
 Lemma IntRedModZp :
- (forall (m n p : 'Z_p), m = n * n -> m = 0) ->
- forall (m n p : int), m = n * n -> (m == 0).
+ (forall (m n : 'Z_p), m = n * n -> m = 0) ->
+ forall (m n : int), m = n * n -> eqmodp m n.
 Proof.
 move=> Hyp.
+rewrite -[*%R]/int_mul/=.
 trocq; simpl.
 exact: Hyp.
 Qed.

theories/Database.v

@@ -36,6 +36,7 @@ Elpi Db trocq.db lp:{{
 
   % constants PType and Weaken registered so that we do not coq.locate every time
   pred trocq.db.ptype o:constant.
+  pred trocq.db.pprop o:constant.
   pred trocq.db.weaken o:constant.
 
   % param-type β α {{ Param(β)_Type(α) }}

theories/Hierarchy.v

@@ -100,11 +100,13 @@ Register sym_rel as trocq.sym_rel.
  * that will be mapped to variables in the constraint graph
  *)
 Definition PType@{i} (m n : map_class) (* : Type@{i+1} *) := Type@{i}.
+Definition PProp@{} (m n : map_class) (* : Type@{i+1} *) := Prop.
 (* placeholder for a weakening from (m, n) to (m', n')
  * replaced with a real weakening function once the ground classes are known
  *)
 Definition weaken@{i} (m n m' n' : map_class) {A : Type@{i}} (a : A) : A := a.
 Register PType as trocq.ptype.
+Register PProp as trocq.pprop.
 Register weaken as trocq.weaken.
 
 Elpi Command genhierarchy.
@@ -116,6 +118,8 @@ Elpi Accumulate File util.
 Elpi Query lp:{{
   {{:gref lib:trocq.ptype}} = const PType,
   coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.ptype PType)),
+  {{:gref lib:trocq.pprop}} = const PProp,
+  coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.pprop PProp)),
   {{:gref lib:trocq.weaken}} = const Weaken,
   coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.weaken Weaken)).
 }}.

theories/Param.v

@@ -146,10 +146,10 @@ Elpi Accumulate lp:{{
       coq.say "***********************************************************************************"
     ),
     % reduce the graph, so the variables all become ground in the terms
-    cstr.reduce-graph,
+    std.spy (cstr.reduce-graph),
     % now we can remove the weaken placeholders and replace them with real weakening functions
     % or nothing if it is weaken α α
-    param.subst-weaken GR GR',
+    std.spy (param.subst-weaken GR GR'),
     util.when-debug dbg.steps (
       coq.say "***********************************************************************************",
       coq.say "after reduction:",

theories/Param_Prop.v

@@ -17,6 +17,7 @@ Require Import HoTT_additions Hierarchy Database.
 From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class.
 From Trocq.Elpi Extra Dependency "util.elpi" as util.
 
+Set Warnings "+elpi.typecheck".
 Set Universe Polymorphism.
 Unset Universe Minimization ToSet.
 
@@ -54,11 +55,11 @@ Elpi Accumulate lp:{{
   ].
 
   pred generate-map-prop i:map-class, i:param-class.
-  generate-map-prop M RClass :- std.spy-do! [
+  generate-map-prop M RClass :- std.do! [
     coq.locate {calc ("Param" ^ {param-class->string RClass} ^ ".Rel")} R,
     Prop = sort prop,
-    coq.univ-instance Empty [],
     coq.env.global R RTm,
+    % RTm = {{fun A B : Prop => lp:RTmNoEta A B}},
     generate-fields M RTm RClass Fields,
     coq.locate "sym_rel" SymRel,
     coq.env.global SymRel SymRelTm,
@@ -75,26 +76,32 @@ Elpi Accumulate lp:{{
       "Map" ^ {map-class->string M} ^ "_Prop_sym" ^
       {param-class->string RClass},
     % these typechecks are very important: they add L < L1 to the constraint graph
-    % std.assert-ok (coq.elaborate-skeleton Decl Ty Decl') "generate-map-prop: Decl cannot be elaborated",
+    std.assert-ok! (coq.elaborate-skeleton Decl _Ty Decl')
+      "generate-map-prop: Decl cannot be elaborated",
+    std.assert-ok! (coq.elaborate-skeleton DeclSym _Ty' DeclSym')
+      "generate-map-prop: Decl cannot be elaborated",
     % std.assert-ok! (coq.typecheck Decl _)
-    %   "generate-map-prop: Decl ill-typed",
+    %    "generate-map-prop: Decl ill-typed",
     % std.assert-ok! (coq.typecheck DeclSym _)
-    %   "generate-map-prop: DeclSym ill-typed",
+    %    "generate-map-prop: DeclSym ill-typed",
     @udecl! [] tt [] tt =>
-      coq.env.add-const MapProp Decl _ @transparent! _,
+      coq.env.add-const MapProp Decl' _ @transparent! _,
     @udecl!  [] tt [] tt =>
-      coq.env.add-const MapPropSym DeclSym _ @transparent! _
+      coq.env.add-const MapPropSym DeclSym' _ @transparent! _
   ].
 }}.
 Elpi Typecheck.
 
 Set Printing Universes.
-Check (@Map0.BuildHas Prop Prop (@Param00.Rel)).
+Set Printing All.
+Print Param00.Rel.
+Eval compute in (@Map0.BuildHas Prop Prop (@Param00.Rel)).
 
 Elpi Query lp:{{
   % cannot have only one binder in the declaration because this line creates a fresh level:
-  Classes = [map0],
-  std.forall [map0] (m\
+  map-classes all Classes,
+  map-classes low LowClasses,
+  std.forall LowClasses (m\
     std.forall Classes (n\
       std.forall Classes (p\
         generate-map-prop m (pc n p)
@@ -103,7 +110,8 @@ Elpi Query lp:{{
   ).
 }}.
 
-Elpi Command genparamtype.
+
+(* Elpi Command genparamtype.
 Elpi Accumulate Db trocq.db.
 Elpi Accumulate File util.
 Elpi Accumulate File param_class.
@@ -183,4 +191,4 @@ Elpi Query lp:{{
  Set Printing Universes. About Param00_Prop40.
 Set Printing Universes. Print Param12a_Prop31.
 Set Printing Universes. About Param30_Prop44.
-Set Printing Universes. Print Param44_Prop44. *)
+Set Printing Universes. Print Param44_Prop44. *) *)