Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: lemmas about Vector.any/all/set #6369

Merged
merged 2 commits into from
Dec 12, 2024
Merged

feat: lemmas about Vector.any/all/set #6369

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
197cfee
feat: lemmas about Vector.any/all/set
kim-em Dec 12, 2024
b6eeab2
deprecation
kim-em Dec 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions src/Init/Data/Array/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -662,9 +662,15 @@ def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool
def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
Id.run <| as.allM p start stop

/-- `as.contains a` is true if there is some element `b` in `as` such that `a == b`. -/
def contains [BEq α] (as : Array α) (a : α) : Bool :=
as.any (a == ·)

/--
Variant of `Array.contains` with arguments reversed.

For verification purposes, we simplify this to `contains`.
-/
def elem [BEq α] (a : α) (as : Array α) : Bool :=
as.contains a

Expand Down
107 changes: 60 additions & 47 deletions src/Init/Data/Array/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -483,7 +483,7 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
rw [Bool.eq_false_iff, Ne, any_eq_true]
simp

theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
@[simp] theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]
simp only [List.mem_iff_getElem, getElem_toList]
exact ⟨fun ⟨_, ⟨i, w, rfl⟩, h⟩ => ⟨i, w, h⟩, fun ⟨i, w, h⟩ => ⟨_, ⟨i, w, rfl⟩, h⟩⟩
Expand Down Expand Up @@ -522,7 +522,7 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
rw [Bool.eq_false_iff, Ne, all_eq_true]
simp

theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
@[simp] theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]
simp only [List.mem_iff_getElem, getElem_toList]
constructor
Expand All @@ -534,20 +534,6 @@ theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all
theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
simp only [← all_toList, List.all_eq_true, mem_def]

theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
l.toArray.anyM p = l.anyM p := by
rw [← anyM_toList]

theorem _root_.List.any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
rw [any_toList]

theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
l.toArray.allM p = l.allM p := by
rw [← allM_toList]

theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
rw [all_toList]

/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
@[simp] theorem _root_.List.anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
(h : stop = l.toArray.size) :
Expand All @@ -574,6 +560,20 @@ theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all
subst h
rw [all_toList]

theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
l.toArray.anyM p = l.anyM p := by
rw [← anyM_toList]

theorem _root_.List.any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
rw [any_toList]

theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
l.toArray.allM p = l.allM p := by
rw [← allM_toList]

theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
rw [all_toList]

/-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
theorem any_eq_true' {p : α → Bool} {as : Array α} :
as.any p = true ↔ (∃ x, x ∈ as ∧ p x) := by
Expand Down Expand Up @@ -641,7 +641,7 @@ theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
l.toArray.contains a = l.contains a := by
simp [Array.contains, List.any_beq]

@[simp] theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
Array.elem a l.toArray = List.elem a l := by
simp [Array.elem]

Expand All @@ -663,26 +663,32 @@ theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Array α} :
(xs.all fun x => x != a) = !xs.contains a := by
simp only [bne_comm, all_bne]

theorem mem_of_elem_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : elem a as = true → a ∈ as := by
theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : as.contains a = true → a ∈ as := by
cases as
simp

theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : elem a as = true := by
@[deprecated mem_of_contains_eq_true (since := "2024-12-12")]
abbrev mem_of_elem_eq_true := @mem_of_contains_eq_true

theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true := by
cases as
simpa using h

@[deprecated contains_eq_true_of_mem (since := "2024-12-12")]
abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem

instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
decidable_of_decidable_of_iff (Iff.intro mem_of_contains_eq_true contains_eq_true_of_mem)

@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : Array α} :
elem a l = l.contains a := by
simp [elem]

theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
elem a as = true ↔ a ∈ as := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩

theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
as.contains a = true ↔ a ∈ as := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩

theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
Expand Down Expand Up @@ -762,24 +768,24 @@ theorem getElem?_set (a : Array α) (i : Nat) (h : i < a.size) (v : α) (j : Nat
cases as <;> cases n <;> simp [set]

theorem set_comm (a b : α)
{n m : Nat} (as : Array α) {hn : n < as.size} {hm : m < (as.set n a).size} (h : n ≠ m) :
(as.set n a).set m b = (as.set m b (by simpa using hm)).set n a (by simpa using hn) := by
{i j : Nat} (as : Array α) {hi : i < as.size} {hj : j < (as.set i a).size} (h : i ≠ j) :
(as.set i a).set j b = (as.set j b (by simpa using hj)).set i a (by simpa using hi) := by
cases as
simp [List.set_comm _ _ _ h]

@[simp]
theorem set_set (a b : α) (as : Array α) (n : Nat) (h : n < as.size) :
(as.set n a).set n b (by simpa using h) = as.set n b := by
theorem set_set (a b : α) (as : Array α) (i : Nat) (h : i < as.size) :
(as.set i a).set i b (by simpa using h) = as.set i b := by
cases as
simp

theorem mem_set (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
a ∈ as.set n a := by
theorem mem_set (as : Array α) (i : Nat) (h : i < as.size) (a : α) :
a ∈ as.set i a := by
simp [mem_iff_getElem]
exact ⟨n, (by simpa using h), by simp⟩
exact ⟨i, (by simpa using h), by simp⟩

theorem mem_or_eq_of_mem_set
{as : Array α} {n : Nat} {a b : α} {w : n < as.size} (h : a ∈ as.set n b) : a ∈ as ∨ a = b := by
{as : Array α} {i : Nat} {a b : α} {w : i < as.size} (h : a ∈ as.set i b) : a ∈ as ∨ a = b := by
cases as
simpa using List.mem_or_eq_of_mem_set (by simpa using h)

Expand All @@ -788,7 +794,10 @@ theorem mem_or_eq_of_mem_set

/-! ### setIfInBounds -/

@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
@[simp] theorem set!_eq_setIfInBounds : @set! = @setIfInBounds := rfl

@[deprecated set!_eq_setIfInBounds (since := "2024-12-12")]
abbrev set!_is_setIfInBounds := @set!_eq_setIfInBounds

@[simp] theorem size_setIfInBounds (as : Array α) (index : Nat) (val : α) :
(as.setIfInBounds index val).size = as.size := by
Expand Down Expand Up @@ -820,19 +829,23 @@ abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
(as.setIfInBounds i v)[j]'hj = as[j]'(by simpa using hj) := by
simp [getElem_setIfInBounds, h]

theorem getElem?_setIfInBounds {as : Array α} {i j : Nat} {a : α} :
(as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]? := by
cases as
simp [List.getElem?_set]

theorem getElem?_setIfInBounds_self (as : Array α) {i : Nat} (v : α) :
(as.setIfInBounds i v)[i]? = if i < as.size then some v else none := by
simp [getElem?_setIfInBounds]

@[simp]
theorem getElem?_setIfInBounds_self (as : Array α) {i : Nat} (p : i < as.size) (v : α) :
theorem getElem?_setIfInBounds_self_of_lt (as : Array α) {i : Nat} (v : α) (h : i < as.size) :
(as.setIfInBounds i v)[i]? = some v := by
simp [getElem?_eq_getElem, p]
simp [getElem?_setIfInBounds, h]

@[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self

theorem getElem?_setIfInBounds {as : Array α} {i j : Nat} {a : α} :
(as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]? := by
cases as
simp [List.getElem?_set]

@[simp] theorem getElem?_setIfInBounds_ne {as : Array α} {i j : Nat} (h : i ≠ j) {a : α} :
(as.setIfInBounds i a)[j]? = as[j]? := by
simp [getElem?_setIfInBounds, h]
Expand All @@ -847,24 +860,24 @@ theorem setIfInBounds_eq_of_size_le {l : Array α} {n : Nat} (h : l.size ≤ n)
cases as <;> cases n <;> simp

theorem setIfInBounds_comm (a b : α)
{n m : Nat} (as : Array α) (h : n ≠ m) :
(as.setIfInBounds n a).setIfInBounds m b = (as.setIfInBounds m b).setIfInBounds n a := by
{i j : Nat} (as : Array α) (h : i ≠ j) :
(as.setIfInBounds i a).setIfInBounds j b = (as.setIfInBounds j b).setIfInBounds i a := by
cases as
simp [List.set_comm _ _ _ h]

@[simp]
theorem setIfInBounds_setIfInBounds (a b : α) (as : Array α) (n : Nat) :
(as.setIfInBounds n a).setIfInBounds n b = as.setIfInBounds n b := by
theorem setIfInBounds_setIfInBounds (a b : α) (as : Array α) (i : Nat) :
(as.setIfInBounds i a).setIfInBounds i b = as.setIfInBounds i b := by
cases as
simp

theorem mem_setIfInBounds (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
a ∈ as.setIfInBounds n a := by
theorem mem_setIfInBounds (as : Array α) (i : Nat) (h : i < as.size) (a : α) :
a ∈ as.setIfInBounds i a := by
simp [mem_iff_getElem]
exact ⟨n, (by simpa using h), by simp⟩
exact ⟨i, (by simpa using h), by simp⟩

theorem mem_or_eq_of_mem_setIfInBounds
{as : Array α} {n : Nat} {a b : α} (h : a ∈ as.setIfInBounds n b) : a ∈ as ∨ a = b := by
{as : Array α} {i : Nat} {a b : α} (h : a ∈ as.setIfInBounds i b) : a ∈ as ∨ a = b := by
cases as
simpa using List.mem_or_eq_of_mem_set (by simpa using h)

Expand Down Expand Up @@ -2395,7 +2408,7 @@ abbrev get?_eq_toList_get? := @get?_eq_get?_toList
@[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero

@[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_is_setIfInBounds
@[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_eq_setIfInBounds
@[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_self
@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_self
Expand Down
Loading
Loading