From e05131122b5b7ee4ed08771d71fa49dec619150c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 29 Jan 2025 15:53:33 +1100 Subject: [PATCH] feat: finish aligning List/Array/Vector.ofFn lemmas (#6838) This PR completes aligning the (limited) verification API for `List/Array/Vector.ofFn`. --- src/Init/Data/Array/Lemmas.lean | 4 ++++ src/Init/Data/Array/OfFn.lean | 30 ++++++++++++++++++++++++++ src/Init/Data/List/Lemmas.lean | 4 ++++ src/Init/Data/List/OfFn.lean | 9 ++++++++ src/Init/Data/Vector.lean | 1 + src/Init/Data/Vector/Lemmas.lean | 8 +++---- src/Init/Data/Vector/OfFn.lean | 37 ++++++++++++++++++++++++++++++++ 7 files changed, 89 insertions(+), 4 deletions(-) create mode 100644 src/Init/Data/Array/OfFn.lean create mode 100644 src/Init/Data/Vector/OfFn.lean diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index d993032e80bf..67d3f5944436 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -397,6 +397,10 @@ theorem getElem_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ (i : Nat) (h : i < theorem getElem?_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ i : Nat, l[i]? = some a := let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩ +theorem mem_of_getElem {l : Array α} {i : Nat} {h} {a : α} (e : l[i] = a) : a ∈ l := by + subst e + simp + theorem mem_of_getElem? {l : Array α} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l := let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem .. diff --git a/src/Init/Data/Array/OfFn.lean b/src/Init/Data/Array/OfFn.lean new file mode 100644 index 000000000000..99030a63c28d --- /dev/null +++ b/src/Init/Data/Array/OfFn.lean @@ -0,0 +1,30 @@ +/- +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.Lemmas +import Init.Data.List.OfFn + +/-! +# Theorems about `Array.ofFn` +-/ + +namespace Array + +@[simp] +theorem ofFn_eq_empty_iff {f : Fin n → α} : ofFn f = #[] ↔ n = 0 := by + rw [← Array.toList_inj] + simp + +@[simp 500] +theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ i, f i = a := by + constructor + · intro w + obtain ⟨i, h, rfl⟩ := getElem_of_mem w + exact ⟨⟨i, by simpa using h⟩, by simp⟩ + · rintro ⟨i, rfl⟩ + apply mem_of_getElem (i := i) <;> simp + +end Array diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index b0617cafa347..77ef29b07481 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -436,6 +436,10 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ i : Nat, l[i]? = s let ⟨n, _, e⟩ := getElem_of_mem h exact ⟨n, e ▸ getElem?_eq_getElem _⟩ +theorem mem_of_getElem {l : List α} {i : Nat} {h} {a : α} (e : l[i] = a) : a ∈ l := by + subst e + simp + theorem mem_of_getElem? {l : List α} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l := let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem .. diff --git a/src/Init/Data/List/OfFn.lean b/src/Init/Data/List/OfFn.lean index e02f0c7c73e4..79b965e25fb1 100644 --- a/src/Init/Data/List/OfFn.lean +++ b/src/Init/Data/List/OfFn.lean @@ -68,6 +68,15 @@ theorem ofFn_succ {n} (f : Fin (n + 1) → α) : ofFn f = f 0 :: ofFn fun i => f theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by cases n <;> simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero, reduceCtorEq] +@[simp 500] +theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ i, f i = a := by + constructor + · intro w + obtain ⟨i, h, rfl⟩ := getElem_of_mem w + exact ⟨⟨i, by simpa using h⟩, by simp⟩ + · rintro ⟨i, rfl⟩ + apply mem_of_getElem (i := i) <;> simp + theorem head_ofFn {n} (f : Fin n → α) (h : ofFn f ≠ []) : (ofFn f).head h = f ⟨0, Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)⟩ := by rw [← getElem_zero (length_ofFn _ ▸ Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)), diff --git a/src/Init/Data/Vector.lean b/src/Init/Data/Vector.lean index 34a3b534ca40..b51acfd417fa 100644 --- a/src/Init/Data/Vector.lean +++ b/src/Init/Data/Vector.lean @@ -10,3 +10,4 @@ import Init.Data.Vector.Lex import Init.Data.Vector.MapIdx import Init.Data.Vector.Count import Init.Data.Vector.DecidableEq +import Init.Data.Vector.OfFn diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index dc8fa7c7f4a1..1d24cf77731d 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -776,6 +776,10 @@ theorem getElem_of_mem {a} {l : Vector α n} (h : a ∈ l) : ∃ (i : Nat) (h : theorem getElem?_of_mem {a} {l : Vector α n} (h : a ∈ l) : ∃ i : Nat, l[i]? = some a := let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩ +theorem mem_of_getElem {l : Vector α n} {i : Nat} {h} {a : α} (e : l[i] = a) : a ∈ l := by + subst e + simp + theorem mem_of_getElem? {l : Vector α n} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l := let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem .. @@ -2136,10 +2140,6 @@ theorem foldr_rel {l : Array α} {f g : α → β → β} {a b : β} (r : β → /-! 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) : - (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by - simp [ofFn] - @[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by rcases v with ⟨data, rfl⟩ simp diff --git a/src/Init/Data/Vector/OfFn.lean b/src/Init/Data/Vector/OfFn.lean new file mode 100644 index 000000000000..d7ff12f8f030 --- /dev/null +++ b/src/Init/Data/Vector/OfFn.lean @@ -0,0 +1,37 @@ +/- +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.Vector.Lemmas +import Init.Data.Array.OfFn + +/-! +# Theorems about `Vector.ofFn` +-/ + +namespace Vector + +@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) : + (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by + simp [ofFn] + +theorem getElem?_ofFn (f : Fin n → α) (i : Nat) : + (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by + simp [getElem?_def] + +@[simp 500] +theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ i, f i = a := by + constructor + · intro w + obtain ⟨i, h, rfl⟩ := getElem_of_mem w + exact ⟨⟨i, by simpa using h⟩, by simp⟩ + · rintro ⟨i, rfl⟩ + apply mem_of_getElem (i := i) <;> simp + +theorem back_ofFn {n} [NeZero n](f : Fin n → α) : + (ofFn f).back = f ⟨n - 1, by have := NeZero.ne n; omega⟩ := by + simp [back] + +end Vector