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]
@[simp]
@[simp]
@[simp]
theorem
List.tailD_cons
{α : Type u_1}
{a : α}
{l : List α}
{l' : List α}
:
List.tailD (a :: l) l' = l
length #
append #
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_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₂
map #
bind #
bounded quantifiers over Lists #
reverse #
theorem
List.reverseAux_eq
{α : Type u_1}
(as : List α)
(bs : List α)
:
List.reverseAux as bs = List.reverse as ++ bs
theorem
List.reverse_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(l : List α)
:
List.reverse (List.map f l) = List.map f (List.reverse l)
take and drop #
@[simp]
theorem
List.length_drop
{α : Type u_1}
(i : Nat)
(l : List α)
:
List.length (List.drop i l) = List.length l - i
@[simp]
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 : α)
:
List.reverse (List.concat l a) = a :: List.reverse l
@[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 α)
:
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
@[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'
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
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 (List.reverse acc ++ __do_lift)