Adding Prop and switching to Vanilla Coq

.devcontainer/Dockerfile

@@ -4,4 +4,4 @@ RUN opam update -y
 RUN opam install -y coq-lsp
 RUN git clone -b strat --depth 1 https://github.com/ecranceMERCE/coq-elpi
 RUN opam install -y ./coq-elpi
-RUN opam install -y coq-hott.8.17
+RUN opam install -y coq-mathcomp-algebra.1.19.0

.devcontainer/devcontainer.json

@@ -1,6 +1,8 @@
 {
     "name": "Trocq",
-    "image": "cohencyril/trocq-deps",
+    "build": {
+        "dockerfile": "Dockerfile"
+    },
     "postAttachCommand": "make -j8 -k",
     "customizations": {
         "vscode": {

.nix/config.nix

@@ -42,6 +42,7 @@
     ## You can override Coq and other Coq coqPackages
     ## through the following attribute
     coqPackages.coq.override.version = "8.17";
+    coqPackages.mathcomp.override.version = "1.19.0";
     coqPackages.coq-elpi.override.version = "ecranceMERCE:strat";
 
     ## In some cases, light overrides are not available/enough

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"447fd9da2820c66dee263a327d62f3f3e9da2688"
+"49d53bfc4d2ffbb834c6ee4360642a9b221704a0"

.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

coq-trocq.opam

@@ -39,7 +39,8 @@ install: [make "install"]
 depends: [
   "coq" {>= "8.17" & < "8.18"}
   "coq-elpi" {= "dev"}
-  "coq-hott" {>= "8.17" & < "8.18~"}
+  "coq-mathcomp-ssreflect" {>= "1.19.0" }
+  "coq-mathcomp-algebra"
 ]
 
 tags: [

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