Adding Prop and switching to Vanilla Coq

.nix/coq-overlays/trocq/default.nix

@@ -4,7 +4,7 @@
 ## but the full doc is on nixos / nix packages website:
 ## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq
 
-{ lib, mkCoqDerivation, which, coq, HoTT, coq-elpi
+{ lib, mkCoqDerivation, which, coq, coq-elpi, mathcomp
   ## declare extra dependencies here, to be used in propagateBuildInputs e.g.
   # , mathcomp, coq-elpi
   , version ? null }:
@@ -40,7 +40,7 @@ with lib; mkCoqDerivation {
   ## - arbitrary nix packages (you need to require them at the beginning of the file)
   ## - Coq packages (require them at the beginning of the file)
   ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file)
-  propagatedBuildInputs = [ HoTT coq-elpi ]; ## e.g. `= [ mathcomp coq-elpi ]`
+  propagatedBuildInputs = [ mathcomp.ssreflect mathcomp.algebra coq-elpi ]; ## e.g. `= [ mathcomp coq-elpi ]`
 
   ## Does the package contain OCaml code?
   mlPlugin = true;

_CoqProject

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

elpi/annot.elpi

@@ -22,7 +22,18 @@ 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 (typ U)) (app [pglobal (const PType) UI, M, N]) :- trocq.db.ptype PType, !,
+term->annot-term (app [pglobal (const PPropGR) _, M, N] as P) P :-
+  trocq.db.pprop PPropGR, !,
+  cstr.univ-link _ M N.
+term->annot-term (app [pglobal (const PTypeGR) _, M, N] as P) P :-
+  trocq.db.ptype PTypeGR, !,
+  cstr.univ-link _ M N.
+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 PTypeGR) UI, M, N]) :-
+  trocq.db.ptype PTypeGR, !,
   coq.univ-instance UI [{coq.univ.variable U}],
   cstr.univ-link _ M N.
 term->annot-term (fun N T F) (fun N T' F') :- !,
@@ -56,10 +67,11 @@ typecheck T ATy :-
 pred sub-type i:term, i:term.
 % SubSort
 sub-type (app [pglobal (const PType) _, M1, N1]) (app [pglobal (const PType) _, M2, N2]) :-
-  trocq.db.ptype PType, !,
+  (trocq.db.ptype PType; trocq.db.pprop PType), !, std.do![
   cstr.univ-link C1 M1 N1,
   cstr.univ-link C2 M2 N2,
-  cstr.geq C1 C2.
+  cstr.geq C1 C2
+  ].
 % SubPi
 sub-type (prod N T F) (prod _ T' F') :- !,
   sub-type T' T, !,
@@ -79,7 +91,7 @@ sub-type X Y :- coq.error "annot.sub-type:" X "vs" Y.
 % syntactic term equality, taking care of adding annotation equalities in the constraint graph
 pred eq i:term, i:term.
 eq (app [pglobal (const PType) UI, M1, N1]) (app [pglobal (const PType) UI, M2, N2]) :-
-  trocq.db.ptype PType, !,
+  (trocq.db.ptype PType; trocq.db.pprop PType), !,
   cstr.univ-link C1 M1 N1,
   cstr.univ-link C2 M2 N2,
   cstr.eq C1 C2.
@@ -99,17 +111,17 @@ eq _ _ :- fail.
 % and none for output types that are not sorts, because it means values of type T are not type
 % constructors, so their translation will be made at class (0,0)
 pred classes i:term, o:list param-class, o:option param-class.
-classes T Cs' Out :-
+classes T Cs' Out :- std.do! [
   all-classes T Cs,
   out-class T Out,
   if (not (Cs = []), Out = some C, std.last Cs LastC, LastC == C) (
     std.drop-last 1 Cs Cs'
   ) (
     Cs' = Cs
-  ).
+  )].
 
 pred all-classes i:term, o:list param-class.
-all-classes (app [pglobal (const PType) _, M, N]) [C] :- trocq.db.ptype PType, !,
+all-classes (app [PCst, M, N]) [C] :- trocq.db.ptype-or-pprop PCst _, !,
   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.
@@ -120,7 +132,7 @@ all-classes X _ :- coq.error "all-classes:" X.
 
 % output class of a term
 pred out-class i:term, o:option param-class.
-out-class (app [pglobal (const PType) _, M, N]) (some C) :- trocq.db.ptype PType, !,
+out-class (app [PCst, M, N]) (some C) :- trocq.db.ptype-or-pprop PCst _, !,
   cstr.univ-link C M N.
 out-class (prod _ _ F) Out :- !, pi x\ out-class (F x) Out.
 out-class (fun _ _ _) none :- !.

elpi/constraints/constraint-graph.elpi

@@ -114,18 +114,19 @@ maximal-class _ _ (pc map4 map4). % default maximal class for an unconstrained v
 
 % assign a constant class to a variable and update all the information in the graph
 % indeed, if the assigned variable was an output class for complex constraints,
-% they can now be computed and reduced to simpler constraints on the other variables
+% they can now be computed and   reduced to simpler constraints on the other variables
 pred instantiate i:class-id, i:param-class, i:constraint-graph, o:constraint-graph.
 instantiate ID Class G _ :-
   util.when-debug dbg.steps (coq.say "instantiate" ID Class G), fail.
 instantiate ID Class (constraint-graph G) (constraint-graph G') :-
-  std.map.find ID G (pr LowerNodes HigherNodes), !,
+  std.map.find ID G (pr LowerNodes HigherNodes), !, std.do! [
   internal.filter-var LowerNodes LowerIDs,
   util.unless (LowerIDs = [])
     (coq.error
       "wrong instantiation order: trying to instantiate" ID "before lower variables" LowerIDs),
   std.fold HigherNodes G (instantiate.aux ID Class) G1,
-  std.map.remove ID G1 G'.
+  std.map.remove ID G1 G'
+  ].
 instantiate ID Class G G :-
   util.when-debug dbg.full (
     coq.say "cannot instantiate" ID "at" Class "because it is not in the graph").
@@ -135,27 +136,30 @@ instantiate.aux ID Class (node.const C) G G :-
   util.unless (param-class.geq C Class)
     (coq.error
       "constraint not respected: instantiating" ID "at class" Class "despite upper bound" C).
-instantiate.aux ID Class (node.var ct.pi [IDA, IDB]) G G' :-
+instantiate.aux ID Class (node.var ct.pi [IDA, IDB]) G G' :- std.do![
   util.map.update IDA (internal.remove-lower-node (node.var ct.pi [ID])) G G1,
   util.map.update IDB (internal.remove-lower-node (node.var ct.pi [ID])) G1 G2,
   % recompute the dependent product constraint and turn it into 2 order constraints
   param-class.dep-pi Class C1 C2,
   util.map.update IDA (internal.add-lower-node (node.const C1)) G2 G3,
-  util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'.
-instantiate.aux ID Class (node.var ct.arrow [IDA, IDB]) G G' :-
+  util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'
+].
+instantiate.aux ID Class (node.var ct.arrow [IDA, IDB]) G G' :- std.do![
   util.map.update IDA (internal.remove-lower-node (node.var ct.arrow [ID])) G G1,
   util.map.update IDB (internal.remove-lower-node (node.var ct.arrow [ID])) G1 G2,
   % recompute the arrow type constraint and turn it into 2 order constraints
   param-class.dep-arrow Class C1 C2,
   util.map.update IDA (internal.add-lower-node (node.const C1)) G2 G3,
-  util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'.
-instantiate.aux ID Class (node.var ct.type [IDR]) G G' :-
+  util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'
+].
+instantiate.aux ID Class (node.var ct.type [IDR]) G G' :- std.do![
   util.map.update IDR (internal.remove-lower-node (node.var ct.type [ID])) G G1,
   % the constraint either vanishes or forces the relation to be (4,4)
   if (param-class.requires-axiom Class)
     (util.map.update IDR (internal.add-lower-node (node.const (pc map4 map4))) G1 G')
-    (G' = G1).
-instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :-
+    (G' = G1)
+].
+instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :- std.do! [
   std.fold {std.filter IDs (id\ id > 0)} G (id\ g\ g'\
     util.map.update id (internal.remove-lower-node (node.var (ct.gref _ _ _ _) [ID])) g g')
       G1,
@@ -164,7 +168,8 @@ instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :-
   trocq.db.gref GR Class Cs GR' GRR, !,
   coq.env.global GR' Tm',
   % make sure the classes are consistent
-  instantiate.gref IDs TCs Cs G1 G'.
+  instantiate.gref IDs TCs Cs G1 G'
+  ].
 pred instantiate.gref
   i:list class-id, i:list param-class, i:list param-class, i:constraint-graph-content,
   o:constraint-graph-content.
@@ -174,12 +179,13 @@ instantiate.gref [-1|IDs] [TC|TCs] [C|Cs] G G' :- !,
   % we just check that it is equal to the required one
   TC = C,
   instantiate.gref IDs TCs Cs G G'.
-instantiate.gref [ID|IDs] [_|TCs] [C|Cs] G G' :-
+instantiate.gref [ID|IDs] [_|TCs] [C|Cs] G G' :- std.do![
   % here the identifier is not -1, which means that the class at this position is in the graph
   % we force it to be equal to C in the graph
   util.map.update ID (internal.add-lower-node (node.const C)) G G1,
   util.map.update ID (internal.add-higher-node (node.const C)) G1 G2,
-  instantiate.gref IDs TCs Cs G2 G'.
+  instantiate.gref IDs TCs Cs G2 G'
+].
 instantiate.aux ID Class (node.var ct.geq [IDH]) G G' :-
   % an order constraint is turned into a lower constant class
   util.map.update IDH (internal.remove-lower-node (node.var ct.geq [ID])) G G1,

elpi/constraints/constraints.elpi

@@ -56,10 +56,10 @@ dep-arrow C CA CB :-
 
 % D_□(C, C_R)
 pred dep-type i:param-class, i:param-class.
-dep-type C CR :- var C, !,
+dep-type C CR :- var C, !, std.do![
   internal.link? C ID,
   internal.link? CR IDR,
-  declare_constraint (internal.c.dep-type ID IDR) [_].
+  declare_constraint (internal.c.dep-type ID IDR) [_]].
 dep-type C CR :-
   util.when (param-class.requires-axiom C)
     (geq CR (pc map4 map4)).
@@ -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,45 +216,49 @@ 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.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
+  ]
   ).
 }
 
 % 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.
-instantiate-coq (pr ID (pc M0 N0)) :-
+instantiate-coq (pr ID (pc M0 N0)) :- std.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
 

elpi/param.elpi

@@ -43,11 +43,13 @@ param (global GR) T' Tm' GrefR :- !,
     cstr.dep-gref GR T' Tm' GRR,
     GrefR = pglobal GRR _
   ) (
-    annot.typecheck (global GR) T,
-    annot.sub-type T T',
-    cstr.dep-gref GR T Tm' GRR,
-    weakening T T' (wfun W),
-    GrefR = (W (pglobal GRR _))
+    std.do![
+      annot.typecheck (global GR) T,
+      annot.sub-type T T',
+      cstr.dep-gref GR T Tm' GRR,
+      weakening T T' (wfun W),
+      GrefR = (W (pglobal GRR _))
+    ]
   ).
 
 % universe-polymorphic case
@@ -74,8 +76,12 @@ param X T' X' (W XR) :- name X, !,
 
 % TrocqSort
 param
-  (app [pglobal (const PType) UI, MR, NR] as Type) (app [pglobal (const PType) _, M, N])
-  Type (app [pglobal (const PParamType) UI1|Args]) :- trocq.db.ptype PType, !, std.do! [
+  (app [pglobal (const PType) UI, MR, NR]  as Type)
+  (app [_, M, N])
+  Type
+  (app [pglobal (const PParamType) UI1|Args]) :-
+    (trocq.db.ptype PType; trocq.db.pprop PType), !,
+    std.do! [
     util.when-debug dbg.steps (coq.say "param/type" MR NR "@" M N),
     cstr.univ-link CR MR NR,
     util.when-debug dbg.full (coq.say "param/type:" MR NR "is linked to" CR),
@@ -127,21 +133,24 @@ param (fun N T F) FunTy (fun N' T' F') FunR :- !,
 param
   (prod _ A (_\ B)) (app [pglobal (const PType) _, M, N])
   (prod `_` A' (_\ B')) (app [pglobal (const ParamArrow) UI|Args]) :-
-    trocq.db.ptype PType, !, std.do! [
+    (trocq.db.ptype PType; trocq.db.pprop PType), !, std.do! [
       util.when-debug dbg.steps (coq.say "param/arrow" A "->" B "@" M N),
-      cstr.univ-link C M N, !,
+      cstr.univ-link C M N,
       util.when-debug dbg.full (coq.say "param/arrow:" M N "is linked to" C),
-      cstr.dep-arrow C CA CB, !,
+      cstr.dep-arrow C CA CB,
       util.when-debug dbg.full (coq.say "param/arrow: added dep-arrow from" C "to" CA "and" CB),
-      cstr.univ-link CA MA NA, !,
+      cstr.univ-link CA MA NA,
       util.when-debug dbg.full (coq.say "param/arrow:" MA NA "is linked to" CA),
-      param A (app [pglobal (const PType) _, MA, NA]) A' AR, !,
-      cstr.univ-link CB MB NB, !,
+      std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A",
+      if (TyA = sort prop) (trocq.db.pprop PTypeGRA) (trocq.db.ptype PTypeGRA),
+      PTypeA = (app [pglobal (const PTypeGRA) _, MA, NA]),
+      param A PTypeA A' AR,
+      cstr.univ-link CB MB NB,
       util.when-debug dbg.full (coq.say "param/arrow:" MB NB "is linked to" CB),
-      param B (app [pglobal (const PType) _, MB, NB]) B' BR, !,
+      param B (app [pglobal (const PType) _, MB, NB]) B' BR,
       util.when-debug dbg.full (coq.say "param/arrow:" B "@" MB NB "~" B' "by" BR),
       util.when-debug dbg.full (coq.say "before db param-arrow" C),
-      trocq.db.param-arrow C ParamArrow, !,
+      trocq.db.param-arrow C ParamArrow,
       util.when-debug dbg.full (coq.say UI),
       prune UI [],
       util.when-debug dbg.full (coq.say "param/arrow: suspending proof on" C),
@@ -158,7 +167,8 @@ param
 % TrocqPi
 param
   (prod N A B) (app [pglobal (const PType) _, M1, M2])
-  (prod N' A' B') (app [pglobal (const ParamForall) UI|Args']) :- trocq.db.ptype PType, !,
+  (prod N' A' B') (app [pglobal (const ParamForall) UI|Args']) :-
+    (trocq.db.ptype PType; trocq.db.pprop PType), !, std.do![
     util.when-debug dbg.steps (coq.say "param/forall" N ":" A "," B "@" M1 M2),
     coq.name-suffix N "'" N',
     coq.name-suffix N "R" NR,
@@ -168,14 +178,17 @@ param
     util.when-debug dbg.full (coq.say "param/forall: added dep-pi from" C "to" CA "and" CB),
     cstr.univ-link CA M1A M2A, !,
     util.when-debug dbg.full (coq.say "param/forall:" M1A M2A "is linked to" CA),
-    param A (app [pglobal (const PType) _, M1A, M2A]) A' AR,
+    std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A",
+    if (TyA = sort prop) (trocq.db.pprop PTypeGRA) (trocq.db.ptype PTypeGRA),
+    PTypeA = (app [pglobal (const PTypeGRA) _, M1A, M2A]),
+    param A PTypeA A' AR,
     cstr.univ-link CB M1B M2B, !,
     util.when-debug dbg.full (coq.say "param/forall:" M1B M2B "is linked to" CB),
-    @annot-pi-decl N A a\ pi a' aR\ param.store a A a' aR => (
+    @annot-pi-decl N A a\ pi a' aR\ param.store a A a' aR => std.do![
       util.when-debug dbg.full (coq.say "param/forall: introducing" a "@" A "~" a' "by" aR),
       param (B a) (app [pglobal (const PType) _, M1B, M2B]) (B' a') (BR a a' aR), !,
       util.when-debug dbg.full (coq.say "param/forall:" (B a) "@" M1B M2B "~" (B' a') "by" (BR a a' aR))
-    ),
+    ],
     trocq.db.r CA RA, !,
     util.when-debug dbg.full (coq.say "param/forall db CA RA"), !,
     prune UIA [],
@@ -193,7 +206,8 @@ param
     ) (
       util.when-debug dbg.full (coq.say "param/forall: resuming proof on" C "(funext not needed)"),
       Args' = Args
-    ).
+    )
+    ].
 
 % TrocqConv for F (argument B in param.args) + TrocqApp
 param (app [F|Xs]) B (app [F'|Xs']) (W AppR) :- std.do! [
@@ -229,7 +243,7 @@ type wsuspend (term -> term) -> (term -> term) -> weakening.
 % cf definition of weakening in the paper
 pred weakening i:term, i:term, o:weakening.
 weakening (app [pglobal (const PType) _, M, N]) (app [pglobal (const PType) _, M', N']) W :-
-  trocq.db.ptype PType, !,
+  (trocq.db.ptype PType; trocq.db.pprop PType), !,
   trocq.db.weaken Weaken,
   prune UI [],
   prune Ty [],