refactor: remove IsPolynomial class (#55)

I added the IsPolynomial typeclass as an experiment to see if we could use typeclass synthesis to keep track of QPFs whose quotient is trivial (in the sense that the QPF is isomorphic to the underlying polynomial functor).

This hasn't really worked out, and as it stands the definition of IsPolynomial is broken: it takes in an [MvFunctor _] instance argument, even though it already extends MvQPF _, which was refactored to extend MvFunctor _, meaning we now have multiple instances of MvFunctor floating around.

We could fix this fairly easily, but I think long-term it will be much easier to just write meta-code that optimistically keeps track of which QPFs are just PFunctors, rather than to use typeclass synthesis to recover this information after the fact. Thus, we should remove IsPolynomial alltogether

Qpf/Macro/Comp.lean

@@ -23,6 +23,7 @@ import Mathlib.Data.QPF.Multivariate.Constructions.Prj
 import Mathlib.Data.Vector.Basic
 
 import Qpf.Qpf
+import Qpf.Qpf.Multivariate.Basic
 import Qpf.Macro.Common
 
 import Qq
@@ -49,7 +50,7 @@ def synthMvFunctor {n : Nat} (F : Q(TypeFun.{u,u} $n)) : MetaM Q(MvFunctor $F) :
     q(MvFunctor $F)
   synthInstanceQ inst_type
 
-def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) (_ : Q(MvFunctor $F)) : MetaM Q(MvQPF $F) := do
+def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) : MetaM Q(MvQPF $F) := do
   let inst_type : Q(Type (u+1)) :=
     q(MvQPF $F)
   synthInstanceQ inst_type
@@ -87,10 +88,9 @@ where
     try
       -- Only try to infer QPF if `F` contains no live variables
       if !F.hasAnyFVar isLiveVar then
-        let F : Q(TypeFun.{u,u} $depth)
-          := q(TypeFun.ofCurried $F)
-        let functor ← synthMvFunctor F
-        let _ ← synthQPF F functor
+        let F : Q(TypeFun.{u,u} $depth) :=
+          q(TypeFun.ofCurried $F)
+        let _ ← synthQPF F
         return ⟨depth, F, args⟩
       throwError "Smallest function subexpression still contains live variables:\n  {F}\ntry marking more variables as dead"
     catch e =>
@@ -106,8 +106,7 @@ where
       trace[QPF] "F := {F}\nargs := {args.toList}\ndepth := {depth}"
       let F : Q(TypeFun.{u,u} $depth)
         := q(TypeFun.ofCurried $F)
-      let functor ← synthMvFunctor F
-      let _ ← synthQPF F functor
+      let _ ← synthQPF F
       return ⟨depth, F, args⟩
 
 
@@ -213,7 +212,6 @@ partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermEl
   else
     let G ← args.mmap (elabQpf vars · none false)
 
-    let Ffunctor ← synthInstanceQ q(MvFunctor $F)
     let Fqpf ← synthInstanceQ q(@MvQPF _ $F)
 
     let G : Vec _ numArgs := fun i => G.get i.inv
@@ -313,14 +311,17 @@ def elabQpfCompositionBody (view: QpfCompositionBodyView) :
       res.F.check
       res.qpf.check
 
-      withOptions (fun opt => opt.insert `pp.explicit true) <| do
+      let (F, qpf) ← withOptions (fun opt => opt.insert `pp.explicit true) <| do
         let F ← delab res.F
         let qpf ← delab res.qpf
+        pure (F, qpf)
 
-        withQPFTraceNode "results …" <| do
-          trace[QPF] "Functor := {F}"
-          trace[QPF] "MvQPF instance := {qpf}"
-        return ⟨F, qpf⟩
+      withQPFTraceNode "results …" <| do
+        trace[QPF] "Functor (expr) := {res.F}"
+        trace[QPF] "Functor (stx)  := {F}"
+        trace[QPF] "MvQPF   (expr) := {res.qpf}"
+        trace[QPF] "MvQPF   (stx)  := {qpf}"
+      return ⟨F, qpf⟩
 
 
 structure QpfCompositionView where
@@ -385,10 +386,6 @@ def elabQpfComposition (view: QpfCompositionView) : CommandElabM Unit := do
   let F_applied ← `($F $deadBinderNamedArgs:namedArgument*)
 
   let cmd ← `(
-    $modifiers:declModifiers
-    instance : MvFunctor (TypeFun.ofCurried $F_applied) :=
-      MvQPF.instMvFunctor_ofCurried_curried
-
     $modifiers:declModifiers
     instance $deadBindersNoHoles:bracketedBinder* : MvQPF (TypeFun.ofCurried $F_applied) :=
       MvQPF.instQPF_ofCurried_curried

Qpf/Macro/Data.lean

@@ -304,8 +304,8 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
       map f x   := ($eqv).invFun <| ($P).map f <| ($eqv).toFun <| x
   )
   elabCommandAndTrace (header := "defining {q}") <|← `(
-    instance $q:ident : MvQPF.IsPolynomial (@TypeFun.ofCurried $(quote arity) $shape) :=
-      .ofEquiv $P $eqv
+    instance $q:ident : MvQPF (@TypeFun.ofCurried $(quote arity) $shape) :=
+      .ofEquiv (fun _ => $eqv)
   )
 
 /-! ## mkShape -/
@@ -382,33 +382,6 @@ def mkShape (view : DataView) : TermElabM MkShapeResult := do
     mkQpf view ctorArgs headTId PId r.expr.size
   ⟩
 
-open Elab.Term Parser.Term in
-/--
-  Checks whether the given term is a polynomial functor, i.e., whether there is an instance of
-  `IsPolynomial F`, and return that instance (if it exists).
--/
-def isPolynomial (view : DataView) (F: Term) : CommandElabM (Option Term) :=
-  withQPFTraceNode "isPolynomial" (tag := "isPolynomial") <|
-  runTermElabM fun _ => do
-  elabBinders view.deadBinders fun _deadVars => do
-    let inst_func ← `(MvFunctor $F:term)
-    let inst_func ← elabTerm inst_func none
-
-    trace[QPF] "F = {F}"
-    let inst_type ← `(MvQPF.IsPolynomial $F:term)
-    trace[QPF] "inst_type_stx: {inst_type}"
-    let inst_type ← elabTerm inst_type none
-    trace[QPF] "inst_type: {inst_type}"
-
-    try
-      let _ ← synthInstance inst_func
-      let inst ← synthInstance inst_type
-      return some <|<- delab inst
-    catch e =>
-      trace[QPF] "Failed to synthesize `IsPolynomial` instance.\
-        \n\n{e.toMessageData}"
-      return none
-
 /--
   Take either the fixpoint or cofixpoint of `base` to produce an `Internal` uncurried QPF,
   and define the desired type as the curried version of `Internal`

Qpf/PFunctor/Multivariate/Constructions/Prod.lean

@@ -6,31 +6,26 @@ import Mathlib.Data.QPF.Multivariate.Basic
 import Mathlib.Tactic.FinCases
 
 import Qpf.Util
-import Qpf.Qpf.Multivariate.Basic
 
 namespace MvQPF
 namespace Prod
 
 open PFin2 (fz fs)
 
-def P : MvPFunctor.{u} 2 := 
+def P : MvPFunctor.{u} 2 :=
   .mk PUnit fun _ _ => PFin2 1
 
 
 abbrev QpfProd' := P.Obj
 abbrev QpfProd  := TypeFun.curried QpfProd'
 
-/--
-  An uncurried version of the root `Prod`
--/
-abbrev Prod' : TypeFun 2
-  := @TypeFun.ofCurried 2 Prod
+/-- An uncurried version of the root `Prod` -/
+def Prod' : TypeFun 2 :=
+  @TypeFun.ofCurried 2 Prod
 
 
-/--
-  Constructor for `QpfProd'`
--/
-def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ := 
+/-- Constructor for `QpfProd'` -/
+def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ :=
   ⟨
       ⟨⟩,
       fun
@@ -56,8 +51,9 @@ def equiv {Γ} : Prod' Γ ≃ QpfProd' Γ := {
 instance : MvFunctor Prod' where
   map f x   := equiv.invFun <| P.map f <| equiv.toFun <| x
 
-instance : MvQPF.IsPolynomial Prod' := .ofEquiv _ equiv
-
+instance : MvQPF Prod' := .ofEquiv (fun _ => equiv)
+instance : MvQPF (@TypeFun.ofCurried 2 Prod) :=
+  inferInstanceAs (MvQPF Prod')
 
 end Prod
 

Qpf/PFunctor/Multivariate/Constructions/Sum.lean

@@ -6,7 +6,6 @@ import Mathlib.Data.QPF.Multivariate.Basic
 import Mathlib.Tactic.FinCases
 
 import Qpf.Util
-import Qpf.Qpf.Multivariate.Basic
 
 namespace MvQPF
 namespace Sum
@@ -38,7 +37,7 @@ def inr {Γ : TypeVec 2} (b : Γ 0) : QpfSum' Γ
     ⟩
 
 
-abbrev Sum' := @TypeFun.ofCurried 2 Sum
+def Sum' := @TypeFun.ofCurried 2 Sum
 
 def box {Γ : TypeVec 2} : Sum' Γ → QpfSum' Γ
   | .inl a => inl a
@@ -70,8 +69,9 @@ def equiv {Γ} : Sum' Γ ≃ QpfSum' Γ :=
 instance : MvFunctor Sum' where
   map f x   := equiv.invFun <| SumPFunctor.map f <| equiv.toFun <| x
 
-instance : MvQPF.IsPolynomial Sum' :=
-  .ofEquiv _ equiv
+instance : MvQPF Sum' := .ofEquiv @equiv
+instance : MvQPF (@TypeFun.ofCurried 2 Sum) :=
+  inferInstanceAs (MvQPF Sum')
 
 end Sum
 

Qpf/Qpf.lean

@@ -1,6 +1,4 @@
 
-import Qpf.Qpf.Multivariate.Basic
-
 import Qpf.PFunctor.Multivariate.Basic
 import Qpf.PFunctor.Multivariate.Constructions.Arrow
 import Qpf.PFunctor.Multivariate.Constructions.Prod

Qpf/Qpf/Multivariate/Basic.lean

@@ -2,86 +2,14 @@ import Mathlib.Data.QPF.Multivariate.Basic
 import Qpf.Util.TypeFun
 
 namespace MvQPF
-  /--
-    A QPF is polynomial, if it is equivalent to the underlying `MvPFunctor`.
-    `repr_abs` is the last property needed to show that `abs` is an isomorphism, with `repr`
-    its inverse
-  -/
-  class IsPolynomial {n} (F : TypeVec n → Type _) extends MvQPF F where
-    repr_abs : ∀ {α} (x : P.Obj α), repr (abs x) = x
-
-
-  namespace IsPolynomial
-    variable {n : ℕ} {F : TypeVec n → Type _}
-
-    /--
-      Show that the desired equivalence follows from `IsPolynomial`
-    -/
-    def equiv [MvFunctor F] [p : IsPolynomial F] :
-      ∀ α, F α ≃ p.P.Obj α
-    := fun _ => {
-      toFun := p.repr,
-      invFun := p.abs,
-      left_inv := p.abs_repr,
-      right_inv := p.repr_abs,
-    }
-
-    def ofEquiv (P : MvPFunctor n) (eqv : ∀ {α}, F α ≃ P.Obj α) [functor : MvFunctor F] (map_eq : ∀ (α β : TypeVec n) (f : TypeVec.Arrow α β) (x : F α), functor.map f x = (eqv.invFun <| P.map f <| eqv.toFun <| x) := by intros; rfl) : IsPolynomial F where
-      P         := P
-      abs       := eqv.invFun
-      repr      := eqv.toFun
-      abs_repr  := eqv.left_inv
-      abs_map   := by intros;
-                      simp only [Equiv.invFun_as_coe, map_eq, Equiv.toFun_as_coe,
-                                 Equiv.apply_symm_apply, Equiv.symm_apply_apply, EmbeddingLike.apply_eq_iff_eq];
-                      rfl
-      repr_abs  := eqv.right_inv
-
-  end IsPolynomial
-
-end MvQPF
-
-namespace MvPFunctor
-  variable {n : Nat} (P : MvPFunctor n)
-
-  /--
-    Every polynomial functor is trivially a QPF
-  -/
-  instance : MvQPF P.Obj :=
-  {
-    P         := P,
-    abs       := id,
-    repr      := id,
-    abs_repr  := by intros; rfl,
-    abs_map   := by intros; rfl,
-  }
-
-  /--
-    Every polynomial functor is a polynomial QPF
-  -/
-  instance : MvQPF.IsPolynomial P.Obj :=
-  {
-    repr_abs := by intros; rfl
-  }
-
-end MvPFunctor
-
-
 variable {n} {F : TypeFun n}
 
-namespace MvQPF
-  instance instMvFunctor_ofCurried_curried [f : MvFunctor F] :
-      MvFunctor <| TypeFun.ofCurried <| F.curried :=
-    TypeFun.ofCurried_curried_involution ▸ f
-
-  instance instQPF_ofCurried_curried [MvFunctor F] [q : MvQPF F] :
-      MvQPF <| TypeFun.ofCurried <| F.curried :=
-    TypeFun.ofCurried_curried_involution ▸ q
+instance instMvFunctor_ofCurried_curried [f : MvFunctor F] :
+    MvFunctor <| TypeFun.ofCurried <| F.curried :=
+  TypeFun.ofCurried_curried_involution ▸ f
 
-  instance instIsPolynomial_ofCurried_curried [functor : MvFunctor F] [p : IsPolynomial F] :
-      IsPolynomial <| TypeFun.ofCurried <| F.curried := by
-    apply cast ?_ p
-    congr
-    · rw [TypeFun.ofCurried_curried_involution]
+instance instQPF_ofCurried_curried [q : MvQPF F] :
+    MvQPF <| TypeFun.ofCurried <| F.curried :=
+  TypeFun.ofCurried_curried_involution ▸ q
 
 end MvQPF