Merge branch 'master' into remove-pfin2

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 1
@@ -17,15 +17,15 @@ namespace List
   abbrev QpfList' := ListPFunctor.Obj
   abbrev List' := @TypeFun.ofCurried 1 List
 
-  abbrev box {Γ} (x : List' Γ) : QpfList' Γ 
+  abbrev box {Γ} (x : List' Γ) : QpfList' Γ
     := ⟨
-        x.length, 
+        x.length,
         fun .fz j => Vec.ofList x j
       ⟩
 
-  abbrev unbox {Γ} (x : QpfList' Γ) : List' Γ 
+  abbrev unbox {Γ} (x : QpfList' Γ) : List' Γ
     := Vec.toList fun i => x.snd 0 i
-    
+
   private theorem typeext {α} {f g : α → Sort _} (f_eq_g: f = g) :
     ((a : α) → f a) = ((a : α) → g a) :=
   by
@@ -35,7 +35,7 @@ namespace List
   instance : MvFunctor List' :=
     MvFunctor.ofIsomorphism _ box unbox
 
-  instance : MvQPF List' := 
+  instance : MvQPF List' :=
     .ofIsomorphism _ box unbox (
       by
         intros Γ x;
@@ -60,7 +60,7 @@ namespace List
           apply HEq.trans cast_fun_arg
           rfl
 
-        case H₃ => 
+        case H₃ =>
           apply typeext;
           fin_destr;
 
@@ -70,7 +70,7 @@ namespace List
 
         case H₄ => intros; rfl
     ) (
-      by 
+      by
         intros _ x;
         induction x
         . rfl

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}"

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)

Qpf/PFunctor/Multivariate/Constructions/Prod.lean

@@ -12,9 +12,9 @@ namespace Prod
 
 open Fin2 (fz fs)
 
-def P : MvPFunctor 2 
+def P : MvPFunctor 2
   := .mk Unit fun _ _ => Fin2 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
 

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

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
@@ -111,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

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
       }
@@ -190,7 +187,7 @@ namespace Vec
     have n_eq : (toList v).length = n := toList_length_eq_n;
     apply hcongr
     . apply ofList_toList_iso
-    . simp_heq 
+    . simp_heq
       -- intros
       -- apply hcongr <;> intros <;> (try rw[n_eq])
       -- . simp_heq

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",