HO unif progress

apps/tc/elpi/compiler.elpi

@@ -58,19 +58,17 @@ compile-aux IsPositive (prod N T F) I RevPremises ListVar Clause :- !,
     (Clause = (pi x\ decl x N T => C x), E = x\[locally-bound x]),
   pi p\ decl p N T => E p => 
     compile-aux-premise IsPositive p T (F p) I RevPremises ListVar (C p).
-% hypothetical instance
+% hypothetical instance (I is a name)
 compile-aux IsPositive Ty I RevPremises ListVar Clause :- 
   ho-twin I X _ TyI, not (ListVar = []) ,!,
   name AppInst X {std.rev ListVar},
   std.unsafe-cast X XX,
   HOPremise = (ho-link I TyI XX),
-  (pi A B C D\ fold-map A B C D :- subst-ho A B C D, !) => fold-map Ty [] TyX HOPremisesRev,
-  std.rev HOPremisesRev HOPremises,
+  ho-preprocess Ty TyX HOPremises,
   compile-aux-conclusion IsPositive TyX AppInst [HOPremise|HOPremises] RevPremises Clause.
 compile-aux IsPositive Ty I RevPremises ListVar Clause :- 
   coq.mk-app I {std.rev ListVar} AppInst,
-  (pi A B C D\ fold-map A B C D :- subst-ho A B C D, !) => fold-map Ty [] TyX HOPremisesRev,
-  std.rev HOPremisesRev HOPremises,
+  ho-preprocess Ty TyX HOPremises,
   compile-aux-conclusion IsPositive TyX AppInst HOPremises RevPremises Clause.
 
 pred compile-aux-conclusion i:bool, i:term, i:term, i:list prop, i:list prop, o:prop.

apps/tc/elpi/ho_unif.elpi

@@ -8,10 +8,26 @@ unify-FO L ArgsNo Head Args :- std.do! [
   coq.mk-app HD Extra Head,
 ].
 
+:index (1)
+pred is-coq-term i:A.
+is-coq-term (sort _).
+is-coq-term (global _).
+is-coq-term (pglobal _ _).
+is-coq-term (app _).
+is-coq-term (fun _ _ _).
+is-coq-term (prod _ _ _ ). 
+is-coq-term (fix _ _ _ _ ). 
+is-coq-term (match _ _ _). 
+is-coq-term (let _ _ _ _).
+is-coq-term (primitive _).
+
 pred locally-bound i:term.
 
 pred build-fun i:term, i:A, o:term.
-build-fun (prod N T Bo) V (fun N T (Bo1)) :- !,
+build-fun (prod N T Bo) V (fun N T Bo1) :- 
+  is-coq-term V, !,
+  pi x\ build-fun (Bo x) {coq.mk-app V [x]} (Bo1 x).
+build-fun (prod N T Bo) V (fun N T Bo1) :- !,
   pi x\ build-fun (Bo x) (V x) (Bo1 x).
 build-fun _ V V.
 
@@ -21,28 +37,57 @@ coq.reduction.eta-expand N P Acc (x\ Q x) :- N > 0, M is N - 1,
   pi x\ coq.reduction.eta-expand M P [x|Acc] (Q x).
 
 pred ho-link o:term, i:term, o:A.
-ho-link C Ty E :- var E, not (var C), !, coq.count-prods Ty N, coq.reduction.eta-expand N C [] E.
-ho-link C Ty E :- var C, not (var E), !, build-fun Ty E ETA, coq.reduction.eta-contract ETA C.
-ho-link C Ty E :- not (var C), not (var E), !, same-eta C Ty [] E.
-ho-link O I A :- coq.error "ho-link:" O I A.
+:name "ho-link"
+ho-link C Ty E :- var E, not (var C), !, 
+  coq.count-prods Ty N, coq.reduction.eta-expand N C [] E.
+ho-link C Ty E :- var C, not (var E), !, 
+  build-fun Ty E ETA, coq.reduction.eta-contract ETA C.
+ho-link C Ty E :- not (var C), not (var E), !, 
+  coq.say "C" C, same-eta C Ty [] E.
+ho-link C Ty E :- build-fun Ty E C', C' = C.
 
 pred same-eta i:term, i:term, i:list term, i:A.
-same-eta C (prod _ _ F) V E :- pi x\ same-eta C (F x) [x|V] (E x).
+:name "same-eta1"
+same-eta C (prod _ _ F) V E :- !, pi x\ same-eta C (F x) [x|V] (E x).
+:name "same-eta2"
 same-eta C _ VarsRev E :-
   coq.mk-app C {std.rev VarsRev} CVars,
   hd-beta E [] Hd Args, coq.mk-app Hd Args EVars,
   std.assert! (same_term CVars EVars) "eta mess".
 
+pred build-fun1 i:int, i:list term, o:term, o:term.
+build-fun1 0 L _ APP :- prune F_ [], std.rev L L1, APP = app [F_ | L1].
+build-fun1 N L _ (fun _ _ X) :-
+   N > 0, N1 is N - 1, pi x\
+  build-fun1 N1 [x|L] _ (X x).
+
+pred coq-intros i:list term, i:list term, i:list term, o:term, o:A.
+coq-intros SC [] V K K :-
+  std.append SC {std.rev V} L, prune K L.
+coq-intros SC [HD|L] LL (fun `elpi_intro` Ty Bo) E :-
+  coq.typecheck HD Ty ok,
+  pi x\ coq-intros SC L [x | LL] (Bo x) (E x).
+
 pred subst-ho i:term, i:A, o:term, o:A.
 % pattern fragment 
-subst-ho (app [X|XS]) A YXS A1 :- ho-twin X Y _ Ty, distinct_names XS, std.forall XS locally-bound, !,
+subst-ho (app [X|XS]) A YXS A1 :- 
+  name X, ho-twin X Y _ Ty, distinct_names XS, std.forall XS locally-bound, !,
   name YXS Y XS,
   std.unsafe-cast Y Y1,
-  %build-fun Ty Y1 Fun,
   A1 = [ho-link X Ty Y1|A].
-subst-ho X A X A1 :- ho-twin X Y _ Ty, !, A1 = [ho-link X Ty Y|A].
+subst-ho X A X A :- var X, !.
+subst-ho (app [X|XArgs]) A R A1 :-
+  var X _ XScope,
+  std.append XScope XArgs Scope,
+  distinct_names Scope, !,
+  coq-intros XScope XArgs [] X' E,
+  hd-beta X' XArgs Aaa Baa,
+  coq.mk-app Aaa Baa R,
+  coq.typecheck X Ty ok,
+  A1 = [ ho-link X Ty E | A].
+subst-ho X A X A1 :- name X, ho-twin X Y _ Ty, !, A1 = [ho-link X Ty Y|A].
 % FO heuristic
-subst-ho (app [X|XS]) A (app L) A2 :- ho-twin X Y L Ty, !,
+subst-ho (app [X|XS]) A (app L) A2 :- name X, ho-twin X Y L Ty, !,
   std.length XS NARGS,
   std.fold-map XS A fold-map YS A1,
   A2 = [ho-link X Ty Y,unify-FO L NARGS X YS|A1].
@@ -52,7 +97,15 @@ subst-ho (prod N T F) A (prod N T1 F1) A2 :- !,
 subst-ho (fun N T F) A (fun N T1 F1) A2 :- !,
   fold-map T A T1 A1, (pi x\ locally-bound x => fold-map (F x) A1 (F1 x) A2).
 
+pred ho-preprocess i:term, o:term, o:list prop.
+ho-preprocess Ty TyX HOPremises :-
+  (pi A B C D\ fold-map A B C D :- subst-ho A B C D, !) => 
+    fold-map Ty [] TyX HOPremisesRev,
+  std.rev HOPremisesRev HOPremises.
+
 % [ho-twin Coq ElpiHO ElpiFO CoqVarTy]
 % app[Coq|Args] -> (app ElpiFO)    / unif-FO ElpiFO N Coq Args
 % app[Coq|Args] -> (ElpiHO Args)   / ho-link Coq CoqVarTy ElpiHO
 pred ho-twin i:term, o:A, o:list term, o:term.
+ho-twin X Y_ Z_ Ty :- var X, !, 
+  coq.typecheck X Ty ok.

apps/tc/elpi/solver.elpi

@@ -35,33 +35,20 @@ build-hypotheses Ctx Clauses :-
   std.append Ctx {section-var->decl} CtxAndSection,
   compile-ctx CtxAndSection Clauses. 
 
-
-namespace ho-goal {
-  % [pf-search T L] lists the terms on which doing HO unification
-  pred pf-search i:term, o:list term.
-  pf-search T S :-
-    (pi T HD TL Acc\ fold-map T ACC _ [T | ACC] :- not (var T), app [HD|TL] = T, var HD, distinct_names TL) => 
-    fold-map T [] _ S.
-
-  pred ho-twin i:term, o:term.
-}
-
 pred tc-recursive-search.aux i:term, i:list term, i:list term, o:term.
-tc-recursive-search.aux T [] L Proof :-
-  std.do![copy T Ty,
-  coq.safe-dest-app Ty (global TC) TL',
-  std.append TL' [Proof] TL,
-  coq.elpi.predicate {gref->pred-name TC} TL Q], Q,
-  std.forall L (x\ sigma TW\ ho-goal.ho-twin x TW, coq.unify-eq x TW ok).
-tc-recursive-search.aux T [HD | TL] L S :-
-  ho-goal.ho-twin HD F_ => copy HD F_ => tc-recursive-search.aux T TL L S.
+tc-recursive-search.aux T _ _ Proof :-
+  ho-preprocess T Ty PostProcess,
+  std.do![
+    coq.safe-dest-app Ty (global TC) TL',
+    std.append TL' [Proof] TL,
+    coq.elpi.predicate {gref->pred-name TC} TL Q], 
+  do [Q | PostProcess].
 
 
 % [tc-recursive-search Goal Solution] takes the type of the goal and solves it
 pred tc-recursive-search i:term, o:term.
 tc-recursive-search Goal Sol :- 
   std.time (
-    ho-goal.pf-search Goal PFVar,
     tc-recursive-search.aux Goal PFVar PFVar Sol
   ) Time,
   if-true (is-option-active oTC-time-instance-search) 

apps/tc/tests/test_HO.v

@@ -65,6 +65,25 @@ Module FO_app1.
 
 End FO_app1.
 
+Module FO_app2.
+
+  Context (A B : Type).
+
+  Class Functional (B: Type).
+
+  Instance s1 F: Functional (F A) -> Functional (F A). Qed.
+
+  Elpi Print TC.Solver.
+
+  Definition F (x : Type) := Type.
+  Context (H : Functional (F B)).
+
+  Goal Functional (F A).
+    apply s1, H.
+  Qed.
+
+End FO_app2.
+
 (************************************************************************)
 
 Module HO_PF.
@@ -113,20 +132,50 @@ End HO_PF.
 Module HO_PF1.
   Parameter A : Type.
   Class Decision (P : Type).
+  (* Global Hint Mode Decision ! : typeclass_instances. *)
+
   Class Exists (P : A -> Type) (l : A).
   Instance Exists_dec (P : A -> Type): (forall x, Decision (P x)) -> forall l, Decision (Exists P l). Qed.
 
-  Goal forall (P : A -> Prop) l, (forall x, Decision (P x)) -> Decision (Exists P l).
-  apply _.
+ Lemma ho_in_elpi (P1: A -> Prop) l:
+    exists (P : A -> A -> A -> Prop), forall z y , (forall x, Decision (P1 x)) 
+      -> Decision (Exists (P z y) l) /\ P z y y = P1 z.
+  Proof.
+    eexists; intros.
+    split.
+    (* We take the most general solution for P, it picks P = (fun a b c => P1 ?x) *)
+    apply _.
+    simpl.
+    (* Reflexivity fix ?x = a hence (fun a b c => P1 a) z y y = P1 z is solvable *)
+    reflexivity.
   Qed.
 
-  Lemma ho_in_goal z (P1: A -> Prop) l:
-    exists (P : A -> A -> Prop), (forall x, Decision (P1 x)) 
-      -> Decision (Exists (P z) l).
+ Lemma ho_in_coq (P1: A -> Prop) l:
+    exists (P : A -> A -> A -> Prop), forall z y , (forall x, Decision (P1 x)) 
+      -> Decision (Exists (P z y) l) /\ P z y y = P1 z.
   Proof.
-    eexists.
+    Elpi Override TC TC.Solver None.
+    eexists; intros.
+    split.
+    (* Coq doesn't give the most general solution for P, it picks P = (fun _ _ x => P1 x) *)
     apply _.
-  Qed.
+    simpl.
+    Fail reflexivity.
+  Abort.
+
+  Section test.
+
+    Axiom (P1: Type -> Prop).
+    Context (H : Decision (P1 nat)).
+    Goal exists P, forall (x y:A) , Decision (P x y).
+    Proof.
+      eexists; intros.
+      Set Printing Existential Instances.
+      apply _.
+    Abort.
+
+  End test.
+
 End HO_PF1.