From 35bbb48916f75ee4abd1ce2d9af899fb11989f34 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 19 Jan 2025 21:30:18 +1100 Subject: [PATCH] feat: refactor List/Array.mapFinIdx to unbundle the Fin argument (#6697) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR changes the arguments of `List/Array.mapFinIdx` from `(f : Fin as.size → α → β)` to `(f : (i : Nat) → α → (h : i < as.size) → β)`, in line with the API design elsewhere for `List/Array`. --- src/Init/Data/Array/Basic.lean | 8 +-- src/Init/Data/Array/MapIdx.lean | 65 ++++++++--------- src/Init/Data/List/MapIdx.lean | 122 +++++++++++++++++--------------- src/Lean/Meta/IndPredBelow.lean | 2 +- 4 files changed, 104 insertions(+), 93 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 69d50d1a9b..8228b236b3 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -455,7 +455,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α /-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/ @[inline] def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] - (as : Array α) (f : Fin as.size → α → m β) : m (Array β) := + (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → m β) : m (Array β) := let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β) := do match i, inv with | 0, _ => pure bs @@ -464,12 +464,12 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm] apply Nat.le_add_right have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc] - map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get j j_lt))) + map i (j+1) this (bs.push (← f j (as.get j j_lt) j_lt)) map as.size 0 rfl (mkEmpty as.size) @[inline] def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) := - as.mapFinIdxM fun i a => f i a + as.mapFinIdxM fun i a _ => f i a @[inline] def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do @@ -588,7 +588,7 @@ def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β : /-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/ @[inline] -def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β := +def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) : Array β := Id.run <| as.mapFinIdxM f @[inline] diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean index 7d19d1f6f0..b25f3653dc 100644 --- a/src/Init/Data/Array/MapIdx.lean +++ b/src/Init/Data/Array/MapIdx.lean @@ -12,81 +12,82 @@ namespace Array /-! ### mapFinIdx -/ -- This could also be proved from `SatisfiesM_mapIdxM` in Batteries. -theorem mapFinIdx_induction (as : Array α) (f : Fin as.size → α → β) +theorem mapFinIdx_induction (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) (motive : Nat → Prop) (h0 : motive 0) - (p : Fin as.size → β → Prop) - (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) : + (p : (i : Nat) → β → (h : i < as.size) → Prop) + (hs : ∀ i h, motive i → p i (f i as[i] h) h ∧ motive (i + 1)) : motive as.size ∧ ∃ eq : (Array.mapFinIdx as f).size = as.size, - ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) := by - let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) : + ∀ i h, p i ((Array.mapFinIdx as f)[i]) h := by + let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p i bs[i] h) (hm : motive j) : let arr : Array β := Array.mapFinIdxM.map (m := Id) as f i j h bs - motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by + motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p i arr[i] h := by induction i generalizing j bs with simp [mapFinIdxM.map] | zero => have := (Nat.zero_add _).symm.trans h exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩ | succ i ih => - apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega) + apply @ih (bs.push (f j as[j] (by omega))) (j + 1) (by omega) (by simp; omega) · intro i i_lt h' rw [getElem_push] split · apply h₂ · simp only [size_push] at h' obtain rfl : i = j := by omega - apply (hs ⟨i, by omega⟩ hm).1 - · exact (hs ⟨j, by omega⟩ hm).2 + apply (hs i (by omega) hm).1 + · exact (hs j (by omega) hm).2 simp [mapFinIdx, mapFinIdxM]; exact go rfl nofun h0 -theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β) - (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) : +theorem mapFinIdx_spec (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) + (p : (i : Nat) → β → (h : i < as.size) → Prop) (hs : ∀ i h, p i (f i as[i] h) h) : ∃ eq : (Array.mapFinIdx as f).size = as.size, - ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) := - (mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2 + ∀ i h, p i ((Array.mapFinIdx as f)[i]) h := + (mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ _ => ⟨hs .., trivial⟩).2 -@[simp] theorem size_mapFinIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapFinIdx f).size = a.size := - (mapFinIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1 +@[simp] theorem size_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) : + (a.mapFinIdx f).size = a.size := + (mapFinIdx_spec (p := fun _ _ _ => True) (hs := fun _ _ => trivial)).1 @[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size := Array.size_mapFinIdx _ _ -@[simp] theorem getElem_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) +@[simp] theorem getElem_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) (i : Nat) (h : i < (mapFinIdx a f).size) : - (a.mapFinIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) := - (mapFinIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _ + (a.mapFinIdx f)[i] = f i (a[i]'(by simp_all)) (by simp_all) := + (mapFinIdx_spec _ _ (fun i b h => b = f i a[i] h) fun _ _ => rfl).2 i _ -@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) : +@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) (i : Nat) : (a.mapFinIdx f)[i]? = - a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by + a[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1 := by simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx] split <;> simp_all -@[simp] theorem toList_mapFinIdx (a : Array α) (f : Fin a.size → α → β) : - (a.mapFinIdx f).toList = a.toList.mapFinIdx (fun i a => f ⟨i, by simp⟩ a) := by +@[simp] theorem toList_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) : + (a.mapFinIdx f).toList = a.toList.mapFinIdx (fun i a h => f i a (by simpa)) := by apply List.ext_getElem <;> simp /-! ### mapIdx -/ theorem mapIdx_induction (f : Nat → α → β) (as : Array α) (motive : Nat → Prop) (h0 : motive 0) - (p : Fin as.size → β → Prop) - (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) : + (p : (i : Nat) → β → (h : i < as.size) → Prop) + (hs : ∀ i h, motive i → p i (f i as[i]) h ∧ motive (i + 1)) : motive as.size ∧ ∃ eq : (as.mapIdx f).size = as.size, - ∀ i h, p ⟨i, h⟩ ((as.mapIdx f)[i]) := - mapFinIdx_induction as (fun i a => f i a) motive h0 p hs + ∀ i h, p i ((as.mapIdx f)[i]) h := + mapFinIdx_induction as (fun i a _ => f i a) motive h0 p hs theorem mapIdx_spec (f : Nat → α → β) (as : Array α) - (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) : + (p : (i : Nat) → β → (h : i < as.size) → Prop) (hs : ∀ i h, p i (f i as[i]) h) : ∃ eq : (as.mapIdx f).size = as.size, - ∀ i h, p ⟨i, h⟩ ((as.mapIdx f)[i]) := - (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2 + ∀ i h, p i ((as.mapIdx f)[i]) h := + (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ _ => ⟨hs .., trivial⟩).2 @[simp] theorem size_mapIdx (f : Nat → α → β) (as : Array α) : (as.mapIdx f).size = as.size := - (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1 + (mapIdx_spec (p := fun _ _ _ => True) (hs := fun _ _ => trivial)).1 @[simp] theorem getElem_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat) (h : i < (as.mapIdx f).size) : (as.mapIdx f)[i] = f i (as[i]'(by simp_all)) := - (mapIdx_spec _ _ (fun i b => b = f i as[i]) fun _ => rfl).2 i (by simp_all) + (mapIdx_spec _ _ (fun i b h => b = f i as[i]) fun _ _ => rfl).2 i (by simp_all) @[simp] theorem getElem?_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat) : (as.mapIdx f)[i]? = @@ -101,7 +102,7 @@ end Array namespace List -@[simp] theorem mapFinIdx_toArray (l : List α) (f : Fin l.length → α → β) : +@[simp] theorem mapFinIdx_toArray (l : List α) (f : (i : Nat) → α → (h : i < l.length) → β) : l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by ext <;> simp diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean index 2e07ff93e3..e1a248b4d5 100644 --- a/src/Init/Data/List/MapIdx.lean +++ b/src/Init/Data/List/MapIdx.lean @@ -22,13 +22,13 @@ namespace List Given a list `as = [a₀, a₁, ...]` function `f : Fin as.length → α → β`, returns the list `[f 0 a₀, f 1 a₁, ...]`. -/ -@[inline] def mapFinIdx (as : List α) (f : Fin as.length → α → β) : List β := go as #[] (by simp) where +@[inline] def mapFinIdx (as : List α) (f : (i : Nat) → α → (h : i < as.length) → β) : List β := go as #[] (by simp) where /-- Auxiliary for `mapFinIdx`: `mapFinIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀, f 1 a₁, ...]` -/ @[specialize] go : (bs : List α) → (acc : Array β) → bs.length + acc.size = as.length → List β | [], acc, h => acc.toList | a :: as, acc, h => - go as (acc.push (f ⟨acc.size, by simp at h; omega⟩ a)) (by simp at h ⊢; omega) + go as (acc.push (f acc.size a (by simp at h; omega))) (by simp at h ⊢; omega) /-- Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁, ...]`, returns the list @@ -44,7 +44,7 @@ Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁, /-! ### mapFinIdx -/ @[simp] -theorem mapFinIdx_nil {f : Fin 0 → α → β} : mapFinIdx [] f = [] := +theorem mapFinIdx_nil {f : (i : Nat) → α → (h : i < 0) → β} : mapFinIdx [] f = [] := rfl @[simp] theorem length_mapFinIdx_go : @@ -53,13 +53,16 @@ theorem mapFinIdx_nil {f : Fin 0 → α → β} : mapFinIdx [] f = [] := | nil => simpa using h | cons _ _ ih => simp [mapFinIdx.go, ih] -@[simp] theorem length_mapFinIdx {as : List α} {f : Fin as.length → α → β} : +@[simp] theorem length_mapFinIdx {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} : (as.mapFinIdx f).length = as.length := by simp [mapFinIdx, length_mapFinIdx_go] -theorem getElem_mapFinIdx_go {as : List α} {f : Fin as.length → α → β} {i : Nat} {h} {w} : +theorem getElem_mapFinIdx_go {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} {w} : (mapFinIdx.go as f bs acc h)[i] = - if w' : i < acc.size then acc[i] else f ⟨i, by simp at w; omega⟩ (bs[i - acc.size]'(by simp at w; omega)) := by + if w' : i < acc.size then + acc[i] + else + f i (bs[i - acc.size]'(by simp at w; omega)) (by simp at w; omega) := by induction bs generalizing acc with | nil => simp only [length_mapFinIdx_go, length_nil, Nat.zero_add] at w h @@ -78,29 +81,30 @@ theorem getElem_mapFinIdx_go {as : List α} {f : Fin as.length → α → β} {i · have h₃ : i - acc.size = (i - (acc.size + 1)) + 1 := by omega simp [h₃] -@[simp] theorem getElem_mapFinIdx {as : List α} {f : Fin as.length → α → β} {i : Nat} {h} : - (as.mapFinIdx f)[i] = f ⟨i, by simp at h; omega⟩ (as[i]'(by simp at h; omega)) := by +@[simp] theorem getElem_mapFinIdx {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} : + (as.mapFinIdx f)[i] = f i (as[i]'(by simp at h; omega)) (by simp at h; omega) := by simp [mapFinIdx, getElem_mapFinIdx_go] -theorem mapFinIdx_eq_ofFn {as : List α} {f : Fin as.length → α → β} : - as.mapFinIdx f = List.ofFn fun i : Fin as.length => f i as[i] := by +theorem mapFinIdx_eq_ofFn {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} : + as.mapFinIdx f = List.ofFn fun i : Fin as.length => f i as[i] i.2 := by apply ext_getElem <;> simp -@[simp] theorem getElem?_mapFinIdx {l : List α} {f : Fin l.length → α → β} {i : Nat} : - (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f ⟨i, by simp [getElem?_eq_some_iff] at m; exact m.1⟩ x := by +@[simp] theorem getElem?_mapFinIdx {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {i : Nat} : + (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f i x (by simp [getElem?_eq_some_iff] at m; exact m.1) := by simp only [getElem?_def, length_mapFinIdx, getElem_mapFinIdx] split <;> simp @[simp] -theorem mapFinIdx_cons {l : List α} {a : α} {f : Fin (l.length + 1) → α → β} : - mapFinIdx (a :: l) f = f 0 a :: mapFinIdx l (fun i => f i.succ) := by +theorem mapFinIdx_cons {l : List α} {a : α} {f : (i : Nat) → α → (h : i < l.length + 1) → β} : + mapFinIdx (a :: l) f = f 0 a (by omega) :: mapFinIdx l (fun i a h => f (i + 1) a (by omega)) := by apply ext_getElem · simp · rintro (_|i) h₁ h₂ <;> simp -theorem mapFinIdx_append {K L : List α} {f : Fin (K ++ L).length → α → β} : +theorem mapFinIdx_append {K L : List α} {f : (i : Nat) → α → (h : i < (K ++ L).length) → β} : (K ++ L).mapFinIdx f = - K.mapFinIdx (fun i => f (i.castLE (by simp))) ++ L.mapFinIdx (fun i => f ((i.natAdd K.length).cast (by simp))) := by + K.mapFinIdx (fun i a h => f i a (by simp; omega)) ++ + L.mapFinIdx (fun i a h => f (i + K.length) a (by simp; omega)) := by apply ext_getElem · simp · intro i h₁ h₂ @@ -108,60 +112,57 @@ theorem mapFinIdx_append {K L : List α} {f : Fin (K ++ L).length → α → β} simp only [getElem_mapFinIdx, length_mapFinIdx] split <;> rename_i h · rw [getElem_append_left] - congr · simp only [Nat.not_lt] at h rw [getElem_append_right h] congr - simp omega -@[simp] theorem mapFinIdx_concat {l : List α} {e : α} {f : Fin (l ++ [e]).length → α → β}: - (l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i => f (i.castLE (by simp))) ++ [f ⟨l.length, by simp⟩ e] := by +@[simp] theorem mapFinIdx_concat {l : List α} {e : α} {f : (i : Nat) → α → (h : i < (l ++ [e]).length) → β}: + (l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i a h => f i a (by simp; omega)) ++ [f l.length e (by simp)] := by simp [mapFinIdx_append] - congr -theorem mapFinIdx_singleton {a : α} {f : Fin 1 → α → β} : - [a].mapFinIdx f = [f ⟨0, by simp⟩ a] := by +theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} : + [a].mapFinIdx f = [f 0 a (by simp)] := by simp -theorem mapFinIdx_eq_enum_map {l : List α} {f : Fin l.length → α → β} : +theorem mapFinIdx_eq_enum_map {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} : l.mapFinIdx f = l.enum.attach.map fun ⟨⟨i, x⟩, m⟩ => - f ⟨i, by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1⟩ x := by + f i x (by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by apply ext_getElem <;> simp @[simp] -theorem mapFinIdx_eq_nil_iff {l : List α} {f : Fin l.length → α → β} : +theorem mapFinIdx_eq_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} : l.mapFinIdx f = [] ↔ l = [] := by rw [mapFinIdx_eq_enum_map, map_eq_nil_iff, attach_eq_nil_iff, enum_eq_nil_iff] -theorem mapFinIdx_ne_nil_iff {l : List α} {f : Fin l.length → α → β} : +theorem mapFinIdx_ne_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} : l.mapFinIdx f ≠ [] ↔ l ≠ [] := by simp -theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : Fin l.length → α → β} - (h : b ∈ l.mapFinIdx f) : ∃ (i : Fin l.length), f i l[i] = b := by +theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} + (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < l.length), f i l[i] h = b := by rw [mapFinIdx_eq_enum_map] at h replace h := exists_of_mem_map h simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_enum_iff_getElem?] at h obtain ⟨i, b, h, rfl⟩ := h rw [getElem?_eq_some_iff] at h obtain ⟨h', rfl⟩ := h - exact ⟨⟨i, h'⟩, rfl⟩ + exact ⟨i, h', rfl⟩ -@[simp] theorem mem_mapFinIdx {b : β} {l : List α} {f : Fin l.length → α → β} : - b ∈ l.mapFinIdx f ↔ ∃ (i : Fin l.length), f i l[i] = b := by +@[simp] theorem mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} : + b ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < l.length), f i l[i] h = b := by constructor · intro h exact exists_of_mem_mapFinIdx h · rintro ⟨i, h, rfl⟩ rw [mem_iff_getElem] - exact ⟨i, by simp⟩ + exact ⟨i, by simpa using h, by simp⟩ -theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : Fin l.length → α → β} : +theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} : l.mapFinIdx f = b :: l₂ ↔ - ∃ (a : α) (l₁ : List α) (h : l = a :: l₁), - f ⟨0, by simp [h]⟩ a = b ∧ l₁.mapFinIdx (fun i => f (i.succ.cast (by simp [h]))) = l₂ := by + ∃ (a : α) (l₁ : List α) (w : l = a :: l₁), + f 0 a (by simp [w]) = b ∧ l₁.mapFinIdx (fun i a h => f (i + 1) a (by simp [w]; omega)) = l₂ := by cases l with | nil => simp | cons x l' => @@ -169,39 +170,48 @@ theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : Fin l.length → α exists_and_left] constructor · rintro ⟨rfl, rfl⟩ - refine ⟨x, rfl, l', by simp⟩ - · rintro ⟨a, ⟨rfl, h⟩, ⟨_, ⟨rfl, rfl⟩, h⟩⟩ - exact ⟨rfl, h⟩ + refine ⟨x, l', ⟨rfl, rfl⟩, by simp⟩ + · rintro ⟨a, l', ⟨rfl, rfl⟩, ⟨rfl, rfl⟩⟩ + exact ⟨rfl, by simp⟩ -theorem mapFinIdx_eq_cons_iff' {l : List α} {b : β} {f : Fin l.length → α → β} : +theorem mapFinIdx_eq_cons_iff' {l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} : l.mapFinIdx f = b :: l₂ ↔ - l.head?.pbind (fun x m => (f ⟨0, by cases l <;> simp_all⟩ x)) = some b ∧ - l.tail?.attach.map (fun ⟨t, m⟩ => t.mapFinIdx fun i => f (i.succ.cast (by cases l <;> simp_all))) = some l₂ := by + l.head?.pbind (fun x m => (f 0 x (by cases l <;> simp_all))) = some b ∧ + l.tail?.attach.map (fun ⟨t, m⟩ => t.mapFinIdx fun i a h => f (i + 1) a (by cases l <;> simp_all)) = some l₂ := by cases l <;> simp -theorem mapFinIdx_eq_iff {l : List α} {f : Fin l.length → α → β} : - l.mapFinIdx f = l' ↔ ∃ h : l'.length = l.length, ∀ (i : Nat) (h : i < l.length), l'[i] = f ⟨i, h⟩ l[i] := by +theorem mapFinIdx_eq_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} : + l.mapFinIdx f = l' ↔ ∃ h : l'.length = l.length, ∀ (i : Nat) (h : i < l.length), l'[i] = f i l[i] h := by constructor · rintro rfl simp · rintro ⟨h, w⟩ apply ext_getElem <;> simp_all -theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : Fin l.length → α → β} : - l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Fin l.length), f i l[i] = g i l[i] := by +theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : (i : Nat) → α → (h : i < l.length) → β} : + l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h := by rw [eq_comm, mapFinIdx_eq_iff] simp [Fin.forall_iff] -@[simp] theorem mapFinIdx_mapFinIdx {l : List α} {f : Fin l.length → α → β} {g : Fin _ → β → γ} : - (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i => g (i.cast (by simp)) ∘ f i) := by +@[simp] theorem mapFinIdx_mapFinIdx {l : List α} + {f : (i : Nat) → α → (h : i < l.length) → β} + {g : (i : Nat) → β → (h : i < (l.mapFinIdx f).length) → γ} : + (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i a h => g i (f i a h) (by simpa)) := by simp [mapFinIdx_eq_iff] -theorem mapFinIdx_eq_replicate_iff {l : List α} {f : Fin l.length → α → β} {b : β} : - l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Fin l.length), f i l[i] = b := by - simp [eq_replicate_iff, length_mapFinIdx, mem_mapFinIdx, forall_exists_index, true_and] +theorem mapFinIdx_eq_replicate_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {b : β} : + l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = b := by + rw [eq_replicate_iff, length_mapFinIdx] + simp only [mem_mapFinIdx, forall_exists_index, true_and] + constructor + · intro w i h + exact w (f i l[i] h) i h rfl + · rintro w b i h rfl + exact w i h -@[simp] theorem mapFinIdx_reverse {l : List α} {f : Fin l.reverse.length → α → β} : - l.reverse.mapFinIdx f = (l.mapFinIdx (fun i => f ⟨l.length - 1 - i, by simp; omega⟩)).reverse := by +@[simp] theorem mapFinIdx_reverse {l : List α} {f : (i : Nat) → α → (h : i < l.reverse.length) → β} : + l.reverse.mapFinIdx f = + (l.mapFinIdx (fun i a h => f (l.length - 1 - i) a (by simp; omega))).reverse := by simp [mapFinIdx_eq_iff] intro i h congr @@ -262,13 +272,13 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat}, rw [← getElem?_eq_getElem, getElem?_mapIdx, getElem?_eq_getElem (by simpa using h)] simp -@[simp] theorem mapFinIdx_eq_mapIdx {l : List α} {f : Fin l.length → α → β} {g : Nat → α → β} - (h : ∀ (i : Fin l.length), f i l[i] = g i l[i]) : +@[simp] theorem mapFinIdx_eq_mapIdx {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {g : Nat → α → β} + (h : ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i]) : l.mapFinIdx f = l.mapIdx g := by simp_all [mapFinIdx_eq_iff] theorem mapIdx_eq_mapFinIdx {l : List α} {f : Nat → α → β} : - l.mapIdx f = l.mapFinIdx (fun i => f i) := by + l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by simp [mapFinIdx_eq_mapIdx] theorem mapIdx_eq_enum_map {l : List α} : diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index 1404d88508..cfb96e6abb 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -296,7 +296,7 @@ where m.apply recursor applyCtors (ms : List MVarId) : MetaM $ List MVarId := do - let mss ← ms.toArray.mapIdxM fun _ m => do + let mss ← ms.toArray.mapM fun m => do let m ← introNPRec m (← m.getType).withApp fun below args => m.withContext do