Temporary fix that enables example append_comm_cons + add cuts

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,19 +62,20 @@ 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 F F', !,
+  sub-type F F',
   std.forall2 Xs Xs' eq.
 % SubConv
 sub-type X X :- (name X ; X = global _ ; X = pglobal _ _), !.
-sub-type X Y :- whd1 X X', !, sub-type X' Y.
-sub-type X Y :- whd1 Y Y', !, sub-type X Y'.
+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
@@ -85,10 +86,10 @@ 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.

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,19 +124,19 @@ 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),
       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),
@@ -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 _ _ :-

examples/Vector_tuple.v

@@ -258,7 +258,7 @@ Trocq Use Param_const.
 Trocq Use Param01_paths.
 
 Lemma head_const' : forall {n : nat} (z : Zp), head (const z (S n)) = z.
-Proof. trocq; exact: @head_const. Qed.
+Proof. trocq. intro n. apply head_const. Qed.
 
 End HeadConst.
 
@@ -285,6 +285,16 @@ Defined.
 
 Trocq Use SR.
 Trocq Use Param_cons.
+Trocq Use Param_add.
+Trocq Use Param_append.
+Trocq Use Param01_paths.
+Trocq Use Param2a0_tuple_vector.
+Trocq Use Param02b_tuple_vector.
+Trocq Use Param2a0_nat.
+Lemma append_comm_cons : forall {A : Type} {n1 n2 : nat}
+    (v1 : tuple A n1) (v2 : tuple A n2) (a : A),
+  @paths (tuple A (S (n1 + n2))) (cons a (append v1 v2)) (append (cons a v1) v2).
+Proof. by trocq. Qed.
 
 (* bounded nat and bitvector *)
 (* NB: we can use transitivity to make the proofs here too *)

theories/Param.v

@@ -34,6 +34,7 @@ Inductive map_class : Set := map0 | map1 | map2a | map2b | map3 | map4.
 (* PType and weaken *)
 
 Elpi Command genpparam.
+Elpi Accumulate File util.
 Elpi Accumulate File param_class.
 Elpi Accumulate Db trocq.db.
 
@@ -53,6 +54,7 @@ Elpi Query lp:{{
 *)
 
 Elpi Command genpparamtype.
+Elpi Accumulate File util.
 Elpi Accumulate File param_class.
 Elpi Accumulate Db trocq.db.
 Elpi Accumulate lp:{{
@@ -159,6 +161,7 @@ Elpi Accumulate lp:{{
     InitialGoal = goal _Context _ G _ [],
     util.when-debug dbg.full (coq.say "goal" G),
     translate-goal G (pc map0 map1) G' GR,
+    util.when-debug dbg.full (coq.say "trocq:" G "~" G' "by" GR),
     FinalProof = {{ @comap lp:G lp:G' lp:GR (_ : lp:G') }},
     util.when-debug dbg.full (coq.say FinalProof),