From 75c104ce06ba4af52173b67932e9a7cc7196598e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 19 Jan 2025 19:40:06 +1100 Subject: [PATCH] feat: align List/Array/Vector.reverse lemmas (#6695) This PR aligns `List/Array/Vector.reverse` lemmas. --- src/Init/Data/Array/Lemmas.lean | 248 ++++++++++++++++++++----------- src/Init/Data/Vector/Lemmas.lean | 93 +++++++++++- tests/lean/run/grind_offset.lean | 2 +- 3 files changed, 251 insertions(+), 92 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 4dcffa7688..506c6813f4 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -2269,7 +2269,7 @@ theorem flatMap_mkArray {β} (f : α → Array β) : (mkArray n a).flatMap f = ( rw [← toList_inj] simp [flatMap_toList, List.flatMap_replicate] -@[simp] theorem isEmpty_replicate : (mkArray n a).isEmpty = decide (n = 0) := by +@[simp] theorem isEmpty_mkArray : (mkArray n a).isEmpty = decide (n = 0) := by rw [← List.toArray_replicate, List.isEmpty_toArray] simp @@ -2277,6 +2277,168 @@ theorem flatMap_mkArray {β} (f : α → Array β) : (mkArray n a).flatMap f = ( rw [← List.toArray_replicate, List.sum_toArray] simp +/-! ### Preliminaries about `swap` needed for `reverse`. -/ + +theorem swap_def (a : Array α) (i j : Nat) (hi hj) : + a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by + simp [swap] + +theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? = + if j = k then some a[i] else if i = k then some a[j] else a[k]? := by + simp [swap_def, getElem?_set] + +/-! ### reverse -/ + +@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by + let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by + rw [reverse.loop] + if h : i < j then + simp [(go · (i+1) ⟨j-1, ·⟩), h] + else simp [h] + termination_by j - i + simp only [reverse]; split <;> simp [go] + +@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by + let rec go (as : Array α) (i j hj) + (h : i + j + 1 = a.size) (h₂ : as.size = a.size) + (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?) + (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by + rw [reverse.loop]; dsimp only; split <;> rename_i h₁ + · match j with | j+1 => ?_ + simp only [Nat.add_sub_cancel] + rw [(go · (i+1) j)] + · rwa [Nat.add_right_comm i] + · simp [size_swap, h₂] + · intro k + rw [getElem?_toList, getElem?_swap] + simp only [H, ← getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁, + ← getElem?_toList] + split <;> rename_i h₂ + · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false] + exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm + split <;> rename_i h₃ + · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and] + exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm + simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃), + Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))] + · rw [H]; split <;> rename_i h₂ + · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2) + cases Nat.le_antisymm h₂.1 h₂.2 + exact (List.getElem?_reverse' _ _ h).symm + · rfl + termination_by j - i + simp only [reverse] + split + · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl + · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›) + refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_ + split + · rfl + · rename_i h + simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le, + true_and, Nat.not_lt] at h + rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)] + +@[simp] theorem _root_.List.reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by + apply ext' + simp only [toList_reverse] + +@[simp] theorem reverse_push (as : Array α) (a : α) : (as.push a).reverse = #[a] ++ as.reverse := by + cases as + simp + +@[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by + cases as + simp + +@[simp] theorem getElem_reverse (as : Array α) (i : Nat) (hi : i < as.reverse.size) : + (as.reverse)[i] = as[as.size - 1 - i]'(by simp at hi; omega) := by + cases as + simp + +@[simp] theorem reverse_eq_empty_iff {xs : Array α} : xs.reverse = #[] ↔ xs = #[] := by + cases xs + simp + +theorem reverse_ne_empty_iff {xs : Array α} : xs.reverse ≠ #[] ↔ xs ≠ #[] := + not_congr reverse_eq_empty_iff + +/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/ +theorem getElem?_reverse' {l : Array α} (i j) (h : i + j + 1 = l.size) : l.reverse[i]? = l[j]? := by + rcases l with ⟨l⟩ + simp at h + simp only [List.reverse_toArray, List.getElem?_toArray] + rw [List.getElem?_reverse' (l := l) _ _ h] + +@[simp] +theorem getElem?_reverse {l : Array α} {i} (h : i < l.size) : + l.reverse[i]? = l[l.size - 1 - i]? := by + cases l + simp_all + +@[simp] theorem reverse_reverse (as : Array α) : as.reverse.reverse = as := by + cases as + simp + +theorem reverse_eq_iff {as bs : Array α} : as.reverse = bs ↔ as = bs.reverse := by + constructor <;> (rintro rfl; simp) + +@[simp] theorem reverse_inj {xs ys : Array α} : xs.reverse = ys.reverse ↔ xs = ys := by + simp [reverse_eq_iff] + +@[simp] theorem reverse_eq_push_iff {xs : Array α} {ys : Array α} {a : α} : + xs.reverse = ys.push a ↔ xs = #[a] ++ ys.reverse := by + rw [reverse_eq_iff, reverse_push] + +@[simp] theorem map_reverse (f : α → β) (l : Array α) : l.reverse.map f = (l.map f).reverse := by + cases l <;> simp [*] + +@[simp] theorem filter_reverse (p : α → Bool) (l : Array α) : (l.reverse.filter p) = (l.filter p).reverse := by + cases l + simp + +@[simp] theorem filterMap_reverse (f : α → Option β) (l : Array α) : (l.reverse.filterMap f) = (l.filterMap f).reverse := by + cases l + simp + +@[simp] theorem reverse_append (as bs : Array α) : (as ++ bs).reverse = bs.reverse ++ as.reverse := by + cases as + cases bs + simp + +@[simp] theorem reverse_eq_append_iff {xs ys zs : Array α} : + xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse := by + cases xs + cases ys + cases zs + simp + +/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts. -/ +theorem reverse_flatten (L : Array (Array α)) : + L.flatten.reverse = (L.map reverse).reverse.flatten := by + cases L using array₂_induction + simp [flatten_toArray, List.reverse_flatten, Function.comp_def] + +/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result. -/ +theorem flatten_reverse (L : Array (Array α)) : + L.reverse.flatten = (L.map reverse).flatten.reverse := by + cases L using array₂_induction + simp [flatten_toArray, List.flatten_reverse, Function.comp_def] + +theorem reverse_flatMap {β} (l : Array α) (f : α → Array β) : + (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by + cases l + simp [List.reverse_flatMap, Function.comp_def] + +theorem flatMap_reverse {β} (l : Array α) (f : α → Array β) : + (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by + cases l + simp [List.flatMap_reverse, Function.comp_def] + +@[simp] theorem reverse_mkArray (n) (a : α) : reverse (mkArray n a) = mkArray n a := by + rw [← toList_inj] + simp + /-! Content below this point has not yet been aligned with `List`. -/ /-! ### sum -/ @@ -2468,6 +2630,7 @@ theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x @[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size +@[deprecated getElem_set_self (since := "2025-01-17")] theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) : (a.set i v h)[i]'(by simp [h]) = v := by simp only [set, ← getElem_toList, List.getElem_set_self] @@ -2491,17 +2654,9 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by simp only [set, ← getElem_toList, List.getElem_set_ne h] -theorem swap_def (a : Array α) (i j : Nat) (hi hj) : - a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by - simp [swap] - @[simp] theorem toList_swap (a : Array α) (i j : Nat) (hi hj) : (a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i] := by simp [swap_def] -theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? = - if j = k then some a[i] else if i = k then some a[j] else a[k]? := by - simp [swap_def, get?_set] - @[simp] theorem swapAt_def (a : Array α) (i : Nat) (v : α) (hi) : a.swapAt i v hi = (a[i], a.set i v) := rfl @@ -2555,15 +2710,6 @@ theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rf @[deprecated size_swapIfInBounds (since := "2024-11-24")] abbrev size_swap! := @size_swapIfInBounds -@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by - let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by - rw [reverse.loop] - if h : i < j then - simp [(go · (i+1) ⟨j-1, ·⟩), h] - else simp [h] - termination_by j - i - simp only [reverse]; split <;> simp [go] - @[simp] theorem size_range {n : Nat} : (range n).size = n := by induction n <;> simp [range] @@ -2574,61 +2720,6 @@ theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rf theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by simp [← getElem_toList] -@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by - let rec go (as : Array α) (i j hj) - (h : i + j + 1 = a.size) (h₂ : as.size = a.size) - (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?) - (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by - rw [reverse.loop]; dsimp only; split <;> rename_i h₁ - · match j with | j+1 => ?_ - simp only [Nat.add_sub_cancel] - rw [(go · (i+1) j)] - · rwa [Nat.add_right_comm i] - · simp [size_swap, h₂] - · intro k - rw [getElem?_toList, getElem?_swap] - simp only [H, ← getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁, - ← getElem?_toList] - split <;> rename_i h₂ - · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false] - exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm - split <;> rename_i h₃ - · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and] - exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm - simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃), - Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))] - · rw [H]; split <;> rename_i h₂ - · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2) - cases Nat.le_antisymm h₂.1 h₂.2 - exact (List.getElem?_reverse' _ _ h).symm - · rfl - termination_by j - i - simp only [reverse] - split - · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl - · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›) - refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_ - split - · rfl - · rename_i h - simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le, - true_and, Nat.not_lt] at h - rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)] - -end Array - -open Array - -namespace List - -@[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by - apply ext' - simp only [toList_reverse] - -end List - -namespace Array - /-! ### foldlM and foldrM -/ theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : Array α) : @@ -3324,17 +3415,6 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β | nil => simp | cons xs xss ih => simp [ih] -/-! ### reverse -/ - -@[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by - cases as - simp - -@[simp] theorem getElem_reverse (as : Array α) (i : Nat) (hi : i < as.reverse.size) : - (as.reverse)[i] = as[as.size - 1 - i]'(by simp at hi; omega) := by - cases as - simp [Array.getElem_reverse] - /-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/ @[simp] theorem findSomeRevM?_eq_findSomeM?_reverse diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 6021842d3f..b12146a9a0 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -1746,6 +1746,92 @@ theorem flatMap_mkArray {β} (f : α → Vector β m) : (mkVector n a).flatMap f @[simp] theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkVector n a).sum = n * a := by simp [toArray_mkVector] +/-! ### reverse -/ + +@[simp] theorem reverse_push (as : Vector α n) (a : α) : + (as.push a).reverse = (#v[a] ++ as.reverse).cast (by omega) := by + rcases as with ⟨as, rfl⟩ + simp [Array.reverse_push] + +@[simp] theorem mem_reverse {x : α} {as : Vector α n} : x ∈ as.reverse ↔ x ∈ as := by + cases as + simp + +@[simp] theorem getElem_reverse (a : Vector α n) (i : Nat) (hi : i < n) : + (a.reverse)[i] = a[n - 1 - i] := by + rcases a with ⟨a, rfl⟩ + simp + +/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/ +theorem getElem?_reverse' {l : Vector α n} (i j) (h : i + j + 1 = n) : l.reverse[i]? = l[j]? := by + rcases l with ⟨l, rfl⟩ + simpa using Array.getElem?_reverse' i j h + +@[simp] +theorem getElem?_reverse {l : Vector α n} {i} (h : i < n) : + l.reverse[i]? = l[n - 1 - i]? := by + cases l + simp_all + +@[simp] theorem reverse_reverse (as : Vector α n) : as.reverse.reverse = as := by + rcases as with ⟨as, rfl⟩ + simp [Array.reverse_reverse] + +theorem reverse_eq_iff {as bs : Vector α n} : as.reverse = bs ↔ as = bs.reverse := by + constructor <;> (rintro rfl; simp) + +@[simp] theorem reverse_inj {xs ys : Vector α n} : xs.reverse = ys.reverse ↔ xs = ys := by + simp [reverse_eq_iff] + +@[simp] theorem reverse_eq_push_iff {xs : Vector α (n + 1)} {ys : Vector α n} {a : α} : + xs.reverse = ys.push a ↔ xs = (#v[a] ++ ys.reverse).cast (by omega) := by + rcases xs with ⟨xs, h⟩ + rcases ys with ⟨ys, rfl⟩ + simp [Array.reverse_eq_push_iff] + +@[simp] theorem map_reverse (f : α → β) (l : Vector α n) : l.reverse.map f = (l.map f).reverse := by + rcases l with ⟨l, rfl⟩ + simp [Array.map_reverse] + +@[simp] theorem reverse_append (as : Vector α n) (bs : Vector α m) : + (as ++ bs).reverse = (bs.reverse ++ as.reverse).cast (by omega) := by + rcases as with ⟨as, rfl⟩ + rcases bs with ⟨bs, rfl⟩ + simp [Array.reverse_append] + +@[simp] theorem reverse_eq_append_iff {xs : Vector α (n + m)} {ys : Vector α n} {zs : Vector α m} : + xs.reverse = ys ++ zs ↔ xs = (zs.reverse ++ ys.reverse).cast (by omega) := by + cases xs + cases ys + cases zs + simp + +/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts. -/ +theorem reverse_flatten (L : Vector (Vector α m) n) : + L.flatten.reverse = (L.map reverse).reverse.flatten := by + cases L using vector₂_induction + simp [Array.reverse_flatten] + +/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result. -/ +theorem flatten_reverse (L : Vector (Vector α m) n) : + L.reverse.flatten = (L.map reverse).flatten.reverse := by + cases L using vector₂_induction + simp [Array.flatten_reverse] + +theorem reverse_flatMap {β} (l : Vector α n) (f : α → Vector β m) : + (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by + rcases l with ⟨l, rfl⟩ + simp [Array.reverse_flatMap, Function.comp_def] + +theorem flatMap_reverse {β} (l : Vector α n) (f : α → Vector β m) : + (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by + rcases l with ⟨l, rfl⟩ + simp [Array.flatMap_reverse, Function.comp_def] + +@[simp] theorem reverse_mkVector (n) (a : α) : reverse (mkVector n a) = mkVector n a := by + rw [← toArray_inj] + simp + /-! 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) : @@ -1877,13 +1963,6 @@ theorem swap_comm (a : Vector α n) {i j : Nat} {hi hj} : cases a simp -/-! ### reverse -/ - -@[simp] theorem getElem_reverse (a : Vector α n) (i : Nat) (hi : i < n) : - (a.reverse)[i] = a[n - 1 - i] := by - rcases a with ⟨a, rfl⟩ - simp - /-! ### Decidable quantifiers. -/ theorem forall_zero_iff {P : Vector α 0 → Prop} : diff --git a/tests/lean/run/grind_offset.lean b/tests/lean/run/grind_offset.lean index a817abe1fb..0b8c3a1a77 100644 --- a/tests/lean/run/grind_offset.lean +++ b/tests/lean/run/grind_offset.lean @@ -23,7 +23,7 @@ info: [grind.assert] f (y + 1) = a [grind.assert] f (y + 1) = g (f y) -/ #guard_msgs (info) in -example : f (y + 1) = a → a = g (f y):= by +example : f (y + 1) = a → a = g (f y) := by grind /--