Bootstrapping theorems for lists

These are theorems used in the definitions of Std.Data.List.Basic and tactics. New theorems should be added to Std.Data.List.Lemmas if they are not needed by the bootstrap.

@[simp]

theorem List.get?_nil {α : Type u_1} {n : Nat} : [].get? n = none

@[simp]

theorem List.get?_cons_zero {α : Type u_1} {a : α} {l : List α} : (a :: l).get? 0 = some a

@[simp]

theorem List.get?_cons_succ {α : Type u_1} {a : α} {l : List α} {n : Nat} : (a :: l).get? (n + 1) = l.get? n

@[simp]

theorem List.get_cons_zero : ∀ {α : Type u_1} {a : α} {l : List α}, (a :: l).get 0 = a

@[simp]

theorem List.head?_nil {α : Type u_1} : [].head? = none

@[simp]

theorem List.head?_cons {α : Type u_1} {a : α} {l : List α} : (a :: l).head? = some a

@[simp]

theorem List.headD_nil {α : Type u_1} {d : α} : [].headD d = d

@[simp]

theorem List.headD_cons {α : Type u_1} {a : α} {l : List α} {d : α} : (a :: l).headD d = a

@[simp]

theorem List.head_cons {α : Type u_1} {a : α} {l : List α} {h : a :: l ≠ []} : (a :: l).head h = a

@[simp]

theorem List.tail?_nil {α : Type u_1} : [].tail? = none

@[simp]

theorem List.tail?_cons {α : Type u_1} {a : α} {l : List α} : (a :: l).tail? = some l

@[simp]

theorem List.tail!_cons {α : Type u_1} {a : α} {l : List α} : (a :: l).tail! = l

@[simp]

theorem List.tailD_nil {α : Type u_1} {l' : List α} : [].tailD l' = l'

@[simp]

theorem List.tailD_cons {α : Type u_1} {a : α} {l : List α} {l' : List α} : (a :: l).tailD l' = l

@[simp]

theorem List.any_nil : ∀ {α : Type u_1} {f : α → Bool}, [].any f = false

@[simp]

theorem List.any_cons : ∀ {α : Type u_1} {a : α} {l : List α} {f : α → Bool}, (a :: l).any f = (f a || l.any f)

@[simp]

theorem List.all_nil : ∀ {α : Type u_1} {f : α → Bool}, [].all f = true

@[simp]

theorem List.all_cons : ∀ {α : Type u_1} {a : α} {l : List α} {f : α → Bool}, (a :: l).all f = (f a && l.all f)

@[simp]

theorem List.or_nil : [].or = false

@[simp]

theorem List.or_cons {a : Bool} {l : List Bool} : (a :: l).or = (a || l.or)

@[simp]

theorem List.and_nil : [].and = true

@[simp]

theorem List.and_cons {a : Bool} {l : List Bool} : (a :: l).and = (a && l.and)

length

theorem List.eq_nil_of_length_eq_zero : ∀ {α : Type u_1} {l : List α}, l.length = 0 → l = []

theorem List.ne_nil_of_length_eq_succ : ∀ {α : Type u_1} {l : List α} {n : Nat}, l.length = n.succ → l ≠ []

theorem List.length_eq_zero : ∀ {α : Type u_1} {l : List α}, l.length = 0 ↔ l = []

mem

@[simp]

theorem List.not_mem_nil {α : Type u_1} (a : α) : ¬a ∈ []

@[simp]

theorem List.mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ l

theorem List.mem_cons_self {α : Type u_1} (a : α) (l : List α) : a ∈ a :: l

theorem List.mem_cons_of_mem {α : Type u_1} (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l

theorem List.eq_nil_iff_forall_not_mem {α : Type u_1} {l : List α} : l = [] ↔ ∀ (a : α), ¬a ∈ l

append

@[simp]

theorem List.singleton_append : ∀ {α : Type u_1} {x : α} {l : List α}, [x] ++ l = x :: l

theorem List.append_inj {α : Type u_1} {s₁ : List α} {s₂ : List α} {t₁ : List α} {t₂ : List α} : s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂ ∧ t₁ = t₂

theorem List.append_inj_right : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → t₁ = t₂

theorem List.append_inj_left : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂

theorem List.append_inj' : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → s₁ = s₂ ∧ t₁ = t₂

theorem List.append_inj_right' : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → t₁ = t₂

theorem List.append_inj_left' : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → s₁ = s₂

theorem List.append_right_inj {α : Type u_1} {t₁ : List α} {t₂ : List α} (s : List α) : s ++ t₁ = s ++ t₂ ↔ t₁ = t₂

theorem List.append_left_inj {α : Type u_1} {s₁ : List α} {s₂ : List α} (t : List α) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂

@[simp]

theorem List.append_eq_nil : ∀ {α : Type u_1} {p q : List α}, p ++ q = [] ↔ p = [] ∧ q = []

theorem List.get_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (n : Nat) (h : n < l₁.length) : (l₁ ++ l₂).get ⟨n, ⋯⟩ = l₁.get ⟨n, h⟩

map

@[simp]

theorem List.map_nil {α : Type u_1} {β : Type u_2} {f : α → β} : List.map f [] = []

@[simp]

theorem List.map_cons {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (l : List α) : List.map f (a :: l) = f a :: List.map f l

@[simp]

theorem List.map_append {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : List α) (l₂ : List α) : List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂

@[simp]

theorem List.map_id {α : Type u_1} (l : List α) : List.map id l = l

@[simp]

theorem List.map_id' {α : Type u_1} (l : List α) : List.map (fun (a : α) => a) l = l

@[simp]

theorem List.mem_map {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {l : List α} : b ∈ List.map f l ↔ ∃ (a : α), a ∈ l ∧ f a = b

theorem List.mem_map_of_mem {α : Type u_1} {β : Type u_2} {a : α} {l : List α} (f : α → β) (h : a ∈ l) : f a ∈ List.map f l

@[simp]

theorem List.map_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (g : β → γ) (f : α → β) (l : List α) : List.map g (List.map f l) = List.map (g ∘ f) l

bind

@[simp]

theorem List.nil_bind {α : Type u_1} {β : Type u_2} (f : α → List β) : [].bind f = []

@[simp]

theorem List.cons_bind {α : Type u_1} {β : Type u_2} (x : α) (xs : List α) (f : α → List β) : (x :: xs).bind f = f x ++ xs.bind f

@[simp]

theorem List.append_bind {α : Type u_1} {β : Type u_2} (xs : List α) (ys : List α) (f : α → List β) : (xs ++ ys).bind f = xs.bind f ++ ys.bind f

@[simp]

theorem List.bind_id {α : Type u_1} (l : List (List α)) : l.bind id = l.join

join

@[simp]

theorem List.join_nil {α : Type u_1} : [].join = []

@[simp]

theorem List.join_cons : ∀ {α : Type u_1} {l : List α} {ls : List (List α)}, (l :: ls).join = l ++ ls.join

bounded quantifiers over Lists

theorem List.forall_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {l : List α} : (∀ (x : α), x ∈ a :: l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l → p x

reverse

@[simp]

theorem List.reverseAux_nil : ∀ {α : Type u_1} {r : List α}, [].reverseAux r = r

@[simp]

theorem List.reverseAux_cons : ∀ {α : Type u_1} {a : α} {l r : List α}, (a :: l).reverseAux r = l.reverseAux (a :: r)

theorem List.reverseAux_eq {α : Type u_1} (as : List α) (bs : List α) : as.reverseAux bs = as.reverse ++ bs

theorem List.reverse_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : (List.map f l).reverse = List.map f l.reverse

@[simp]

theorem List.reverse_eq_nil_iff {α : Type u_1} {xs : List α} : xs.reverse = [] ↔ xs = []

nth element

theorem List.get_of_mem {α : Type u_1} {a : α} {l : List α} : a ∈ l → ∃ (n : Fin l.length), l.get n = a

theorem List.get_mem {α : Type u_1} (l : List α) (n : Nat) (h : n < l.length) : l.get ⟨n, h⟩ ∈ l

theorem List.mem_iff_get {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (n : Fin l.length), l.get n = a

theorem List.get?_len_le {α : Type u_1} {l : List α} {n : Nat} : l.length ≤ n → l.get? n = none

theorem List.get?_eq_get {α : Type u_1} {l : List α} {n : Nat} (h : n < l.length) : l.get? n = some (l.get ⟨n, h⟩)

theorem List.get?_eq_some : ∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, l.get? n = some a ↔ ∃ (h : n < l.length), l.get ⟨n, h⟩ = a

@[simp]

theorem List.get?_eq_none : ∀ {α : Type u_1} {l : List α} {n : Nat}, l.get? n = none ↔ l.length ≤ n

@[simp]

theorem List.get?_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (n : Nat) : (List.map f l).get? n = Option.map f (l.get? n)

theorem List.get?_append {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (hn : n < l₁.length) : (l₁ ++ l₂).get? n = l₁.get? n

@[simp]

theorem List.get?_concat_length {α : Type u_1} (l : List α) (a : α) : (l ++ [a]).get? l.length = some a

theorem List.getLast_eq_get {α : Type u_1} (l : List α) (h : l ≠ []) : l.getLast h = l.get ⟨l.length - 1, ⋯⟩

@[simp]

theorem List.getLast?_nil {α : Type u_1} : [].getLast? = none

theorem List.getLast?_eq_getLast {α : Type u_1} (l : List α) (h : l ≠ []) : l.getLast? = some (l.getLast h)

theorem List.getLast?_eq_get? {α : Type u_1} (l : List α) : l.getLast? = l.get? (l.length - 1)

@[simp]

theorem List.getLast?_concat {α : Type u_1} {a : α} (l : List α) : (l ++ [a]).getLast? = some a

theorem List.getD_eq_get? {α : Type u_1} (l : List α) (n : Nat) (a : α) : l.getD n a = (l.get? n).getD a

theorem List.get?_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} : l₁.length ≤ n → (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)

theorem List.get?_reverse' {α : Type u_1} {l : List α} (i : Nat) (j : Nat) : i + j + 1 = l.length → l.reverse.get? i = l.get? j

theorem List.get?_reverse {α : Type u_1} {l : List α} (i : Nat) (h : i < l.length) : l.reverse.get? i = l.get? (l.length - 1 - i)

@[simp]

theorem List.getD_nil {n : Nat} : ∀ {α : Type u_1} {d : α}, [].getD n d = d

@[simp]

theorem List.getD_cons_zero : ∀ {α : Type u_1} {x : α} {xs : List α} {d : α}, (x :: xs).getD 0 d = x

@[simp]

theorem List.getD_cons_succ : ∀ {α : Type u_1} {x : α} {xs : List α} {n : Nat} {d : α}, (x :: xs).getD (n + 1) d = xs.getD n d

theorem List.ext_get {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : l₁.length = l₂.length) (h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) : l₁ = l₂

@[simp]

theorem List.get_map {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {n : Fin (List.map f l).length} : (List.map f l).get n = f (l.get ⟨↑n, ⋯⟩)

take and drop

@[simp]

theorem List.take_append_drop {α : Type u_1} (n : Nat) (l : List α) : List.take n l ++ List.drop n l = l

@[simp]

theorem List.length_drop {α : Type u_1} (i : Nat) (l : List α) : (List.drop i l).length = l.length - i

theorem List.drop_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length ≤ i) : List.drop i l = []

theorem List.take_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length ≤ i) : List.take i l = l

@[simp]

theorem List.take_zero {α : Type u_1} (l : List α) : List.take 0 l = []

@[simp]

theorem List.take_nil {α : Type u_1} {i : Nat} : List.take i [] = []

@[simp]

theorem List.take_cons_succ : ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as

@[simp]

theorem List.drop_zero {α : Type u_1} (l : List α) : List.drop 0 l = l

@[simp]

theorem List.drop_succ_cons : ∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, List.drop (n + 1) (a :: l) = List.drop n l

@[simp]

theorem List.drop_length {α : Type u_1} (l : List α) : List.drop l.length l = []

@[simp]

theorem List.take_length {α : Type u_1} (l : List α) : List.take l.length l = l

theorem List.take_concat_get {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) : (List.take i l).concat l[i] = List.take (i + 1) l

theorem List.reverse_concat {α : Type u_1} (l : List α) (a : α) : (l.concat a).reverse = a :: l.reverse

takeWhile and dropWhile

@[simp]

theorem List.dropWhile_nil {α : Type u_1} {p : α → Bool} : List.dropWhile p [] = []

theorem List.dropWhile_cons {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} : List.dropWhile p (x :: xs) = if p x = true then List.dropWhile p xs else x :: xs

foldlM and foldrM

@[simp]

theorem List.foldlM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (f : β → α → m β) (b : β) : List.foldlM f b l.reverse = List.foldrM (fun (x : α) (y : β) => f y x) b l

@[simp]

theorem List.foldlM_nil {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (b : β) : List.foldlM f b [] = pure b

@[simp]

theorem List.foldlM_cons {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (b : β) (a : α) (l : List α) : List.foldlM f b (a :: l) = do let init ← f b a List.foldlM f init l

@[simp]

theorem List.foldlM_append {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [LawfulMonad m] (f : β → α → m β) (b : β) (l : List α) (l' : List α) : List.foldlM f b (l ++ l') = do let init ← List.foldlM f b l List.foldlM f init l'

@[simp]

theorem List.foldrM_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (b : β) : List.foldrM f b [] = pure b

@[simp]

theorem List.foldrM_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (a : α) (l : List α) (f : α → β → m β) (b : β) : List.foldrM f b (a :: l) = List.foldrM f b l >>= f a

@[simp]

theorem List.foldrM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (f : α → β → m β) (b : β) : List.foldrM f b l.reverse = List.foldlM (fun (x : β) (y : α) => f y x) b l

theorem List.foldl_eq_foldlM {β : Type u_1} {α : Type u_2} (f : β → α → β) (b : β) (l : List α) : List.foldl f b l = List.foldlM f b l

theorem List.foldr_eq_foldrM {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (l : List α) : List.foldr f b l = List.foldrM f b l

foldl and foldr

@[simp]

theorem List.foldl_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : β → α → β) (b : β) : List.foldl f b l.reverse = List.foldr (fun (x : α) (y : β) => f y x) b l

@[simp]

theorem List.foldr_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β → β) (b : β) : List.foldr f b l.reverse = List.foldl (fun (x : β) (y : α) => f y x) b l

@[simp]

theorem List.foldrM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β → m β) (b : β) (l : List α) (l' : List α) : List.foldrM f b (l ++ l') = do let init ← List.foldrM f b l' List.foldrM f init l

@[simp]

theorem List.foldl_append {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (l : List α) (l' : List α) : List.foldl f b (l ++ l') = List.foldl f (List.foldl f b l) l'

@[simp]

theorem List.foldr_append {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (l : List α) (l' : List α) : List.foldr f b (l ++ l') = List.foldr f (List.foldr f b l') l

@[simp]

theorem List.foldl_nil : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → α} {b : α}, List.foldl f b [] = b

@[simp]

theorem List.foldl_cons {α : Type u_1} {β : Type u_2} {a : α} {f : β → α → β} (l : List α) (b : β) : List.foldl f b (a :: l) = List.foldl f (f b a) l

@[simp]

theorem List.foldr_nil : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1 → α_1} {b : α_1}, List.foldr f b [] = b

@[simp]

theorem List.foldr_cons {α : Type u_1} {a : α} : ∀ {α_1 : Type u_2} {f : α → α_1 → α_1} {b : α_1} (l : List α), List.foldr f b (a :: l) = f a (List.foldr f b l)

@[simp]

theorem List.foldr_self_append {α : Type u_1} {l' : List α} (l : List α) : List.foldr List.cons l' l = l ++ l'

theorem List.foldr_self {α : Type u_1} (l : List α) : List.foldr List.cons [] l = l

theorem List.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) : List.foldl g init (List.map f l) = List.foldl (fun (x : α) (y : β₁) => g x (f y)) init l

theorem List.foldr_map {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) : List.foldr g init (List.map f l) = List.foldr (fun (x : α₁) (y : β) => g (f x) y) init l

mapM

def List.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : List α → m (List β)

Alternate (non-tail-recursive) form of mapM for proofs.

Equations

• List.mapM' f [] = pure []
• List.mapM' f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)

@[simp]

theorem List.mapM'_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → m β} : List.mapM' f [] = pure []

@[simp]

theorem List.mapM'_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [Monad m] {f : α → m β} : List.mapM' f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)

theorem List.mapM'_eq_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) : List.mapM' f l = List.mapM f l

theorem List.mapM'_eq_mapM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) (acc : List β) : List.mapM.loop f l acc = do let __do_lift ← List.mapM' f l pure (acc.reverse ++ __do_lift)

@[simp]

theorem List.mapM_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : List.mapM f [] = pure []

@[simp]

theorem List.mapM_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [Monad m] [LawfulMonad m] (f : α → m β) : List.mapM f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM f l pure (__do_lift :: __do_lift_1)

@[simp]

theorem List.mapM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) {l₁ : List α} {l₂ : List α} : List.mapM f (l₁ ++ l₂) = do let __do_lift ← List.mapM f l₁ let __do_lift_1 ← List.mapM f l₂ pure (__do_lift ++ __do_lift_1)

forM

@[simp]

theorem List.forM_nil' {m : Type u_1 → Type u_2} {α : Type u_3} {f : α → m PUnit} [Monad m] : [].forM f = pure PUnit.unit

@[simp]

theorem List.forM_cons' {m : Type u_1 → Type u_2} : ∀ {α : Type u_3} {a : α} {as : List α} {f : α → m PUnit} [inst : Monad m], (a :: as).forM f = do f a as.forM f

eraseIdx

@[simp]

theorem List.eraseIdx_nil {α : Type u_1} {i : Nat} : [].eraseIdx i = []

@[simp]

theorem List.eraseIdx_cons_zero : ∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).eraseIdx 0 = as

@[simp]

theorem List.eraseIdx_cons_succ : ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, (a :: as).eraseIdx (i + 1) = a :: as.eraseIdx i

find?

@[simp]

theorem List.find?_nil {α : Type u_1} {p : α → Bool} : List.find? p [] = none

theorem List.find?_cons : ∀ {α : Type u_1} {a : α} {as : List α} {p : α → Bool}, List.find? p (a :: as) = match p a with | true => some a | false => List.find? p as

filter

@[simp]

theorem List.filter_nil {α : Type u_1} (p : α → Bool) : List.filter p [] = []

@[simp]

theorem List.filter_cons_of_pos {α : Type u_1} {p : α → Bool} {a : α} (l : List α) (pa : p a = true) : List.filter p (a :: l) = a :: List.filter p l

@[simp]

theorem List.filter_cons_of_neg {α : Type u_1} {p : α → Bool} {a : α} (l : List α) (pa : ¬p a = true) : List.filter p (a :: l) = List.filter p l

theorem List.filter_cons {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} : List.filter p (x :: xs) = if p x = true then x :: List.filter p xs else List.filter p xs

theorem List.mem_filter : ∀ {α : Type u_1} {x : α} {p : α → Bool} {as : List α}, x ∈ List.filter p as ↔ x ∈ as ∧ p x = true

theorem List.filter_eq_nil : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = [] ↔ ∀ (a : α), a ∈ l → ¬p a = true

findSome?

@[simp]

theorem List.findSome?_nil {α : Type u_1} : ∀ {α_1 : Type u_2} {f : α → Option α_1}, List.findSome? f [] = none

theorem List.findSome?_cons {α : Type u_1} {β : Type u_2} {a : α} {as : List α} {f : α → Option β} : List.findSome? f (a :: as) = match f a with | some b => some b | none => List.findSome? f as

replace

@[simp]

theorem List.replace_nil {α : Type u_1} {a : α} {b : α} [BEq α] : [].replace a b = []

theorem List.replace_cons {α : Type u_1} {as : List α} {b : α} {c : α} [BEq α] {a : α} : (a :: as).replace b c = match a == b with | true => c :: as | false => a :: as.replace b c

@[simp]

theorem List.replace_cons_self {α : Type u_1} {as : List α} {b : α} [BEq α] [LawfulBEq α] {a : α} : (a :: as).replace a b = b :: as

elem

@[simp]

theorem List.elem_nil {α : Type u_1} {a : α} [BEq α] : List.elem a [] = false

theorem List.elem_cons {α : Type u_1} {as : List α} {b : α} [BEq α] {a : α} : List.elem b (a :: as) = match b == a with | true => true | false => List.elem b as

@[simp]

theorem List.elem_cons_self {α : Type u_1} {as : List α} [BEq α] [LawfulBEq α] {a : α} : List.elem a (a :: as) = true

lookup

@[simp]

theorem List.lookup_nil {α : Type u_1} {β : Type u_2} {a : α} [BEq α] : List.lookup a [] = none

theorem List.lookup_cons {α : Type u_1} : ∀ {β : Type u_2} {b : β} {es : List (α × β)} {a : α} [inst : BEq α] {k : α}, List.lookup a ((k, b) :: es) = match a == k with | true => some b | false => List.lookup a es

@[simp]

theorem List.lookup_cons_self {α : Type u_1} : ∀ {β : Type u_2} {b : β} {es : List (α × β)} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α}, List.lookup k ((k, b) :: es) = some b

zipWith

@[simp]

theorem List.zipWith_nil_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List β} {f : α → β → γ} : List.zipWith f [] l = []

@[simp]

theorem List.zipWith_nil_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : α → β → γ} : List.zipWith f l [] = []

@[simp]

theorem List.zipWith_cons_cons {α : Type u_1} {β : Type u_2} {γ : Type u_3} {a : α} {as : List α} {b : β} {bs : List β} {f : α → β → γ} : List.zipWith f (a :: as) (b :: bs) = f a b :: List.zipWith f as bs

theorem List.zipWith_get? {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : α → β → γ} : (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with | some a, some b => some (f a b) | x, x_1 => none

zipWithAll

theorem List.zipWithAll_get? {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : Option α → Option β → γ} : (List.zipWithAll f as bs).get? i = match as.get? i, bs.get? i with | none, none => none | a?, b? => some (f a? b?)

zip

@[simp]

theorem List.zip_nil_left {α : Type u_1} {β : Type u_2} {l : List β} : [].zip l = []

@[simp]

theorem List.zip_nil_right {α : Type u_1} {l : List α} {β : Type u_2} : l.zip [] = []

@[simp]

theorem List.zip_cons_cons : ∀ {α : Type u_1} {a : α} {as : List α} {α_1 : Type u_2} {b : α_1} {bs : List α_1}, (a :: as).zip (b :: bs) = (a, b) :: as.zip bs

unzip

@[simp]

theorem List.unzip_nil {α : Type u_1} {β : Type u_2} : [].unzip = ([], [])

@[simp]

theorem List.unzip_cons {α : Type u_1} {β : Type u_2} {t : List (α × β)} {h : α × β} : (h :: t).unzip = match t.unzip with | (al, bl) => (h.fst :: al, h.snd :: bl)

all / any

@[simp]

theorem List.all_eq_true {α : Type u_1} {p : α → Bool} {l : List α} : l.all p = true ↔ ∀ (x : α), x ∈ l → p x = true

@[simp]

theorem List.any_eq_true {α : Type u_1} {p : α → Bool} {l : List α} : l.any p = true ↔ ∃ (x : α), x ∈ l ∧ p x = true

enumFrom

@[simp]

theorem List.enumFrom_nil {α : Type u_1} {i : Nat} : List.enumFrom i [] = []

@[simp]

theorem List.enumFrom_cons : ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.enumFrom i (a :: as) = (i, a) :: List.enumFrom (i + 1) as

iota

@[simp]

theorem List.iota_zero : List.iota 0 = []

@[simp]

theorem List.iota_succ {i : Nat} : List.iota (i + 1) = (i + 1) :: List.iota i

intersperse

@[simp]

theorem List.intersperse_nil {α : Type u_1} (sep : α) : List.intersperse sep [] = []

@[simp]

theorem List.intersperse_single {α : Type u_1} {x : α} (sep : α) : List.intersperse sep [x] = [x]

@[simp]

theorem List.intersperse_cons₂ {α : Type u_1} {x : α} {y : α} {zs : List α} (sep : α) : List.intersperse sep (x :: y :: zs) = x :: sep :: List.intersperse sep (y :: zs)

isPrefixOf

@[simp]

theorem List.isPrefixOf_nil_left {α : Type u_1} {l : List α} [BEq α] : [].isPrefixOf l = true

@[simp]

theorem List.isPrefixOf_cons_nil {α : Type u_1} {a : α} {as : List α} [BEq α] : (a :: as).isPrefixOf [] = false

theorem List.isPrefixOf_cons₂ {α : Type u_1} {as : List α} {b : α} {bs : List α} [BEq α] {a : α} : (a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)

@[simp]

theorem List.isPrefixOf_cons₂_self {α : Type u_1} {as : List α} {bs : List α} [BEq α] [LawfulBEq α] {a : α} : (a :: as).isPrefixOf (a :: bs) = as.isPrefixOf bs

isEqv

@[simp]

theorem List.isEqv_nil_nil {α : Type u_1} {eqv : α → α → Bool} : [].isEqv [] eqv = true

@[simp]

theorem List.isEqv_nil_cons {α : Type u_1} {a : α} {as : List α} {eqv : α → α → Bool} : [].isEqv (a :: as) eqv = false

@[simp]

theorem List.isEqv_cons_nil {α : Type u_1} {a : α} {as : List α} {eqv : α → α → Bool} : (a :: as).isEqv [] eqv = false

theorem List.isEqv_cons₂ : ∀ {α : Type u_1} {a : α} {as : List α} {b : α} {bs : List α} {eqv : α → α → Bool}, (a :: as).isEqv (b :: bs) eqv = (eqv a b && as.isEqv bs eqv)

dropLast

@[simp]

theorem List.dropLast_nil {α : Type u_1} : [].dropLast = []

@[simp]

theorem List.dropLast_single : ∀ {α : Type u_1} {x : α}, [x].dropLast = []

@[simp]

theorem List.dropLast_cons₂ : ∀ {α : Type u_1} {x y : α} {zs : List α}, (x :: y :: zs).dropLast = x :: (y :: zs).dropLast

minimum?

@[simp]

theorem List.minimum?_nil {α : Type u_1} [Min α] : [].minimum? = none

theorem List.minimum?_cons {α : Type u_1} {x : α} [Min α] {xs : List α} : (x :: xs).minimum? = some (List.foldl min x xs)

@[simp]

theorem List.minimum?_eq_none_iff {α : Type u_1} {xs : List α} [Min α] : xs.minimum? = none ↔ xs = []

theorem List.minimum?_mem {α : Type u_1} {a : α} [Min α] (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) {xs : List α} : xs.minimum? = some a → a ∈ xs

theorem List.le_minimum?_iff {α : Type u_1} {a : α} [Min α] [LE α] (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} : xs.minimum? = some a → ∀ (x : α), x ≤ a ↔ ∀ (b : α), b ∈ xs → x ≤ b

theorem List.minimum?_eq_some_iff {α : Type u_1} {a : α} [Min α] [LE α] [anti : Antisymm fun (x x_1 : α) => x ≤ x_1] (le_refl : ∀ (a : α), a ≤ a) (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} : xs.minimum? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b

@[simp]

theorem List.get_cons_succ {α : Type u_1} {i : Nat} {a : α} {as : List α} {h : i + 1 < (a :: as).length} : (a :: as).get ⟨i + 1, h⟩ = as.get ⟨i, ⋯⟩

@[simp]

theorem List.get_cons_succ' {α : Type u_1} {a : α} {as : List α} {i : Fin as.length} : (a :: as).get i.succ = as.get i

@[simp]

theorem List.set_nil {α : Type u_1} (n : Nat) (a : α) : [].set n a = []

@[simp]

theorem List.set_zero {α : Type u_1} (x : α) (xs : List α) (a : α) : (x :: xs).set 0 a = a :: xs

@[simp]

theorem List.set_succ {α : Type u_1} (x : α) (xs : List α) (n : Nat) (a : α) : (x :: xs).set n.succ a = x :: xs.set n a

@[simp]

theorem List.get_set_eq {α : Type u_1} (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) : (l.set i a).get ⟨i, h⟩ = a

@[simp]

theorem List.get_set_ne {α : Type u_1} (l : List α) {i : Nat} {j : Nat} (h : i ≠ j) (a : α) (hj : j < (l.set i a).length) : (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, ⋯⟩