From 789630cb25b7f005999d43a17eacc801bc328d3c Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Fri, 17 May 2024 21:04:38 +0100
Subject: [PATCH] chore: upgrade to Lean v4.7.0

---
 Qpf/Builtins/List.lean                        | 20 +++++------
 Qpf/Macro/Comp.lean                           |  2 +-
 Qpf/Macro/Data.lean                           | 29 +++------------
 Qpf/Macro/Tactic/FinDestr.lean                | 18 +++++-----
 Qpf/MathlibPort/Fin2.lean                     |  1 -
 .../Multivariate/Constructions/Prod.lean      | 10 +++---
 Qpf/Qpf/Multivariate/Constructions/Comp.lean  | 35 +++++++++----------
 Qpf/Util/TypeFun.lean                         | 23 ++++++------
 Qpf/Util/Vec.lean                             |  9 ++---
 lake-manifest.json                            | 18 +++++-----
 lakefile.lean                                 |  2 +-
 lean-toolchain                                |  2 +-
 12 files changed, 71 insertions(+), 98 deletions(-)

diff --git a/Qpf/Builtins/List.lean b/Qpf/Builtins/List.lean
index cb4820c..faf31eb 100644
--- a/Qpf/Builtins/List.lean
+++ b/Qpf/Builtins/List.lean
@@ -6,7 +6,7 @@ import Qpf.Macro.Data
 import Qpf.Qpf.Multivariate.ofPolynomial
 import Qpf.Util
 
-namespace MvQPF 
+namespace MvQPF
 namespace List
 
   def ListPFunctor : MvPFunctor.{u} 1
@@ -16,15 +16,15 @@ namespace List
   abbrev QpfList' := ListPFunctor.Obj
   abbrev List' := @TypeFun.ofCurried 1 List
 
-  abbrev box {Γ} (x : List' Γ) : QpfList' Γ 
+  abbrev box {Γ} (x : List' Γ) : QpfList' Γ
     := ⟨
-        ULift.up x.length, 
+        ULift.up x.length,
         fun .fz j => Vec.ofList x (PFin2.toFin2 j)
       ⟩
 
-  abbrev unbox {Γ} (x : QpfList' Γ) : List' Γ 
+  abbrev unbox {Γ} (x : QpfList' Γ) : List' Γ
     := Vec.toList fun i => x.snd 0 (PFin2.ofFin2 i)
-    
+
   private theorem typeext {α} {f g : α → Sort _} (f_eq_g: f = g) :
     ((a : α) → f a) = ((a : α) → g a) :=
   by
@@ -34,7 +34,7 @@ namespace List
   instance : MvFunctor List' :=
     MvFunctor.ofIsomorphism _ box unbox
 
-  instance : MvQPF List' := 
+  instance : MvQPF List' :=
     .ofIsomorphism _ box unbox (
       by
         intros Γ x;
@@ -59,19 +59,17 @@ namespace List
           apply HEq.trans cast_fun_arg
           rfl
 
-        case H₃ => 
+        case H₃ =>
           apply typeext;
           fin_destr;
 
           simp only [ListPFunctor, TypeVec.Arrow, DVec];
-          have : List.length (unbox { fst := { down := n }, snd := v }) = n; {
-            simp
-          }
+          have : List.length (unbox { fst := { down := n }, snd := v }) = n := by simp
           simp[this]
 
         case H₄ => intros; rfl
     ) (
-      by 
+      by
         intros _ x;
         induction x
         . rfl
diff --git a/Qpf/Macro/Comp.lean b/Qpf/Macro/Comp.lean
index cccf884..65ce150 100644
--- a/Qpf/Macro/Comp.lean
+++ b/Qpf/Macro/Comp.lean
@@ -178,7 +178,7 @@ partial def elabQpf {arity : Nat} (vars : Vector Q(Type u) arity) (target : Q(Ty
     | none      => throwError "Free variable {target} is not one of the qpf arguments"
     | some ind  => pure ind
 
-    let ind : Fin2 arity := cast (by simp) ind.inv
+    let ind : Fin2 arity := cast (by simp [vars']) ind.inv
     let prj := q(@Prj.{u} $arity $ind)
     trace[QPF] "represented by: {prj}"
     pure ⟨prj, q(Prj.mvfunctor _), q(Prj.mvqpf _)⟩
diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean
index e9cd778..eabc9de 100644
--- a/Qpf/Macro/Data.lean
+++ b/Qpf/Macro/Data.lean
@@ -150,23 +150,6 @@ def mkHeadT (view : InductiveView) : CommandElabM Name := do
   elabInductiveViews #[view]
   pure declName
 
-
-open Parser in
-private def matchAltsOfArray (matchAlts : Array Syntax) : Syntax :=
-  mkNode ``Term.matchAlts #[mkNullNode matchAlts]
-
-
-open Parser in
-/--
-  Wraps an array of `matchAltExpr` syntax objects into a single `Command.declValEqns` node, for
-  use in inductive definitions
--/
-private def declValEqnsOfMatchAltArray (matchAlts : Array Syntax) : TSyntax ``Command.declValEqns :=
-  let body := matchAltsOfArray matchAlts
-  let body := mkNode ``Term.matchAltsWhereDecls #[body, mkNullNode]
-  mkNode ``Command.declValEqns #[body]
-
-
 open Parser Parser.Term Parser.Command in
 /--
   Defines the "child" family of type vectors for an `n`-ary polynomial functor
@@ -190,11 +173,11 @@ def mkChildT (view : InductiveView) (r : Replace) (headTName : Name) : CommandEl
 
     `(matchAltExpr| | $head => (!![ $counts,* ]))
 
-  let body := declValEqnsOfMatchAltArray matchAlts
+  let body ← `(declValEqns|
+    $[$matchAlts:matchAlt]*
+  )
   let headT := mkIdent headTName
 
-
-
   let cmd ← `(
     def $declId : $headT → $target_type
       $body:declValEqns
@@ -403,11 +386,10 @@ def mkShape (view: DataView) : TermElabM MkShapeResult := do
     let childTId := mkIdent childTName
 
     elabCommand <|<- `(
-      def $PDeclId :=
+      def $PDeclId:declId :=
         MvPFunctor.mk $headTId $childTId
     )
 
-
     mkQpf view ctorArgs headTId PId r.expr.size
   ⟩
 
@@ -540,8 +522,7 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
 
     let cmd ← `(
       $(quote modifiers):declModifiers
-      def $declId:ident : $type
-        := $body:term
+      def $declId:ident : $type := $body:term
     )
 
     trace[QPF] "mkConstructor.cmd = {cmd}"
diff --git a/Qpf/Macro/Tactic/FinDestr.lean b/Qpf/Macro/Tactic/FinDestr.lean
index 0bf9075..29020ab 100644
--- a/Qpf/Macro/Tactic/FinDestr.lean
+++ b/Qpf/Macro/Tactic/FinDestr.lean
@@ -12,7 +12,7 @@ open Lean Syntax Elab Elab.Tactic Meta
 
 def elabFinDestrAux (i_stx : TSyntax `ident) : TacticM Unit := do
   let n ← mkFreshExprMVar (mkConst ``Nat) (kind:=MetavarKind.synthetic);
-  
+
   try {
     let u ← mkFreshLevelMVar;
     let us := [u]
@@ -38,7 +38,7 @@ def elabFinDestrAux (i_stx : TSyntax `ident) : TacticM Unit := do
   if let some n := n.natLit? then
     let rec genTactic : Nat → TacticM (TSyntax `tactic)
     | 0   =>  `(tactic| cases $i_stx:ident)
-    | n+1 => do 
+    | n+1 => do
               let tct ← genTactic n
               `(tactic| (cases $i_stx:ident; swap; rename_i $i_stx:ident; $tct:tactic))
 
@@ -47,7 +47,7 @@ def elabFinDestrAux (i_stx : TSyntax `ident) : TacticM Unit := do
 
   else
     let rec genTacticExpr : Expr → TacticM (Option <| TSyntax `tactic)
-      | Expr.const ``Nat.zero .. => 
+      | Expr.const ``Nat.zero .. =>
         `(tactic| cases $i_stx:ident)
 
       | Expr.app (Expr.const ``Nat.succ ..) n .. => do
@@ -66,26 +66,26 @@ elab "fin_destr_one " i:ident : tactic => do
   withMainContext <|
     elabFinDestrAux i
 
-syntax "fin_destr' " ident* : tactic 
+syntax "fin_destr' " ident* : tactic
 macro_rules
 | `(tactic| fin_destr' $i:ident $is:ident*) => `(tactic| fin_destr_one $i <;> dsimp (config := {failIfUnchanged := false}) <;> fin_destr' $is:ident*)
 | `(tactic| fin_destr') => `(tactic| skip)
 
-syntax "fin_destr " ident* : tactic 
+syntax "fin_destr " ident* : tactic
 macro_rules
-| `(tactic| fin_destr $i:ident $is:ident*) => `(tactic| 
-      fin_destr' $i:ident $is:ident* 
+| `(tactic| fin_destr $i:ident $is:ident*) => `(tactic|
+      fin_destr' $i:ident $is:ident*
       <;> try fin_destr
     )
 
-| `(tactic| fin_destr) => `(tactic| 
+| `(tactic| fin_destr) => `(tactic|
       first
       | intro i;  fin_destr i
       | funext i; fin_destr i
   )
 
 
-syntax "vec_eq " (tactic)? : tactic 
+syntax "vec_eq " (tactic)? : tactic
 macro_rules
 | `(tactic| vec_eq) => `(tactic| vec_eq trivial)
 | `(tactic| vec_eq $tct:tactic ) => `(tactic| funext i; fin_destr i <;> $tct:tactic)
diff --git a/Qpf/MathlibPort/Fin2.lean b/Qpf/MathlibPort/Fin2.lean
index a664101..f85458e 100644
--- a/Qpf/MathlibPort/Fin2.lean
+++ b/Qpf/MathlibPort/Fin2.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 
 import Mathlib.Data.Fin.Fin2
-import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Init.Order.Defs
 
 /-!
diff --git a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
index 292c1a4..5901867 100644
--- a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
+++ b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
@@ -12,9 +12,9 @@ namespace Prod
 
 open PFin2 (fz fs)
 
-def P : MvPFunctor 2 
+def P : MvPFunctor 2
   := .mk Unit fun _ _ => PFin2 1
-  
+
 
 abbrev QpfProd' := P.Obj
 abbrev QpfProd  := TypeFun.curried QpfProd'
@@ -31,8 +31,8 @@ abbrev Prod' : TypeFun 2
 -/
 def mk (a : Γ 1) (b : Γ 0) : QpfProd' Γ
   := ⟨
-      (), 
-      fun 
+      (),
+      fun
       | 1, _ => a
       | 0, _ => b
   ⟩
@@ -55,7 +55,7 @@ instance : MvFunctor Prod' where
   map f x   := equiv.invFun <| P.map f <| equiv.toFun <| x
 
 instance : MvQPF.IsPolynomial Prod' := .ofEquiv _ equiv
-  
+
 
 end Prod
 
diff --git a/Qpf/Qpf/Multivariate/Constructions/Comp.lean b/Qpf/Qpf/Multivariate/Constructions/Comp.lean
index 9c029cc..664b414 100644
--- a/Qpf/Qpf/Multivariate/Constructions/Comp.lean
+++ b/Qpf/Qpf/Multivariate/Constructions/Comp.lean
@@ -14,12 +14,12 @@ import Qpf.Util
 
 universe u
 
-
 namespace MvQPF.Comp
-  open MvPFunctor MvFunctor
 
-variable {n m : ℕ} 
-         (F : TypeFun n) 
+open MvPFunctor MvFunctor
+
+variable {n m : ℕ}
+         (F : TypeFun n)
          (G : Vec (TypeFun m) n)
          [p : IsPolynomial F]
          [p' : ∀ i, IsPolynomial <| G i]
@@ -46,25 +46,25 @@ variable {n m : ℕ}
               snd := fun x a =>
                 (repr (abs { fst := f' x a, snd := fun j b => f j { fst := x, snd := { fst := a, snd := b } } })).fst }
             i =
-          B (P (Comp F G)) { fst := a', snd := f' } i := 
+          B (P (Comp F G)) { fst := a', snd := f' } i :=
           by simp only [IsPolynomial.repr_abs]; rfl
-        
+
         apply HEq.funext'
-        case type_eq_β => 
+        case type_eq_β =>
           intros; rfl
-        case type_eq_α => 
+        case type_eq_α =>
           exact type_eq_α
 
         rintro ⟨b, ⟨b', g'⟩⟩
         simp only [heq_eq_eq]
-        
-        have : repr (abs 
-                  ⟨ f' b b', 
-                    fun j b_1 => 
+
+        have : repr (abs
+                  ⟨ f' b b',
+                    fun j b_1 =>
                       f j ⟨b, ⟨b', b_1⟩⟩
                   ⟩)
-                = ⟨ f' b b', 
-                    fun j b_1 => 
+                = ⟨ f' b b',
+                    fun j b_1 =>
                       f j ⟨b, ⟨b', b_1⟩⟩
                   ⟩;
         {
@@ -77,10 +77,9 @@ variable {n m : ℕ}
         sorry
       }
 
-    
-    
-    
 
 
-end MvQPF.Comp
 
+
+
+end MvQPF.Comp
diff --git a/Qpf/Util/TypeFun.lean b/Qpf/Util/TypeFun.lean
index 131777e..6a2be85 100644
--- a/Qpf/Util/TypeFun.lean
+++ b/Qpf/Util/TypeFun.lean
@@ -14,15 +14,15 @@ abbrev CurriedFun (α : Type u) (β : Type v) : Nat → Type (max u v)
 abbrev CurriedTypeFun : Nat → Type ((max u v) + 1)
   := CurriedFun (Type u) (Type v)
 
-/-- An uncurried type function, all `n` arguments are collected into a single `TypeVec n` 
+/-- An uncurried type function, all `n` arguments are collected into a single `TypeVec n`
     Note that all arguments live in the same universe, but the result may be in a different universe
 -/
-abbrev TypeFun (n : Nat) : Type ((max u v) + 1) := 
+abbrev TypeFun (n : Nat) : Type ((max u v) + 1) :=
   TypeVec.{u} n → Type v
 
 namespace TypeFun
   def reverseArgs : TypeFun n → TypeFun n :=
-    fun v α => v <| Vec.reverse α 
+    fun v α => v <| Vec.reverse α
 
   @[simp]
   theorem reverseArgs_involution (F : TypeFun n) :
@@ -33,7 +33,7 @@ namespace TypeFun
 
   def curriedAux : {n : Nat} → TypeFun n → CurriedTypeFun n
     | 0,    F => fun _ => F !![]
-    | 1,    F => fun a => F !![a] 
+    | 1,    F => fun a => F !![a]
     | _+2,  F => fun a => curriedAux fun αs => F (αs ::: a)
 
   def curried (F : TypeFun n) : CurriedTypeFun n
@@ -53,7 +53,7 @@ namespace TypeFun
   @[simp]
   theorem curriedAux_ofCurriedAux_involution {F : CurriedTypeFun n} :
     curriedAux (ofCurriedAux F) = F :=
-  by    
+  by
     cases n
     case zero => simp [curriedAux, ofCurriedAux]
     case succ n => {
@@ -64,12 +64,12 @@ namespace TypeFun
         funext a;
         apply @ih (F a);
       }
-    } 
+    }
 
   @[simp]
   theorem curried_ofCurried_involution {F : CurriedTypeFun n} :
     curried (ofCurried F) = F :=
-  by    
+  by
     simp only [curried, ofCurried, reverseArgs_involution]
     apply curriedAux_ofCurriedAux_involution
 
@@ -78,9 +78,9 @@ namespace TypeFun
   @[simp]
   theorem ofCurriedAux_curriedAux_involution {F : TypeFun n} :
     ofCurriedAux (curriedAux F) = F :=
-  by    
+  by
     cases n
-    case zero => 
+    case zero =>
       funext x;
       simp [curriedAux, ofCurriedAux, Matrix.vecEmpty]
       congr
@@ -102,8 +102,7 @@ namespace TypeFun
         funext x;
         simp [ofCurriedAux, curriedAux];
         let F' := fun α => F (α ::: x.last);
-        have : F x = F' x.drop;
-        . simp
+        have : F x = F' x.drop := by simp [F']
         rw [this]
         rw [@ih F']
       }
@@ -112,7 +111,7 @@ namespace TypeFun
   @[simp]
   theorem ofCurried_curried_involution {F : TypeFun n} :
     ofCurried (curried F) = F :=
-  by    
+  by
     simp only [ofCurried, curried, ofCurriedAux_curriedAux_involution]
     apply reverseArgs_involution
 end TypeFun
diff --git a/Qpf/Util/Vec.lean b/Qpf/Util/Vec.lean
index 958f0ef..8f04f7f 100644
--- a/Qpf/Util/Vec.lean
+++ b/Qpf/Util/Vec.lean
@@ -31,10 +31,6 @@ namespace Vec
     := fun _ => a
 end Vec
 
-unif_hint (n : Nat) where |- Fin2 n → Type u =?= Vec.{u+1} (Type u) n
-
-unif_hint {α : Type _} (n : Nat) where |- DVec.{u+1} (Vec.constVec α n) =?= Vec.{u+1} α n
-
 namespace DVec
   /-- Return the last element from a `DVec` -/
   abbrev last (v : @DVec (n+1) αs ) : αs 0
@@ -159,9 +155,10 @@ namespace Vec
 
       induction n <;> cases i;
       case succ.fz n ih => {
-        dsimp[ofList, toList, append1, last, DVec.last]
+        dsimp only [toList, last, DVec.last, ofList, append1, List.length_cons, Nat.succ_eq_add_one]
+        show HEq (v .fz) (v <| cast _ Fin2.fz)
         apply hcongr <;> (try solve | intros; rfl)
-        simp_heq;
+        simp_heq
         apply hcongr <;> (try solve | intros; rfl)
         simp
       }
diff --git a/lake-manifest.json b/lake-manifest.json
index 13938f1..43b4ccc 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "cebd10ba6d22457e364ba03320cfd9fc7511e520",
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,16 +31,16 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,10 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "feec58a7ee9185f92abddcf7631643b53181a7d3",
+   "rev": "a45ae63747140c1b2cbad9d46f518015c047047a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.5.0",
+   "inputRev": "v4.7.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "qpf",
diff --git a/lakefile.lean b/lakefile.lean
index 1419683..b2118c4 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -10,4 +10,4 @@ lean_lib Qpf
 lean_lib Test
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"@"v4.5.0"
+  "https://github.com/leanprover-community/mathlib4.git"@"v4.7.0"
diff --git a/lean-toolchain b/lean-toolchain
index bd59abf..9ad3040 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.7.0