Basic properties of Lists #
length #
theorem
List.length_pos_iff_exists_mem
{α : Type u_1}
{l : List α}
:
0 < List.length l ↔ ∃ a, a ∈ l
mem #
append #
map #
@[simp]
theorem
List.length_zipWith
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(l₁ : List α)
(l₂ : List β)
:
List.length (List.zipWith f l₁ l₂) = min (List.length l₁) (List.length l₂)
join #
bind #
set-theoretic notation of Lists #
bounded quantifiers over Lists #
List subset #
replicate #
theorem
List.replicate_succ
{α : Type u_1}
(a : α)
(n : Nat)
:
List.replicate (n + 1) a = a :: List.replicate n a
theorem
List.eq_of_mem_replicate
{α : Type u_1}
{a : α}
{b : α}
{n : Nat}
(h : b ∈ List.replicate n a)
:
b = a
getLast #
theorem
List.getLast_cons'
{α : Type u_1}
{a : α}
{l : List α}
(h₁ : a :: l ≠ [])
(h₂ : l ≠ [])
:
List.getLast (a :: l) h₁ = List.getLast l h₂
@[simp]
theorem
List.getLast_append
{α : Type u_1}
{a : α}
(l : List α)
(h : l ++ [a] ≠ [])
:
List.getLast (l ++ [a]) h = a
theorem
List.getLast_concat :
∀ {α : Type u_1} {l : List α} {a : α} (h : List.concat l a ≠ []), List.getLast (List.concat l a) h = a
sublists #
theorem
List.Sublist.trans
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{l₃ : List α}
(h₁ : List.Sublist l₁ l₂)
(h₂ : List.Sublist l₂ l₃)
:
List.Sublist l₁ l₃
Equations
- List.instTransListSublist = { trans := (_ : ∀ {a b c : List α}, List.Sublist a b → List.Sublist b c → List.Sublist a c) }
@[simp]
theorem
List.sublist_of_cons_sublist :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, List.Sublist (a :: l₁) l₂ → List.Sublist l₁ l₂
@[simp]
theorem
List.sublist_append_left
{α : Type u_1}
(l₁ : List α)
(l₂ : List α)
:
List.Sublist l₁ (l₁ ++ l₂)
@[simp]
theorem
List.sublist_append_right
{α : Type u_1}
(l₁ : List α)
(l₂ : List α)
:
List.Sublist l₂ (l₁ ++ l₂)
theorem
List.sublist_append_of_sublist_left :
∀ {α : Type u_1} {l l₁ l₂ : List α}, List.Sublist l l₁ → List.Sublist l (l₁ ++ l₂)
theorem
List.sublist_append_of_sublist_right :
∀ {α : Type u_1} {l l₂ l₁ : List α}, List.Sublist l l₂ → List.Sublist l (l₁ ++ l₂)
theorem
List.cons_sublist_cons :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, List.Sublist (a :: l₁) (a :: l₂) ↔ List.Sublist l₁ l₂
@[simp]
theorem
List.append_sublist_append_left :
∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), List.Sublist (l ++ l₁) (l ++ l₂) ↔ List.Sublist l₁ l₂
theorem
List.Sublist.append_right :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist l₁ l₂ → ∀ (l : List α), List.Sublist (l₁ ++ l) (l₂ ++ l)
theorem
List.sublist_or_mem_of_sublist :
∀ {α : Type u_1} {l l₁ : List α} {a : α} {l₂ : List α},
List.Sublist l (l₁ ++ a :: l₂) → List.Sublist l (l₁ ++ l₂) ∨ a ∈ l
theorem
List.Sublist.reverse :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist l₁ l₂ → List.Sublist (List.reverse l₁) (List.reverse l₂)
@[simp]
theorem
List.reverse_sublist :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist (List.reverse l₁) (List.reverse l₂) ↔ List.Sublist l₁ l₂
@[simp]
theorem
List.append_sublist_append_right :
∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), List.Sublist (l₁ ++ l) (l₂ ++ l) ↔ List.Sublist l₁ l₂
theorem
List.Sublist.append :
∀ {α : Type u_1} {l₁ l₂ r₁ r₂ : List α}, List.Sublist l₁ l₂ → List.Sublist r₁ r₂ → List.Sublist (l₁ ++ r₁) (l₂ ++ r₂)
theorem
List.Sublist.subset
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
:
List.Sublist l₁ l₂ → l₁ ⊆ l₂
theorem
List.Sublist.length_le :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist l₁ l₂ → List.length l₁ ≤ List.length l₂
head #
theorem
List.head!_of_head?
{α : Type u_1}
{a : α}
[inst : Inhabited α]
{l : List α}
:
List.head? l = some a → List.head! l = a
theorem
List.head?_eq_head
{α : Type u_1}
(l : List α)
(h : l ≠ [])
:
List.head? l = some (List.head l h)
tail #
@[simp]
theorem
List.tailD_eq_tail?
{α : Type u_1}
(l : List α)
(l' : List α)
:
List.tailD l l' = Option.getD (List.tail? l) l'
next? #
@[simp]
getLast #
@[simp]
theorem
List.getLastD_cons
{α : Type u_1}
(a : α)
(b : α)
(l : List α)
:
List.getLastD (b :: l) a = List.getLastD l b
theorem
List.getLast_eq_getLastD
{α : Type u_1}
(a : α)
(l : List α)
(h : a :: l ≠ [])
:
List.getLast (a :: l) h = List.getLastD l a
theorem
List.getLast!_cons
{α : Type u_1}
{a : α}
{l : List α}
[inst : Inhabited α]
:
List.getLast! (a :: l) = List.getLastD l a
theorem
List.getLast?_cons
{α : Type u_1}
{a : α}
{l : List α}
:
List.getLast? (a :: l) = some (List.getLastD l a)
theorem
List.getLast?_eq_getLast
{α : Type u_1}
(l : List α)
(h : l ≠ [])
:
List.getLast? l = some (List.getLast l h)
dropLast #
@[simp]
theorem
List.dropLast_cons₂ :
∀ {α : Type u_1} {a b : α} {l : List α}, List.dropLast (a :: b :: l) = a :: List.dropLast (b :: l)
@[simp]
theorem
List.dropLast_append_cons :
∀ {α : Type u_1} {l₁ : List α} {b : α} {l₂ : List α}, List.dropLast (l₁ ++ b :: l₂) = l₁ ++ List.dropLast (b :: l₂)
@[simp]
theorem
List.dropLast_concat :
∀ {α : Type u_1} {l₁ : List α} {b : α}, List.dropLast (l₁ ++ [b]) = l₁
nth element #
theorem
List.get?_len_le
{α : Type u_1}
{l : List α}
{n : Nat}
:
List.length l ≤ n → List.get? l n = none
@[simp]
theorem
List.get?_inj
{i : Nat}
:
∀ {α : Type u_1} {xs : List α} {j : Nat}, i < List.length xs → List.Nodup xs → List.get? xs i = List.get? xs j → i = j
@[simp]
theorem
List.get_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
{l : List α}
{n : Fin (List.length (List.map f l))}
:
theorem
List.get_of_eq
{α : Type u_1}
{l : List α}
{l' : List α}
(h : l = l')
(i : Fin (List.length l))
:
List.get l i = List.get l' { val := i.val, isLt := (_ : i.val < List.length l') }
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)
.
theorem
List.get_zero
{α : Type u_1}
{l : List α}
(h : 0 < List.length l)
:
some (List.get l { val := 0, isLt := h }) = List.head? l
theorem
List.get?_append_right
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{n : Nat}
:
List.length l₁ ≤ n → List.get? (l₁ ++ l₂) n = List.get? l₂ (n - List.length l₁)
theorem
List.get_append_right_aux
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{n : Nat}
(h₁ : List.length l₁ ≤ n)
(h₂ : n < List.length (l₁ ++ l₂))
:
n - List.length l₁ < List.length l₂
theorem
List.get_append_right'
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{n : Nat}
(h₁ : List.length l₁ ≤ n)
(h₂ : n < List.length (l₁ ++ l₂))
:
List.get (l₁ ++ l₂) { val := n, isLt := h₂ } = List.get l₂ { val := n - List.length l₁, isLt := (_ : n - List.length l₁ < List.length l₂) }
theorem
List.get_of_append_proof
{α : Type u_1}
{l₁ : List α}
{a : α}
{l₂ : List α}
{n : Nat}
{l : List α}
(eq : l = l₁ ++ a :: l₂)
(h : List.length l₁ = n)
:
n < List.length l
@[simp]
theorem
List.get_replicate
{α : Type u_1}
(a : α)
{n : Nat}
(m : Fin (List.length (List.replicate n a)))
:
List.get (List.replicate n a) m = a
theorem
List.getLast_eq_get
{α : Type u_1}
(l : List α)
(h : l ≠ [])
:
List.getLast l h = List.get l { val := List.length l - 1, isLt := (_ : List.length l - 1 < List.length l) }
theorem
List.getLast?_eq_get?
{α : Type u_1}
(l : List α)
:
List.getLast? l = List.get? l (List.length l - 1)
@[simp]
theorem
List.get?_concat_length
{α : Type u_1}
(l : List α)
(a : α)
:
List.get? (l ++ [a]) (List.length l) = some a
@[simp]
theorem
List.get_cons_length
{α : Type u_1}
(x : α)
(xs : List α)
(n : Nat)
(h : n = List.length xs)
:
List.get (x :: xs) { val := n, isLt := (_ : n < Nat.succ (List.length xs)) } = List.getLast (x :: xs) (_ : x :: xs ≠ [])
theorem
List.ext_get
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
(hl : List.length l₁ = List.length l₂)
(h : ∀ (n : Nat) (h₁ : n < List.length l₁) (h₂ : n < List.length l₂),
List.get l₁ { val := n, isLt := h₁ } = List.get l₂ { val := n, isLt := h₂ })
:
l₁ = l₂
theorem
List.get?_reverse'
{α : Type u_1}
{l : List α}
(i : Nat)
(j : Nat)
:
i + j + 1 = List.length l → List.get? (List.reverse l) i = List.get? l j
theorem
List.get?_reverse
{α : Type u_1}
{l : List α}
(i : Nat)
(h : i < List.length l)
:
List.get? (List.reverse l) i = List.get? l (List.length l - 1 - i)
theorem
List.getD_eq_get?
{α : Type u_1}
(l : List α)
(n : Nat)
(a : α)
:
List.getD l n a = Option.getD (List.get? l n) a
take and drop #
@[simp]
theorem
List.length_take
{α : Type u_1}
(i : Nat)
(l : List α)
:
List.length (List.take i l) = min i (List.length l)
theorem
List.length_take_of_le
{n : Nat}
:
∀ {α : Type u_1} {l : List α}, n ≤ List.length l → List.length (List.take n l) = n
modify nth #
theorem
List.removeNth_eq_nth_tail
{α : Type u_1}
(n : Nat)
(l : List α)
:
List.removeNth l n = List.modifyNthTail List.tail n l
theorem
List.modifyNthTail_length
{α : Type u_1}
(f : List α → List α)
(H : ∀ (l : List α), List.length (f l) = List.length l)
(n : Nat)
(l : List α)
:
List.length (List.modifyNthTail f n l) = List.length l
theorem
List.modifyNthTail_add
{α : Type u_1}
(f : List α → List α)
(n : Nat)
(l₁ : List α)
(l₂ : List α)
:
List.modifyNthTail f (List.length l₁ + n) (l₁ ++ l₂) = l₁ ++ List.modifyNthTail f n l₂
theorem
List.exists_of_modifyNthTail
{α : Type u_1}
(f : List α → List α)
{n : Nat}
{l : List α}
(h : n ≤ List.length l)
:
∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.length l₁ = n ∧ List.modifyNthTail f n l = l₁ ++ f l₂
@[simp]
theorem
List.modify_get?_length
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
List.length (List.modifyNth f n l) = List.length l
theorem
List.exists_of_modifyNth
{α : Type u_1}
(f : α → α)
{n : Nat}
{l : List α}
(h : n < List.length l)
:
set #
theorem
List.set_eq_modifyNth
{α : Type u_1}
(a : α)
(n : Nat)
(l : List α)
:
List.set l n a = List.modifyNth (fun x => a) n l
theorem
List.modifyNth_eq_set_get?
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
List.modifyNth f n l = Option.getD ((fun a => List.set l n (f a)) <$> List.get? l n) l
theorem
List.modifyNth_eq_set_get
{α : Type u_1}
(f : α → α)
{n : Nat}
{l : List α}
(h : n < List.length l)
:
List.modifyNth f n l = List.set l n (f (List.get l { val := n, isLt := h }))
remove nth #
theorem
List.length_removeNth
{α : Type u_1}
{l : List α}
{i : Nat}
:
i < List.length l → List.length (List.removeNth l i) = List.length l - 1
tail #
@[simp]
all / any #
reverse #
@[simp]
insert #
@[simp]
theorem
List.insert_of_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : a ∈ l)
:
List.insert a l = l
@[simp]
theorem
List.insert_of_not_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : ¬a ∈ l)
:
List.insert a l = a :: l
@[simp]
@[simp]
theorem
List.mem_insert_self
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l : List α)
:
a ∈ List.insert a l
theorem
List.mem_insert_of_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{b : α}
{l : List α}
(h : a ∈ l)
:
a ∈ List.insert b l
theorem
List.eq_or_mem_of_mem_insert
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{b : α}
{l : List α}
(h : a ∈ List.insert b l)
:
@[simp]
theorem
List.length_insert_of_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : a ∈ l)
:
List.length (List.insert a l) = List.length l
@[simp]
theorem
List.length_insert_of_not_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : ¬a ∈ l)
:
List.length (List.insert a l) = List.length l + 1
eraseP #
theorem
List.eraseP_cons
{α : Type u_1}
{p : α → Bool}
(a : α)
(l : List α)
:
List.eraseP p (a :: l) = bif p a then l else a :: List.eraseP p l
@[simp]
theorem
List.eraseP_cons_of_neg
{α : Type u_1}
{a : α}
{l : List α}
(p : α → Bool)
(h : ¬p a = true)
:
List.eraseP p (a :: l) = a :: List.eraseP p l
@[simp]
theorem
List.length_eraseP_of_mem :
∀ {α : Type u_1} {a : α} {l : List α} {p : α → Bool},
a ∈ l → p a = true → List.length (List.eraseP p l) = Nat.pred (List.length l)
theorem
List.eraseP_append_left
{α : Type u_1}
{p : α → Bool}
{a : α}
(pa : p a = true)
{l₁ : List α}
(l₂ : List α)
:
a ∈ l₁ → List.eraseP p (l₁ ++ l₂) = List.eraseP p l₁ ++ l₂
theorem
List.eraseP_sublist
{α : Type u_1}
{p : α → Bool}
(l : List α)
:
List.Sublist (List.eraseP p l) l
theorem
List.Sublist.eraseP
{α : Type u_1}
{p : α → Bool}
{l₁ : List α}
{l₂ : List α}
:
List.Sublist l₁ l₂ → List.Sublist (List.eraseP p l₁) (List.eraseP p l₂)
theorem
List.mem_of_mem_eraseP
{α : Type u_1}
{a : α}
{p : α → Bool}
{l : List α}
:
a ∈ List.eraseP p l → a ∈ l
theorem
List.eraseP_map
{β : Type u_1}
{α : Type u_2}
{p : α → Bool}
(f : β → α)
(l : List β)
:
List.eraseP p (List.map f l) = List.map f (List.eraseP (p ∘ f) l)
@[simp]
theorem
List.extractP_eq_find?_eraseP
{α : Type u_1}
{p : α → Bool}
(l : List α)
:
List.extractP p l = (List.find? p l, List.eraseP p l)
theorem
List.extractP_eq_find?_eraseP.go
{α : Type u_1}
{p : α → Bool}
(l : List α)
(acc : Array α)
(xs : List α)
:
l = acc.data ++ xs → List.extractP.go p l xs acc = (List.find? p xs, acc.data ++ List.eraseP p xs)
erase #
@[simp]
theorem
List.erase_cons
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
List.erase (b :: l) a = if b = a then l else b :: List.erase l a
@[simp]
theorem
List.erase_cons_head
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l : List α)
:
List.erase (a :: l) a = l
@[simp]
theorem
List.erase_cons_tail
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{b : α}
(l : List α)
(h : b ≠ a)
:
List.erase (b :: l) a = b :: List.erase l a
theorem
List.erase_eq_eraseP
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l : List α)
:
List.erase l a = List.eraseP (fun b => decide (a = b)) l
theorem
List.erase_of_not_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l : List α}
:
¬a ∈ l → List.erase l a = l
@[simp]
theorem
List.length_erase_of_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : a ∈ l)
:
List.length (List.erase l a) = Nat.pred (List.length l)
theorem
List.erase_append_left
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l₁ : List α}
(l₂ : List α)
(h : a ∈ l₁)
:
List.erase (l₁ ++ l₂) a = List.erase l₁ a ++ l₂
theorem
List.erase_append_right
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l₁ : List α}
(l₂ : List α)
(h : ¬a ∈ l₁)
:
List.erase (l₁ ++ l₂) a = l₁ ++ List.erase l₂ a
theorem
List.erase_sublist
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l : List α)
:
List.Sublist (List.erase l a) l
theorem
List.erase_subset
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l : List α)
:
List.erase l a ⊆ l
theorem
List.sublist.erase
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
{l₁ : List α}
{l₂ : List α}
(h : List.Sublist l₁ l₂)
:
List.Sublist (List.erase l₁ a) (List.erase l₂ a)
theorem
List.mem_of_mem_erase
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{b : α}
{l : List α}
(h : a ∈ List.erase l b)
:
a ∈ l
@[simp]
theorem
List.mem_erase_of_ne
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{b : α}
{l : List α}
(ab : a ≠ b)
:
a ∈ List.erase l b ↔ a ∈ l
theorem
List.erase_comm
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
List.erase (List.erase l a) b = List.erase (List.erase l b) a
filter and partition #
@[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)
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) = (List.reverse as ++ List.filter p l, List.reverse bs ++ List.filter (not ∘ p) l)
pairwise #
theorem
List.Pairwise.sublist :
∀ {α : Type u_1} {l₁ l₂ : List α} {R : α → α → Prop}, List.Sublist l₁ l₂ → List.Pairwise R l₂ → List.Pairwise R l₁
theorem
List.pairwise_map
{α : Type u_1}
:
∀ {α : Type u_2} {f : α → α} {R : α → α → Prop} {l : List α},
List.Pairwise R (List.map f l) ↔ List.Pairwise (fun a b => R (f a) (f b)) l
theorem
List.pairwise_append
{α : Type u_1}
{R : α → α → Prop}
{l₁ : List α}
{l₂ : List α}
:
List.Pairwise R (l₁ ++ l₂) ↔ List.Pairwise R l₁ ∧ List.Pairwise R l₂ ∧ ((a : α) → a ∈ l₁ → (b : α) → b ∈ l₂ → R a b)
theorem
List.pairwise_reverse
{α : Type u_1}
{R : α → α → Prop}
{l : List α}
:
List.Pairwise R (List.reverse l) ↔ List.Pairwise (fun a b => R b a) l
theorem
List.Pairwise.imp
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
(H : {a b : α} → R a b → S a b)
{l : List α}
:
List.Pairwise R l → List.Pairwise S l
replaceF #
@[simp]
theorem
List.length_replaceF :
∀ {α : Type u_1} {f : α → Option α} {l : List α}, List.length (List.replaceF f l) = List.length l
disjoint #
theorem
List.disjoint_symm :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Disjoint l₁ l₂ → List.Disjoint l₂ l₁
theorem
List.disjoint_comm :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Disjoint l₁ l₂ ↔ List.Disjoint l₂ l₁
theorem
List.disjoint_of_subset_left :
∀ {α : Type u_1} {l₁ l l₂ : List α}, l₁ ⊆ l → List.Disjoint l l₂ → List.Disjoint l₁ l₂
theorem
List.disjoint_of_subset_right :
∀ {α : Type u_1} {l₂ l l₁ : List α}, l₂ ⊆ l → List.Disjoint l₁ l → List.Disjoint l₁ l₂
theorem
List.disjoint_of_disjoint_cons_left :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, List.Disjoint (a :: l₁) l₂ → List.Disjoint l₁ l₂
theorem
List.disjoint_of_disjoint_cons_right :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, List.Disjoint l₁ (a :: l₂) → List.Disjoint l₁ l₂
@[simp]
@[simp]
@[simp]
theorem
List.disjoint_append_left :
∀ {α : Type u_1} {l₁ l₂ l : List α}, List.Disjoint (l₁ ++ l₂) l ↔ List.Disjoint l₁ l ∧ List.Disjoint l₂ l
@[simp]
theorem
List.disjoint_append_right :
∀ {α : Type u_1} {l l₁ l₂ : List α}, List.Disjoint l (l₁ ++ l₂) ↔ List.Disjoint l l₁ ∧ List.Disjoint l l₂
@[simp]
theorem
List.disjoint_cons_left :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, List.Disjoint (a :: l₁) l₂ ↔ ¬a ∈ l₂ ∧ List.Disjoint l₁ l₂
@[simp]
theorem
List.disjoint_cons_right :
∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, List.Disjoint l₁ (a :: l₂) ↔ ¬a ∈ l₁ ∧ List.Disjoint l₁ l₂
theorem
List.disjoint_of_disjoint_append_left_left :
∀ {α : Type u_1} {l₁ l₂ l : List α}, List.Disjoint (l₁ ++ l₂) l → List.Disjoint l₁ l
theorem
List.disjoint_of_disjoint_append_left_right :
∀ {α : Type u_1} {l₁ l₂ l : List α}, List.Disjoint (l₁ ++ l₂) l → List.Disjoint l₂ l
theorem
List.disjoint_of_disjoint_append_right_left :
∀ {α : Type u_1} {l l₁ l₂ : List α}, List.Disjoint l (l₁ ++ l₂) → List.Disjoint l l₁
theorem
List.disjoint_of_disjoint_append_right_right :
∀ {α : Type u_1} {l l₁ l₂ : List α}, List.Disjoint l (l₁ ++ l₂) → List.Disjoint l l₂
theorem
List.disjoint_take_drop
{α : Type u_1}
{m : Nat}
{n : Nat}
{l : List α}
:
List.Nodup l → m ≤ n → List.Disjoint (List.take m l) (List.drop n l)
foldl / foldr #
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
theorem
List.foldl_hom
{α₁ : Type u_1}
{α₂ : Type u_2}
{β : Type u_3}
(f : α₁ → α₂)
(g₁ : α₁ → β → α₁)
(g₂ : α₂ → β → α₂)
(l : List β)
(init : α₁)
(H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y))
:
List.foldl g₂ (f init) l = f (List.foldl g₁ init l)
theorem
List.foldr_hom
{β₁ : Type u_1}
{β₂ : Type u_2}
{α : Type u_3}
(f : β₁ → β₂)
(g₁ : α → β₁ → β₁)
(g₂ : α → β₂ → β₂)
(l : List α)
(init : β₁)
(H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y))
:
List.foldr g₂ (f init) l = f (List.foldr g₁ init l)
union #
@[simp]
@[simp]
theorem
List.cons_union
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l₁ : List α)
(l₂ : List α)
:
List.union (a :: l₁) l₂ = List.insert a (List.union l₁ l₂)
@[simp]
theorem
List.mem_union_iff
{α : Type u_1}
[inst : DecidableEq α]
{x : α}
{l₁ : List α}
{l₂ : List α}
:
inter #
@[simp]
theorem
List.mem_inter_iff
{α : Type u_1}
[inst : DecidableEq α]
{x : α}
{l₁ : List α}
{l₂ : List α}
:
product #
leftpad #
theorem
List.leftpad_length
{α : Type u_1}
(n : Nat)
(a : α)
(l : List α)
:
List.length (List.leftpad n a l) = max n (List.length l)
The length of the List returned by List.leftpad n a l
is equal
to the larger of n
and l.length
theorem
List.leftpad_prefix
{α : Type u_1}
(n : Nat)
(a : α)
(l : List α)
:
List.replicate (n - List.length l) a <+: List.leftpad n a l
theorem
List.leftpad_suffix
{α : Type u_1}
(n : Nat)
(a : α)
(l : List α)
:
l <:+ List.leftpad n a l
monadic operations #
theorem
List.forIn_eq_bindList
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(f : α → β → m (ForInStep β))
(l : List α)
(init : β)
:
forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)