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

chore: review of List API (#5264)

Browse source
This commit is contained in:
Kim Morrison 2024-09-05 23:08:31 +10:00 • committed by GitHub
parent 1b099521c1
commit 76ea33c4c6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 205 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

142
src/Init/Data/List/Find.lean
View file

@ -35,9 +35,11 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]
split at w <;> simp_all
@[simp] theorem findSome?_eq_none : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
@[simp] theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
induction l <;> simp [findSome?_cons]; split <;> simp [*]
@[deprecated findSome?_eq_none_iff (since := "2024-09-05")] abbrev findSome?_eq_none := @findSome?_eq_none_iff
@[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : List α} :
(l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome := by
induction l with
@ -46,6 +48,41 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
simp only [findSome?_cons]
split <;> simp_all
theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
l.findSome? f = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ x ∈ l₁, f x = none := by
induction l with
| nil => simp
| cons p l ih =>
simp only [findSome?_cons]
split <;> rename_i b' h
· simp only [Option.some.injEq, exists_and_right]
constructor
· rintro rfl
exact ⟨[], p, ⟨l, rfl⟩, h, by simp⟩
· rintro ⟨(⟨⟩ | ⟨p', l₁⟩), a, ⟨l₂, h₁⟩, h₂, h₃⟩
· simp only [nil_append, cons.injEq] at h₁
apply Option.some.inj
simp [← h, ← h₂, h₁.1]
· simp only [cons_append, cons.injEq] at h₁
obtain ⟨rfl, rfl⟩ := h₁
specialize h₃ p
simp_all
· rw [ih]
constructor
· rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
refine ⟨p :: l₁, a, l₂, rfl, h₁, ?_⟩
intro a w
simp at w
rcases w with rfl | w
· exact h
· exact h₂ _ w
· rintro ⟨l₁, a, l₂, h₁, h₂, h₃⟩
rcases l₁ with (⟨⟩ | ⟨a', l₁⟩)
· simp_all
· simp only [cons_append, cons.injEq] at h₁
obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h₁
exact ⟨l₁, a, l₂, rfl, h₂, fun a' w => h₃ a' (mem_cons_of_mem p w)⟩
@[simp] theorem findSome?_guard (l : List α) : findSome? (Option.guard fun x => p x) l = find? p l := by
induction l with
| nil => simp
@ -95,6 +132,15 @@ theorem findSome?_append {l₁ l₂ : List α} : (l₁ ++ l₂).findSome? f = (l
simp only [cons_append, findSome?]
split <;> simp_all
theorem head_join {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
(join L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h) := by
simp [head_eq_iff_head?_eq_some, head?_join]
theorem getLast_join {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
(join L).getLast (by simpa using h) =
(L.reverse.findSome? fun l => l.getLast?).get (by simpa using h) := by
simp [getLast_eq_iff_getLast_eq_some, getLast?_join]
theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
cases n with
| zero => simp
@ -126,7 +172,7 @@ theorem Sublist.findSome?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
theorem Sublist.findSome?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) :
l₂.findSome? f = none → l₁.findSome? f = none := by
simp only [List.findSome?_eq_none, Bool.not_eq_true]
simp only [List.findSome?_eq_none_iff, Bool.not_eq_true]
exact fun w x m => w x (Sublist.mem m h)
theorem IsPrefix.findSome?_eq_some {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) :
@ -776,4 +822,96 @@ theorem indexOf_cons [BEq α] :
dsimp [indexOf]
simp [findIdx_cons]
/-! ### lookup -/
section lookup
variable [BEq α] [LawfulBEq α]
@[simp] theorem lookup_cons_self {k : α} : ((k,b) :: es).lookup k = some b := by
simp [lookup_cons]
theorem lookup_eq_findSome? (l : List (α × β)) (k : α) :
l.lookup k = l.findSome? fun p => if k == p.1 then some p.2 else none := by
induction l with
| nil => rfl
| cons p l ih =>
match p with
| (k', v) =>
simp only [lookup_cons, findSome?_cons]
split <;> simp_all
@[simp] theorem lookup_eq_none_iff {l : List (α × β)} {k : α} :
l.lookup k = none ↔ ∀ p ∈ l, k != p.1 := by
simp [lookup_eq_findSome?]
@[simp] theorem lookup_isSome_iff {l : List (α × β)} {k : α} :
(l.lookup k).isSome ↔ ∃ p ∈ l, k == p.1 := by
simp [lookup_eq_findSome?]
theorem lookup_eq_some_iff {l : List (α × β)} {k : α} {b : β} :
l.lookup k = some b ↔ ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ p ∈ l₁, k != p.1 := by
simp only [lookup_eq_findSome?, findSome?_eq_some_iff]
constructor
· rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
simp only [beq_iff_eq, ite_some_none_eq_some] at h₁
obtain ⟨rfl, rfl⟩ := h₁
simp at h₂
exact ⟨l₁, l₂, rfl, by simpa using h₂⟩
· rintro ⟨l₁, l₂, rfl, h⟩
exact ⟨l₁, (k, b), l₂, rfl, by simp, by simpa using h⟩
theorem lookup_append {l₁ l₂ : List (α × β)} {k : α} :
(l₁ ++ l₂).lookup k = (l₁.lookup k).or (l₂.lookup k) := by
simp [lookup_eq_findSome?, findSome?_append]
theorem lookup_replicate {k : α} :
(replicate n (a,b)).lookup k = if n = 0 then none else if k == a then some b else none := by
induction n with
| zero => simp
| succ n ih =>
simp only [replicate_succ, lookup_cons]
split <;> simp_all
theorem lookup_replicate_of_pos {k : α} (h : 0 < n) :
(replicate n (a, b)).lookup k = if k == a then some b else none := by
simp [lookup_replicate, Nat.ne_of_gt h]
theorem lookup_replicate_self {a : α} :
(replicate n (a, b)).lookup a = if n = 0 then none else some b := by
simp [lookup_replicate]
@[simp] theorem lookup_replicate_self_of_pos {a : α} (h : 0 < n) :
(replicate n (a, b)).lookup a = some b := by
simp [lookup_replicate_self, Nat.ne_of_gt h]
@[simp] theorem lookup_replicate_ne {k : α} (h : !k == a) :
(replicate n (a, b)).lookup k = none := by
simp_all [lookup_replicate]
theorem Sublist.lookup_isSome {l₁ l₂ : List (α × β)} (h : l₁ <+ l₂) :
(l₁.lookup k).isSome → (l₂.lookup k).isSome := by
simp only [lookup_eq_findSome?]
exact h.findSome?_isSome
theorem Sublist.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <+ l₂) :
l₂.lookup k = none → l₁.lookup k = none := by
simp only [lookup_eq_findSome?]
exact h.findSome?_eq_none
theorem IsPrefix.lookup_eq_some {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) :
List.lookup k l₁ = some b → List.lookup k l₂ = some b := by
simp only [lookup_eq_findSome?]
exact h.findSome?_eq_some
theorem IsPrefix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) :
List.lookup k l₂ = none → List.lookup k l₁ = none :=
h.sublist.lookup_eq_none
theorem IsSuffix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+ l₂) :
List.lookup k l₂ = none → List.lookup k l₁ = none :=
h.sublist.lookup_eq_none
theorem IsInfix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+: l₂) :
List.lookup k l₂ = none → List.lookup k l₁ = none :=
h.sublist.lookup_eq_none
end lookup
end List

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

@ -939,8 +939,8 @@ theorem getLast_eq_iff_getLast?_eq_some {xs : List α} (h) :
rw [getLast?_eq_getLast _ h]
simp
-- `getLast?_eq_none_iff`, `getLast?_eq_some_iff`, and `getLast_mem` are proved later
-- once more `reverse` theorems are available.
-- `getLast?_eq_none_iff`, `getLast?_eq_some_iff`, `getLast?_isSome`, and `getLast_mem`
-- are proved later once more `reverse` theorems are available.
theorem getLast?_cons {a : α} : (a::l).getLast? = l.getLast?.getD a := by
cases l <;> simp [getLast?, getLast]
@ -986,6 +986,9 @@ theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head
theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys, xs = a :: ys := by
cases xs <;> simp_all
@[simp] theorem head?_isSome : l.head?.isSome ↔ l ≠ [] := by
cases l <;> simp
@[simp] theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
| [], h => absurd rfl h
| _::_, _ => .head ..
@ -1151,6 +1154,10 @@ theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs =
@[simp] theorem tail?_map (f : α → β) (l : List α) : tail? (map f l) = (tail? l).map (map f) := by
cases l <;> rfl
@[simp] theorem tail_map (f : α → β) (l : List α) :
(map f l).tail = map f l.tail := by
cases l <;> simp_all
theorem headD_map (f : α → β) (l : List α) (a : α) : headD (map f l) (f a) = f (headD l a) := by
cases l <;> rfl
@ -1643,9 +1650,27 @@ theorem head_append_right {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l
-- `getLast_append_of_ne_nil`, `getLast_append` and `getLast?_append`
-- are stated and proved later in the `reverse` section.
theorem nil_eq_append : [] = a ++ b ↔ a = [] ∧ b = [] := by
theorem tail?_append {l l' : List α} : (l ++ l').tail? = (l.tail?.map (· ++ l')).or l'.tail? := by
cases l <;> simp
theorem tail?_append_of_ne_nil {l l' : List α} (_ : l ≠ []) : (l ++ l').tail? = some (l.tail ++ l') :=
match l with
| _ :: _ => by simp
theorem tail_append {l l' : List α} : (l ++ l').tail = if l.isEmpty then l'.tail else l.tail ++ l' := by
cases l <;> simp
@[simp] theorem tail_append_of_ne_nil {xs ys : List α} (h : xs ≠ []) :
(xs ++ ys).tail = xs.tail ++ ys := by
simp_all [tail_append]
@[deprecated tail_append_of_ne_nil (since := "2024-07-24")] abbrev tail_append_left := @tail_append_of_ne_nil
theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
rw [eq_comm, append_eq_nil]
@[deprecated nil_eq_append_iff (since := "2024-07-24")] abbrev nil_eq_append := @nil_eq_append_iff
theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all
theorem append_ne_nil_of_right_ne_nil (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
@ -1654,22 +1679,6 @@ theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s ≠ []) (t : List α)
@[deprecated append_ne_nil_of_right_ne_nil (since := "2024-07-24")]
theorem append_ne_nil_of_ne_nil_right (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
theorem tail_append (xs ys : List α) :
(xs ++ ys).tail = if xs.isEmpty then ys.tail else xs.tail ++ ys := by
cases xs <;> simp
theorem tail_append_left {xs ys : List α} (h : xs ≠ []) :
(xs ++ ys).tail = xs.tail ++ ys := by
simp [tail_append, h]
theorem tail_append_right {xs ys : List α} (h : ys = []) :
(xs ++ ys).tail = xs.tail := by
simp [tail_append, h]
@[simp] theorem tail_append_of_ne_nil (xs ys : List α) (h : xs ≠ []) :
(xs ++ ys).tail = xs.tail ++ ys := by
simp_all [tail_append]
theorem append_eq_cons_iff :
a ++ b = x :: c ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
cases a with simp | cons a as => ?_
@ -1749,7 +1758,7 @@ theorem filterMap_eq_append_iff {f : α → Option β} :
constructor
· induction l generalizing L₁ with
| nil =>
simp only [filterMap_nil, nil_eq_append, and_imp]
simp only [filterMap_nil, nil_eq_append_iff, and_imp]
rintro rfl rfl
exact ⟨[], [], by simp⟩
| cons x l ih =>
@ -1895,7 +1904,8 @@ theorem head?_join {L : List (List α)} : (join L).head? = L.findSome? fun l =>
simp only [findSome?_cons]
split <;> simp_all
-- `getLast?_join` is proved later, after the `reverse` section
-- `getLast?_join` is proved later, after the `reverse` section.
-- `head_join` and `getLast_join` are proved in `Init.Data.List.Find`.
theorem foldl_join (f : β → α → β) (b : β) (L : List (List α)) :
(join L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
@ -2465,6 +2475,10 @@ theorem getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔
simp only [reverse_eq_cons_iff]
exact ⟨fun ⟨ys, h⟩ => ⟨ys.reverse, by simpa using h⟩, fun ⟨ys, h⟩ => ⟨ys.reverse, by simpa using h⟩⟩
@[simp] theorem getLast?_isSome : l.getLast?.isSome ↔ l ≠ [] := by
rw [getLast?_eq_head?_reverse, head?_isSome]
simp
theorem mem_of_getLast?_eq_some {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
obtain ⟨ys, rfl⟩ := getLast?_eq_some_iff.1 h
exact mem_concat_self ys a
@ -2790,6 +2804,14 @@ theorem replace_append [LawfulBEq α] {l₁ l₂ : List α} :
simp only [cons_append, replace_cons]
split <;> split <;> simp_all
theorem replace_append_left [LawfulBEq α] {l₁ l₂ : List α} (h : a ∈ l₁) :
(l₁ ++ l₂).replace a b = l₁.replace a b ++ l₂ := by
simp [replace_append, h]
theorem replace_append_right [LawfulBEq α] {l₁ l₂ : List α} (h : ¬ a ∈ l₁) :
(l₁ ++ l₂).replace a b = l₁ ++ l₂.replace a b := by
simp [replace_append, h]
theorem replace_take {l : List α} {n : Nat} :
(l.take n).replace a b = (l.replace a b).take n := by
induction l generalizing n with
@ -2868,7 +2890,8 @@ theorem length_insert_pos {l : List α} {a : α} : 0 < (l.insert a).length := by
theorem insert_eq {l : List α} {a : α} : l.insert a = if a ∈ l then l else a :: l := by
simp [List.insert]
theorem getElem?_insert_zero (l : List α) (a : α) : (l.insert a)[0]? = if a ∈ l then l[0]? else some a := by
theorem getElem?_insert_zero (l : List α) (a : α) :
(l.insert a)[0]? = if a ∈ l then l[0]? else some a := by
simp only [insert_eq]
split <;> simp
@ -2912,6 +2935,14 @@ theorem insert_append {l₁ l₂ : List α} {a : α} :
simp only [insert_eq, mem_append]
(repeat split) <;> simp_all
theorem insert_append_of_mem_left {l₁ l₂ : List α} (h : a ∈ l₂) :
(l₁ ++ l₂).insert a = l₁ ++ l₂ := by
simp [insert_append, h]
theorem insert_append_of_not_mem_left {l₁ l₂ : List α} (h : ¬ a ∈ l₂) :
(l₁ ++ l₂).insert a = l₁.insert a ++ l₂ := by
simp [insert_append, h]
@[simp] theorem insert_replicate_self {a : α} (h : 0 < n) : (replicate n a).insert a = replicate n a := by
cases n <;> simp_all
@ -2922,39 +2953,6 @@ theorem insert_append {l₁ l₂ : List α} {a : α} :
end insert
/-! ### lookup -/
section lookup
variable [BEq α] [LawfulBEq α]
@[simp] theorem lookup_cons_self {k : α} : ((k,b)::es).lookup k = some b := by
simp [lookup_cons]
theorem lookup_replicate {k : α} :
(replicate n (a,b)).lookup k = if n = 0 then none else if k == a then some b else none := by
induction n with
| zero => simp
| succ n ih =>
simp only [replicate_succ, lookup_cons]
split <;> simp_all
theorem lookup_replicate_of_pos {k : α} (h : 0 < n) :
(replicate n (a, b)).lookup k = if k == a then some b else none := by
simp [lookup_replicate, Nat.ne_of_gt h]
theorem lookup_replicate_self {a : α} :
(replicate n (a, b)).lookup a = if n = 0 then none else some b := by
simp [lookup_replicate]
@[simp] theorem lookup_replicate_self_of_pos {a : α} (h : 0 < n) :
(replicate n (a, b)).lookup a = some b := by
simp [lookup_replicate_self, Nat.ne_of_gt h]
@[simp] theorem lookup_replicate_ne {k : α} (h : !k == a) :
(replicate n (a, b)).lookup k = none := by
simp_all [lookup_replicate]
end lookup
/-! ## Logic -/
/-! ### any / all -/

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

@ -436,6 +436,18 @@ theorem take_takeWhile {l : List α} (p : α → Bool) n :
| nil => rfl
| cons h t ih => by_cases p h <;> simp_all
theorem replace_takeWhile [BEq α] [LawfulBEq α] {l : List α} {p : α → Bool} (h : p a = p b) :
(l.takeWhile p).replace a b = (l.replace a b).takeWhile p := by
induction l with
| nil => rfl
| cons x xs ih =>
simp only [takeWhile_cons, replace_cons]
split <;> rename_i h₁ <;> split <;> rename_i h₂
· simp_all
· simp [replace_cons, h₂, takeWhile_cons, h₁, ih]
· simp_all
· simp_all
/-! ### splitAt -/
@[simp] theorem splitAt_eq (n : Nat) (l : List α) : splitAt n l = (l.take n, l.drop n) := by