Documentation

Std.Data.List.Init.Lemmas

Bootstrapping theorems for lists #

These are theorems used in the definitions of Std.Data.List.Basic. 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} :
List.get? [] n = none
@[simp]
theorem List.get?_cons_zero {α : Type u_1} {a : α} {l : List α} :
List.get? (a :: l) 0 = some a
@[simp]
theorem List.get?_cons_succ {α : Type u_1} {a : α} {l : List α} {n : Nat} :
List.get? (a :: l) (n + 1) = List.get? l n
@[simp]
theorem List.head?_nil {α : Type u_1} :
List.head? [] = none
@[simp]
theorem List.head?_cons {α : Type u_1} {a : α} {l : List α} :
@[simp]
theorem List.headD_nil {α : Type u_1} {d : α} :
List.headD [] d = d
@[simp]
theorem List.headD_cons {α : Type u_1} {a : α} {l : List α} {d : α} :
List.headD (a :: l) d = a
@[simp]
theorem List.head_cons {α : Type u_1} {a : α} {l : List α} {h : a :: l []} :
List.head (a :: l) h = a
@[simp]
theorem List.tail?_nil {α : Type u_1} :
List.tail? [] = none
@[simp]
theorem List.tail?_cons {α : Type u_1} {a : α} {l : List α} :
@[simp]
theorem List.tail!_cons {α : Type u_1} {a : α} {l : List α} :
List.tail! (a :: l) = l
@[simp]
theorem List.tailD_nil {α : Type u_1} {l' : List α} :
List.tailD [] l' = l'
@[simp]
theorem List.tailD_cons {α : Type u_1} {a : α} {l : List α} {l' : List α} :
List.tailD (a :: l) l' = l
@[simp]
theorem List.any_nil :
∀ {α : Type u_1} {f : αBool}, List.any [] f = false
@[simp]
theorem List.any_cons :
∀ {α : Type u_1} {a : α} {l : List α} {f : αBool}, List.any (a :: l) f = (f a || List.any l f)
@[simp]
theorem List.all_nil :
∀ {α : Type u_1} {f : αBool}, List.all [] f = true
@[simp]
theorem List.all_cons :
∀ {α : Type u_1} {a : α} {l : List α} {f : αBool}, List.all (a :: l) f = (f a && List.all l f)
@[simp]
@[simp]
theorem List.or_cons {a : Bool} {l : List Bool} :
List.or (a :: l) = (a || List.or l)
@[simp]
@[simp]
theorem List.and_cons {a : Bool} {l : List Bool} :
List.and (a :: l) = (a && List.and l)

length #

theorem List.eq_nil_of_length_eq_zero :
∀ {α : Type u_1} {l : List α}, List.length l = 0l = []
theorem List.ne_nil_of_length_eq_succ :
∀ {α : Type u_1} {l : List α} {n : Nat}, List.length l = Nat.succ nl []
theorem List.length_eq_zero :
∀ {α : Type u_1} {l : List α}, List.length l = 0 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₂List.length s₁ = List.length s₂s₁ = s₂ t₁ = t₂
theorem List.append_inj_right :
∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂List.length s₁ = List.length s₂t₁ = t₂
theorem List.append_inj_left :
∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂List.length s₁ = List.length s₂s₁ = s₂
theorem List.append_inj' :
∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂List.length t₁ = List.length t₂s₁ = s₂ t₁ = t₂
theorem List.append_inj_right' :
∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂List.length t₁ = List.length t₂t₁ = t₂
theorem List.append_inj_left' :
∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂List.length t₁ = List.length t₂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₂

map #

theorem List.map_nil {α : Type u_1} {β : Type u_2} {f : αβ} :
List.map f [] = []
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_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 β) :
List.bind [] f = []
@[simp]
theorem List.cons_bind {α : Type u_1} {β : Type u_2} (x : α) (xs : List α) (f : αList β) :
List.bind (x :: xs) f = f x ++ List.bind xs f
@[simp]
theorem List.append_bind {α : Type u_1} {β : Type u_2} (xs : List α) (ys : List α) (f : αList β) :
List.bind (xs ++ ys) f = List.bind xs f ++ List.bind ys f
@[simp]
theorem List.bind_id {α : Type u_1} (l : List (List α)) :

bounded quantifiers over Lists #

theorem List.forall_mem_cons {α : Type u_1} {p : αProp} {a : α} {l : List α} :
((x : α) → x a :: lp x) p a ((x : α) → x lp x)

reverse #

theorem List.reverseAux_eq {α : Type u_1} (as : List α) (bs : List α) :
theorem List.reverse_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :

take and drop #

@[simp]
theorem List.take_append_drop {α : Type u_1} (n : Nat) (l : List α) :
@[simp]
theorem List.length_drop {α : Type u_1} (i : Nat) (l : List α) :
theorem List.drop_length_le {α : Type u_1} {i : Nat} {l : List α} (h : List.length l i) :
List.drop i l = []
theorem List.take_length_le {α : Type u_1} {i : Nat} {l : List α} (h : List.length l i) :
List.take i l = l
@[simp]
theorem List.drop_length {α : Type u_1} (l : List α) :
@[simp]
theorem List.take_length {α : Type u_1} (l : List α) :
theorem List.take_concat_get {α : Type u_1} (l : List α) (i : Nat) (h : i < List.length l) :
List.concat (List.take i l) l[i] = List.take (i + 1) l
theorem List.reverse_concat {α : Type u_1} (l : List α) (a : α) :
@[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 (List.reverse l) = List.foldrM (fun x y => f y x) b 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 (List.reverse l) = 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 α) :
theorem List.foldr_eq_foldrM {α : Type u_1} {β : Type u_2} (f : αββ) (b : β) (l : List α) :
@[simp]
theorem List.foldl_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : βαβ) (b : β) :
List.foldl f b (List.reverse l) = 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 (List.reverse l) = 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.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
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
Instances For
    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 α) :
    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 (List.reverse acc ++ __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)