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.
length #
mem #
append #
map #
bind #
join #
bounded quantifiers over Lists #
reverse #
nth element #
@[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)
take and drop #
takeWhile and dropWhile #
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.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 #
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
@[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)
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
eraseIdx #
find? #
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_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
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 #
elem #
lookup #
@[simp]
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
zipWithAll #
zip #
unzip #
all / any #
enumFrom #
@[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 #
intersperse #
@[simp]
@[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 #
isEqv #
dropLast #
minimum? #
theorem
List.minimum?_cons
{α : Type u_1}
{x : α}
[Min α]
{xs : List α}
:
(x :: xs).minimum? = some (List.foldl min x xs)