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 =>
let r := f a s.fst;
(r.fst, r.snd :: s.snd))
(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 =>
let r := f ab.fst ab.snd s.fst;
(r.fst, r.snd :: s.snd))
(s, []) (List.zip as bs)