chore: delete fin_destr code

alexkeizer · May 20, 2024 · 1e0f7ea · 1e0f7ea
1 parent cefe5e6
commit 1e0f7ea
Show file tree

Hide file tree

Showing 6 changed files with 14 additions and 110 deletions.
diff --git a/Qpf/Examples/_02_Tree.lean b/Qpf/Examples/_02_Tree.lean
@@ -1,6 +1,5 @@
 import Qpf
 import Qpf.Examples._01_List
-import Qpf.Macro.Tactic.FinDestr
 
 open MvQPF
 

diff --git a/Qpf/Macro/Tactic/FinDestr.lean b/Qpf/Macro/Tactic/FinDestr.lean
diff --git a/Qpf/PFunctor/Multivariate/Constructions/Arrow.lean b/Qpf/PFunctor/Multivariate/Constructions/Arrow.lean
@@ -2,7 +2,6 @@ import Mathlib.Data.QPF.Multivariate.Basic
 import Mathlib.Tactic.FinCases
 
 import Qpf.Util
-import Qpf.Macro.Tactic.FinDestr
 import Qpf.PFunctor.Multivariate.Basic
 
 namespace MvQPF

diff --git a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
@@ -6,7 +6,6 @@ import Mathlib.Data.QPF.Multivariate.Basic
 import Mathlib.Tactic.FinCases
 
 import Qpf.Util
-import Qpf.Macro.Tactic.FinDestr
 import Qpf.Qpf.Multivariate.Basic
 
 namespace MvQPF

diff --git a/Qpf/PFunctor/Multivariate/Constructions/Sum.lean b/Qpf/PFunctor/Multivariate/Constructions/Sum.lean
@@ -5,7 +5,6 @@
 import Mathlib.Data.QPF.Multivariate.Basic
 import Mathlib.Tactic.FinCases
 
-import Qpf.Macro.Tactic.FinDestr
 import Qpf.Util
 import Qpf.Qpf.Multivariate.Basic
 

diff --git a/Qpf/Qpf/Multivariate/ofPolynomial.lean b/Qpf/Qpf/Multivariate/ofPolynomial.lean
@@ -1,38 +1,37 @@
 import Mathlib.Data.QPF.Multivariate.Basic
 import Qpf.Util
-import Qpf.Macro.Tactic.FinDestr
 
 /-!
-  This file provides a way to show some typefunction `F` is a QPF by establishing an isomorphism 
+  This file provides a way to show some typefunction `F` is a QPF by establishing an isomorphism
   to some polynomial functor `P`
 
   This is especially useful to show functoriality of external type functions, which are not
   easily redefined in terms of `MvPFunctor`
 -/
 
-namespace MvFunctor 
+namespace MvFunctor
   /-- If `F` is isomorphic to a MvFunctor `F'`, then `F` is also a MvFunctor -/
   def ofIsomorphism {F : TypeFun n}
                     (F' : TypeFun n)
                     [q : MvFunctor F']
-                    (box    : ∀{α}, F α → F' α) 
-                    (unbox  : ∀{α}, F' α → F α) 
+                    (box    : ∀{α}, F α → F' α)
+                    (unbox  : ∀{α}, F' α → F α)
                   : MvFunctor F
     where
       map f a     := unbox <| q.map f <| box a
 end MvFunctor
 
 namespace MvQPF
   /-- If `F` is isomorphic to a QPF `F'`, then `F` is also a QPF -/
-  def ofIsomorphism {F : TypeFun n} 
+  def ofIsomorphism {F : TypeFun n}
                     (F' : TypeFun n)
                     [functor' : MvFunctor F']
                     [functor : MvFunctor F]
                     [q : MvQPF F']
-                    (box    : ∀{α}, F α → F' α) 
-                    (unbox  : ∀{α}, F' α → F α) 
+                    (box    : ∀{α}, F α → F' α)
+                    (unbox  : ∀{α}, F' α → F α)
                     (box_unbox_id : ∀{α} (x : F' α), box (unbox x) = x)
-                    (unbox_box_id : ∀{α} (x : F α), unbox (box x) = x 
+                    (unbox_box_id : ∀{α} (x : F α), unbox (box x) = x
                                   := by intros; rfl
                                 )
                     (map_eq : ∀ (α β : TypeVec n) (f : TypeVec.Arrow α β) (a : F α), functor.map f a = (unbox <| functor'.map f <| box a) := by intros; rfl)
@@ -41,19 +40,19 @@ namespace MvQPF
       P           := q.P
       abs         := unbox ∘ q.abs
       repr        := q.repr ∘ box
-      abs_repr    := by 
-                      intros  
+      abs_repr    := by
+                      intros
                       simp only [q.abs_repr, unbox_box_id, Function.comp]
-      abs_map f x := by 
+      abs_map f x := by
                       dsimp
                       rw [map_eq]
                       apply congrArg
                       simp [box_unbox_id, q.abs_map]
 
   /-- If `F` is isomorphic to a polynomial functor `P'`, then `F` is a QPF -/
-  def ofPolynomial  {F : TypeFun n} 
+  def ofPolynomial  {F : TypeFun n}
                     (P : MvPFunctor n)
-    := @ofIsomorphism _ F P.Obj 
-  
+    := @ofIsomorphism _ F P.Obj
+
 
 end MvQPF