From af4a7d7e984e275d2d7091908c7172d4414e2128 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2025 17:22:06 -0800 Subject: [PATCH 1/3] fix: `grind` term preprocessor (#6659) This PR fixes a bug in the `grind` term preprocessor. It was abstracting nested proofs **before** reducible constants were unfolded. --------- Co-authored-by: Kim Morrison --- src/Lean/Meta/Tactic/Grind/Simp.lean | 2 +- tests/lean/run/grind_cat.lean | 119 ++++++++++++++++++++++++++- 2 files changed, 119 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Simp.lean b/src/Lean/Meta/Tactic/Grind/Simp.lean index bf0c7a7bfce3..e10637e8d82c 100644 --- a/src/Lean/Meta/Tactic/Grind/Simp.lean +++ b/src/Lean/Meta/Tactic/Grind/Simp.lean @@ -28,9 +28,9 @@ def simp (e : Expr) : GoalM Simp.Result := do let e ← instantiateMVars e let r ← simpCore e let e' := r.expr + let e' ← unfoldReducible e' let e' ← abstractNestedProofs e' let e' ← markNestedProofs e' - let e' ← unfoldReducible e' let e' ← eraseIrrelevantMData e' let e' ← foldProjs e' let e' ← normalizeLevels e' diff --git a/tests/lean/run/grind_cat.lean b/tests/lean/run/grind_cat.lean index bc4101848b55..41143c034315 100644 --- a/tests/lean/run/grind_cat.lean +++ b/tests/lean/run/grind_cat.lean @@ -36,6 +36,8 @@ structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category. /-- A functor preserves composition. -/ map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) := by cat_tac +scoped infixr:26 " ⥤ " => Functor + attribute [simp] Functor.map_id Functor.map_comp attribute [grind =] Functor.map_id @@ -51,6 +53,8 @@ def comp (F : Functor C D) (G : Functor D E) : Functor C E where map f := G.map (F.map f) -- Note `map_id` and `map_comp` are handled by `cat_tac`. +infixr:80 " ⋙ " => Functor.comp + variable {X Y : C} {G : Functor D E} @[simp, grind =] theorem comp_obj : (F.comp G).obj X = G.obj (F.obj X) := rfl @@ -73,7 +77,7 @@ variable {X : C} protected def id (F : Functor C D) : NatTrans F F where app X := 𝟙 (F.obj X) -@[simp, grind =] theorem id_app : (NatTrans.id F).app X = 𝟙 (F.obj X) := rfl +@[simp, grind =] theorem id_app' : (NatTrans.id F).app X = 𝟙 (F.obj X) := rfl protected def vcomp (α : NatTrans F G) (β : NatTrans G H) : NatTrans F H where app X := α.app X ≫ β.app X @@ -96,6 +100,11 @@ instance Functor.category : Category.{max u₁ v₂} (Functor C D) where comp α β := NatTrans.vcomp α β -- Here we're okay: all the proofs are handled by `cat_tac`. +namespace NatTrans + +@[ext] +theorem ext' {α β : F ⟶ G} (w : α.app = β.app) : α = β := NatTrans.ext w + @[simp, grind =] theorem id_app (F : Functor C D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl @@ -122,6 +131,30 @@ def hcomp {H I : Functor D E} (α : F ⟶ G) (β : H ⟶ I) : F.comp H ⟶ G.com -- rw [Functor.comp_map, Functor.comp_map, ← assoc, naturality, assoc, ← I.map_comp, naturality, -- map_comp, assoc] +/-- Notation for horizontal composition of natural transformations. -/ +infixl:80 " ◫ " => hcomp + +@[simp] theorem hcomp_app {H I : Functor D E} (α : F ⟶ G) (β : H ⟶ I) (X : C) : + (α ◫ β).app X = β.app (F.obj X) ≫ I.map (α.app X) := rfl + +attribute [grind =] hcomp_app + +theorem hcomp_id_app {H : D ⥤ E} (α : F ⟶ G) (X : C) : (α ◫ 𝟙 H).app X = H.map (α.app X) := by + cat_tac + +theorem id_hcomp_app {H : E ⥤ C} (α : F ⟶ G) (X : E) : (𝟙 H ◫ α).app X = α.app _ := by cat_tac + +-- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we +-- need to use associativity of functor composition. (It's true without the explicit associator, +-- because functor composition is definitionally associative, +-- but relying on the definitional equality causes bad problems with elaboration later.) +theorem exchange {I J K : D ⥤ E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) : + (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ := by + ext X + cat_tac + +end NatTrans + structure Iso {C : Type u} [Category.{v} C] (X Y : C) where hom : X ⟶ Y inv : Y ⟶ X @@ -179,4 +212,88 @@ def homToEquiv (α : X ≅ Y) {Z : C} : (Z ⟶ X) ≃ (Z ⟶ Y) where right_inv := sorry end Iso + +section Mathlib.CategoryTheory.Functor.Category + + +open NatTrans Category CategoryTheory.Functor + +variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] + +attribute [local simp] vcomp_app + +variable {C D} {E : Type u₃} [Category.{v₃} E] +variable {E' : Type u₄} [Category.{v₄} E'] +variable {F G H I : C ⥤ D} + + +namespace NatTrans + +@[simp] +theorem vcomp_eq_comp (α : F ⟶ G) (β : G ⟶ H) : NatTrans.vcomp α β = α ≫ β := rfl + +theorem vcomp_app' (α : F ⟶ G) (β : G ⟶ H) (X : C) : (α ≫ β).app X = α.app X ≫ β.app X := rfl + +theorem congr_app {α β : F ⟶ G} (h : α = β) (X : C) : α.app X = β.app X := by rw [h] + +theorem naturality_app_app {F G : C ⥤ D ⥤ E ⥤ E'} + (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) : + ((F.map f).app X₂).app X₃ ≫ ((α.app Y₁).app X₂).app X₃ = + ((α.app X₁).app X₂).app X₃ ≫ ((G.map f).app X₂).app X₃ := + congr_app (NatTrans.naturality_app α X₂ f) X₃ + +end NatTrans + +open NatTrans + +namespace Functor + +/-- Flip the arguments of a bifunctor. See also `Currying.lean`. -/ +protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E where + obj k := + { obj := fun j => (F.obj j).obj k, + map := fun f => (F.map f).app k, } + map f := { app := fun j => (F.obj j).map f } + map_id k := by cat_tac + map_comp f g := sorry + +@[simp] theorem flip_obj_obj (F : C ⥤ D ⥤ E) (k : D) : (F.flip.obj k).obj = fun j => (F.obj j).obj k := rfl +@[simp] theorem flip_obj_map (F : C ⥤ D ⥤ E) (k : D) {X Y : C}(f : X ⟶ Y) : (F.flip.obj k).map f = (F.map f).app k := rfl +@[simp] theorem flip_map_app (F : C ⥤ D ⥤ E) {X Y : D} (f : X ⟶ Y) (k : C) : (F.flip.map f).app k = (F.obj k).map f := rfl + +attribute [grind =] flip_obj_obj flip_obj_map flip_map_app + +end Functor + +variable (C D E) in +/-- The functor `(C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E` which flips the variables. -/ +def flipFunctor : (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E where + obj F := F.flip + map {F₁ F₂} φ := + { app := fun Y => + { app := fun X => (φ.app X).app Y + naturality := fun X₁ X₂ f => by + dsimp + simp only [← NatTrans.comp_app, naturality] } + naturality := sorry } + map_id := sorry + map_comp := sorry + +namespace Iso + +@[simp] +theorem map_hom_inv_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) : + (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 _ := by + cat_tac + +@[simp] +theorem map_inv_hom_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) : + (F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 _ := by + cat_tac + +end Iso + + +end Mathlib.CategoryTheory.Functor.Category + end CategoryTheory From 3a6c5cf4f189cb0725a42a609c16338fa8db6661 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2025 20:59:18 -0800 Subject: [PATCH 2/3] feat: canonicalizer diagnostics (#6662) This PR improves the canonicalizer used in the `grind` tactic and the diagnostics it produces. It also adds a new configuration option, `canonHeartbeats`, to address (some of) the issues. Here is an example illustrating the new diagnostics, where we intentionally create a problem by using a very small number of heartbeats. image --- src/Init/Grind/Tactics.lean | 2 + src/Lean/Meta/Tactic/Grind/Canon.lean | 99 +++++++------- src/Lean/Meta/Tactic/Grind/Internalize.lean | 6 +- src/Lean/Meta/Tactic/Grind/Simp.lean | 1 + src/Lean/Meta/Tactic/Grind/Types.lean | 15 +-- tests/lean/run/grind_cat2.lean | 135 +++++++++++++------- 6 files changed, 155 insertions(+), 103 deletions(-) diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index 5e817636e203..cb30c0073849 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -47,6 +47,8 @@ structure Config where splitIndPred : Bool := true /-- By default, `grind` halts as soon as it encounters a sub-goal where no further progress can be made. -/ failures : Nat := 1 + /-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/ + canonHeartbeats : Nat := 1000 deriving Inhabited, BEq end Lean.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean index 2493dae7cdb1..ae60269872c2 100644 --- a/src/Lean/Meta/Tactic/Grind/Canon.lean +++ b/src/Lean/Meta/Tactic/Grind/Canon.lean @@ -10,6 +10,7 @@ import Lean.Meta.FunInfo import Lean.Util.FVarSubset import Lean.Util.PtrSet import Lean.Util.FVarSubset +import Lean.Meta.Tactic.Grind.Types namespace Lean.Meta.Grind namespace Canon @@ -40,42 +41,37 @@ additions will still use structurally different (and definitionally different) i Furthermore, `grind` will not be able to infer that `HEq (a + a) (b + b)` even if we add the assumptions `n = m` and `HEq a b`. -/ -structure State where - argMap : PHashMap (Expr × Nat) (List Expr) := {} - canon : PHashMap Expr Expr := {} - proofCanon : PHashMap Expr Expr := {} - deriving Inhabited +@[inline] private def get' : GoalM State := + return (← get).canon -inductive CanonElemKind where - | /-- - Type class instances are canonicalized using `TransparencyMode.instances`. - -/ - instance - | /-- - Types and Type formers are canonicalized using `TransparencyMode.default`. - Remark: propositions are just visited. We do not invoke `canonElemCore` for them. - -/ - type - | /-- - Implicit arguments that are not types, type formers, or instances, are canonicalized - using `TransparencyMode.reducible` - -/ - implicit - deriving BEq +@[inline] private def modify' (f : State → State) : GoalM Unit := + modify fun s => { s with canon := f s.canon } -def CanonElemKind.explain : CanonElemKind → String - | .instance => "type class instances" - | .type => "types (or type formers)" - | .implicit => "implicit arguments (which are not type class instances or types)" +/-- +Helper function for `canonElemCore`. It tries `isDefEq a b` with default transparency, but using +at most `canonHeartbeats` heartbeats. It reports an issue if the threshold is reached. +Remark: `parent` is use only to report an issue +-/ +private def isDefEqBounded (a b : Expr) (parent : Expr) : GoalM Bool := do + withCurrHeartbeats do + let config ← getConfig + tryCatchRuntimeEx + (withTheReader Core.Context (fun ctx => { ctx with maxHeartbeats := config.canonHeartbeats }) do + withDefault <| isDefEq a b) + fun ex => do + if ex.isRuntime then + let curr := (← getConfig).canonHeartbeats + reportIssue m!"failed to show that{indentExpr a}\nis definitionally equal to{indentExpr b}\nwhile canonicalizing{indentExpr parent}\nusing `{curr}*1000` heartbeats, `(canonHeartbeats := {curr})`" + return false + else + throw ex /-- Helper function for canonicalizing `e` occurring as the `i`th argument of an `f`-application. - -Thus, if diagnostics are enabled, we also re-check them using `TransparencyMode.default`. If the result is different -we report to the user. +If `useIsDefEqBounded` is `true`, we try `isDefEqBounded` before returning false -/ -def canonElemCore (f : Expr) (i : Nat) (e : Expr) (kind : CanonElemKind) : StateT State MetaM Expr := do - let s ← get +def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBounded : Bool) : GoalM Expr := do + let s ← get' if let some c := s.canon.find? e then return c let key := (f, i) @@ -87,20 +83,21 @@ def canonElemCore (f : Expr) (i : Nat) (e : Expr) (kind : CanonElemKind) : State -- However, we don't revert previously canonicalized elements in the `grind` tactic. -- Moreover, we store the canonicalizer state in the `Goal` because we case-split -- and different locals are added in different branches. - modify fun s => { s with canon := s.canon.insert e c } - trace[grind.debug.canon] "found {e} ===> {c}" + modify' fun s => { s with canon := s.canon.insert e c } + trace[grind.debugn.canon] "found {e} ===> {c}" return c - if kind != .type then - if (← isTracingEnabledFor `grind.issues <&&> (withDefault <| isDefEq e c)) then - -- TODO: consider storing this information in some structure that can be browsed later. - trace[grind.issues] "the following {kind.explain} are definitionally equal with `default` transparency but not with a more restrictive transparency{indentExpr e}\nand{indentExpr c}" + if useIsDefEqBounded then + if (← isDefEqBounded e c parent) then + modify' fun s => { s with canon := s.canon.insert e c } + trace[grind.debugn.canon] "found using `isDefEqBounded`: {e} ===> {c}" + return c trace[grind.debug.canon] "({f}, {i}) ↦ {e}" - modify fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key (e::cs) } + modify' fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key (e::cs) } return e -abbrev canonType (f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore f i e .type -abbrev canonInst (f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore f i e .instance -abbrev canonImplicit (f : Expr) (i : Nat) (e : Expr) := withReducible <| canonElemCore f i e .implicit +abbrev canonType (parent f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore parent f i e (useIsDefEqBounded := false) +abbrev canonInst (parent f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore parent f i e (useIsDefEqBounded := true) +abbrev canonImplicit (parent f : Expr) (i : Nat) (e : Expr) := withReducible <| canonElemCore parent f i e (useIsDefEqBounded := true) /-- Return type for the `shouldCanon` function. @@ -148,10 +145,10 @@ def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Should else return .visit -unsafe def canonImpl (e : Expr) : StateT State MetaM Expr := do +unsafe def canonImpl (e : Expr) : GoalM Expr := do visit e |>.run' mkPtrMap where - visit (e : Expr) : StateRefT (PtrMap Expr Expr) (StateT State MetaM) Expr := do + visit (e : Expr) : StateRefT (PtrMap Expr Expr) GoalM Expr := do unless e.isApp || e.isForall do return e -- Check whether it is cached if let some r := (← get).find? e then @@ -161,11 +158,11 @@ where if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then let prop := args[0]! let prop' ← visit prop - if let some r := (← getThe State).proofCanon.find? prop' then + if let some r := (← get').proofCanon.find? prop' then pure r else let e' := if ptrEq prop prop' then e else mkAppN f (args.set! 0 prop') - modifyThe State fun s => { s with proofCanon := s.proofCanon.insert prop' e' } + modify' fun s => { s with proofCanon := s.proofCanon.insert prop' e' } pure e' else let pinfos := (← getFunInfo f).paramInfo @@ -175,9 +172,9 @@ where let arg := args[i] trace[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}" let arg' ← match (← shouldCanon pinfos i arg) with - | .canonType => canonType f i arg - | .canonInst => canonInst f i arg - | .canonImplicit => canonImplicit f i (← visit arg) + | .canonType => canonType e f i arg + | .canonInst => canonInst e f i arg + | .canonImplicit => canonImplicit e f i (← visit arg) | .visit => visit arg unless ptrEq arg arg' do args := args.set i arg' @@ -193,11 +190,11 @@ where modify fun s => s.insert e e' return e' +end Canon + /-- Canonicalizes nested types, type formers, and instances in `e`. -/ -def canon (e : Expr) : StateT State MetaM Expr := do +def canon (e : Expr) : GoalM Expr := do trace[grind.debug.canon] "{e}" - unsafe canonImpl e - -end Canon + unsafe Canon.canonImpl e end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index a0d68ab2d440..705eb298536e 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -11,6 +11,7 @@ import Lean.Meta.Match.MatcherInfo import Lean.Meta.Match.MatchEqsExt import Lean.Meta.Tactic.Grind.Types import Lean.Meta.Tactic.Grind.Util +import Lean.Meta.Tactic.Grind.Canon import Lean.Meta.Tactic.Grind.Arith.Internalize namespace Lean.Meta.Grind @@ -98,13 +99,16 @@ private def pushCastHEqs (e : Expr) : GoalM Unit := do | f@Eq.recOn α a motive b h v => pushHEq e v (mkApp6 (mkConst ``Grind.eqRecOn_heq f.constLevels!) α a motive b h v) | _ => return () +private def preprocessGroundPattern (e : Expr) : GoalM Expr := do + shareCommon (← canon (← normalizeLevels (← unfoldReducible e))) + mutual /-- Internalizes the nested ground terms in the given pattern. -/ private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do if pattern.isBVar || isPatternDontCare pattern then return pattern else if let some e := groundPattern? pattern then - let e ← shareCommon (← canon (← normalizeLevels (← unfoldReducible e))) + let e ← preprocessGroundPattern e internalize e generation none return mkGroundPattern e else pattern.withApp fun f args => do diff --git a/src/Lean/Meta/Tactic/Grind/Simp.lean b/src/Lean/Meta/Tactic/Grind/Simp.lean index e10637e8d82c..e6bd7fdba72a 100644 --- a/src/Lean/Meta/Tactic/Grind/Simp.lean +++ b/src/Lean/Meta/Tactic/Grind/Simp.lean @@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Grind.Util import Lean.Meta.Tactic.Grind.Types import Lean.Meta.Tactic.Grind.DoNotSimp import Lean.Meta.Tactic.Grind.MarkNestedProofs +import Lean.Meta.Tactic.Grind.Canon namespace Lean.Meta.Grind /-- Simplifies the given expression using the `grind` simprocs and normalization theorems. -/ diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index a4f0390e6d64..ef8880d04fd9 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -14,7 +14,6 @@ import Lean.Meta.AbstractNestedProofs import Lean.Meta.Tactic.Simp.Types import Lean.Meta.Tactic.Util import Lean.Meta.Tactic.Grind.ENodeKey -import Lean.Meta.Tactic.Grind.Canon import Lean.Meta.Tactic.Grind.Attr import Lean.Meta.Tactic.Grind.Arith.Types import Lean.Meta.Tactic.Grind.EMatchTheorem @@ -333,6 +332,13 @@ structure NewFact where generation : Nat deriving Inhabited +/-- Canonicalizer state. See `Canon.lean` for additional details. -/ +structure Canon.State where + argMap : PHashMap (Expr × Nat) (List Expr) := {} + canon : PHashMap Expr Expr := {} + proofCanon : PHashMap Expr Expr := {} + deriving Inhabited + structure Goal where mvarId : MVarId canon : Canon.State := {} @@ -402,13 +408,6 @@ abbrev GoalM := StateRefT Goal GrindM @[inline] def GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal := goal.mvarId.withContext do StateRefT'.run' (x *> get) goal -/-- Canonicalizes nested types, type formers, and instances in `e`. -/ -def canon (e : Expr) : GoalM Expr := do - let canonS ← modifyGet fun s => (s.canon, { s with canon := {} }) - let (e, canonS) ← Canon.canon e |>.run canonS - modify fun s => { s with canon := canonS } - return e - def updateLastTag : GoalM Unit := do if (← isTracingEnabledFor `grind) then let currTag ← (← get).mvarId.getTag diff --git a/tests/lean/run/grind_cat2.lean b/tests/lean/run/grind_cat2.lean index b9b03ea222db..3a5102c7f883 100644 --- a/tests/lean/run/grind_cat2.lean +++ b/tests/lean/run/grind_cat2.lean @@ -244,68 +244,117 @@ instance functorial_id : Functorial.{v₁, v₁} (id : C → C) where map' f := namespace Ex1 variable {E : Type u₃} [Category.{v₃} E] -/-- -info: [grind.issues] the following implicit arguments (which are not type class instances or types) are definitionally equal with `default` transparency but not with a more restrictive transparency - G (F X) - and - (G ∘ F) X -[grind.issues] the following implicit arguments (which are not type class instances or types) are definitionally equal with `default` transparency but not with a more restrictive transparency - G (F Y) - and - (G ∘ F) Y -[grind.issues] the following implicit arguments (which are not type class instances or types) are definitionally equal with `default` transparency but not with a more restrictive transparency - G (F Z) - and - (G ∘ F) Z --/ -#guard_msgs (info) in def functorial_comp (F : C → D) [Functorial.{v₁, v₂} F] (G : D → E) [Functorial.{v₂, v₃} G] : Functorial.{v₁, v₃} (G ∘ F) := { Functor.of F ⋙ Functor.of G with map' := fun f => map G (map F f) map_id' := sorry - map_comp' := by - set_option trace.grind.issues true in - fail_if_success grind - sorry + map_comp' := by grind } end Ex1 namespace Ex2 variable {E : Type u₃} [Category.{v₃} E] --- Since in the trace above, `Function.comp` generated problems because it is not `reducible`, --- we can fix the issue by instructing `grind` to unfold it. -attribute [local grind] Function.comp - +/- +In this example, we restrict the number of heartbeats used by the canonicalizer. +The idea is to test the issue tracker. +-/ -def functorial_comp (F : C → D) [Functorial.{v₁, v₂} F] (G : D → E) [Functorial.{v₂, v₃} G] : +/-- +error: `grind` failed +case grind +C✝¹ : Type u₁ +inst✝⁸ : Category C✝¹ +D✝ : Type u₂ +inst✝⁷ : Category D✝ +E✝ : Type u₃ +inst✝⁶ : Category E✝ +F✝ G✝ H : C✝¹ ⥤ D✝ +C✝ : Type u +inst✝⁵ : Category C✝ +X✝ Y✝ Z✝ : C✝ +C : Type u₁ +inst✝⁴ : Category C +D : Type u₂ +inst✝³ : Category D +E : Type u₃ +inst✝² : Category E +F : C → D +inst✝¹ : Functorial F +G : D → E +inst✝ : Functorial G +__src✝ : C ⥤ E := of F ⋙ of G +X Y Z : C +f : X ⟶ Y +g : Y ⟶ Z +x✝ : ¬map G (map F (f ≫ g)) = map G (map F f) ≫ map G (map F g) +⊢ False +[grind] Diagnostics + [facts] Asserted facts + [prop] __src✝ = of F ⋙ of G + [prop] ¬map G (map F (f ≫ g)) = map G (map F f) ≫ map G (map F g) + [prop] map F (f ≫ g) = map F f ≫ map F g + [prop] map G (map F f ≫ map F g) = map G (map F f) ≫ map G (map F g) + [eqc] False propositions + [prop] map G (map F (f ≫ g)) = map G (map F f) ≫ map G (map F g) + [eqc] Equivalence classes + [eqc] {map G (map F f ≫ map F g), map G (map F (f ≫ g)), map G (map F f) ≫ map G (map F g)} + [eqc] {map F (f ≫ g), map F f ≫ map F g} + [eqc] {__src✝, of F ⋙ of G} + [ematch] E-matching + [thm] Functorial.map_comp: + ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C → D} [inst_2 : Functorial F] + {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z}, map F (f ≫ g) = map F f ≫ map F g + patterns: [@map #10 #9 #8 #7 #6 #5 #4 #2 (@Category.comp ? ? #4 #3 #2 #1 #0)] + [thm] assoc: + ∀ {obj : Type u} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), + (f ≫ g) ≫ h = f ≫ g ≫ h + patterns: [@Category.comp #8 #7 #6 #5 #3 #2 (@Category.comp ? ? #5 #4 #3 #1 #0)] + [thm] assoc: + ∀ {obj : Type u} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), + (f ≫ g) ≫ h = f ≫ g ≫ h + patterns: [@Category.comp #8 #7 #6 #4 #3 (@Category.comp ? ? #6 #5 #4 #2 #1) #0] + [issues] Issues + [issue] failed to show that + F Y + is definitionally equal to + F Z + while canonicalizing + map G (map F f) + using `100*1000` heartbeats, `(canonHeartbeats := 100)` + [issue] failed to show that + G (F X) + is definitionally equal to + (G ∘ F) X + while canonicalizing + map G (map F f) ≫ map G (map F g) + using `100*1000` heartbeats, `(canonHeartbeats := 100)` + [issue] failed to show that + G (F Y) + is definitionally equal to + (G ∘ F) Y + while canonicalizing + map G (map F f) ≫ map G (map F g) + using `100*1000` heartbeats, `(canonHeartbeats := 100)` + [issue] failed to show that + G (F Z) + is definitionally equal to + (G ∘ F) Z + while canonicalizing + map G (map F f) ≫ map G (map F g) + using `100*1000` heartbeats, `(canonHeartbeats := 100)` +-/ +#guard_msgs (error) in +def functorial_comp' (F : C → D) [Functorial.{v₁, v₂} F] (G : D → E) [Functorial.{v₂, v₃} G] : Functorial.{v₁, v₃} (G ∘ F) := { Functor.of F ⋙ Functor.of G with map' := fun f => map G (map F f) map_id' := sorry - map_comp' := by grind + map_comp' := by grind (canonHeartbeats := 100) } end Ex2 -namespace Ex3 -variable {E : Type u₃} [Category.{v₃} E] - --- Since in the trace above, `Function.comp` generated problems because it is not `reducible`, --- we set it to reducible. -set_option allowUnsafeReducibility true -attribute [reducible] Function.comp - -def functorial_comp (F : C → D) [Functorial.{v₁, v₂} F] (G : D → E) [Functorial.{v₂, v₃} G] : - Functorial.{v₁, v₃} (G ∘ F) := - { Functor.of F ⋙ Functor.of G with - map' := fun f => map G (map F f) - map_id' := sorry - map_comp' := by grind - } - -end Ex3 - end CategoryTheory From 80ddbf45eb92794b1df2cb625e9432753d41601b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 16 Jan 2025 16:19:28 +1100 Subject: [PATCH 3/3] feat: align List/Array/Vector.flatMap (#6660) This PR defines `Vector.flatMap`, changes the order of arguments in `List.flatMap` for consistency, and aligns the lemmas for `List`/`Array`/`Vector` `flatMap`. --- src/Init/Data/Array/Lemmas.lean | 114 +++++++++++++++++++++++++++++-- src/Init/Data/List/Basic.lean | 6 +- src/Init/Data/List/Impl.lean | 6 +- src/Init/Data/List/Lemmas.lean | 10 +-- src/Init/Data/Vector/Basic.lean | 3 + src/Init/Data/Vector/Lemmas.lean | 69 +++++++++++++++++++ 6 files changed, 193 insertions(+), 15 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 1acf464ca378..b78fe308f0a5 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -1560,6 +1560,11 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array cases bs simp +theorem toArray_append {xs : List α} {ys : Array α} : + xs.toArray ++ ys = (xs ++ ys.toList).toArray := by + rcases ys with ⟨ys⟩ + simp + @[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} : xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList := by cases as @@ -1871,6 +1876,11 @@ theorem append_eq_map_iff {f : α → β} : rw [← flatten_map_toArray] simp +theorem flatten_toArray (l : List (Array α)) : + l.toArray.flatten = (l.map Array.toList).flatten.toArray := by + apply ext' + simp + @[simp] theorem size_flatten (L : Array (Array α)) : L.flatten.size = (L.map size).sum := by cases L using array₂_induction simp [Function.comp_def] @@ -1886,14 +1896,14 @@ theorem mem_flatten : ∀ {L : Array (Array α)}, a ∈ L.flatten ↔ ∃ l, l · rintro ⟨s, h₁, h₂⟩ refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩ -@[simp] theorem flatten_eq_nil_iff {L : Array (Array α)} : L.flatten = #[] ↔ ∀ l ∈ L, l = #[] := by +@[simp] theorem flatten_eq_empty_iff {L : Array (Array α)} : L.flatten = #[] ↔ ∀ l ∈ L, l = #[] := by induction L using array₂_induction simp -@[simp] theorem nil_eq_flatten_iff {L : Array (Array α)} : #[] = L.flatten ↔ ∀ l ∈ L, l = #[] := by - rw [eq_comm, flatten_eq_nil_iff] +@[simp] theorem empty_eq_flatten_iff {L : Array (Array α)} : #[] = L.flatten ↔ ∀ l ∈ L, l = #[] := by + rw [eq_comm, flatten_eq_empty_iff] -theorem flatten_ne_nil_iff {xs : Array (Array α)} : xs.flatten ≠ #[] ↔ ∃ x, x ∈ xs ∧ x ≠ #[] := by +theorem flatten_ne_empty_iff {xs : Array (Array α)} : xs.flatten ≠ #[] ↔ ∃ x, x ∈ xs ∧ x ≠ #[] := by simp theorem exists_of_mem_flatten : a ∈ flatten L → ∃ l, l ∈ L ∧ a ∈ l := mem_flatten.1 @@ -2029,6 +2039,102 @@ theorem eq_iff_flatten_eq {L L' : Array (Array α)} : rw [List.map_inj_right] simp +contextual +/-! ### flatMap -/ + +theorem flatMap_def (l : Array α) (f : α → Array β) : l.flatMap f = flatten (map f l) := by + rcases l with ⟨l⟩ + simp [flatten_toArray, Function.comp_def, List.flatMap_def] + +theorem flatMap_toList (l : Array α) (f : α → List β) : + l.toList.flatMap f = (l.flatMap (fun a => (f a).toArray)).toList := by + rcases l with ⟨l⟩ + simp + +@[simp] theorem flatMap_id (l : Array (Array α)) : l.flatMap id = l.flatten := by simp [flatMap_def] + +@[simp] theorem flatMap_id' (l : Array (Array α)) : l.flatMap (fun a => a) = l.flatten := by simp [flatMap_def] + +@[simp] +theorem size_flatMap (l : Array α) (f : α → Array β) : + (l.flatMap f).size = sum (map (fun a => (f a).size) l) := by + rcases l with ⟨l⟩ + simp [Function.comp_def] + +@[simp] theorem mem_flatMap {f : α → Array β} {b} {l : Array α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by + simp [flatMap_def, mem_flatten] + exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩ + +theorem exists_of_mem_flatMap {b : β} {l : Array α} {f : α → Array β} : + b ∈ l.flatMap f → ∃ a, a ∈ l ∧ b ∈ f a := mem_flatMap.1 + +theorem mem_flatMap_of_mem {b : β} {l : Array α} {f : α → Array β} {a} (al : a ∈ l) (h : b ∈ f a) : + b ∈ l.flatMap f := mem_flatMap.2 ⟨a, al, h⟩ + +@[simp] +theorem flatMap_eq_empty_iff {l : Array α} {f : α → Array β} : l.flatMap f = #[] ↔ ∀ x ∈ l, f x = #[] := by + rw [flatMap_def, flatten_eq_empty_iff] + simp + +theorem forall_mem_flatMap {p : β → Prop} {l : Array α} {f : α → Array β} : + (∀ (x) (_ : x ∈ l.flatMap f), p x) ↔ ∀ (a) (_ : a ∈ l) (b) (_ : b ∈ f a), p b := by + simp only [mem_flatMap, forall_exists_index, and_imp] + constructor <;> (intros; solve_by_elim) + +theorem flatMap_singleton (f : α → Array β) (x : α) : #[x].flatMap f = f x := by + simp + +@[simp] theorem flatMap_singleton' (l : Array α) : (l.flatMap fun x => #[x]) = l := by + rcases l with ⟨l⟩ + simp + +@[simp] theorem flatMap_append (xs ys : Array α) (f : α → Array β) : + (xs ++ ys).flatMap f = xs.flatMap f ++ ys.flatMap f := by + rcases xs with ⟨xs⟩ + rcases ys with ⟨ys⟩ + simp + +theorem flatMap_assoc {α β} (l : Array α) (f : α → Array β) (g : β → Array γ) : + (l.flatMap f).flatMap g = l.flatMap fun x => (f x).flatMap g := by + rcases l with ⟨l⟩ + simp [List.flatMap_assoc, flatMap_toList] + +theorem map_flatMap (f : β → γ) (g : α → Array β) (l : Array α) : + (l.flatMap g).map f = l.flatMap fun a => (g a).map f := by + rcases l with ⟨l⟩ + simp [List.map_flatMap] + +theorem flatMap_map (f : α → β) (g : β → Array γ) (l : Array α) : + (map f l).flatMap g = l.flatMap (fun a => g (f a)) := by + rcases l with ⟨l⟩ + simp [List.flatMap_map] + +theorem map_eq_flatMap {α β} (f : α → β) (l : Array α) : map f l = l.flatMap fun x => #[f x] := by + simp only [← map_singleton] + rw [← flatMap_singleton' l, map_flatMap, flatMap_singleton'] + +theorem filterMap_flatMap {β γ} (l : Array α) (g : α → Array β) (f : β → Option γ) : + (l.flatMap g).filterMap f = l.flatMap fun a => (g a).filterMap f := by + rcases l with ⟨l⟩ + simp [List.filterMap_flatMap] + +theorem filter_flatMap (l : Array α) (g : α → Array β) (f : β → Bool) : + (l.flatMap g).filter f = l.flatMap fun a => (g a).filter f := by + rcases l with ⟨l⟩ + simp [List.filter_flatMap] + +theorem flatMap_eq_foldl (f : α → Array β) (l : Array α) : + l.flatMap f = l.foldl (fun acc a => acc ++ f a) #[] := by + rcases l with ⟨l⟩ + simp only [List.flatMap_toArray, List.flatMap_eq_foldl, size_toArray, List.foldl_toArray'] + suffices ∀ l', (List.foldl (fun acc a => acc ++ (f a).toList) l' l).toArray = + List.foldl (fun acc a => acc ++ f a) l'.toArray l by + simpa using this [] + induction l with + | nil => simp + | cons a l ih => + intro l' + simp [ih ((l' ++ (f a).toList)), toArray_append] + /-! Content below this point has not yet been aligned with `List`. -/ -- This is a duplicate of `List.toArray_toList`. diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 3352b90f44d5..3b9b7efb09a0 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -606,11 +606,11 @@ set_option linter.missingDocs false in to get a list of lists, and then concatenates them all together. * `[2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]` -/ -@[inline] def flatMap {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β := flatten (map b a) +@[inline] def flatMap {α : Type u} {β : Type v} (b : α → List β) (a : List α) : List β := flatten (map b a) -@[simp] theorem flatMap_nil (f : α → List β) : List.flatMap [] f = [] := by simp [flatten, List.flatMap] +@[simp] theorem flatMap_nil (f : α → List β) : List.flatMap f [] = [] := by simp [flatten, List.flatMap] @[simp] theorem flatMap_cons x xs (f : α → List β) : - List.flatMap (x :: xs) f = f x ++ List.flatMap xs f := by simp [flatten, List.flatMap] + List.flatMap f (x :: xs) = f x ++ List.flatMap f xs := by simp [flatten, List.flatMap] set_option linter.missingDocs false in @[deprecated flatMap (since := "2024-10-16")] abbrev bind := @flatMap diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean index 5fb32bf0b59c..20f324dba419 100644 --- a/src/Init/Data/List/Impl.lean +++ b/src/Init/Data/List/Impl.lean @@ -96,14 +96,14 @@ The following operations are given `@[csimp]` replacements below: /-! ### flatMap -/ /-- Tail recursive version of `List.flatMap`. -/ -@[inline] def flatMapTR (as : List α) (f : α → List β) : List β := go as #[] where +@[inline] def flatMapTR (f : α → List β) (as : List α) : List β := go as #[] where /-- Auxiliary for `flatMap`: `flatMap.go f as = acc.toList ++ bind f as` -/ @[specialize] go : List α → Array β → List β | [], acc => acc.toList | x::xs, acc => go xs (acc ++ f x) @[csimp] theorem flatMap_eq_flatMapTR : @List.flatMap = @flatMapTR := by - funext α β as f + funext α β f as let rec go : ∀ as acc, flatMapTR.go f as acc = acc.toList ++ as.flatMap f | [], acc => by simp [flatMapTR.go, flatMap] | x::xs, acc => by simp [flatMapTR.go, flatMap, go xs] @@ -112,7 +112,7 @@ The following operations are given `@[csimp]` replacements below: /-! ### flatten -/ /-- Tail recursive version of `List.flatten`. -/ -@[inline] def flattenTR (l : List (List α)) : List α := flatMapTR l id +@[inline] def flattenTR (l : List (List α)) : List α := l.flatMapTR id @[csimp] theorem flatten_eq_flattenTR : @flatten = @flattenTR := by funext α l; rw [← List.flatMap_id, List.flatMap_eq_flatMapTR]; rfl diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index f6f11494a15d..a0f8aa260b64 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -2070,14 +2070,14 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)}, theorem flatMap_def (l : List α) (f : α → List β) : l.flatMap f = flatten (map f l) := by rfl -@[simp] theorem flatMap_id (l : List (List α)) : List.flatMap l id = l.flatten := by simp [flatMap_def] +@[simp] theorem flatMap_id (l : List (List α)) : l.flatMap id = l.flatten := by simp [flatMap_def] -@[simp] theorem flatMap_id' (l : List (List α)) : List.flatMap l (fun a => a) = l.flatten := by simp [flatMap_def] +@[simp] theorem flatMap_id' (l : List (List α)) : l.flatMap (fun a => a) = l.flatten := by simp [flatMap_def] @[simp] theorem length_flatMap (l : List α) (f : α → List β) : - length (l.flatMap f) = sum (map (length ∘ f) l) := by - rw [List.flatMap, length_flatten, map_map] + length (l.flatMap f) = sum (map (fun a => (f a).length) l) := by + rw [List.flatMap, length_flatten, map_map, Function.comp_def] @[simp] theorem mem_flatMap {f : α → List β} {b} {l : List α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by simp [flatMap_def, mem_flatten] @@ -2090,7 +2090,7 @@ theorem mem_flatMap_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : b ∈ l.flatMap f := mem_flatMap.2 ⟨a, al, h⟩ @[simp] -theorem flatMap_eq_nil_iff {l : List α} {f : α → List β} : List.flatMap l f = [] ↔ ∀ x ∈ l, f x = [] := +theorem flatMap_eq_nil_iff {l : List α} {f : α → List β} : l.flatMap f = [] ↔ ∀ x ∈ l, f x = [] := flatten_eq_nil_iff.trans <| by simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index 269a6577e3d4..32b336c4801d 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -174,6 +174,9 @@ result is empty. If `stop` is greater than the size of the vector, the size is u ⟨(v.toArray.map Vector.toArray).flatten, by rcases v; simp_all [Function.comp_def, Array.map_const']⟩ +@[inline] def flatMap (v : Vector α n) (f : α → Vector β m) : Vector β (n * m) := + ⟨v.toArray.flatMap fun a => (f a).toArray, by simp [Array.map_const']⟩ + /-- Maps corresponding elements of two vectors of equal size using the function `f`. -/ @[inline] def zipWith (a : Vector α n) (b : Vector β n) (f : α → β → φ) : Vector φ n := ⟨Array.zipWith a.toArray b.toArray f, by simp⟩ diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 00ea12d7cee3..17964a63efd9 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -1525,6 +1525,75 @@ theorem eq_iff_flatten_eq {L L' : Vector (Vector α n) m} : subst this rfl + +/-! ### flatMap -/ + +@[simp] theorem flatMap_mk (l : Array α) (h : l.size = m) (f : α → Vector β n) : + (mk l h).flatMap f = + mk (l.flatMap (fun a => (f a).toArray)) (by simp [Array.map_const', h]) := by + simp [flatMap] + +@[simp] theorem flatMap_toArray (l : Vector α n) (f : α → Vector β m) : + l.toArray.flatMap (fun a => (f a).toArray) = (l.flatMap f).toArray := by + rcases l with ⟨l, rfl⟩ + simp + +theorem flatMap_def (l : Vector α n) (f : α → Vector β m) : l.flatMap f = flatten (map f l) := by + rcases l with ⟨l, rfl⟩ + simp [Array.flatMap_def, Function.comp_def] + +@[simp] theorem flatMap_id (l : Vector (Vector α m) n) : l.flatMap id = l.flatten := by simp [flatMap_def] + +@[simp] theorem flatMap_id' (l : Vector (Vector α m) n) : l.flatMap (fun a => a) = l.flatten := by simp [flatMap_def] + +@[simp] theorem mem_flatMap {f : α → Vector β m} {b} {l : Vector α n} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by + simp [flatMap_def, mem_flatten] + exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩ + +theorem exists_of_mem_flatMap {b : β} {l : Vector α n} {f : α → Vector β m} : + b ∈ l.flatMap f → ∃ a, a ∈ l ∧ b ∈ f a := mem_flatMap.1 + +theorem mem_flatMap_of_mem {b : β} {l : Vector α n} {f : α → Vector β m} {a} (al : a ∈ l) (h : b ∈ f a) : + b ∈ l.flatMap f := mem_flatMap.2 ⟨a, al, h⟩ + +theorem forall_mem_flatMap {p : β → Prop} {l : Vector α n} {f : α → Vector β m} : + (∀ (x) (_ : x ∈ l.flatMap f), p x) ↔ ∀ (a) (_ : a ∈ l) (b) (_ : b ∈ f a), p b := by + simp only [mem_flatMap, forall_exists_index, and_imp] + constructor <;> (intros; solve_by_elim) + +theorem flatMap_singleton (f : α → Vector β m) (x : α) : #v[x].flatMap f = (f x).cast (by simp) := by + simp [flatMap_def] + +@[simp] theorem flatMap_singleton' (l : Vector α n) : (l.flatMap fun x => #v[x]) = l.cast (by simp) := by + rcases l with ⟨l, rfl⟩ + simp + +@[simp] theorem flatMap_append (xs ys : Vector α n) (f : α → Vector β m) : + (xs ++ ys).flatMap f = (xs.flatMap f ++ ys.flatMap f).cast (by simp [Nat.add_mul]) := by + rcases xs with ⟨xs⟩ + rcases ys with ⟨ys⟩ + simp [flatMap_def, flatten_append] + +theorem flatMap_assoc {α β} (l : Vector α n) (f : α → Vector β m) (g : β → Vector γ k) : + (l.flatMap f).flatMap g = (l.flatMap fun x => (f x).flatMap g).cast (by simp [Nat.mul_assoc]) := by + rcases l with ⟨l, rfl⟩ + simp [Array.flatMap_assoc] + +theorem map_flatMap (f : β → γ) (g : α → Vector β m) (l : Vector α n) : + (l.flatMap g).map f = l.flatMap fun a => (g a).map f := by + rcases l with ⟨l, rfl⟩ + simp [Array.map_flatMap] + +theorem flatMap_map (f : α → β) (g : β → Vector γ k) (l : Vector α n) : + (map f l).flatMap g = l.flatMap (fun a => g (f a)) := by + rcases l with ⟨l, rfl⟩ + simp [Array.flatMap_map] + +theorem map_eq_flatMap {α β} (f : α → β) (l : Vector α n) : + map f l = (l.flatMap fun x => #v[f x]).cast (by simp) := by + rcases l with ⟨l, rfl⟩ + simp [Array.map_eq_flatMap] + /-! Content below this point has not yet been aligned with `List` and `Array`. -/ @[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :