Documentation

Init.Data.List.Nat.Basic

Miscellaneous List lemmas, that require more Nat lemmas than are available in Init.Data.List.Lemmas. #

In particular, omega is available here.

filter #

theorem List.length_filter_lt_length_iff_exists :
∀ {α : Type u_1} {p : αBool} (l : List α), (List.filter p l).length < l.length ∃ (x : α), x l ¬p x = true

leftpad #

@[simp]
theorem List.leftpad_length {α : Type u_1} (n : Nat) (a : α) (l : List α) :
(List.leftpad n a l).length = max n l.length

The length of the List returned by List.leftpad n a l is equal to the larger of n and l.length

eraseIdx #

theorem List.mem_eraseIdx_iff_getElem {α : Type u_1} {x : α} {l : List α} {k : Nat} :
x l.eraseIdx k ∃ (i : Nat), ∃ (h : i < l.length), i k l[i] = x
theorem List.mem_eraseIdx_iff_getElem? {α : Type u_1} {x : α} {l : List α} {k : Nat} :
x l.eraseIdx k ∃ (i : Nat), i k l[i]? = some x

minimum? #

theorem List.minimum?_eq_some_iff' {a : Nat} {xs : List Nat} :
xs.minimum? = some a a xs ∀ (b : Nat), b xsa b
theorem List.minimum?_cons' {a : Nat} {l : List Nat} :
(a :: l).minimum? = some (match l.minimum? with | none => a | some m => min a m)

maximum? #

theorem List.maximum?_eq_some_iff' {a : Nat} {xs : List Nat} :
xs.maximum? = some a a xs ∀ (b : Nat), b xsb a
theorem List.maximum?_cons' {a : Nat} {l : List Nat} :
(a :: l).maximum? = some (match l.maximum? with | none => a | some m => max a m)