From d615e615d92d3a0fb3ce5863626bf429ccca7e5c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 25 Feb 2025 11:13:00 +1100 Subject: [PATCH] chore: align List.dropLast/Array.pop lemmas (#7208) This PR aligns lemmas for `List.dropLast` / `Array.pop` / `Vector.pop`. --- src/Init/Data/Array/Lemmas.lean | 94 ++++++++++++++++++++++++-------- src/Init/Data/Vector/Lemmas.lean | 66 ++++++++++++++++++++-- 2 files changed, 134 insertions(+), 26 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index ac3c972943..3531bb42e8 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -3349,6 +3349,78 @@ theorem size_leftpad (n : Nat) (a : α) (xs : Array α) : theorem size_rightpad (n : Nat) (a : α) (xs : Array α) : (rightpad n a xs).size = max n xs.size := by simp; omega +/-! ### contains -/ + +theorem elem_cons_self [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : (xs.push a).elem a = true := by simp + +theorem contains_eq_any_beq [BEq α] (xs : Array α) (a : α) : xs.contains a = xs.any (a == ·) := by + rcases xs with ⟨xs⟩ + simp [List.contains_eq_any_beq] + +theorem contains_iff_exists_mem_beq [BEq α] {xs : Array α} {a : α} : + xs.contains a ↔ ∃ a' ∈ xs, a == a' := by + rcases xs with ⟨xs⟩ + simp [List.contains_iff_exists_mem_beq] + +theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : + xs.contains a ↔ a ∈ xs := by + simp + +/-! ### more lemmas about `pop` -/ + +@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl + +@[simp] theorem pop_push (xs : Array α) : (xs.push x).pop = xs := by simp [pop] + +@[simp] theorem getElem_pop {xs : Array α} {i : Nat} (h : i < xs.pop.size) : + xs.pop[i] = xs[i]'(by simp at h; omega) := by + rcases xs with ⟨xs⟩ + simp [List.getElem_dropLast] + +theorem getElem?_pop (xs : Array α) (i : Nat) : + xs.pop[i]? = if i < xs.size - 1 then xs[i]? else none := by + rcases xs with ⟨xs⟩ + simp [List.getElem?_dropLast] + +theorem back_pop {xs : Array α} (h) : + xs.pop.back h = + xs[xs.size - 2]'(by simp at h; omega) := by + rcases xs with ⟨xs⟩ + simp [List.getLast_dropLast] + +theorem back?_pop {xs : Array α} : + xs.pop.back? = if xs.size ≤ 1 then none else xs[xs.size - 2]? := by + rcases xs with ⟨xs⟩ + simp [List.getLast?_dropLast] + +@[simp] theorem pop_append_of_ne_empty {xs : Array α} {ys : Array α} (h : ys ≠ #[]) : + (xs ++ ys).pop = xs ++ ys.pop := by + rcases xs with ⟨xs⟩ + rcases ys with ⟨ys⟩ + simp only [List.append_toArray, List.pop_toArray, mk.injEq] + rw [List.dropLast_append_of_ne_nil _ (by simpa using h)] + +theorem pop_append {xs ys : Array α} : + (xs ++ ys).pop = if ys.isEmpty then xs.pop else xs ++ ys.pop := by + split <;> simp_all + +@[simp] theorem pop_mkArray (n) (a : α) : (mkArray n a).pop = mkArray (n - 1) a := by + ext <;> simp + +theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {xs : Array α} (h : xs.size ≠ 0) : + xs = xs.pop.push xs.back! := by + apply ext + · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)] + · intros i h h' + if hlt : i < xs.pop.size then + rw [getElem_push_lt (h:=hlt), getElem_pop] + else + have heq : i = xs.pop.size := + Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt) + cases heq + rw [getElem_push_eq, back!] + simp [← getElem!_pos] + /-! Content below this point has not yet been aligned with `List`. -/ /-! ### sum -/ @@ -3588,28 +3660,6 @@ theorem swapAt!_def (xs : Array α) (i : Nat) (v : α) (h : i < xs.size) : · simp · rfl -@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl - -@[simp] theorem pop_push (xs : Array α) : (xs.push x).pop = xs := by simp [pop] - -@[simp] theorem getElem_pop (xs : Array α) (i : Nat) (hi : i < xs.pop.size) : - xs.pop[i] = xs[i]'(Nat.lt_of_lt_of_le (xs.size_pop ▸ hi) (Nat.sub_le _ _)) := - List.getElem_dropLast .. - -theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {xs : Array α} (h : xs.size ≠ 0) : - xs = xs.pop.push xs.back! := by - apply ext - · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)] - · intros i h h' - if hlt : i < xs.pop.size then - rw [getElem_push_lt (h:=hlt), getElem_pop] - else - have heq : i = xs.pop.size := - Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt) - cases heq - rw [getElem_push_eq, back!] - simp [← getElem!_pos] - theorem eq_push_of_size_ne_zero {xs : Array α} (h : xs.size ≠ 0) : ∃ (bs : Array α) (c : α), xs = bs.push c := let _ : Inhabited α := ⟨xs[0]⟩ diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 342e118051..ea96df0200 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -2442,6 +2442,68 @@ theorem back?_mkVector (a : α) (n : Nat) : (Vector.mk xs h).rightpad n a = Vector.mk (Array.rightpad n a xs) (by simp [h]; omega) := by simp [h] +/-! ### contains -/ + +theorem contains_eq_any_beq [BEq α] (xs : Vector α n) (a : α) : xs.contains a = xs.any (a == ·) := by + rcases xs with ⟨xs, rfl⟩ + simp [Array.contains_eq_any_beq] + +theorem contains_iff_exists_mem_beq [BEq α] {xs : Vector α n} {a : α} : + xs.contains a ↔ ∃ a' ∈ xs, a == a' := by + rcases xs with ⟨xs, rfl⟩ + simp [Array.contains_iff_exists_mem_beq] + +theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} : + xs.contains a ↔ a ∈ xs := by + simp + +/-! ### more lemmas about `pop` -/ + +@[simp] theorem pop_empty : (#v[] : Vector α 0).pop = #v[] := rfl + +@[simp] theorem pop_push (xs : Vector α n) : (xs.push x).pop = xs := by simp [pop] + +@[simp] theorem getElem_pop {xs : Vector α n} {i : Nat} (h : i < n - 1) : + xs.pop[i] = xs[i] := by + rcases xs with ⟨xs, rfl⟩ + simp + +theorem getElem?_pop (xs : Vector α n) (i : Nat) : + xs.pop[i]? = if i < n - 1 then xs[i]? else none := by + rcases xs with ⟨xs, rfl⟩ + simp [Array.getElem?_pop] + +theorem back_pop {xs : Vector α n} [h : NeZero (n - 1)] : + xs.pop.back = + xs[n - 2]'(by have := h.out; omega) := by + rcases xs with ⟨xs, rfl⟩ + simp [Array.back_pop] + +theorem back?_pop {xs : Vector α n} : + xs.pop.back? = if n ≤ 1 then none else xs[n - 2]? := by + rcases xs with ⟨xs, rfl⟩ + simp [Array.back?_pop] + +@[simp] theorem pop_append_of_size_ne_zero {xs : Vector α n} {ys : Vector α m} (h : m ≠ 0) : + (xs ++ ys).pop = (xs ++ ys.pop).cast (by omega) := by + rcases xs with ⟨xs, rfl⟩ + rcases ys with ⟨ys, rfl⟩ + simp only [mk_append_mk, pop_mk, cast_mk, eq_mk] + rw [Array.pop_append_of_ne_empty] + apply Array.ne_empty_of_size_pos + omega + +theorem pop_append {xs : Vector α n} {ys : Vector α m} : + (xs ++ ys).pop = if h : m = 0 then xs.pop.cast (by omega) else (xs ++ ys.pop).cast (by omega) := by + rcases xs with ⟨xs, rfl⟩ + rcases ys with ⟨ys, rfl⟩ + simp only [mk_append_mk, pop_mk, List.length_eq_zero_iff, Array.toList_eq_nil_iff, cast_mk, mk_eq] + rw [Array.pop_append] + split <;> simp_all + +@[simp] theorem pop_mkVector (n) (a : α) : (mkVector n a).pop = mkVector (n - 1) a := by + ext <;> simp + /-! Content below this point has not yet been aligned with `List` and `Array`. -/ set_option linter.indexVariables false in @@ -2449,10 +2511,6 @@ set_option linter.indexVariables false in rcases xs with ⟨xs, rfl⟩ simp -@[simp] theorem getElem_pop {xs : Vector α n} {i : Nat} (h : i < n - 1) : (xs.pop)[i] = xs[i] := by - rcases xs with ⟨xs, rfl⟩ - simp - /-- Variant of `getElem_pop` that will sometimes fire when `getElem_pop` gets stuck because of defeq issues in the implicit size argument.