From bc234f9f8da5071bfaeec2453a6400b6f51681db Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 29 Jan 2025 18:58:17 +1100 Subject: [PATCH] feat: align List/Array/Vector.zip/zipWith/zipWithAll/unzip (#6840) This PR completes the alignment of `List/Array/Vector.zip/zipWith/zipWithAll/unzip` lemmas. --- src/Init/Data/Array.lean | 1 + src/Init/Data/Array/Basic.lean | 6 +- src/Init/Data/Array/Lemmas.lean | 12 +- src/Init/Data/Array/Zip.lean | 363 +++++++++++++++++++ src/Init/Data/List/ToArray.lean | 4 +- src/Init/Data/List/Zip.lean | 11 +- src/Init/Data/Vector.lean | 1 + src/Init/Data/Vector/Basic.lean | 7 +- src/Init/Data/Vector/Lemmas.lean | 16 +- src/Init/Data/Vector/Zip.lean | 287 +++++++++++++++ src/Lean/Compiler/LCNF/ElimDeadBranches.lean | 2 +- src/Lean/Compiler/LCNF/SpecInfo.lean | 2 +- src/Lean/Elab/Command.lean | 4 +- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 2 +- src/Lean/Elab/StructInst.lean | 2 +- src/Lean/Elab/Tactic/Induction.lean | 5 +- src/Lean/Meta/ArgsPacker.lean | 10 +- tests/lean/run/array_isEqvAux.lean | 2 +- 18 files changed, 700 insertions(+), 37 deletions(-) create mode 100644 src/Init/Data/Array/Zip.lean create mode 100644 src/Init/Data/Vector/Zip.lean diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean index 36b1ff3e5f..827ba902f9 100644 --- a/src/Init/Data/Array.lean +++ b/src/Init/Data/Array.lean @@ -23,3 +23,4 @@ import Init.Data.Array.FinRange import Init.Data.Array.Perm import Init.Data.Array.Find import Init.Data.Array.Lex +import Init.Data.Array.Zip diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 37d253b8fe..4f39cd788b 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -941,13 +941,13 @@ def zipWithAux (as : Array α) (bs : Array β) (f : α → β → γ) (i : Nat) cs decreasing_by simp_wf; decreasing_trivial_pre_omega -@[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ := +@[inline] def zipWith (f : α → β → γ) (as : Array α) (bs : Array β) : Array γ := zipWithAux as bs f 0 #[] def zip (as : Array α) (bs : Array β) : Array (α × β) := - zipWith as bs Prod.mk + zipWith Prod.mk as bs -def zipWithAll (as : Array α) (bs : Array β) (f : Option α → Option β → γ) : Array γ := +def zipWithAll (f : Option α → Option β → γ) (as : Array α) (bs : Array β) : Array γ := go as bs 0 #[] where go (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) := if i < max as.size bs.size then diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 67d3f59444..4c0aa534ac 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -3543,23 +3543,23 @@ theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size) /-! ### zipWith -/ @[simp] theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) : - (Array.zipWith as bs f).toList = List.zipWith f as.toList bs.toList := by + (zipWith f as bs).toList = List.zipWith f as.toList bs.toList := by cases as cases bs simp @[simp] theorem toList_zip (as : Array α) (bs : Array β) : - (Array.zip as bs).toList = List.zip as.toList bs.toList := by + (zip as bs).toList = List.zip as.toList bs.toList := by simp [zip, toList_zipWith, List.zip] @[simp] theorem toList_zipWithAll (f : Option α → Option β → γ) (as : Array α) (bs : Array β) : - (Array.zipWithAll as bs f).toList = List.zipWithAll f as.toList bs.toList := by + (zipWithAll f as bs).toList = List.zipWithAll f as.toList bs.toList := by cases as cases bs simp @[simp] theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : - (as.zipWith bs f).size = min as.size bs.size := by + (zipWith f as bs).size = min as.size bs.size := by rw [size_eq_length_toList, toList_zipWith, List.length_zipWith] @[simp] theorem size_zip (as : Array α) (bs : Array β) : @@ -3567,8 +3567,8 @@ theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size) as.size_zipWith bs Prod.mk @[simp] theorem getElem_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) (i : Nat) - (hi : i < (as.zipWith bs f).size) : - (as.zipWith bs f)[i] = f (as[i]'(by simp at hi; omega)) (bs[i]'(by simp at hi; omega)) := by + (hi : i < (zipWith f as bs).size) : + (zipWith f as bs)[i] = f (as[i]'(by simp at hi; omega)) (bs[i]'(by simp at hi; omega)) := by cases as cases bs simp diff --git a/src/Init/Data/Array/Zip.lean b/src/Init/Data/Array/Zip.lean new file mode 100644 index 0000000000..bf734807bf --- /dev/null +++ b/src/Init/Data/Array/Zip.lean @@ -0,0 +1,363 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +prelude +import Init.Data.Array.TakeDrop +import Init.Data.List.Zip + +/-! +# Lemmas about `Array.zip`, `Array.zipWith`, `Array.zipWithAll`, and `Array.unzip`. +-/ + +namespace Array + +open Nat + +/-! ## Zippers -/ + +/-! ### zipWith -/ + +theorem zipWith_comm (f : α → β → γ) (la : Array α) (lb : Array β) : + zipWith f la lb = zipWith (fun b a => f a b) lb la := by + cases la + cases lb + simpa using List.zipWith_comm _ _ _ + +theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y = f y x) (l l' : Array α) : + zipWith f l l' = zipWith f l' l := by + rw [zipWith_comm] + simp only [comm] + +@[simp] +theorem zipWith_self (f : α → α → δ) (l : Array α) : zipWith f l l = l.map fun a => f a a := by + cases l + simp + +/-- +See also `getElem?_zipWith'` for a variant +using `Option.map` and `Option.bind` rather than a `match`. +-/ +theorem getElem?_zipWith {f : α → β → γ} {i : Nat} : + (zipWith f as bs)[i]? = match as[i]?, bs[i]? with + | some a, some b => some (f a b) | _, _ => none := by + cases as + cases bs + simp [List.getElem?_zipWith] + rfl + +/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`. -/ +theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} : + (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g := by + cases l₁ + cases l₂ + simp [List.getElem?_zipWith'] + +theorem getElem?_zipWith_eq_some {f : α → β → γ} {l₁ : Array α} {l₂ : Array β} {z : γ} {i : Nat} : + (zipWith f l₁ l₂)[i]? = some z ↔ + ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z := by + cases l₁ + cases l₂ + simp [List.getElem?_zipWith_eq_some] + +theorem getElem?_zip_eq_some {l₁ : Array α} {l₂ : Array β} {z : α × β} {i : Nat} : + (zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2 := by + cases z + rw [zip, getElem?_zipWith_eq_some]; constructor + · rintro ⟨x, y, h₀, h₁, h₂⟩ + simpa [h₀, h₁] using h₂ + · rintro ⟨h₀, h₁⟩ + exact ⟨_, _, h₀, h₁, rfl⟩ + +@[simp] +theorem zipWith_map {μ} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : Array α) (l₂ : Array β) : + zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂ := by + cases l₁ + cases l₂ + simp [List.zipWith_map] + +theorem zipWith_map_left (l₁ : Array α) (l₂ : Array β) (f : α → α') (g : α' → β → γ) : + zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂ := by + cases l₁ + cases l₂ + simp [List.zipWith_map_left] + +theorem zipWith_map_right (l₁ : Array α) (l₂ : Array β) (f : β → β') (g : α → β' → γ) : + zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂ := by + cases l₁ + cases l₂ + simp [List.zipWith_map_right] + +theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} (i : δ): + (zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i := by + cases l₁ + cases l₂ + simp [List.zipWith_foldr_eq_zip_foldr] + +theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ): + (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i := by + cases l₁ + cases l₂ + simp [List.zipWith_foldl_eq_zip_foldl] + +@[simp] +theorem zipWith_eq_empty_iff {f : α → β → γ} {l l'} : zipWith f l l' = #[] ↔ l = #[] ∨ l' = #[] := by + cases l <;> cases l' <;> simp + +theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : Array γ) (l' : Array δ) : + map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l' := by + cases l + cases l' + simp [List.map_zipWith] + +theorem take_zipWith : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n) := by + cases l + cases l' + simp [List.take_zipWith] + +theorem extract_zipWith : (zipWith f l l').extract m n = zipWith f (l.extract m n) (l'.extract m n) := by + cases l + cases l' + simp [List.drop_zipWith, List.take_zipWith] + +theorem zipWith_append (f : α → β → γ) (l la : Array α) (l' lb : Array β) + (h : l.size = l'.size) : + zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb := by + cases l + cases l' + cases la + cases lb + simp at h + simp [List.zipWith_append, h] + +theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : Array α} {l₂ : Array β} : + zipWith f l₁ l₂ = l₁' ++ l₂' ↔ + ∃ w x y z, w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z := by + cases l₁ + cases l₂ + cases l₁' + cases l₂' + simp only [List.zipWith_toArray, List.append_toArray, mk.injEq, List.zipWith_eq_append_iff, + toArray_eq_append_iff] + constructor + · rintro ⟨w, x, y, z, h, rfl, rfl, rfl, rfl⟩ + exact ⟨w.toArray, x.toArray, y.toArray, z.toArray, by simp [h]⟩ + · rintro ⟨⟨w⟩, ⟨x⟩, ⟨y⟩, ⟨z⟩, h, rfl, rfl, h₁, h₂⟩ + exact ⟨w, x, y, z, by simp_all⟩ + +@[simp] theorem zipWith_mkArray {a : α} {b : β} {m n : Nat} : + zipWith f (mkArray m a) (mkArray n b) = mkArray (min m n) (f a b) := by + simp [← List.toArray_replicate] + +theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (l : Array α) (l' : Array β) : + map (Function.uncurry f) (l.zip l') = zipWith f l l' := by + cases l + cases l' + simp [List.map_uncurry_zip_eq_zipWith] + +theorem map_zip_eq_zipWith (f : α × β → γ) (l : Array α) (l' : Array β) : + map f (l.zip l') = zipWith (Function.curry f) l l' := by + cases l + cases l' + simp [List.map_zip_eq_zipWith] + +theorem lt_size_left_of_zipWith {f : α → β → γ} {i : Nat} {l : Array α} {l' : Array β} + (h : i < (zipWith f l l').size) : i < l.size := by rw [size_zipWith] at h; omega + +theorem lt_size_right_of_zipWith {f : α → β → γ} {i : Nat} {l : Array α} {l' : Array β} + (h : i < (zipWith f l l').size) : i < l'.size := by rw [size_zipWith] at h; omega + +theorem zipWith_eq_zipWith_take_min (l₁ : Array α) (l₂ : Array β) : + zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.size l₂.size)) (l₂.take (min l₁.size l₂.size)) := by + cases l₁ + cases l₂ + simp + rw [List.zipWith_eq_zipWith_take_min] + +theorem reverse_zipWith (h : l.size = l'.size) : + (zipWith f l l').reverse = zipWith f l.reverse l'.reverse := by + cases l + cases l' + simp [List.reverse_zipWith (by simpa using h)] + +/-! ### zip -/ + +theorem lt_size_left_of_zip {i : Nat} {l : Array α} {l' : Array β} (h : i < (zip l l').size) : + i < l.size := + lt_size_left_of_zipWith h + +theorem lt_size_right_of_zip {i : Nat} {l : Array α} {l' : Array β} (h : i < (zip l l').size) : + i < l'.size := + lt_size_right_of_zipWith h + +@[simp] +theorem getElem_zip {l : Array α} {l' : Array β} {i : Nat} {h : i < (zip l l').size} : + (zip l l')[i] = + (l[i]'(lt_size_left_of_zip h), l'[i]'(lt_size_right_of_zip h)) := + getElem_zipWith (hi := by simpa using h) + +theorem zip_eq_zipWith (l₁ : Array α) (l₂ : Array β) : zip l₁ l₂ = zipWith Prod.mk l₁ l₂ := by + cases l₁ + cases l₂ + simp [List.zip_eq_zipWith] + +theorem zip_map (f : α → γ) (g : β → δ) (l₁ : Array α) (l₂ : Array β) : + zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g) := by + cases l₁ + cases l₂ + simp [List.zip_map] + +theorem zip_map_left (f : α → γ) (l₁ : Array α) (l₂ : Array β) : + zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id] + +theorem zip_map_right (f : β → γ) (l₁ : Array α) (l₂ : Array β) : + zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id] + +theorem zip_append {l₁ r₁ : Array α} {l₂ r₂ : Array β} (_h : l₁.size = l₂.size) : + zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂ := by + cases l₁ + cases l₂ + cases r₁ + cases r₂ + simp_all [List.zip_append] + +theorem zip_map' (f : α → β) (g : α → γ) (l : Array α) : + zip (l.map f) (l.map g) = l.map fun a => (f a, g a) := by + cases l + simp [List.zip_map'] + +theorem of_mem_zip {a b} {l₁ : Array α} {l₂ : Array β} : (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂ := by + cases l₁ + cases l₂ + simpa using List.of_mem_zip + +theorem map_fst_zip (l₁ : Array α) (l₂ : Array β) (h : l₁.size ≤ l₂.size) : + map Prod.fst (zip l₁ l₂) = l₁ := by + cases l₁ + cases l₂ + simp_all [List.map_fst_zip] + +theorem map_snd_zip (l₁ : Array α) (l₂ : Array β) (h : l₂.size ≤ l₁.size) : + map Prod.snd (zip l₁ l₂) = l₂ := by + cases l₁ + cases l₂ + simp_all [List.map_snd_zip] + +theorem map_prod_left_eq_zip {l : Array α} (f : α → β) : + (l.map fun x => (x, f x)) = l.zip (l.map f) := by + rw [← zip_map'] + congr + simp + +theorem map_prod_right_eq_zip {l : Array α} (f : α → β) : + (l.map fun x => (f x, x)) = (l.map f).zip l := by + rw [← zip_map'] + congr + simp + +@[simp] theorem zip_eq_empty_iff {l₁ : Array α} {l₂ : Array β} : + zip l₁ l₂ = #[] ↔ l₁ = #[] ∨ l₂ = #[] := by + cases l₁ + cases l₂ + simp [List.zip_eq_nil_iff] + +theorem zip_eq_append_iff {l₁ : Array α} {l₂ : Array β} : + zip l₁ l₂ = l₁' ++ l₂' ↔ + ∃ w x y z, w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z := by + simp [zip_eq_zipWith, zipWith_eq_append_iff] + +@[simp] theorem zip_mkArray {a : α} {b : β} {m n : Nat} : + zip (mkArray m a) (mkArray n b) = mkArray (min m n) (a, b) := by + simp [← List.toArray_replicate] + +theorem zip_eq_zip_take_min (l₁ : Array α) (l₂ : Array β) : + zip l₁ l₂ = zip (l₁.take (min l₁.size l₂.size)) (l₂.take (min l₁.size l₂.size)) := by + cases l₁ + cases l₂ + simp only [List.zip_toArray, size_toArray, List.take_toArray, mk.injEq] + rw [List.zip_eq_zip_take_min] + + +/-! ### zipWithAll -/ + +theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} : + (zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with + | none, none => .none | a?, b? => some (f a? b?) := by + cases as + cases bs + simp [List.getElem?_zipWithAll] + rfl + +theorem zipWithAll_map {μ} (f : Option γ → Option δ → μ) (g : α → γ) (h : β → δ) (l₁ : Array α) (l₂ : Array β) : + zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂ := by + cases l₁ + cases l₂ + simp [List.zipWithAll_map] + +theorem zipWithAll_map_left (l₁ : Array α) (l₂ : Array β) (f : α → α') (g : Option α' → Option β → γ) : + zipWithAll g (l₁.map f) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂ := by + cases l₁ + cases l₂ + simp [List.zipWithAll_map_left] + +theorem zipWithAll_map_right (l₁ : Array α) (l₂ : Array β) (f : β → β') (g : Option α → Option β' → γ) : + zipWithAll g l₁ (l₂.map f) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂ := by + cases l₁ + cases l₂ + simp [List.zipWithAll_map_right] + +theorem map_zipWithAll {δ : Type _} (f : α → β) (g : Option γ → Option δ → α) (l : Array γ) (l' : Array δ) : + map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l' := by + cases l + cases l' + simp [List.map_zipWithAll] + + +@[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} : + zipWithAll f (mkArray n a) (mkArray n b) = mkArray n (f a b) := by + simp [← List.toArray_replicate] + +/-! ### unzip -/ + +@[simp] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by + induction l <;> simp_all + +@[simp] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by + induction l <;> simp_all + +theorem unzip_eq_map (l : Array (α × β)) : unzip l = (l.map Prod.fst, l.map Prod.snd) := by + cases l + simp [List.unzip_eq_map] + +theorem zip_unzip (l : Array (α × β)) : zip (unzip l).1 (unzip l).2 = l := by + cases l + simp only [List.unzip_toArray, Prod.map_fst, Prod.map_snd, List.zip_toArray, List.zip_unzip] + +theorem unzip_zip_left {l₁ : Array α} {l₂ : Array β} (h : l₁.size ≤ l₂.size) : + (unzip (zip l₁ l₂)).1 = l₁ := by + cases l₁ + cases l₂ + simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, Prod.map_fst, + List.unzip_zip_left] + +theorem unzip_zip_right {l₁ : Array α} {l₂ : Array β} (h : l₂.size ≤ l₁.size) : + (unzip (zip l₁ l₂)).2 = l₂ := by + cases l₁ + cases l₂ + simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, Prod.map_snd, + List.unzip_zip_right] + +theorem unzip_zip {l₁ : Array α} {l₂ : Array β} (h : l₁.size = l₂.size) : + unzip (zip l₁ l₂) = (l₁, l₂) := by + cases l₁ + cases l₂ + simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, List.unzip_zip, Prod.map_apply] + +theorem zip_of_prod {l : Array α} {l' : Array β} {lp : Array (α × β)} (hl : lp.map Prod.fst = l) + (hr : lp.map Prod.snd = l') : lp = l.zip l' := by + rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip] + +@[simp] theorem unzip_mkArray {n : Nat} {a : α} {b : β} : + unzip (mkArray n (a, b)) = (mkArray n a, mkArray n b) := by + ext1 <;> simp diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index d6337ac0aa..9a2c53d79f 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -312,7 +312,7 @@ theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray] @[simp] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) : - Array.zipWith as.toArray bs.toArray f = (List.zipWith f as bs).toArray := by + Array.zipWith f as.toArray bs.toArray = (List.zipWith f as bs).toArray := by rw [Array.zipWith] simp [zipWithAux_toArray_zero] @@ -355,7 +355,7 @@ theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → O decreasing_by simp_wf; decreasing_trivial_pre_omega @[simp] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) : - Array.zipWithAll as.toArray bs.toArray f = (List.zipWithAll f as bs).toArray := by + Array.zipWithAll f as.toArray bs.toArray = (List.zipWithAll f as bs).toArray := by simp [Array.zipWithAll, zipWithAll_go_toArray] @[simp] theorem toArray_appendList (l₁ l₂ : List α) : diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean index 0b247f89f7..7c6ab01bd5 100644 --- a/src/Init/Data/List/Zip.lean +++ b/src/Init/Data/List/Zip.lean @@ -31,16 +31,18 @@ theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y simp only [comm] @[simp] -theorem zipWith_same (f : α → α → δ) : ∀ l : List α, zipWith f l l = l.map fun a => f a a +theorem zipWith_self (f : α → α → δ) : ∀ l : List α, zipWith f l l = l.map fun a => f a a | [] => rfl - | _ :: xs => congrArg _ (zipWith_same f xs) + | _ :: xs => congrArg _ (zipWith_self f xs) + +@[deprecated zipWith_self (since := "2025-01-29")] abbrev zipWith_same := @zipWith_self /-- See also `getElem?_zipWith'` for a variant using `Option.map` and `Option.bind` rather than a `match`. -/ theorem getElem?_zipWith {f : α → β → γ} {i : Nat} : - (List.zipWith f as bs)[i]? = match as[i]?, bs[i]? with + (zipWith f as bs)[i]? = match as[i]?, bs[i]? with | some a, some b => some (f a b) | _, _ => none := by induction as generalizing bs i with | nil => cases bs with @@ -257,8 +259,7 @@ theorem zip_map (f : α → γ) (g : β → δ) : ∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g) | [], _ => rfl | _, [] => by simp only [map, zip_nil_right] - | _ :: _, _ :: _ => by - simp only [map, zip_cons_cons, zip_map, Prod.map]; try constructor -- TODO: remove try constructor after update stage0 + | _ :: _, _ :: _ => by simp only [map, zip_cons_cons, zip_map, Prod.map] theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) : zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id] diff --git a/src/Init/Data/Vector.lean b/src/Init/Data/Vector.lean index b51acfd417..e6474dd81f 100644 --- a/src/Init/Data/Vector.lean +++ b/src/Init/Data/Vector.lean @@ -10,4 +10,5 @@ import Init.Data.Vector.Lex import Init.Data.Vector.MapIdx import Init.Data.Vector.Count import Init.Data.Vector.DecidableEq +import Init.Data.Vector.Zip import Init.Data.Vector.OfFn diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index b697bc3b91..1f803c8e96 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -206,8 +206,11 @@ abbrev zipWithIndex := @zipIdx ⟨v.toArray.zip w.toArray, by simp⟩ /-- 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⟩ +@[inline] def zipWith (f : α → β → φ) (a : Vector α n) (b : Vector β n) : Vector φ n := + ⟨Array.zipWith f a.toArray b.toArray, by simp⟩ + +@[inline] def unzip (v : Vector (α × β) n) : Vector α n × Vector β n := + ⟨⟨v.toArray.unzip.1, by simp⟩, ⟨v.toArray.unzip.2, by simp⟩⟩ /-- The vector of length `n` whose `i`-th element is `f i`. -/ @[inline] def ofFn (f : Fin n → α) : Vector α n := diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 1d24cf7773..b49debe895 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -158,8 +158,14 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a abbrev zipWithIndex_mk := @zipIdx_mk @[simp] theorem mk_zipWith_mk (f : α → β → γ) (a : Array α) (b : Array β) - (ha : a.size = n) (hb : b.size = n) : zipWith (Vector.mk a ha) (Vector.mk b hb) f = - Vector.mk (Array.zipWith a b f) (by simp [ha, hb]) := rfl + (ha : a.size = n) (hb : b.size = n) : zipWith f (Vector.mk a ha) (Vector.mk b hb) = + Vector.mk (Array.zipWith f a b) (by simp [ha, hb]) := rfl + +@[simp] theorem mk_zip_mk (a : Array α) (b : Array β) (ha : a.size = n) (hb : b.size = n) : + zip (Vector.mk a ha) (Vector.mk b hb) = Vector.mk (Array.zip a b) (by simp [ha, hb]) := rfl + +@[simp] theorem unzip_mk (a : Array (α × β)) (h : a.size = n) : + (Vector.mk a h).unzip = (Vector.mk a.unzip.1 (by simp_all), Vector.mk a.unzip.2 (by simp_all)) := rfl @[simp] theorem anyM_mk [Monad m] (p : α → m Bool) (a : Array α) (h : a.size = n) : (Vector.mk a h).anyM p = a.anyM p := rfl @@ -280,7 +286,7 @@ abbrev zipWithIndex_mk := @zipIdx_mk (a.zipIdx k).toArray = a.toArray.zipIdx k := rfl @[simp] theorem toArray_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) : - (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl + (Vector.zipWith f a b).toArray = Array.zipWith f a.toArray b.toArray := rfl @[simp] theorem anyM_toArray [Monad m] (p : α → m Bool) (v : Vector α n) : v.toArray.anyM p = v.anyM p := by @@ -417,7 +423,7 @@ theorem toList_swap (a : Vector α n) (i j) (hi hj) : simp [List.take_of_length_le] @[simp] theorem toList_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) : - (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl + (Vector.zipWith f a b).toArray = Array.zipWith f a.toArray b.toArray := rfl @[simp] theorem anyM_toList [Monad m] (p : α → m Bool) (v : Vector α n) : v.toList.anyM p = v.anyM p := by @@ -2167,7 +2173,7 @@ defeq issues in the implicit size argument. /-! ### zipWith -/ @[simp] theorem getElem_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) (i : Nat) - (hi : i < n) : (zipWith a b f)[i] = f a[i] b[i] := by + (hi : i < n) : (zipWith f a b)[i] = f a[i] b[i] := by cases a cases b simp diff --git a/src/Init/Data/Vector/Zip.lean b/src/Init/Data/Vector/Zip.lean new file mode 100644 index 0000000000..fb451aef0b --- /dev/null +++ b/src/Init/Data/Vector/Zip.lean @@ -0,0 +1,287 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +prelude +import Init.Data.Array.Zip +import Init.Data.Vector.Lemmas + +/-! +# Lemmas about `Vector.zip`, `Vector.zipWith`, `Vector.zipWithAll`, and `Vector.unzip`. +-/ + +namespace Vector + +open Nat + +/-! ## Zippers -/ + +/-! ### zipWith -/ + +theorem zipWith_comm (f : α → β → γ) (la : Vector α n) (lb : Vector β n) : + zipWith f la lb = zipWith (fun b a => f a b) lb la := by + rcases la with ⟨la, rfl⟩ + rcases lb with ⟨lb, h⟩ + simpa using Array.zipWith_comm _ _ _ + +theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y = f y x) (l l' : Vector α n) : + zipWith f l l' = zipWith f l' l := by + rw [zipWith_comm] + simp only [comm] + +@[simp] +theorem zipWith_self (f : α → α → δ) (l : Vector α n) : zipWith f l l = l.map fun a => f a a := by + cases l + simp + +/-- +See also `getElem?_zipWith'` for a variant +using `Option.map` and `Option.bind` rather than a `match`. +-/ +theorem getElem?_zipWith {f : α → β → γ} {i : Nat} : + (zipWith f as bs)[i]? = match as[i]?, bs[i]? with + | some a, some b => some (f a b) | _, _ => none := by + cases as + cases bs + simp [Array.getElem?_zipWith] + rfl + +/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`. -/ +theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} : + (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g := by + cases l₁ + cases l₂ + simp [Array.getElem?_zipWith'] + +theorem getElem?_zipWith_eq_some {f : α → β → γ} {l₁ : Vector α n} {l₂ : Vector β n} {z : γ} {i : Nat} : + (zipWith f l₁ l₂)[i]? = some z ↔ + ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z := by + cases l₁ + cases l₂ + simp [Array.getElem?_zipWith_eq_some] + +theorem getElem?_zip_eq_some {l₁ : Vector α n} {l₂ : Vector β n} {z : α × β} {i : Nat} : + (zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2 := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simp [Array.getElem?_zip_eq_some] + +@[simp] +theorem zipWith_map {μ} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : Vector α n) (l₂ : Vector β n) : + zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂ := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simp [Array.zipWith_map] + +theorem zipWith_map_left (l₁ : Vector α n) (l₂ : Vector β n) (f : α → α') (g : α' → β → γ) : + zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂ := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simp [Array.zipWith_map_left] + +theorem zipWith_map_right (l₁ : Vector α n) (l₂ : Vector β n) (f : β → β') (g : α → β' → γ) : + zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂ := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simp [Array.zipWith_map_right] + +theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} (i : δ): + (zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simpa using Array.zipWith_foldr_eq_zip_foldr _ + +theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ): + (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simpa using Array.zipWith_foldl_eq_zip_foldl _ + + +theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : Vector γ n) (l' : Vector δ n) : + map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l' := by + rcases l with ⟨l, rfl⟩ + rcases l' with ⟨l', h⟩ + simp [Array.map_zipWith] + +theorem take_zipWith : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n) := by + rcases l with ⟨l, rfl⟩ + rcases l' with ⟨l', h⟩ + simp [Array.take_zipWith] + +theorem extract_zipWith : (zipWith f l l').extract m n = zipWith f (l.extract m n) (l'.extract m n) := by + rcases l with ⟨l, rfl⟩ + rcases l' with ⟨l', h⟩ + simp [Array.extract_zipWith] + +theorem zipWith_append (f : α → β → γ) + (l : Vector α n) (la : Vector α m) (l' : Vector β n) (lb : Vector β m) : + zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb := by + rcases l with ⟨l, rfl⟩ + rcases l' with ⟨l', h⟩ + rcases la with ⟨la, rfl⟩ + rcases lb with ⟨lb, h'⟩ + simp [Array.zipWith_append, *] + +theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : Vector α (n + m)} {l₂ : Vector β (n + m)} : + zipWith f l₁ l₂ = l₁' ++ l₂' ↔ + ∃ w x y z, l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z := by + rcases l₁ with ⟨l₁, h₁⟩ + rcases l₂ with ⟨l₂, h₂⟩ + rcases l₁' with ⟨l₁', rfl⟩ + rcases l₂' with ⟨l₂', rfl⟩ + simp only [mk_zipWith_mk, mk_append_mk, eq_mk, Array.zipWith_eq_append_iff, + mk_eq, toArray_append, toArray_zipWith] + constructor + · rintro ⟨w, x, y, z, h, rfl, rfl, rfl, rfl⟩ + simp only [Array.size_append, Array.size_zipWith] at h₁ h₂ + exact ⟨mk w (by simp; omega), mk x (by simp; omega), mk y (by simp; omega), mk z (by simp; omega), by simp⟩ + · rintro ⟨⟨w, hw⟩, ⟨x, hx⟩, ⟨y, hy⟩, ⟨z, hz⟩, rfl, rfl, w₁, w₂⟩ + simp only at w₁ w₂ + exact ⟨w, x, y, z, by simpa [hw, hy] using ⟨w₁, w₂⟩⟩ + +@[simp] theorem zipWith_mkVector {a : α} {b : β} {n : Nat} : + zipWith f (mkVector n a) (mkVector n b) = mkVector n (f a b) := by + ext + simp + +theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (l : Vector α n) (l' : Vector β n) : + map (Function.uncurry f) (l.zip l') = zipWith f l l' := by + rcases l with ⟨l, rfl⟩ + rcases l' with ⟨l', h⟩ + simp [Array.map_uncurry_zip_eq_zipWith] + +theorem map_zip_eq_zipWith (f : α × β → γ) (l : Vector α n) (l' : Vector β n) : + map f (l.zip l') = zipWith (Function.curry f) l l' := by + rcases l with ⟨l, rfl⟩ + rcases l' with ⟨l', h⟩ + simp [Array.map_zip_eq_zipWith] + +theorem reverse_zipWith : + (zipWith f l l').reverse = zipWith f l.reverse l'.reverse := by + rcases l with ⟨l, rfl⟩ + rcases l' with ⟨l', h⟩ + simp [Array.reverse_zipWith, h] + +/-! ### zip -/ + +@[simp] +theorem getElem_zip {l : Vector α n} {l' : Vector β n} {i : Nat} {h : i < n} : + (zip l l')[i] = (l[i], l'[i]) := + getElem_zipWith .. + +theorem zip_eq_zipWith (l₁ : Vector α n) (l₂ : Vector β n) : zip l₁ l₂ = zipWith Prod.mk l₁ l₂ := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simp [Array.zip_eq_zipWith, h] + +theorem zip_map (f : α → γ) (g : β → δ) (l₁ : Vector α n) (l₂ : Vector β n) : + zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g) := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simp [Array.zip_map, h] + +theorem zip_map_left (f : α → γ) (l₁ : Vector α n) (l₂ : Vector β n) : + zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id] + +theorem zip_map_right (f : β → γ) (l₁ : Vector α n) (l₂ : Vector β n) : + zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id] + +theorem zip_append {l₁ : Vector α n} {l₂ : Vector β n} {r₁ : Vector α m} {r₂ : Vector β m} : + zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂ := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + rcases r₁ with ⟨r₁, rfl⟩ + rcases r₂ with ⟨r₂, h'⟩ + simp [Array.zip_append, h, h'] + +theorem zip_map' (f : α → β) (g : α → γ) (l : Vector α n) : + zip (l.map f) (l.map g) = l.map fun a => (f a, g a) := by + rcases l with ⟨l, rfl⟩ + simp [Array.zip_map'] + +theorem of_mem_zip {a b} {l₁ : Vector α n} {l₂ : Vector β n} : (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂ := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simpa using Array.of_mem_zip + +theorem map_fst_zip (l₁ : Vector α n) (l₂ : Vector β n) : + map Prod.fst (zip l₁ l₂) = l₁ := by + cases l₁ + cases l₂ + simp_all [Array.map_fst_zip] + +theorem map_snd_zip (l₁ : Vector α n) (l₂ : Vector β n) : + map Prod.snd (zip l₁ l₂) = l₂ := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simp [Array.map_snd_zip, h] + +theorem map_prod_left_eq_zip {l : Vector α n} (f : α → β) : + (l.map fun x => (x, f x)) = l.zip (l.map f) := by + rcases l with ⟨l, rfl⟩ + rw [← zip_map'] + congr + simp + +theorem map_prod_right_eq_zip {l : Vector α n} (f : α → β) : + (l.map fun x => (f x, x)) = (l.map f).zip l := by + rcases l with ⟨l, rfl⟩ + rw [← zip_map'] + congr + simp + +theorem zip_eq_append_iff {l₁ : Vector α (n + m)} {l₂ : Vector β (n + m)} {l₁' : Vector (α × β) n} {l₂' : Vector (α × β) m} : + zip l₁ l₂ = l₁' ++ l₂' ↔ + ∃ w x y z, l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z := by + simp [zip_eq_zipWith, zipWith_eq_append_iff] + +@[simp] theorem zip_mkVector {a : α} {b : β} {n : Nat} : + zip (mkVector n a) (mkVector n b) = mkVector n (a, b) := by + ext <;> simp + + +/-! ### unzip -/ + +@[simp] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by + induction l <;> simp_all + +@[simp] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by + induction l <;> simp_all + +theorem unzip_eq_map (l : Vector (α × β) n) : unzip l = (l.map Prod.fst, l.map Prod.snd) := by + cases l + simp [List.unzip_eq_map] + +theorem zip_unzip (l : Vector (α × β) n) : zip (unzip l).1 (unzip l).2 = l := by + rcases l with ⟨l, rfl⟩ + simp only [unzip_mk, mk_zip_mk, Array.zip_unzip] + +theorem unzip_zip_left {l₁ : Vector α n} {l₂ : Vector β n} : + (unzip (zip l₁ l₂)).1 = l₁ := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simp [Array.unzip_zip_left, h, Array.map_fst_zip] + +theorem unzip_zip_right {l₁ : Vector α n} {l₂ : Vector β n} : + (unzip (zip l₁ l₂)).2 = l₂ := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simp [Array.unzip_zip_right, h, Array.map_snd_zip] + +theorem unzip_zip {l₁ : Vector α n} {l₂ : Vector β n} : + unzip (zip l₁ l₂) = (l₁, l₂) := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, h⟩ + simp [Array.unzip_zip, h, Array.map_fst_zip, Array.map_snd_zip] + +theorem zip_of_prod {l : Vector α n} {l' : Vector β n} {lp : Vector (α × β) n} (hl : lp.map Prod.fst = l) + (hr : lp.map Prod.snd = l') : lp = l.zip l' := by + rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip] + +@[simp] theorem unzip_mkVector {n : Nat} {a : α} {b : β} : + unzip (mkVector n (a, b)) = (mkVector n a, mkVector n b) := by + ext1 <;> simp + +end Vector diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean index 34c2c6bf72..d06ec02ba1 100644 --- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean +++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean @@ -80,7 +80,7 @@ partial def merge (v1 v2 : Value) : Value := | top, _ | _, top => top | ctor i1 vs1, ctor i2 vs2 => if i1 == i2 then - ctor i1 (vs1.zipWith vs2 merge) + ctor i1 (Array.zipWith merge vs1 vs2) else choice [v1, v2] | choice vs1, choice vs2 => diff --git a/src/Lean/Compiler/LCNF/SpecInfo.lean b/src/Lean/Compiler/LCNF/SpecInfo.lean index 0e7f2cefa7..8b4468cd47 100644 --- a/src/Lean/Compiler/LCNF/SpecInfo.lean +++ b/src/Lean/Compiler/LCNF/SpecInfo.lean @@ -186,7 +186,7 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do let mut paramsInfo := declsInfo[i]! let some mask := m.find? decl.name | unreachable! trace[Compiler.specialize.info] "{decl.name} {mask}" - paramsInfo := paramsInfo.zipWith mask fun info fixed => if fixed || info matches .user then info else .other + paramsInfo := Array.zipWith (fun info fixed => if fixed || info matches .user then info else .other) paramsInfo mask for j in [:paramsInfo.size] do let mut info := paramsInfo[j]! if info matches .fixedNeutral && !hasFwdDeps decl paramsInfo j then diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 54fcc53651..0774df29b5 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -496,8 +496,8 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do newStx := stxNew newNextMacroScope := nextMacroScope hasTraces - next := cmdPromises.zipWith cmds fun cmdPromise cmd => - { range? := cmd.getRange?, task := cmdPromise.result } + next := Array.zipWith (fun cmdPromise cmd => + { range? := cmd.getRange?, task := cmdPromise.result }) cmdPromises cmds : MacroExpandedSnapshot } -- After the first command whose syntax tree changed, we must disable diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index f15a7555ff..eab60edd2b 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -790,7 +790,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) -- (One for each non-forbiddend arg) let basicMeassures₁ ← simpleMeasures preDefs fixedPrefixSize userVarNamess let basicMeassures₂ ← complexMeasures preDefs fixedPrefixSize userVarNamess recCalls - let basicMeasures := Array.zipWith basicMeassures₁ basicMeassures₂ (· ++ ·) + let basicMeasures := Array.zipWith (· ++ ·) basicMeassures₁ basicMeassures₂ -- The list of measures, including the measures that order functions. -- The function ordering measures come last diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 91872d4831..e638e737fa 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -120,7 +120,7 @@ Expands fields. let fields? ← fields.mapM expandStructInstField if fields?.all (·.isNone) then Macro.throwUnsupported - let fields := fields?.zipWith fields Option.getD + let fields := Array.zipWith Option.getD fields? fields let structInstFields := structInstFields.setArg 0 <| Syntax.mkSep fields (mkAtomFrom stx ", ") return stx.setArg 2 structInstFields diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index a9b4d650aa..ce7e46cd66 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -286,8 +286,9 @@ where diagnostics := .empty inner? := none finished := { range? := none, task := finished.result } - next := altStxs.zipWith altPromises fun stx prom => - { range? := stx.getRange?, task := prom.result } + next := Array.zipWith + (fun stx prom => { range? := stx.getRange?, task := prom.result }) + altStxs altPromises } goWithIncremental <| altPromises.mapIdx fun i prom => { old? := do diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean index d6d84de667..05a4f8d34b 100644 --- a/src/Lean/Meta/ArgsPacker.lean +++ b/src/Lean/Meta/ArgsPacker.lean @@ -471,7 +471,7 @@ Given types `(x : A) → (y : B[x]) → R₁[x,y]` and `(z : C) → R₂[z]`, re ``` -/ def uncurryType (argsPacker : ArgsPacker) (types : Array Expr) : MetaM Expr := do - let unary ← (Array.zipWith argsPacker.varNamess types Unary.uncurryType).mapM id + let unary ← (Array.zipWith Unary.uncurryType argsPacker.varNamess types).mapM id Mutual.uncurryType unary /-- @@ -482,11 +482,11 @@ and `(z : C) → R₂[z]`, returns an expression of type ``` -/ def uncurry (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr := do - let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id + let unary ← (Array.zipWith Unary.uncurry argsPacker.varNamess es).mapM id Mutual.uncurry unary def uncurryWithType (argsPacker : ArgsPacker) (resultType : Expr) (es : Array Expr) : MetaM Expr := do - let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id + let unary ← (Array.zipWith Unary.uncurry argsPacker.varNamess es).mapM id Mutual.uncurryWithType resultType unary /-- @@ -497,7 +497,7 @@ and `(z : C) → R`, returns an expression of type ``` -/ def uncurryND (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr := do - let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id + let unary ← (Array.zipWith Unary.uncurry argsPacker.varNamess es).mapM id Mutual.uncurryND unary /-- @@ -533,7 +533,7 @@ Given type `(x : a ⊗' b ⊕' c ⊗' d) → R` (non-dependent), return types -/ def curryType (argsPacker : ArgsPacker) (t : Expr) : MetaM (Array Expr) := do let unary ← Mutual.curryType argsPacker.numFuncs t - (Array.zipWith argsPacker.varNamess unary Unary.curryType).mapM id + (Array.zipWith Unary.curryType argsPacker.varNamess unary).mapM id /-- Given expression `e` of type `(x : a ⊗' b ⊕' c ⊗' d) → e[x]`, wraps that expression diff --git a/tests/lean/run/array_isEqvAux.lean b/tests/lean/run/array_isEqvAux.lean index ea607f32ee..e8bfe5ddf7 100644 --- a/tests/lean/run/array_isEqvAux.lean +++ b/tests/lean/run/array_isEqvAux.lean @@ -42,6 +42,6 @@ example : #[0, 1, 2].insertIdx 1 3 = #[0, 3, 1, 2] := by decide example : #[0, 1, 2].isPrefixOf #[0, 1, 2, 3] = true := by decide -example : #[0, 1, 2].zipWith #[3, 4, 5] (· + ·) = #[3, 5, 7] := by decide +example : Array.zipWith (· + ·) #[0, 1, 2] #[3, 4, 5] = #[3, 5, 7] := by decide example : #[0, 1, 2].allDiff = true := by decide