max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: improvements to List.set and List.concat API (#4470)

Browse source
This commit is contained in:
Kim Morrison 2024-06-17 06:10:35 +01:00 • committed by GitHub
parent 03d01f4024
commit 2efcbfe803
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 148 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/Array/Lemmas.lean
View file

@ -242,7 +242,7 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
(h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
simp only [set, getElem_eq_data_getElem, List.getElem_set_ne _ h]
simp only [set, getElem_eq_data_getElem, List.getElem_set_ne h]
theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
(h : j < (a.set i v).size) :
@ -419,7 +419,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
(h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
simp only [set, getElem_eq_data_getElem, List.getElem_set_ne _ h]
simp only [set, getElem_eq_data_getElem, List.getElem_set_ne h]
theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
(setD a i v)[i] = v := by

182
src/Init/Data/List/Lemmas.lean
View file

@ -58,7 +58,7 @@ theorem head_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : h₁ = h₂ := (c
theorem tail_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : t₁ = t₂ := (cons.inj H).2
theorem cons_inj (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' :=
theorem cons_inj_right (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' :=
⟨tail_eq_of_cons_eq, congrArg _⟩
theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' :=
@ -71,7 +71,10 @@ theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b L, l = b :
theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [] => rfl
theorem ne_nil_of_length_eq_succ (_ : length l = succ n) : l ≠ [] := fun _ => nomatch l
theorem ne_nil_of_length_eq_add_one (_ : length l = n + 1) : l ≠ [] := fun _ => nomatch l
@[deprecated ne_nil_of_length_eq_add_one (since := "2024-06-16")]
abbrev ne_nil_of_length_eq_succ := @ne_nil_of_length_eq_add_one
@[simp] theorem length_eq_zero : length l = 0 ↔ l = [] :=
⟨eq_nil_of_length_eq_zero, fun h => h ▸ rfl⟩
@ -92,16 +95,13 @@ theorem length_pos_iff_exists_cons :
∀ {l : List α}, 0 < l.length ↔ ∃ h t, l = h :: t :=
⟨exists_cons_of_length_pos, fun ⟨_, _, eq⟩ => eq ▸ Nat.succ_pos _⟩
theorem exists_cons_of_length_succ :
theorem exists_cons_of_length_eq_add_one :
∀ {l : List α}, l.length = n + 1 → ∃ h t, l = h :: t
| _::_, _ => ⟨_, _, rfl⟩
theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero)
theorem exists_mem_of_ne_nil (l : List α) (h : l ≠ []) : ∃ x, x ∈ l :=
exists_mem_of_length_pos (length_pos.2 h)
theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
@ -252,32 +252,6 @@ theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
@[deprecated getElem?_concat_length (since := "2024-06-12")]
theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp
/-! ### concat -/
-- As `List.concat` is defined in `Init.Prelude`, we write the basic simplification lemmas here.
theorem concat_nil (a : α) : concat [] a = [a] :=
rfl
theorem concat_cons (a b : α) (l : List α) : concat (a :: l) b = a :: concat l b :=
rfl
theorem init_eq_of_concat_eq {a : α} {l₁ l₂ : List α} : concat l₁ a = concat l₂ a → l₁ = l₂ := by
simp
theorem last_eq_of_concat_eq {a b : α} {l : List α} : concat l a = concat l b → a = b := by
simp
theorem concat_ne_nil (a : α) (l : List α) : concat l a ≠ [] := by cases l <;> simp
theorem concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l₁ ++ a :: l₂ := by simp
theorem append_concat (a : α) (l₁ l₂ : List α) : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a := by simp
theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = L ++ [b]
| [] => .inl rfl
| a::l => match l, eq_nil_or_concat l with
| _, .inl rfl => .inr ⟨[], a, rfl⟩
| _, .inr ⟨L, b, rfl⟩ => .inr ⟨a::L, b, rfl⟩
/-! ### mem -/
@[simp] theorem not_mem_nil (a : α) : ¬ a ∈ [] := nofun
@ -290,6 +264,9 @@ theorem mem_cons_self (a : α) (l : List α) : a ∈ a :: l := .head ..
theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
theorem exists_mem_of_ne_nil (l : List α) (h : l ≠ []) : ∃ x, x ∈ l :=
exists_mem_of_length_pos (length_pos.2 h)
theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := by
cases l <;> simp [-not_or]
@ -387,52 +364,90 @@ theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a :=
/-! ### set -/
-- As `List.set` is defined in `Init.Prelude`, we write the basic simplification lemmas here.
@[simp] theorem set_nil (n : Nat) (a : α) : [].set n a = [] := rfl
@[simp] theorem set_zero (x : α) (xs : List α) (a : α) :
@[simp] theorem set_cons_zero (x : α) (xs : List α) (a : α) :
(x :: xs).set 0 a = a :: xs := rfl
@[simp] theorem set_succ (x : α) (xs : List α) (n : Nat) (a : α) :
@[simp] theorem set_cons_succ (x : α) (xs : List α) (n : Nat) (a : α) :
(x :: xs).set (n + 1) a = x :: xs.set n a := rfl
@[simp] theorem getElem_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) :
@[simp] theorem getElem_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
(l.set i a)[i] = a :=
match l, i with
| [], _ => by
simp at h
contradiction
| _ :: _, 0 => by
simp
| _ :: l, i + 1 => by
simp [getElem_set_eq l]
| _ :: _, 0 => by simp
| _ :: l, i + 1 => by simp [getElem_set_eq]
@[deprecated getElem_set_eq (since := "2024-06-12")]
theorem get_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) :
(l.set i a).get ⟨i, h⟩ = a :=
by simp
theorem get_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
(l.set i a).get ⟨i, h⟩ = a := by
simp
@[simp] theorem getElem_set_ne (l : List α) {i j : Nat} (h : i ≠ j) (a : α)
@[simp] theorem getElem?_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
(l.set i a)[i]? = some a := by
simp_all [getElem?_eq_some]
@[simp] theorem getElem_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α}
(hj : j < (l.set i a).length) :
(l.set i a)[j] = l[j]'(by simp at hj; exact hj) :=
match l, i, j with
| [], _, _ => by
simp
| _ :: _, 0, 0 => by
contradiction
| _ :: _, 0, _ + 1 => by
simp
| _ :: _, _ + 1, 0 => by
simp
| [], _, _ => by simp
| _ :: _, 0, 0 => by contradiction
| _ :: _, 0, _ + 1 => by simp
| _ :: _, _ + 1, 0 => by simp
| _ :: l, i + 1, j + 1 => by
have g : i ≠ j := h ∘ congrArg (· + 1)
simp [getElem_set_ne l g]
simp [getElem_set_ne g]
@[deprecated getElem_set_ne (since := "2024-06-12")]
theorem get_set_ne (l : List α) {i j : Nat} (h : i ≠ j) (a : α)
theorem get_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α}
(hj : j < (l.set i a).length) :
(l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ := by
simp [h]
@[simp] theorem getElem?_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α} :
(l.set i a)[j]? = l[j]? := by
by_cases hj : j < (l.set i a).length
· rw [getElem?_eq_getElem hj, getElem?_eq_getElem (by simp_all)]
simp_all
· rw [getElem?_eq_none.mpr (by simp_all), getElem?_eq_none.mpr (by simp_all)]
theorem getElem_set {l : List α} {m n} {a} (h) :
(set l m a)[n]'h = if m = n then a else l[n]'(length_set .. ▸ h) := by
if h : m = n then
subst m; simp only [getElem_set_eq, ↓reduceIte]
else
simp [h]
@[deprecated getElem_set (since := "2024-06-12")]
theorem get_set {l : List α} {m n} {a : α} (h) :
(set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by
simp [getElem_set]
theorem getElem?_set {l : List α} {i j : Nat} {a : α} :
(l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]? := by
if h : i = j then
subst h
rw [if_pos rfl]
split <;> rename_i h
· simp only [getElem?_set_eq (by simpa), h]
· simp_all
else
simp [h]
theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α} :
l.set n a = l := by
induction l generalizing n with
| nil => simp_all
| cons a l ih =>
induction n
· simp_all
· simp only [set_cons_succ, cons.injEq, true_and]
rw [ih]
exact Nat.succ_le_succ_iff.mp h
@[simp] theorem set_eq_nil (l : List α) (n : Nat) (a : α) : l.set n a = [] ↔ l = [] := by
cases l <;> cases n <;> simp only [set]
@ -450,23 +465,18 @@ theorem set_set (a b : α) : ∀ (l : List α) (n : Nat), (l.set n a).set n b =
| _ :: _, 0 => by simp [set]
| _ :: _, _+1 => by simp [set, set_set]
theorem getElem_set (a : α) {m n} (l : List α) (h) :
(set l m a)[n]'h = if m = n then a else l[n]'(length_set .. ▸ h) := by
if h : m = n then
subst m; simp only [getElem_set_eq, ↓reduceIte]
else
simp [h]
@[deprecated getElem_set (since := "2024-06-12")]
theorem get_set (a : α) {m n} (l : List α) (h) :
(set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by
simp [getElem_set]
theorem mem_set (l : List α) (n : Nat) (h : n < l.length) (a : α) :
a ∈ l.set n a := by
simp [mem_iff_getElem]
exact ⟨n, (by simpa using h), by simp⟩
theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.set n b → a ∈ l ∨ a = b
| _ :: _, 0, _, _, h => ((mem_cons ..).1 h).symm.imp_left (.tail _)
| _ :: _, _+1, _, _, .head .. => .inl (.head ..)
| _ :: _, _+1, _, _, .tail _ h => (mem_or_eq_of_mem_set h).imp_left (.tail _)
-- See also `set_eq_take_append_cons_drop` in `Init.Data.List.TakeDrop`.
/-! ### foldlM and foldrM -/
@[simp] theorem foldlM_reverse [Monad m] (l : List α) (f : β → α → m β) (b) :
@ -980,6 +990,46 @@ theorem forall_mem_append {p : α → Prop} {l₁ l₂ : List α} :
(∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by
simp only [mem_append, or_imp, forall_and]
/-! ### concat
Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals.
As such there's no need for a thorough set of lemmas describing `concat`.
-/
-- As `List.concat` is defined in `Init.Prelude`, we write the basic simplification lemmas here.
theorem concat_nil (a : α) : concat [] a = [a] :=
rfl
theorem concat_cons (a b : α) (l : List α) : concat (a :: l) b = a :: concat l b :=
rfl
theorem init_eq_of_concat_eq {a b : α} {l₁ l₂ : List α} : concat l₁ a = concat l₂ b → l₁ = l₂ := by
simp only [concat_eq_append]
intro h
apply append_inj_left' h (by simp)
theorem last_eq_of_concat_eq {a b : α} {l₁ l₂ : List α} : concat l₁ a = concat l₂ b → a = b := by
simp only [concat_eq_append]
intro h
simpa using append_inj_right' h (by simp)
theorem concat_inj_left {l l' : List α} (a : α) : concat l a = concat l' a ↔ l = l' :=
⟨init_eq_of_concat_eq, by simp⟩
theorem concat_eq_concat {l l' : List α} {a b : α} : concat l a = concat l' b ↔ l = l' ∧ a = b :=
⟨fun h => ⟨init_eq_of_concat_eq h, last_eq_of_concat_eq h⟩, by rintro ⟨rfl, rfl⟩; rfl⟩
theorem concat_ne_nil (a : α) (l : List α) : concat l a ≠ [] := by cases l <;> simp
theorem concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l₁ ++ a :: l₂ := by simp
theorem append_concat (a : α) (l₁ l₂ : List α) : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a := by simp
theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b
| [] => .inl rfl
| a::l => match l, eq_nil_or_concat l with
| _, .inl rfl => .inr ⟨[], a, rfl⟩
| _, .inr ⟨L, b, rfl⟩ => .inr ⟨a::L, b, rfl⟩
/-! ### join -/
theorem mem_join : ∀ {L : List (List α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l

31
src/Init/Data/List/TakeDrop.lean
View file

@ -240,6 +240,33 @@ theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? :=
theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
simp
theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} :
l.set n a = if n < l.length then l.take n ++ a :: l.drop (n + 1) else l := by
split <;> rename_i h
· ext1 m
by_cases h' : m < n
· rw [getElem?_append (by simp [length_take]; omega), getElem?_set_ne (by omega),
getElem?_take h']
· by_cases h'' : m = n
· subst h''
rw [getElem?_set_eq (by simp; omega), getElem?_append_right, length_take,
Nat.min_eq_left (by omega), Nat.sub_self, getElem?_cons_zero]
rw [length_take]
exact Nat.min_le_left m l.length
· have h''' : n < m := by omega
rw [getElem?_set_ne (by omega), getElem?_append_right, length_take,
Nat.min_eq_left (by omega)]
· obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h'''
have p : n + k + 1 - n = k + 1 := by omega
rw [p]
rw [getElem?_cons_succ, getElem?_drop]
congr 1
omega
· rw [length_take]
exact Nat.le_trans (Nat.min_le_left _ _) (by omega)
· rw [set_eq_of_length_le]
omega
theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
| 0, _, _ => by simp
| _, 0, _ => by simp
@ -249,7 +276,7 @@ theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m -
congr 1
omega
theorem reverse_take {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
theorem take_reverse {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
induction xs generalizing n <;>
simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
@ -269,6 +296,8 @@ theorem reverse_take {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
rw [length_append, length_reverse]
rfl
@[deprecated (since := "2024-06-15")] abbrev reverse_take := @take_reverse
/-! ### zipWith -/
@[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :