From e7d8948fa6d57e291efb8afd531a6ff6bc2d2318 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 30 Jan 2025 18:04:50 +1100 Subject: [PATCH] feat: lemmas relating findIdx?/findFinIdx?/idxOf?/findIdxOf?/eraseP/erase on List and Array (#6864) This PR adds lemmas relating the operations on findIdx?/findFinIdx?/idxOf?/findIdxOf?/eraseP/erase on List and on Array. It's preliminary to aligning the verification lemmas for `find...` and `erase...`. --- src/Init/Data/Array/Basic.lean | 18 ++++++++ src/Init/Data/List/Find.lean | 25 ++++++++++ src/Init/Data/List/ToArray.lean | 81 +++++++++++++++++++++++++++++++++ 3 files changed, 124 insertions(+) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 1a30761a29..52fa2889b5 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -682,6 +682,24 @@ def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as decreasing_by simp_wf; decreasing_trivial_pre_omega loop 0 +theorem findIdx?_loop_eq_map_findFinIdx?_loop_val {xs : Array α} {p : α → Bool} {j} : + findIdx?.loop p xs j = (findFinIdx?.loop p xs j).map (·.val) := by + unfold findIdx?.loop + unfold findFinIdx?.loop + split <;> rename_i h + case isTrue => + split + case isTrue => simp + case isFalse => + have : xs.size - (j + 1) < xs.size - j := Nat.sub_succ_lt_self xs.size j h + rw [findIdx?_loop_eq_map_findFinIdx?_loop_val (j := j + 1)] + case isFalse => simp +termination_by xs.size - j + +theorem findIdx?_eq_map_findFinIdx?_val {xs : Array α} {p : α → Bool} : + xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by + simp [findIdx?, findFinIdx?, findIdx?_loop_eq_map_findFinIdx?_loop_val] + @[inline] def findIdx (p : α → Bool) (as : Array α) : Nat := (as.findIdx? p).getD as.size diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 82f406b395..17d7ebfcd3 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -886,6 +886,25 @@ theorem IsInfix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l List.findIdx? p l₂ = none → List.findIdx? p l₁ = none := h.sublist.findIdx?_eq_none +/-! ### findFinIdx? -/ + +theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} : + List.findIdx?.go p xs i = + (List.findFinIdx?.go p l xs i h).map (·.val) := by + unfold findIdx?.go + unfold findFinIdx?.go + split <;> rename_i a xs + · simp_all + · simp only + split + · simp + · rw [findIdx?_go_eq_map_findFinIdx?_go_val] + +theorem findIdx?_eq_map_findFinIdx?_val {xs : List α} {p : α → Bool} : + xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by + simp [findIdx?, findFinIdx?] + rw [findIdx?_go_eq_map_findFinIdx?_go_val] + /-! ### idxOf The verification API for `idxOf` is still incomplete. @@ -970,6 +989,12 @@ theorem idxOf?_cons [BEq α] (a : α) (xs : List α) (b : α) : @[deprecated idxOf?_eq_none_iff (since := "2025-01-29")] abbrev indexOf?_eq_none_iff := @idxOf?_eq_none_iff +/-! ### finIdxOf? -/ + +theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : List α} {a : α} : + xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by + simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val] + /-! ### lookup -/ section lookup diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 9a2c53d79f..3265ce85ce 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -462,4 +462,85 @@ decreasing_by · simp · simp_all [eraseIdx_eq_self.2] +@[simp] theorem findIdx?_toArray {as : List α} {p : α → Bool} : + as.toArray.findIdx? p = as.findIdx? p := by + unfold Array.findIdx? + suffices ∀ i, i ≤ as.length → + Array.findIdx?.loop p as.toArray (as.length - i) = + (findIdx? p (as.drop (as.length - i))).map fun j => j + (as.length - i) by + specialize this as.length + simpa + intro i + induction i with + | zero => simp [findIdx?.loop] + | succ i ih => + unfold findIdx?.loop + simp only [size_toArray, getElem_toArray] + split <;> rename_i h + · rw [drop_eq_getElem_cons h] + rw [findIdx?_cons] + split <;> rename_i h' + · simp + · intro w + have : as.length - (i + 1) + 1 = as.length - i := by omega + specialize ih (by omega) + simp only [Option.map_map, this, ih] + congr + ext + simp + omega + · have : as.length = 0 := by omega + simp_all + +@[simp] theorem findFinIdx?_toArray {as : List α} {p : α → Bool} : + as.toArray.findFinIdx? p = as.findFinIdx? p := by + have h := findIdx?_toArray (as := as) (p := p) + rw [findIdx?_eq_map_findFinIdx?_val, Array.findIdx?_eq_map_findFinIdx?_val] at h + rwa [Option.map_inj_right] at h + rintro ⟨x, hx⟩ ⟨y, hy⟩ rfl + simp + +theorem findFinIdx?_go_beq_eq_idxOfAux_toArray [BEq α] + {xs as : List α} {a : α} {i : Nat} {h} (w : as = xs.drop i) : + findFinIdx?.go (fun x => x == a) xs as i h = + xs.toArray.idxOfAux a i := by + unfold findFinIdx?.go + unfold idxOfAux + split <;> rename_i b as + · simp at h + simp [h] + · simp at h + rw [dif_pos (by simp; omega)] + simp only [getElem_toArray] + erw [getElem_drop' (j := 0)] + simp only [← w, getElem_cons_zero] + have : xs.length - (i + 1) < xs.length - i := by omega + rw [findFinIdx?_go_beq_eq_idxOfAux_toArray] + rw [← drop_drop, ← w] + simp +termination_by xs.length - i + +@[simp] theorem finIdxOf?_toArray [BEq α] {as : List α} {a : α} : + as.toArray.finIdxOf? a = as.finIdxOf? a := by + unfold Array.finIdxOf? + unfold finIdxOf? + unfold findFinIdx? + rw [findFinIdx?_go_beq_eq_idxOfAux_toArray] + simp + +@[simp] theorem idxOf?_toArray [BEq α] {as : List α} {a : α} : + as.toArray.idxOf? a = as.idxOf? a := by + rw [Array.idxOf?, finIdxOf?_toArray, idxOf?_eq_map_finIdxOf?_val] + +@[simp] theorem eraseP_toArray {as : List α} {p : α → Bool} : + as.toArray.eraseP p = (as.eraseP p).toArray := by + rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray] + split <;> simp [*, findIdx?_eq_map_findFinIdx?_val] + +@[simp] theorem erase_toArray [BEq α] [LawfulBEq α] {as : List α} {a : α} : + as.toArray.erase a = (as.erase a).toArray := by + rw [Array.erase, finIdxOf?_toArray, List.erase_eq_eraseIdx] + rw [idxOf?_eq_map_finIdxOf?_val] + split <;> simp_all + end List