Some lemmas about lists involving sets #
Split out from Data.List.Basic to reduce its dependencies.
theorem
List.injOn_insertNth_index_of_not_mem
{α : Type u_1}
(l : List α)
(x : α)
(hx : x ∉ l)
:
Set.InjOn (fun (k : ℕ) => List.insertNth k x l) {n : ℕ | n ≤ List.length l}
theorem
List.foldr_range_subset_of_range_subset
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : β → α → α}
{g : γ → α → α}
(hfg : Set.range f ⊆ Set.range g)
(a : α)
:
Set.range (List.foldr f a) ⊆ Set.range (List.foldr g a)
theorem
List.foldl_range_subset_of_range_subset
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → α}
{g : α → γ → α}
(hfg : (Set.range fun (a : β) (c : α) => f c a) ⊆ Set.range fun (b : γ) (c : α) => g c b)
(a : α)
:
Set.range (List.foldl f a) ⊆ Set.range (List.foldl g a)
theorem
List.foldr_range_eq_of_range_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : β → α → α}
{g : γ → α → α}
(hfg : Set.range f = Set.range g)
(a : α)
:
Set.range (List.foldr f a) = Set.range (List.foldr g a)
theorem
List.foldl_range_eq_of_range_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → α}
{g : α → γ → α}
(hfg : (Set.range fun (a : β) (c : α) => f c a) = Set.range fun (b : γ) (c : α) => g c b)
(a : α)
:
Set.range (List.foldl f a) = Set.range (List.foldl g a)
MapAccumr and Foldr #
Some lemmas relation mapAccumr and foldr
theorem
List.mapAccumr_eq_foldr
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
(f : α → σ → σ × β)
(as : List α)
(s : σ)
:
List.mapAccumr f as s = List.foldr
(fun (a : α) (s : σ × List β) =>
let r := f a s.1;
(r.1, r.2 :: s.2))
(s, []) as
theorem
List.mapAccumr₂_eq_foldr
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
{φ : Type u_5}
(f : α → β → σ → σ × φ)
(as : List α)
(bs : List β)
(s : σ)
:
List.mapAccumr₂ f as bs s = List.foldr
(fun (ab : α × β) (s : σ × List φ) =>
let r := f ab.1 ab.2 s.1;
(r.1, r.2 :: s.2))
(s, []) (List.zip as bs)