🚧 Additional example relating tuples and vectors

_CoqProject

@@ -9,19 +9,24 @@ theories/Hierarchy.v
 theories/Param_Type.v
 theories/Param_forall.v
 theories/Param_arrow.v
+theories/Common.v
+theories/Param_trans.v
 theories/Database.v
 theories/Param.v
 theories/Trocq.v
 theories/Vernac.v
+theories/Param_bool.v
+theories/Param_nat.v
 theories/Param_paths.v
 theories/Param_sigma.v
 theories/Param_prod.v
 theories/Param_option.v
-theories/Common.v
+theories/Param_vector.v
 
 examples/Example.v
 examples/int_to_Zp.v
 examples/peano_bin_nat.v
 examples/setoid_rewrite.v
 examples/summable.v
 examples/trocq_setoid_rewrite.v
+examples/Vector_tuple.v

artifact-clean/INSTRUCTIONS.md

@@ -0,0 +1,32 @@
+# Trocq
+
+0. We use the Opam package manager, please install it from the
+   official Opam webpage: https://opam.ocaml.org/doc/Install.html
+   and add the Coq opam repository, with the following command:
+   `opam repo add coq-released https://coq.*/opam/released`
+
+1. Create a fresh Opam switch (development was done with
+   OCaml 4.12.0, but anything newer should work). An existing switch may
+   also be used, if:
+   - the version the `coq` package is at least 8.17 and
+   - the `coq-hott` packaged is either not installed or at version 8.17 and
+   - package `coq-elpi` is **not** installed.
+
+   The plugin indeed requires a custom version of Coq-Elpi, with features
+   related to universe polymorphism that are still experimental. This
+   is why a version of the Coq-Elpi sources is included in this
+   artifact.
+
+2. Install Trocq and its dependencies by running `make` in the root
+   directory of the archive.
+
+3. Open your IDE at the root of the `trocq` directory. Open and execute
+   any of the example files present in the `trocq/examples` directory.
+
+   The examples have been put inside the `trocq` project for the sake of
+   convenience, so that the `-noinit`  and `-indices-matter` options of `coqtop` are taken into account in the IDE.
+
+   Please use either:
+   - CoqIDE (available in your switch via `opam install coqide`)
+   - VSCode or VSCodium with the **VSCoq Legacy** extension.
+   - emacs together with proof-general

artifact-clean/Makefile

@@ -0,0 +1,8 @@
+.PHONY: all
+
+all:
+	opam install ./coq-elpi
+	opam install ./trocq
+
+clean:
+	opam uninstall coq-elpi coq-trocq

elpi/annot.elpi

@@ -26,10 +26,10 @@ term->annot-term (sort (typ U)) (app [pglobal (const PType) UI, M, N]) :- trocq.
   coq.univ-instance UI [{coq.univ.variable U}],
   cstr.univ-link _ M N.
 term->annot-term (fun N T F) (fun N T' F') :- !,
-  term->annot-term T T',
+  term->annot-term T T', !,
   pi x\ term->annot-term (F x) (F' x).
 term->annot-term (prod N T F) (prod N T' F') :- !,
-  term->annot-term T T',
+  term->annot-term T T', !,
   pi x\ term->annot-term (F x) (F' x).
 term->annot-term (app L) (app L') :- !,
   std.map L term->annot-term L'.
@@ -62,18 +62,21 @@ sub-type (app [pglobal (const PType) _, M1, N1]) (app [pglobal (const PType) _,
   cstr.geq C1 C2.
 % SubPi
 sub-type (prod N T F) (prod _ T' F') :- !,
-  sub-type T' T,
+  sub-type T' T, !,
   @annot-pi-decl N T' x\ sub-type (F x) (F' x).
 % SubLam
 sub-type (fun N T F) (fun _ T F') :- !,
   @annot-pi-decl N T x\ sub-type (F x) (F' x).
 % SubApp
-sub-type (app [F|Xs]) (app [F'|Xs']) :- !,
+sub-type (app [F|Xs]) (app [F'|Xs']) :-
   sub-type F F',
   std.forall2 Xs Xs' eq.
 % SubConv
 sub-type X X :- (name X ; X = global _ ; X = pglobal _ _), !.
-sub-type X _ :- coq.error "annot.sub-type:" X.
+sub-type X Y :- coq.unify-eq X Y _.
+% TODO: perform controlled reduction
+% and extend implementation to fix, match, etc.
+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.
@@ -83,15 +86,15 @@ eq (app [pglobal (const PType) UI, M1, N1]) (app [pglobal (const PType) UI, M2,
   cstr.univ-link C2 M2 N2,
   cstr.eq C1 C2.
 eq (prod _ T F) (prod _ T' F') :- !,
-  eq T T',
+  eq T T', !,
   pi x\ eq (F x) (F' x).
 eq (fun _ T F) (fun _ T' F') :- !,
-  eq T T',
+  eq T T', !,
   pi x\ eq (F x) (F' x).
 eq (app L) (app L') :- !,
   std.forall2 L L' eq.
 eq X X :- (name X ; X = global _ ; X = pglobal _ _), !.
-eq X _ :- coq.error "annot.eq:" X.
+eq _ _ :- fail.
 
 % get all the annotations in a type T, as well as the "output class", i.e., the parametricity class
 % of the output type of T, as an option basically returning some (A,B) for an output type PType A B,

elpi/constraints/constraint-graph.elpi

@@ -116,7 +116,8 @@ maximal-class _ _ (pc map4 map4). % default maximal class for an unconstrained v
 % 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
 pred instantiate i:class-id, i:param-class, i:constraint-graph, o:constraint-graph.
-instantiate ID Class G _ :- coq.say "instantiate" ID Class G, fail.
+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), !,
   internal.filter-var LowerNodes LowerIDs,
@@ -126,7 +127,8 @@ instantiate ID Class (constraint-graph G) (constraint-graph G') :-
   std.fold HigherNodes G (instantiate.aux ID Class) G1,
   std.map.remove ID G1 G'.
 instantiate ID Class G G :-
-  coq.say "cannot instantiate" ID "at" Class "because it is not in the graph".
+  util.when-debug dbg.full (
+    coq.say "cannot instantiate" ID "at" Class "because it is not in the graph").
 pred instantiate.aux
   i:class-id, i:param-class, i:node, i:constraint-graph-content, o:constraint-graph-content.
 instantiate.aux ID Class (node.const C) G G :-
@@ -159,7 +161,7 @@ instantiate.aux ID Class (node.var (ct.gref GR T GR' GRR) IDs) G G' :-
       G1,
   annot.classes T TCs _,
   % find the output constant and proof, as well as the required classes Cs
-  trocq.db.gref GR Class Cs GR' GRR,
+  trocq.db.gref GR Class Cs GR' GRR, !,
   % make sure the classes are consistent
   instantiate.gref IDs TCs Cs G1 G'.
 pred instantiate.gref
@@ -194,9 +196,10 @@ pred pp i:constraint-graph.
 pp (constraint-graph G) :-
   std.forall {std.map.bindings G} pp.aux.
 pp.aux (pr ID (pr LowerNodes HigherNodes)) :-
-  coq.say "id" ID,
-  coq.say "higher than:" LowerNodes,
-  coq.say "lower than:" HigherNodes.
+  util.when-debug dbg.full (
+    coq.say "id" ID,
+    coq.say "higher than:" LowerNodes,
+    coq.say "lower than:" HigherNodes).
 
 namespace internal {
 

elpi/constraints/constraints.elpi

@@ -74,7 +74,7 @@ dep-gref GR T GR' GRR :-
     std.map TCs internal.link? IDs,
     declare_constraint (internal.c.dep-gref ID GR T GR' GRR IDs) [_]
   ) (
-    trocq.db.gref GR Out Cs GR' GRR,
+    trocq.db.gref GR Out Cs GR' GRR, !,
     std.forall2 TCs Cs eq
   ).
 

elpi/param-class.elpi

@@ -205,7 +205,7 @@ union (pc M1 N1) (pc M2 N2) (pc M N) :-
   map-class.union N1 N2 N.
 
 pred inter i:param-class, i:param-class, o:param-class.
-inter C C' _ :- coq.say C C', fail.
+inter C C' _ :- util.when-debug dbg.full (coq.say C C'), fail.
 inter (pc M1 N1) (pc M2 N2) (pc M N) :-
   map-class.inter M1 M2 M,
   map-class.inter N1 N2 N.

elpi/param.elpi

@@ -66,9 +66,9 @@ param (pglobal GR UI) T' (pglobal GR' UI) GrefR :- !,
 % ParamSub + ParamVar
 param X T' X' (W XR) :- name X, !,
   util.when-debug dbg.steps (coq.say "param/var" X "@" T'),
-  param.store X T X' XR,
+  param.store X T X' XR, !,
   util.when-debug dbg.steps (coq.say "param/var: found" X "@" T "~" X' "by" XR),
-  annot.sub-type T T',
+  annot.sub-type T T', !,
   weakening T T' (wfun W).
 
 % ParamUniv
@@ -106,7 +106,7 @@ param (fun N T F) FunTy (fun N' T' F') FunR :- !,
   coq.name-suffix N "'" N',
   coq.name-suffix N "R" NR,
   map-class->term map0 Map0,
-  param T (app [pglobal (const {trocq.db.ptype}) _, Map0, Map0]) T' TR,
+  param T (app [pglobal (const {trocq.db.ptype}) _, Map0, Map0]) T' TR, !,
   util.when-debug dbg.full (coq.say "param/fun:" T "@ 0,0 ~" T' "by" TR),
   @annot-pi-decl N T x\ pi x' xR\ param.store x T x' xR => (
     util.when-debug dbg.full (coq.say "param/fun: introducing" x "@" T "~" x' "by" xR),
@@ -124,20 +124,20 @@ param
   (prod `_` A' (_\ B')) (app [pglobal (const ParamArrow) UI|Args]) :-
     trocq.db.ptype 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,
+      param A (app [pglobal (const PType) _, MA, NA]) 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),
-      coq.say "before db param-arrow" C,
-      trocq.db.param-arrow C ParamArrow,
-      coq.say UI,
+      util.when-debug dbg.full (coq.say "before db param-arrow" C),
+      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),
       util.if-suspend C (param-class.requires-axiom C) (
@@ -157,21 +157,22 @@ param
     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,
-    cstr.univ-link C M1 M2,
+    cstr.univ-link C M1 M2, !,
     util.when-debug dbg.full (coq.say "param/forall:" M1 M2 "is linked to" C),
-    cstr.dep-pi C CA CB,
+    cstr.dep-pi C CA CB, !,
     util.when-debug dbg.full (coq.say "param/forall: added dep-pi from" C "to" CA "and" CB),
-    cstr.univ-link CA M1A M2A,
+    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,
-    cstr.univ-link CB M1B M2B,
+    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 => (
       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),
+      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,
+    trocq.db.r CA RA, !,
+    util.when-debug dbg.full (coq.say "param/forall db CA RA"), !,
     prune UIA [],
     Args =
       [ A, A', AR, fun N A B, fun N' A' B',
@@ -190,22 +191,22 @@ param
     ).
 
 % ParamSub for F (argument B in param.args) + ParamApp
-param (app [F|Xs]) B (app [F'|Xs']) (W AppR) :- !,
+param (app [F|Xs]) B (app [F'|Xs']) (W AppR) :- std.do! [
   util.when-debug dbg.steps (coq.say "param/app" F Xs "@" B),
   annot.typecheck F FTy,
   fresh-type => param F FTy F' FR,
   util.when-debug dbg.full (coq.say "param/app:" F "@" FTy "~" F' "by" FR),
   param.args FTy B Xs Xs' XsR W,
-  coq.subst-fun XsR FR AppR.
+  coq.subst-fun XsR FR AppR].
 
 pred param.args i:term, i:term, i:list term, o:list term, o:list term, o:term -> term.
-param.args T B [] [] [] W :- !,
+param.args T B [] [] [] W :- std.do! [
   annot.sub-type T B,
-  weakening T B (wfun W).
-param.args FunTy B [X|Xs] [X'|Xs'] [X, X', XR|XsR] W :-
+  weakening T B (wfun W)].
+param.args FunTy B [X|Xs] [X'|Xs'] [X, X', XR|XsR] W :- !,
   std.assert-ok! (coq.unify-eq FunTy (prod _ T TF)) {std.string.concat " "
-    ["type not convertible to Π:", {coq.term->string FunTy}]},
-  param X T X' XR,
+    ["type not convertible to Π:", {coq.term->string FunTy}]}, !,
+  param X T X' XR, !,
   param.args (TF X) B Xs Xs' XsR W.
 
 param X T _ _ :-