Lemmas about list.*_with_index functions. #
Some specification lemmas for list.map_with_index
, list.mmap_with_index
, list.foldl_with_index
and list.foldr_with_index
.
@[simp]
theorem
list.map_with_index_core_eq
{α : Type u}
{β : Type v}
(l : list α)
(f : ℕ → α → β)
(n : ℕ) :
list.map_with_index_core f n l = list.map_with_index (λ (i : ℕ) (a : α), f (i + n) a) l
theorem
list.map_with_index_eq_enum_map
{α : Type u}
{β : Type v}
(l : list α)
(f : ℕ → α → β) :
list.map_with_index f l = list.map (function.uncurry f) l.enum
@[simp]
theorem
list.map_with_index_cons
{α : Type u_1}
{β : Type u_2}
(l : list α)
(f : ℕ → α → β)
(a : α) :
list.map_with_index f (a :: l) = f 0 a :: list.map_with_index (λ (i : ℕ), f (i + 1)) l
@[simp]
theorem
list.length_map_with_index
{α : Type u_1}
{β : Type u_2}
(l : list α)
(f : ℕ → α → β) :
(list.map_with_index f l).length = l.length
@[simp]
theorem
list.nth_le_map_with_index
{α : Type u_1}
{β : Type u_2}
(l : list α)
(f : ℕ → α → β)
(i : ℕ)
(h : i < l.length)
(h' : i < (list.map_with_index f l).length := _) :
(list.map_with_index f l).nth_le i h' = f i (l.nth_le i h)
theorem
list.map_with_index_eq_of_fn
{α : Type u_1}
{β : Type u_2}
(l : list α)
(f : ℕ → α → β) :
list.map_with_index f l = list.of_fn (λ (i : fin l.length), f ↑i (l.nth_le ↑i _))
def
list.foldr_with_index_aux_spec
{α : Type u}
{β : Type v}
(f : ℕ → α → β → β)
(start : ℕ)
(b : β)
(as : list α) :
β
Specification of foldr_with_index_aux
.
Equations
- list.foldr_with_index_aux_spec f start b as = list.foldr (function.uncurry f) b (list.enum_from start as)
theorem
list.foldr_with_index_aux_spec_cons
{α : Type u}
{β : Type v}
(f : ℕ → α → β → β)
(start : ℕ)
(b : β)
(a : α)
(as : list α) :
list.foldr_with_index_aux_spec f start b (a :: as) = f start a (list.foldr_with_index_aux_spec f (start + 1) b as)
theorem
list.foldr_with_index_aux_eq_foldr_with_index_aux_spec
{α : Type u}
{β : Type v}
(f : ℕ → α → β → β)
(start : ℕ)
(b : β)
(as : list α) :
list.foldr_with_index_aux f start b as = list.foldr_with_index_aux_spec f start b as
theorem
list.foldr_with_index_eq_foldr_enum
{α : Type u}
{β : Type v}
(f : ℕ → α → β → β)
(b : β)
(as : list α) :
list.foldr_with_index f b as = list.foldr (function.uncurry f) b as.enum
theorem
list.indexes_values_eq_filter_enum
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(as : list α) :
list.indexes_values p as = list.filter (p ∘ prod.snd) as.enum
theorem
list.find_indexes_eq_map_indexes_values
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(as : list α) :
list.find_indexes p as = list.map prod.fst (list.indexes_values p as)
def
list.foldl_with_index_aux_spec
{α : Type u}
{β : Type v}
(f : ℕ → α → β → α)
(start : ℕ)
(a : α)
(bs : list β) :
α
Specification of foldl_with_index_aux
.
Equations
- list.foldl_with_index_aux_spec f start a bs = list.foldl (λ (a : α) (p : ℕ × β), f p.fst a p.snd) a (list.enum_from start bs)
theorem
list.foldl_with_index_aux_spec_cons
{α : Type u}
{β : Type v}
(f : ℕ → α → β → α)
(start : ℕ)
(a : α)
(b : β)
(bs : list β) :
list.foldl_with_index_aux_spec f start a (b :: bs) = list.foldl_with_index_aux_spec f (start + 1) (f start a b) bs
theorem
list.foldl_with_index_aux_eq_foldl_with_index_aux_spec
{α : Type u}
{β : Type v}
(f : ℕ → α → β → α)
(start : ℕ)
(a : α)
(bs : list β) :
list.foldl_with_index_aux f start a bs = list.foldl_with_index_aux_spec f start a bs
theorem
list.foldl_with_index_eq_foldl_enum
{α : Type u}
{β : Type v}
(f : ℕ → α → β → α)
(a : α)
(bs : list β) :
list.foldl_with_index f a bs = list.foldl (λ (a : α) (p : ℕ × β), f p.fst a p.snd) a bs.enum
theorem
list.mfoldr_with_index_eq_mfoldr_enum
{m : Type u → Type v}
[monad m]
{α : Type u_1}
{β : Type u}
(f : ℕ → α → β → m β)
(b : β)
(as : list α) :
list.mfoldr_with_index f b as = list.mfoldr (function.uncurry f) b as.enum
theorem
list.mfoldl_with_index_eq_mfoldl_enum
{m : Type u → Type v}
[monad m]
[is_lawful_monad m]
{α : Type u_1}
{β : Type u}
(f : ℕ → β → α → m β)
(b : β)
(as : list α) :
list.mfoldl_with_index f b as = list.mfoldl (λ (b : β) (p : ℕ × α), f p.fst b p.snd) b as.enum
def
list.mmap_with_index_aux_spec
{m : Type u → Type v}
[applicative m]
{α : Type u_1}
{β : Type u}
(f : ℕ → α → m β)
(start : ℕ)
(as : list α) :
m (list β)
Specification of mmap_with_index_aux
.
Equations
- list.mmap_with_index_aux_spec f start as = list.traverse (function.uncurry f) (list.enum_from start as)
theorem
list.mmap_with_index_aux_spec_cons
{m : Type u → Type v}
[applicative m]
{α : Type u_1}
{β : Type u}
(f : ℕ → α → m β)
(start : ℕ)
(a : α)
(as : list α) :
list.mmap_with_index_aux_spec f start (a :: as) = list.cons <$> f start a <*> list.mmap_with_index_aux_spec f (start + 1) as
theorem
list.mmap_with_index_aux_eq_mmap_with_index_aux_spec
{m : Type u → Type v}
[applicative m]
{α : Type u_1}
{β : Type u}
(f : ℕ → α → m β)
(start : ℕ)
(as : list α) :
list.mmap_with_index_aux f start as = list.mmap_with_index_aux_spec f start as
theorem
list.mmap_with_index_eq_mmap_enum
{m : Type u → Type v}
[applicative m]
{α : Type u_1}
{β : Type u}
(f : ℕ → α → m β)
(as : list α) :
list.mmap_with_index f as = list.traverse (function.uncurry f) as.enum
theorem
list.mmap_with_index'_aux_eq_mmap_with_index_aux
{m : Type u → Type v}
[applicative m]
[is_lawful_applicative m]
{α : Type u_1}
(f : ℕ → α → m punit)
(start : ℕ)
(as : list α) :
list.mmap_with_index'_aux f start as = list.mmap_with_index_aux f start as *> has_pure.pure punit.star
theorem
list.mmap_with_index'_eq_mmap_with_index
{m : Type u → Type v}
[applicative m]
[is_lawful_applicative m]
{α : Type u_1}
(f : ℕ → α → m punit)
(as : list α) :
list.mmap_with_index' f as = list.mmap_with_index f as *> has_pure.pure punit.star