[TC] canonical proj solved with coq.unify-eq

Author: FissoreD

apps/tc/elpi/ho_compile.elpi

@@ -24,6 +24,11 @@ namespace tc {
         decompile-term-aux (sort _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (uvar as X) L X L :- !.
         decompile-term-aux (primitive _ as X) L X L :- !.
+        decompile-term-aux (tc.canonical-projection T S _) (pr [X|Xs] L1) Y (pr Xs' L3) :- !,
+          name Y X S,
+          decompile-term-aux T (pr Xs L1) T' (pr Xs' L2),
+          P = coq.unify-eq Y T' ok,
+          L3 = [P | L2].
 
         decompile-term-aux (tc.maybe-eta-tm T S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- !,
           name Y X S,

apps/tc/elpi/ho_precompile.elpi

@@ -106,6 +106,8 @@ namespace tc {
       precompile-aux _ (pglobal _ _ as C) A C A :- !.
       precompile-aux _ (sort _ as C) A C A :- !.
       precompile-aux _ (primitive _ as C) A C A :- !.
+      precompile-aux _ (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) (s A) :- coq.env.projection? C N, !, free-var Scope.
+      precompile-aux _ (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) (s A) :- coq.env.primitive-projection? P _, !, free-var Scope.
 
       % Detect maybe-eta term
       % TODO: should I precompile also the type of the fun and put it in the output term
@@ -173,7 +175,7 @@ namespace tc {
                 (tc.prod-range (prod _ T Bo) 3)
               since x is applied at most 3 times in Bo
                 ==> This helps charging the right number of `eta-link` for map-deduplication rule
-        N is the number of problematic terms in T
+        N is the number of problematic terms in T + nb of projections
     */
     pred instance i:term, o:term, o:nat, o:list univ, o:list univ-instance.
     instance T T' N UnivConstL UnivInstL :-

apps/tc/elpi/tc_aux.elpi

@@ -213,3 +213,9 @@ namespace tc {
     list term ->     % The eta-expanded version of X, from X^{len(PF)} to X^{len(PF)+len(NPF)}
     term.
 }
+
+type tc.canonical-projection
+  term ->       % The current precompiled subterm
+  list term ->  % The list of FV in the precomp subterm
+  int ->
+  term.

apps/tc/tests/canonical_struct.v

@@ -0,0 +1,102 @@
+From elpi.apps Require Import tc.
+
+Module CS1.
+
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Class C (I : Type).
+
+  Instance c : C (ofe_car ofe_nat). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS1.
+
+Module CS2.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Class C (I : Type).
+
+  Instance c : C (Ofe nat). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS2.
+
+(* With primitive projection *)
+Module CS3.
+  Class C (I : Type).
+
+  #[local] Set Primitive Projections.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Instance c : C ofe_nat.(ofe_car). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS3.
+
+Module CS4.
+  Class C (I : Type).
+
+  #[local] Set Primitive Projections.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Instance c : C (Ofe nat).(ofe_car). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS4.
+
+(* With bound variables *)
+Module CS5.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_any x : ofe := Ofe x.
+
+  Class C (I : Type -> Type).
+  Axiom f : ofe -> Type.
+
+  Instance c X : C (fun x => (Ofe (f (X x)))). Qed.
+  Goal C (fun x => (Ofe (f x))). apply _. Qed. (* No CS search *)
+  Goal C (fun (_: Type) => Ofe (f nat)). apply _. Qed. (* CS Search to assign x *)
+  Goal exists X, C (fun y => ofe_car (X y)). eexists.
+    apply _.
+    Unshelve.
+    apply (ofe_any nat).
+  Qed.
+
+  Lemma coq_unif_fail: exists X Y, (fun (y: Type) => ofe_car (X y)) = (fun _ => Y).
+    do 2 eexists.
+    Fail reflexivity.
+  Abort.
+    
+  Goal exists Z, C (fun _ => Z). eexists.
+    (* 
+      Note that here, coq8.20 unification algorithm would fail to unify
+      with error 
+        Unable to unify "?Y" with "ofe_car (?X x)" as "ofe_car (?X x)" 
+        contains local variables.
+    *)
+    apply _.
+    Unshelve.
+    apply (ofe_any nat).
+  Qed.
+End CS5.