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₂

source

@[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 #

source

@[simp]

theorem List.take_append_drop {α : Type u_1} (n : Nat) (l : List α) :

List.take n l ++ List.drop n l = l

source

@[simp]

theorem List.length_drop {α : Type u_1} (i : Nat) (l : List α) :

(List.drop i l).length = l.length - i

source

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

List.drop i l = []

source

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

List.take i l = l

source

@[simp]

theorem List.take_zero {α : Type u_1} (l : List α) :

List.take 0 l = []

source

@[simp]

theorem List.take_nil {α : Type u_1} {i : Nat} :

List.take i [] = []

source

@[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

source

@[simp]

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

List.drop 0 l = l

source

@[simp]

theorem List.drop_succ_cons :

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

source

@[simp]

theorem List.drop_length {α : Type u_1} (l : List α) :

List.drop l.length l = []

source

@[simp]

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

List.take l.length l = l

source

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

source

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

(l.concat a).reverse = a :: l.reverse

takeWhile and dropWhile #

source

@[simp]

theorem List.dropWhile_nil {α : Type u_1} {p : α → Bool} :

List.dropWhile p [] = []

source

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 #

source

@[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

source

@[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

source

@[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

source

@[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'

source

@[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

source

@[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

source

@[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

source

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

source

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 #

source

@[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

source

@[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

source

@[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

source

@[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'

source

@[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

source

@[simp]

theorem List.foldl_nil :

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

source

@[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

source

@[simp]

theorem List.foldr_nil :

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

source

@[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)

source

@[simp]

theorem List.foldr_self_append {α : Type u_1} {l' : List α} (l : List α) :

List.foldr List.cons l' l = l ++ l'

source

theorem List.foldr_self {α : Type u_1} (l : List α) :

List.foldr List.cons [] l = l

source

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

source

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 #

source

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)

Instances For

source

@[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 []

source

@[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)

source

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

source

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)

source

@[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 []

source

@[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)

source

@[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 #

source

@[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

source

@[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 #

source

@[simp]

theorem List.eraseIdx_nil {α : Type u_1} {i : Nat} :

[].eraseIdx i = []

source

@[simp]

theorem List.eraseIdx_cons_zero :

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

source

@[simp]

theorem List.eraseIdx_cons_succ :

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

find? #

source

@[simp]

theorem List.find?_nil {α : Type u_1} {p : α → Bool} :

List.find? p [] = none

source

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 #

source

@[simp]

theorem List.filter_nil {α : Type u_1} (p : α → Bool) :

List.filter p [] = []

source

@[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

source

@[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

source

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

source

theorem List.mem_filter :

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

source

theorem List.filter_eq_nil :

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

findSome? #

source

@[simp]

theorem List.findSome?_nil {α : Type u_1} :

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

source

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 #

source

@[simp]

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

[].replace a b = []

source

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

source

@[simp]

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

(a :: as).replace a b = b :: as

elem #

source

@[simp]

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

List.elem a [] = false

source

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

source

@[simp]

theorem List.elem_cons_self {α : Type u_1} {as : List α} [BEq α] [LawfulBEq α] {a : α} :

List.elem a (a :: as) = true

lookup #

source

@[simp]

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

List.lookup a [] = none

source

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

source

@[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 #

source

@[simp]

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

List.zipWith f [] l = []

source

@[simp]

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

List.zipWith f l [] = []

source

@[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

source

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 #

source

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 #

source

@[simp]

theorem List.zip_nil_left {α : Type u_1} {β : Type u_2} {l : List β} :

[].zip l = []

source

@[simp]

theorem List.zip_nil_right {α : Type u_1} {l : List α} {β : Type u_2} :

l.zip [] = []

source

@[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 #

source

@[simp]

theorem List.unzip_nil {α : Type u_1} {β : Type u_2} :

[].unzip = ([], [])

source

@[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 #

source

@[simp]

theorem List.all_eq_true {α : Type u_1} {p : α → Bool} {l : List α} :

l.all p = true ↔ ∀ (x : α), x ∈ l → p x = true

source

@[simp]

theorem List.any_eq_true {α : Type u_1} {p : α → Bool} {l : List α} :

l.any p = true ↔ ∃ (x : α), x ∈ l ∧ p x = true

enumFrom #

source

@[simp]

theorem List.enumFrom_nil {α : Type u_1} {i : Nat} :

List.enumFrom i [] = []

source

@[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 #

source

@[simp]

theorem List.iota_zero :

List.iota 0 = []

source

@[simp]

theorem List.iota_succ {i : Nat} :

List.iota (i + 1) = (i + 1) :: List.iota i

intersperse #

source

@[simp]

theorem List.intersperse_nil {α : Type u_1} (sep : α) :

List.intersperse sep [] = []

source

@[simp]

theorem List.intersperse_single {α : Type u_1} {x : α} (sep : α) :

List.intersperse sep [x] = [x]

source

@[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 #

source

@[simp]

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

[].isPrefixOf l = true

source

@[simp]

theorem List.isPrefixOf_cons_nil {α : Type u_1} {a : α} {as : List α} [BEq α] :

(a :: as).isPrefixOf [] = false

source

theorem List.isPrefixOf_cons₂ {α : Type u_1} {as : List α} {b : α} {bs : List α} [BEq α] {a : α} :

(a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)

source

@[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 #

source

@[simp]

theorem List.isEqv_nil_nil {α : Type u_1} {eqv : α → α → Bool} :

[].isEqv [] eqv = true

source

@[simp]

theorem List.isEqv_nil_cons {α : Type u_1} {a : α} {as : List α} {eqv : α → α → Bool} :

[].isEqv (a :: as) eqv = false

source

@[simp]

theorem List.isEqv_cons_nil {α : Type u_1} {a : α} {as : List α} {eqv : α → α → Bool} :

(a :: as).isEqv [] eqv = false

source

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 #

source

@[simp]

theorem List.dropLast_nil {α : Type u_1} :

[].dropLast = []

source

@[simp]

theorem List.dropLast_single :

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

source

@[simp]

theorem List.dropLast_cons₂ :

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

minimum? #

source

@[simp]

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

[].minimum? = none

source

theorem List.minimum?_cons {α : Type u_1} {x : α} [Min α] {xs : List α} :

(x :: xs).minimum? = some (List.foldl min x xs)

source

@[simp]

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

xs.minimum? = none ↔ xs = []

source

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

source

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

source

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

source

@[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, ⋯⟩

source

@[simp]

theorem List.get_cons_succ' {α : Type u_1} {a : α} {as : List α} {i : Fin as.length} :

(a :: as).get i.succ = as.get i

source

@[simp]

theorem List.set_nil {α : Type u_1} (n : Nat) (a : α) :

[].set n a = []

source

@[simp]

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

(x :: xs).set 0 a = a :: xs

source

@[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

source

@[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

source

@[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, ⋯⟩

Basic properties of Lists #

source

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

a :: l ≠ []

source

@[simp]

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

a :: l ≠ l

source

theorem List.head_eq_of_cons_eq :

∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → h₁ = h₂

source

theorem List.tail_eq_of_cons_eq :

∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → t₁ = t₂

source

theorem List.cons_inj {α : Type u_1} (a : α) {l : List α} {l' : List α} :

a :: l = a :: l' ↔ l = l'

source

theorem List.cons_eq_cons {α : Type u_1} {a : α} {b : α} {l : List α} {l' : List α} :

a :: l = b :: l' ↔ a = b ∧ l = l'

source

theorem List.exists_cons_of_ne_nil {α : Type u_1} {l : List α} :

l ≠ [] → ∃ (b : α), ∃ (L : List α), l = b :: L

length #

source

theorem List.length_pos_of_mem {α : Type u_1} {a : α} {l : List α} :

a ∈ l → 0 < l.length

source

theorem List.exists_mem_of_length_pos {α : Type u_1} {l : List α} :

0 < l.length → ∃ (a : α), a ∈ l

source

theorem List.length_pos_iff_exists_mem {α : Type u_1} {l : List α} :

0 < l.length ↔ ∃ (a : α), a ∈ l

source

theorem List.exists_cons_of_length_pos {α : Type u_1} {l : List α} :

0 < l.length → ∃ (h : α), ∃ (t : List α), l = h :: t

source

theorem List.length_pos_iff_exists_cons {α : Type u_1} {l : List α} :

0 < l.length ↔ ∃ (h : α), ∃ (t : List α), l = h :: t

source

theorem List.exists_cons_of_length_succ {α : Type u_1} {n : Nat} {l : List α} :

l.length = n + 1 → ∃ (h : α), ∃ (t : List α), l = h :: t

source

theorem List.length_pos {α : Type u_1} {l : List α} :

0 < l.length ↔ l ≠ []

source

theorem List.exists_mem_of_ne_nil {α : Type u_1} (l : List α) (h : l ≠ []) :

∃ (x : α), x ∈ l

source

theorem List.length_eq_one {α : Type u_1} {l : List α} :

l.length = 1 ↔ ∃ (a : α), l = [a]

mem #

source

theorem List.mem_nil_iff {α : Type u_1} (a : α) :

a ∈ [] ↔ False

source

theorem List.mem_singleton_self {α : Type u_1} (a : α) :

a ∈ [a]

source

theorem List.eq_of_mem_singleton :

∀ {α : Type u_1} {a b : α}, a ∈ [b] → a = b

source

@[simp]

theorem List.mem_singleton {α : Type u_1} {a : α} {b : α} :

a ∈ [b] ↔ a = b

source

theorem List.mem_of_mem_cons_of_mem {α : Type u_1} {a : α} {b : α} {l : List α} :

a ∈ b :: l → b ∈ l → a ∈ l

source

theorem List.eq_or_ne_mem_of_mem {α : Type u_1} {a : α} {b : α} {l : List α} (h' : a ∈ b :: l) :

a = b ∨ a ≠ b ∧ a ∈ l

source

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

l ≠ []

source

theorem List.append_of_mem {α : Type u_1} {a : α} {l : List α} :

a ∈ l → ∃ (s : List α), ∃ (t : List α), l = s ++ a :: t

source

theorem List.elem_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : List α} :

List.elem a as = true ↔ a ∈ as

source

@[simp]

theorem List.elem_eq_mem {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (as : List α) :

List.elem a as = decide (a ∈ as)

source

theorem List.mem_of_ne_of_mem {α : Type u_1} {a : α} {y : α} {l : List α} (h₁ : a ≠ y) (h₂ : a ∈ y :: l) :

a ∈ l

source

theorem List.ne_of_not_mem_cons {α : Type u_1} {a : α} {b : α} {l : List α} :

¬a ∈ b :: l → a ≠ b

source

theorem List.not_mem_of_not_mem_cons {α : Type u_1} {a : α} {b : α} {l : List α} :

¬a ∈ b :: l → ¬a ∈ l

source

theorem List.not_mem_cons_of_ne_of_not_mem {α : Type u_1} {a : α} {y : α} {l : List α} :

a ≠ y → ¬a ∈ l → ¬a ∈ y :: l

source

theorem List.ne_and_not_mem_of_not_mem_cons {α : Type u_1} {a : α} {y : α} {l : List α} :

¬a ∈ y :: l → a ≠ y ∧ ¬a ∈ l

drop #

source

theorem List.drop_add {α : Type u_1} (m : Nat) (n : Nat) (l : List α) :

List.drop (m + n) l = List.drop m (List.drop n l)

source

@[simp]

theorem List.drop_left {α : Type u_1} (l₁ : List α) (l₂ : List α) :

List.drop l₁.length (l₁ ++ l₂) = l₂

source

theorem List.drop_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : l₁.length = n) :

List.drop n (l₁ ++ l₂) = l₂

isEmpty #

source

@[simp]

theorem List.isEmpty_nil {α : Type u_1} :

[].isEmpty = true

source

@[simp]

theorem List.isEmpty_cons {α : Type u_1} {x : α} {xs : List α} :

(x :: xs).isEmpty = false

append #

source

theorem List.append_eq_append :

∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.append l₂ = l₁ ++ l₂

source

theorem List.append_ne_nil_of_ne_nil_left {α : Type u_1} (s : List α) (t : List α) :

s ≠ [] → s ++ t ≠ []

source

theorem List.append_ne_nil_of_ne_nil_right {α : Type u_1} (s : List α) (t : List α) :

t ≠ [] → s ++ t ≠ []

source

@[simp]

theorem List.nil_eq_append :

∀ {α : Type u_1} {a b : List α}, [] = a ++ b ↔ a = [] ∧ b = []

source

theorem List.append_ne_nil_of_left_ne_nil {α : Type u_1} (a : List α) (b : List α) (h0 : a ≠ []) :

a ++ b ≠ []

source

theorem List.append_eq_cons :

∀ {α : Type u_1} {a b : List α} {x : α} {c : List α}, a ++ b = x :: c ↔ a = [] ∧ b = x :: c ∨ ∃ (a' : List α), a = x :: a' ∧ c = a' ++ b

source

theorem List.cons_eq_append :

∀ {α : Type u_1} {x : α} {c a b : List α}, x :: c = a ++ b ↔ a = [] ∧ b = x :: c ∨ ∃ (a' : List α), a = x :: a' ∧ c = a' ++ b

source

theorem List.append_eq_append_iff {α : Type u_1} {a : List α} {b : List α} {c : List α} {d : List α} :

a ++ b = c ++ d ↔ (∃ (a' : List α), c = a ++ a' ∧ b = a' ++ d) ∨ ∃ (c' : List α), a = c ++ c' ∧ d = c' ++ b

source

@[simp]

theorem List.mem_append {α : Type u_1} {a : α} {s : List α} {t : List α} :

a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

source

theorem List.not_mem_append {α : Type u_1} {a : α} {s : List α} {t : List α} (h₁ : ¬a ∈ s) (h₂ : ¬a ∈ t) :

¬a ∈ s ++ t

source

theorem List.mem_append_eq {α : Type u_1} (a : α) (s : List α) (t : List α) :

(a ∈ s ++ t) = (a ∈ s ∨ a ∈ t)

source

theorem List.mem_append_left {α : Type u_1} {a : α} {l₁ : List α} (l₂ : List α) (h : a ∈ l₁) :

a ∈ l₁ ++ l₂

source

theorem List.mem_append_right {α : Type u_1} {a : α} (l₁ : List α) {l₂ : List α} (h : a ∈ l₂) :

a ∈ l₁ ++ l₂

source

theorem List.mem_iff_append {α : Type u_1} {a : α} {l : List α} :

a ∈ l ↔ ∃ (s : List α), ∃ (t : List α), l = s ++ a :: t

concat #

source

theorem List.concat_nil {α : Type u_1} (a : α) :

[].concat a = [a]

source

theorem List.concat_cons {α : Type u_1} (a : α) (b : α) (l : List α) :

(a :: l).concat b = a :: l.concat b

source

theorem List.init_eq_of_concat_eq {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} :

l₁.concat a = l₂.concat a → l₁ = l₂

source

theorem List.last_eq_of_concat_eq {α : Type u_1} {a : α} {b : α} {l : List α} :

l.concat a = l.concat b → a = b

source

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

l.concat a ≠ []

source

theorem List.concat_append {α : Type u_1} (a : α) (l₁ : List α) (l₂ : List α) :

l₁.concat a ++ l₂ = l₁ ++ a :: l₂

source

theorem List.append_concat {α : Type u_1} (a : α) (l₁ : List α) (l₂ : List α) :

l₁ ++ l₂.concat a = (l₁ ++ l₂).concat a

map #

source

theorem List.map_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :

List.map f [a] = [f a]

source

theorem List.exists_of_mem_map :

∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {f : α_1 → α} {l : List α_1}, b ∈ List.map f l → ∃ (a : α_1), a ∈ l ∧ f a = b

source

theorem List.forall_mem_map_iff {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {P : β → Prop} :

(∀ (i : β), i ∈ List.map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)

source

@[simp]

theorem List.map_eq_nil {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} :

List.map f l = [] ↔ l = []

zipWith #

source

@[simp]

theorem List.zipWith_map {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {μ : Type u_5} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) :

List.zipWith f (List.map g l₁) (List.map h l₂) = List.zipWith (fun (a : α) (b : β) => f (g a) (h b)) l₁ l₂

source

theorem List.zipWith_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} (l₁ : List α) (l₂ : List β) (f : α → α') (g : α' → β → γ) :

List.zipWith g (List.map f l₁) l₂ = List.zipWith (fun (a : α) (b : β) => g (f a) b) l₁ l₂

source

theorem List.zipWith_map_right {α : Type u_1} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} (l₁ : List α) (l₂ : List β) (f : β → β') (g : α → β' → γ) :

List.zipWith g l₁ (List.map f l₂) = List.zipWith (fun (a : α) (b : β) => g a (f b)) l₁ l₂

source

theorem List.zipWith_foldr_eq_zip_foldr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {g : γ → δ → δ} {f : α → β → γ} (i : δ) :

List.foldr g i (List.zipWith f l₁ l₂) = List.foldr (fun (p : α × β) (r : δ) => g (f p.fst p.snd) r) i (l₁.zip l₂)

source

theorem List.zipWith_foldl_eq_zip_foldl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {g : δ → γ → δ} {f : α → β → γ} (i : δ) :

List.foldl g i (List.zipWith f l₁ l₂) = List.foldl (fun (r : δ) (p : α × β) => g r (f p.fst p.snd)) i (l₁.zip l₂)

source

@[simp]

theorem List.zipWith_eq_nil_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l : List α} {l' : List β} :

List.zipWith f l l' = [] ↔ l = [] ∨ l' = []

source

theorem List.map_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ → α) (l : List γ) (l' : List δ) :

List.map f (List.zipWith g l l') = List.zipWith (fun (x : γ) (y : δ) => f (g x y)) l l'

source

theorem List.zipWith_distrib_take :

∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1} {n : Nat}, List.take n (List.zipWith f l l') = List.zipWith f (List.take n l) (List.take n l')

source

theorem List.zipWith_distrib_drop :

∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1} {n : Nat}, List.drop n (List.zipWith f l l') = List.zipWith f (List.drop n l) (List.drop n l')

source

theorem List.zipWith_append {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (l : List α) (la : List α) (l' : List β) (lb : List β) (h : l.length = l'.length) :

List.zipWith f (l ++ la) (l' ++ lb) = List.zipWith f l l' ++ List.zipWith f la lb

zip #

source

theorem List.zip_map {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (l₁ : List α) (l₂ : List β) :

(List.map f l₁).zip (List.map g l₂) = List.map (Prod.map f g) (l₁.zip l₂)

source

theorem List.zip_map_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : α → γ) (l₁ : List α) (l₂ : List β) :

(List.map f l₁).zip l₂ = List.map (Prod.map f id) (l₁.zip l₂)

source

theorem List.zip_map_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) (l₁ : List α) (l₂ : List β) :

l₁.zip (List.map f l₂) = List.map (Prod.map id f) (l₁.zip l₂)

source

theorem List.zip_append {α : Type u_1} {β : Type u_2} {l₁ : List α} {r₁ : List α} {l₂ : List β} {r₂ : List β} (_h : l₁.length = l₂.length) :

(l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂

source

theorem List.zip_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (l : List α) :

(List.map f l).zip (List.map g l) = List.map (fun (a : α) => (f a, g a)) l

source

theorem List.of_mem_zip {α : Type u_1} {β : Type u_2} {a : α} {b : β} {l₁ : List α} {l₂ : List β} :

(a, b) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂

source

theorem List.map_fst_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :

l₁.length ≤ l₂.length → List.map Prod.fst (l₁.zip l₂) = l₁

source

theorem List.map_snd_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :

l₂.length ≤ l₁.length → List.map Prod.snd (l₁.zip l₂) = l₂

join #

source

theorem List.mem_join {α : Type u_1} {a : α} {L : List (List α)} :

a ∈ L.join ↔ ∃ (l : List α), l ∈ L ∧ a ∈ l

source

theorem List.exists_of_mem_join :

∀ {α : Type u_1} {a : α} {L : List (List α)}, a ∈ L.join → ∃ (l : List α), l ∈ L ∧ a ∈ l

source

theorem List.mem_join_of_mem :

∀ {α : Type u_1} {l : List α} {L : List (List α)} {a : α}, l ∈ L → a ∈ l → a ∈ L.join

bind #

source

theorem List.mem_bind {α : Type u_1} {β : Type u_2} {f : α → List β} {b : β} {l : List α} :

b ∈ l.bind f ↔ ∃ (a : α), a ∈ l ∧ b ∈ f a

source

theorem List.exists_of_mem_bind {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : α → List β} :

b ∈ l.bind f → ∃ (a : α), a ∈ l ∧ b ∈ f a

source

theorem List.mem_bind_of_mem {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : α → List β} {a : α} (al : a ∈ l) (h : b ∈ f a) :

b ∈ l.bind f

source

theorem List.bind_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) (g : α → List β) (l : List α) :

List.map f (l.bind g) = l.bind fun (a : α) => List.map f (g a)

set-theoretic notation of Lists #

source

@[simp]

theorem List.empty_eq {α : Type u_1} :

∅ = []

bounded quantifiers over Lists #

source

theorem List.exists_mem_nil {α : Type u_1} (p : α → Prop) :

¬∃ (x : α), ∃ (x_1 : x ∈ []), p x

source

theorem List.forall_mem_nil {α : Type u_1} (p : α → Prop) (x : α) :

x ∈ [] → p x

source

theorem List.exists_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {l : List α} :

(∃ (x : α), ∃ (x_1 : x ∈ a :: l), p x) ↔ p a ∨ ∃ (x : α), ∃ (x_1 : x ∈ l), p x

source

theorem List.forall_mem_singleton {α : Type u_1} {p : α → Prop} {a : α} :

(∀ (x : α), x ∈ [a] → p x) ↔ p a

source

theorem List.forall_mem_append {α : Type u_1} {p : α → Prop} {l₁ : List α} {l₂ : List α} :

(∀ (x : α), x ∈ l₁ ++ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

replicate #

source

theorem List.replicate_succ {α : Type u_1} (a : α) (n : Nat) :

List.replicate (n + 1) a = a :: List.replicate n a

source

theorem List.mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} :

b ∈ List.replicate n a ↔ n ≠ 0 ∧ b = a

source

theorem List.eq_of_mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} (h : b ∈ List.replicate n a) :

b = a

source

theorem List.eq_replicate_of_mem {α : Type u_1} {a : α} {l : List α} :

(∀ (b : α), b ∈ l → b = a) → l = List.replicate l.length a

source

theorem List.eq_replicate {α : Type u_1} {a : α} {n : Nat} {l : List α} :

l = List.replicate n a ↔ l.length = n ∧ ∀ (b : α), b ∈ l → b = a

getLast #

source

theorem List.getLast_cons' {α : Type u_1} {a : α} {l : List α} (h₁ : a :: l ≠ []) (h₂ : l ≠ []) :

(a :: l).getLast h₁ = l.getLast h₂

source

@[simp]

theorem List.getLast_append {α : Type u_1} {a : α} (l : List α) (h : l ++ [a] ≠ []) :

(l ++ [a]).getLast h = a

source

theorem List.getLast_concat :

∀ {α : Type u_1} {l : List α} {a : α} (h : l.concat a ≠ []), (l.concat a).getLast h = a

source

theorem List.eq_nil_or_concat {α : Type u_1} (l : List α) :

l = [] ∨ ∃ (L : List α), ∃ (b : α), l = L ++ [b]

head #

source

theorem List.head!_of_head? {α : Type u_1} {a : α} [Inhabited α] {l : List α} :

l.head? = some a → l.head! = a

source

theorem List.head?_eq_head {α : Type u_1} (l : List α) (h : l ≠ []) :

l.head? = some (l.head h)

tail #

source

@[simp]

theorem List.tailD_eq_tail? {α : Type u_1} (l : List α) (l' : List α) :

l.tailD l' = l.tail?.getD l'

getLast #

source

@[simp]

theorem List.getLastD_nil {α : Type u_1} (a : α) :

[].getLastD a = a

source

@[simp]

theorem List.getLastD_cons {α : Type u_1} (a : α) (b : α) (l : List α) :

(b :: l).getLastD a = l.getLastD b

source

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

(a :: l).getLast h = l.getLastD a

source

theorem List.getLastD_eq_getLast? {α : Type u_1} (a : α) (l : List α) :

l.getLastD a = l.getLast?.getD a

source

@[simp]

theorem List.getLast_singleton {α : Type u_1} (a : α) (h : [a] ≠ []) :

[a].getLast h = a

source

theorem List.getLast!_cons {α : Type u_1} {a : α} {l : List α} [Inhabited α] :

(a :: l).getLast! = l.getLastD a

source

theorem List.getLast?_cons {α : Type u_1} {a : α} {l : List α} :

(a :: l).getLast? = some (l.getLastD a)

source

@[simp]

theorem List.getLast?_singleton {α : Type u_1} (a : α) :

[a].getLast? = some a

source

theorem List.getLast_mem {α : Type u_1} {l : List α} (h : l ≠ []) :

l.getLast h ∈ l

source

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

l.getLastD a ∈ a :: l

source

@[simp]

theorem List.getLast?_reverse {α : Type u_1} (l : List α) :

l.reverse.getLast? = l.head?

source

@[simp]

theorem List.head?_reverse {α : Type u_1} (l : List α) :

l.reverse.head? = l.getLast?

dropLast #

NB: dropLast is the specification for Array.pop, so theorems about List.dropLast are often used for theorems about Array.pop.

source

theorem List.dropLast_cons_of_ne_nil {α : Type u} {x : α} {l : List α} (h : l ≠ []) :

(x :: l).dropLast = x :: l.dropLast

source

@[simp]

theorem List.dropLast_append_of_ne_nil {α : Type u} {l : List α} (l' : List α) :

l ≠ [] → (l' ++ l).dropLast = l' ++ l.dropLast

source

theorem List.dropLast_append_cons :

∀ {α : Type u_1} {l₁ : List α} {b : α} {l₂ : List α}, (l₁ ++ b :: l₂).dropLast = l₁ ++ (b :: l₂).dropLast

source

@[simp]

theorem List.dropLast_concat :

∀ {α : Type u_1} {l₁ : List α} {b : α}, (l₁ ++ [b]).dropLast = l₁

source

@[simp]

theorem List.length_dropLast {α : Type u_1} (xs : List α) :

xs.dropLast.length = xs.length - 1

source

@[simp]

theorem List.get_dropLast {α : Type u_1} (xs : List α) (i : Fin xs.dropLast.length) :

xs.dropLast.get i = xs.get ⟨↑i, ⋯⟩

nth element #

source

@[simp]

theorem List.get_cons_cons_one :

∀ {α : Type u_1} {a₁ a₂ : α} {as : List α}, (a₁ :: a₂ :: as).get 1 = a₂

source

theorem List.get!_cons_succ {α : Type u_1} [Inhabited α] (l : List α) (a : α) (n : Nat) :

(a :: l).get! (n + 1) = l.get! n

source

theorem List.get!_cons_zero {α : Type u_1} [Inhabited α] (l : List α) (a : α) :

(a :: l).get! 0 = a

source

theorem List.get!_nil {α : Type u_1} [Inhabited α] (n : Nat) :

[].get! n = default

source

theorem List.get!_len_le {α : Type u_1} [Inhabited α] {l : List α} {n : Nat} :

l.length ≤ n → l.get! n = default

source

theorem List.get?_of_mem {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) :

∃ (n : Nat), l.get? n = some a

source

theorem List.get?_mem {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : l.get? n = some a) :

a ∈ l

source

theorem List.Fin.exists_iff {n : Nat} (p : Fin n → Prop) :

(∃ (i : Fin n), p i) ↔ ∃ (i : Nat), ∃ (h : i < n), p ⟨i, h⟩

source

theorem List.mem_iff_get? {α : Type u_1} {a : α} {l : List α} :

a ∈ l ↔ ∃ (n : Nat), l.get? n = some a

source

theorem List.get?_zero {α : Type u_1} (l : List α) :

l.get? 0 = l.head?

source

@[simp]

theorem List.getElem_eq_get {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) :

l[i] = l.get ⟨i, h⟩

source

@[simp]

theorem List.getElem?_eq_get? {α : Type u_1} (l : List α) (i : Nat) :

l[i]? = l.get? i

source

theorem List.get_of_eq {α : Type u_1} {l : List α} {l' : List α} (h : l = l') (i : Fin l.length) :

l.get i = l'.get ⟨↑i, ⋯⟩

If one has get l i hi in a formula and h : l = l', one can not rw h in the formula as hi gives i < l.length and not i < l'.length. The theorem get_of_eq can be used to make such a rewrite, with rw [get_of_eq h].

source

@[simp]

theorem List.get_singleton {α : Type u_1} (a : α) (n : Fin 1) :

[a].get n = a

source

theorem List.get_mk_zero {α : Type u_1} {l : List α} (h : 0 < l.length) :

l.get ⟨0, h⟩ = l.head ⋯

source

theorem List.get_append_right_aux {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) :

n - l₁.length < l₂.length

source

theorem List.get_append_right' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) :

(l₁ ++ l₂).get ⟨n, h₂⟩ = l₂.get ⟨n - l₁.length, ⋯⟩

source

theorem List.get_of_append_proof {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) :

n < l.length

source

theorem List.get_of_append {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) :

l.get ⟨n, ⋯⟩ = a

source

@[simp]

theorem List.get_replicate {α : Type u_1} (a : α) {n : Nat} (m : Fin (List.replicate n a).length) :

(List.replicate n a).get m = a

source

@[simp]

theorem List.getLastD_concat {α : Type u_1} (a : α) (b : α) (l : List α) :

(l ++ [b]).getLastD a = b

source

theorem List.get_cons_length {α : Type u_1} (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :

(x :: xs).get ⟨n, ⋯⟩ = (x :: xs).getLast ⋯

source

theorem List.get!_of_get? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} :

l.get? n = some a → l.get! n = a

source

@[simp]

theorem List.get!_eq_getD {α : Type u_1} [Inhabited α] (l : List α) (n : Nat) :

l.get! n = l.getD n default

set #

source

@[simp]

theorem List.set_eq_nil {α : Type u_1} (l : List α) (n : Nat) (a : α) :

l.set n a = [] ↔ l = []

source

theorem List.set_comm {α : Type u_1} (a : α) (b : α) {n : Nat} {m : Nat} (l : List α) :

n ≠ m → (l.set n a).set m b = (l.set m b).set n a

source

@[simp]

theorem List.set_set {α : Type u_1} (a : α) (b : α) (l : List α) (n : Nat) :

(l.set n a).set n b = l.set n b

source

theorem List.get_set {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : n < (l.set m a).length) :

(l.set m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, ⋯⟩

source

theorem List.mem_or_eq_of_mem_set {α : Type u_1} {l : List α} {n : Nat} {a : α} {b : α} :

a ∈ l.set n b → a ∈ l ∨ a = b

all / any #

source

@[simp]

theorem List.contains_nil {α : Type u_1} {a : α} [BEq α] :

[].contains a = false

source

@[simp]

theorem List.contains_cons {α : Type u_1} {a : α} {as : List α} {x : α} [BEq α] :

(a :: as).contains x = (x == a || as.contains x)

source

theorem List.contains_eq_any_beq {α : Type u_1} [BEq α] (l : List α) (a : α) :

l.contains a = l.any fun (x : α) => a == x

source

theorem List.not_all_eq_any_not {α : Type u_1} (l : List α) (p : α → Bool) :

(!l.all p) = l.any fun (a : α) => !p a

source

theorem List.not_any_eq_all_not {α : Type u_1} (l : List α) (p : α → Bool) :

(!l.any p) = l.all fun (a : α) => !p a

source

theorem List.or_all_distrib_left {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) :

(q || l.all p) = l.all fun (a : α) => q || p a

source

theorem List.or_all_distrib_right {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) :

(l.all p || q) = l.all fun (a : α) => p a || q

source

theorem List.and_any_distrib_left {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) :

(q && l.any p) = l.any fun (a : α) => q && p a

source

theorem List.and_any_distrib_right {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) :

(l.any p && q) = l.any fun (a : α) => p a && q

source

theorem List.any_eq_not_all_not {α : Type u_1} (l : List α) (p : α → Bool) :

l.any p = !l.all fun (x : α) => !p x

source

theorem List.all_eq_not_any_not {α : Type u_1} (l : List α) (p : α → Bool) :

l.all p = !l.any fun (x : α) => !p x

reverse #

source

@[simp]

theorem List.mem_reverseAux {α : Type u_1} {x : α} {as : List α} {bs : List α} :

x ∈ as.reverseAux bs ↔ x ∈ as ∨ x ∈ bs

source

@[simp]

theorem List.mem_reverse {α : Type u_1} {x : α} {as : List α} :

x ∈ as.reverse ↔ x ∈ as

insert #

source

@[simp]

theorem List.insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :

List.insert a l = l

source

@[simp]

theorem List.insert_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a ∈ l) :

List.insert a l = a :: l

source

@[simp]

theorem List.mem_insert_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} :

a ∈ List.insert b l ↔ a = b ∨ a ∈ l

source

@[simp]

theorem List.mem_insert_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :

a ∈ List.insert a l

source

theorem List.mem_insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} (h : a ∈ l) :

a ∈ List.insert b l

source

theorem List.eq_or_mem_of_mem_insert {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} (h : a ∈ List.insert b l) :

a = b ∨ a ∈ l

source

@[simp]

theorem List.length_insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :

(List.insert a l).length = l.length

source

@[simp]

theorem List.length_insert_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a ∈ l) :

(List.insert a l).length = l.length + 1

erase #

source

@[simp]

theorem List.erase_nil {α : Type u_1} [BEq α] (a : α) :

[].erase a = []

source

theorem List.erase_cons {α : Type u_1} [BEq α] (a : α) (b : α) (l : List α) :

(b :: l).erase a = if (b == a) = true then l else b :: l.erase a

source

@[simp]

theorem List.erase_cons_head {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :

(a :: l).erase a = l

source

@[simp]

theorem List.erase_cons_tail {α : Type u_1} [BEq α] {a : α} {b : α} (l : List α) (h : ¬(b == a) = true) :

(b :: l).erase a = b :: l.erase a

source

theorem List.erase_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :

¬a ∈ l → l.erase a = l

filter and partition #

source

@[simp]

theorem List.filter_append {α : Type u_1} {p : α → Bool} (l₁ : List α) (l₂ : List α) :

List.filter p (l₁ ++ l₂) = List.filter p l₁ ++ List.filter p l₂

source

@[simp]

theorem List.partition_eq_filter_filter {α : Type u_1} (p : α → Bool) (l : List α) :

List.partition p l = (List.filter p l, List.filter (not ∘ p) l)

source

theorem List.partition_eq_filter_filter.aux {α : Type u_1} (p : α → Bool) (l : List α) {as : List α} {bs : List α} :

List.partition.loop p l (as, bs) = (as.reverse ++ List.filter p l, bs.reverse ++ List.filter (not ∘ p) l)

source

theorem List.filter_congr' {α : Type u_1} {p : α → Bool} {q : α → Bool} {l : List α} :

(∀ (x : α), x ∈ l → (p x = true ↔ q x = true)) → List.filter p l = List.filter q l

filterMap #

source

@[simp]

theorem List.filterMap_nil {α : Type u_1} {β : Type u_2} (f : α → Option β) :

List.filterMap f [] = []

source

@[simp]

theorem List.filterMap_cons {α : Type u_1} {β : Type u_2} (f : α → Option β) (a : α) (l : List α) :

List.filterMap f (a :: l) = match f a with | none => List.filterMap f l | some b => b :: List.filterMap f l

source

theorem List.filterMap_cons_none {α : Type u_1} {β : Type u_2} {f : α → Option β} (a : α) (l : List α) (h : f a = none) :

List.filterMap f (a :: l) = List.filterMap f l

source

theorem List.filterMap_cons_some {α : Type u_1} {β : Type u_2} (f : α → Option β) (a : α) (l : List α) {b : β} (h : f a = some b) :

List.filterMap f (a :: l) = b :: List.filterMap f l

source

theorem List.filterMap_append {α : Type u_1} {β : Type u_2} (l : List α) (l' : List α) (f : α → Option β) :

List.filterMap f (l ++ l') = List.filterMap f l ++ List.filterMap f l'

source

@[simp]

theorem List.filterMap_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) :

List.filterMap (some ∘ f) = List.map f

source

@[simp]

theorem List.filterMap_eq_filter {α : Type u_1} (p : α → Bool) :

List.filterMap (Option.guard fun (x : α) => p x = true) = List.filter p

source

theorem List.filterMap_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : β → Option γ) (l : List α) :

List.filterMap g (List.filterMap f l) = List.filterMap (fun (x : α) => (f x).bind g) l

source

theorem List.map_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : β → γ) (l : List α) :

List.map g (List.filterMap f l) = List.filterMap (fun (x : α) => Option.map g (f x)) l

source

@[simp]

theorem List.filterMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → Option γ) (l : List α) :

List.filterMap g (List.map f l) = List.filterMap (g ∘ f) l

source

theorem List.filter_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (p : β → Bool) (l : List α) :

List.filter p (List.filterMap f l) = List.filterMap (fun (x : α) => Option.filter p (f x)) l

source

theorem List.filterMap_filter {α : Type u_1} {β : Type u_2} (p : α → Bool) (f : α → Option β) (l : List α) :

List.filterMap f (List.filter p l) = List.filterMap (fun (x : α) => if p x = true then f x else none) l

source

@[simp]

theorem List.filterMap_some {α : Type u_1} (l : List α) :

List.filterMap some l = l

source

theorem List.map_filterMap_some_eq_filter_map_is_some {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) :

List.map some (List.filterMap f l) = List.filter (fun (b : Option β) => b.isSome) (List.map f l)

source

@[simp]

theorem List.mem_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) {b : β} :

b ∈ List.filterMap f l ↔ ∃ (a : α), a ∈ l ∧ f a = some b

source

@[simp]

theorem List.filterMap_join {α : Type u_1} {β : Type u_2} (f : α → Option β) (L : List (List α)) :

List.filterMap f L.join = (List.map (List.filterMap f) L).join

source

theorem List.map_filterMap_of_inv {α : Type u_1} {β : Type u_2} (f : α → Option β) (g : β → α) (H : ∀ (x : α), Option.map g (f x) = some x) (l : List α) :

List.map g (List.filterMap f l) = l

source

theorem List.map_filter {β : Type u_1} {α : Type u_2} {p : α → Bool} (f : β → α) (l : List β) :

List.filter p (List.map f l) = List.map f (List.filter (p ∘ f) l)

source

@[simp]

theorem List.filter_filter :

∀ {α : Type u_1} {p : α → Bool} (q : α → Bool) (l : List α), List.filter p (List.filter q l) = List.filter (fun (a : α) => decide (p a = true ∧ q a = true)) l

find? #

source

theorem List.find?_cons_of_pos :

∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), p a = true → List.find? p (a :: l) = some a

source

theorem List.find?_cons_of_neg :

∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), ¬p a = true → List.find? p (a :: l) = List.find? p l

source

theorem List.find?_eq_none :

∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.find? p l = none ↔ ∀ (x : α), x ∈ l → ¬p x = true

source

theorem List.find?_some :

∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → p a = true

source

@[simp]

theorem List.mem_of_find?_eq_some :

∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → a ∈ l

findSome? #

source

theorem List.exists_of_findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → Option β} (w : List.findSome? f l = some b) :

∃ (a : α), a ∈ l ∧ f a = some b

takeWhile and dropWhile #

source

@[simp]

theorem List.takeWhile_append_dropWhile {α : Type u_1} (p : α → Bool) (l : List α) :

List.takeWhile p l ++ List.dropWhile p l = l

source

theorem List.dropWhile_append {α : Type u_1} {p : α → Bool} {xs : List α} {ys : List α} :

List.dropWhile p (xs ++ ys) = if (List.dropWhile p xs).isEmpty = true then List.dropWhile p ys else List.dropWhile p xs ++ ys

enum, enumFrom #

source

@[simp]

theorem List.enumFrom_length {α : Type u_1} {n : Nat} {l : List α} :

(List.enumFrom n l).length = l.length

source

@[simp]

theorem List.enum_length :

∀ {α : Type u_1} {l : List α}, l.enum.length = l.length

maximum? #

source

@[simp]

theorem List.maximum?_nil {α : Type u_1} [Max α] :

[].maximum? = none

source

theorem List.maximum?_cons {α : Type u_1} {x : α} [Max α] {xs : List α} :

(x :: xs).maximum? = some (List.foldl max x xs)

source

@[simp]

theorem List.maximum?_eq_none_iff {α : Type u_1} {xs : List α} [Max α] :

xs.maximum? = none ↔ xs = []

source

theorem List.maximum?_mem {α : Type u_1} {a : α} [Max α] (min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b) {xs : List α} :

xs.maximum? = some a → a ∈ xs

source

theorem List.maximum?_le_iff {α : Type u_1} {a : α} [Max α] [LE α] (max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :

xs.maximum? = some a → ∀ (x : α), a ≤ x ↔ ∀ (b : α), b ∈ xs → b ≤ x

source

theorem List.maximum?_eq_some_iff {α : Type u_1} {a : α} [Max α] [LE α] [anti : Antisymm fun (x x_1 : α) => x ≤ x_1] (le_refl : ∀ (a : α), a ≤ a) (max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b) (max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :

xs.maximum? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a

lt #

source

theorem List.lt_irrefl' {α : Type u_1} [LT α] (lt_irrefl : ∀ (x : α), ¬x < x) (l : List α) :

¬l < l

source

theorem List.lt_trans' {α : Type u_1} [LT α] [DecidableRel LT.lt] (lt_trans : ∀ {x y z : α}, x < y → y < z → x < z) (le_trans : ∀ {x y z : α}, ¬x < y → ¬y < z → ¬x < z) {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) :

l₁ < l₃

source

theorem List.lt_antisymm' {α : Type u_1} [LT α] (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y) {l₁ : List α} {l₂ : List α} (h₁ : ¬l₁ < l₂) (h₂ : ¬l₂ < l₁) :

l₁ = l₂