Streams a.k.a. infinite lists a.k.a. infinite sequences #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file used to be in the core library. It was moved to mathlib and renamed to init to avoid
name clashes.
@[protected, instance]
Equations
theorem
stream.tail_drop
{α : Type u}
(n : ℕ)
(s : stream α) :
(stream.drop n s).tail = stream.drop n s.tail
theorem
stream.nth_drop
{α : Type u}
(n m : ℕ)
(s : stream α) :
(stream.drop m s).nth n = s.nth (n + m)
theorem
stream.drop_drop
{α : Type u}
(n m : ℕ)
(s : stream α) :
stream.drop n (stream.drop m s) = stream.drop (n + m) s
theorem
stream.drop_succ
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.drop n.succ s = stream.drop n s.tail
@[simp]
theorem
stream.cons_injective_left
{α : Type u}
(s : stream α) :
function.injective (λ (x : α), x::s)
theorem
stream.all_def
{α : Type u}
(p : α → Prop)
(s : stream α) :
stream.all p s = ∀ (n : ℕ), p (s.nth n)
theorem
stream.drop_map
{α : Type u}
{β : Type v}
(f : α → β)
(n : ℕ)
(s : stream α) :
stream.drop n (stream.map f s) = stream.map f (stream.drop n s)
theorem
stream.tail_map
{α : Type u}
{β : Type v}
(f : α → β)
(s : stream α) :
(stream.map f s).tail = stream.map f s.tail
theorem
stream.head_map
{α : Type u}
{β : Type v}
(f : α → β)
(s : stream α) :
(stream.map f s).head = f s.head
theorem
stream.map_eq
{α : Type u}
{β : Type v}
(f : α → β)
(s : stream α) :
stream.map f s = f s.head::stream.map f s.tail
theorem
stream.map_cons
{α : Type u}
{β : Type v}
(f : α → β)
(a : α)
(s : stream α) :
stream.map f (a::s) = f a::stream.map f s
theorem
stream.map_map
{α : Type u}
{β : Type v}
{δ : Type w}
(g : β → δ)
(f : α → β)
(s : stream α) :
stream.map g (stream.map f s) = stream.map (g ∘ f) s
theorem
stream.map_tail
{α : Type u}
{β : Type v}
(f : α → β)
(s : stream α) :
stream.map f s.tail = (stream.map f s).tail
theorem
stream.mem_map
{α : Type u}
{β : Type v}
(f : α → β)
{a : α}
{s : stream α} :
a ∈ s → f a ∈ stream.map f s
theorem
stream.drop_zip
{α : Type u}
{β : Type v}
{δ : Type w}
(f : α → β → δ)
(n : ℕ)
(s₁ : stream α)
(s₂ : stream β) :
stream.drop n (stream.zip f s₁ s₂) = stream.zip f (stream.drop n s₁) (stream.drop n s₂)
theorem
stream.tail_zip
{α : Type u}
{β : Type v}
{δ : Type w}
(f : α → β → δ)
(s₁ : stream α)
(s₂ : stream β) :
(stream.zip f s₁ s₂).tail = stream.zip f s₁.tail s₂.tail
theorem
stream.map_const
{α : Type u}
{β : Type v}
(f : α → β)
(a : α) :
stream.map f (stream.const a) = stream.const (f a)
theorem
stream.drop_const
{α : Type u}
(n : ℕ)
(a : α) :
stream.drop n (stream.const a) = stream.const a
theorem
stream.tail_iterate
{α : Type u}
(f : α → α)
(a : α) :
(stream.iterate f a).tail = stream.iterate f (f a)
theorem
stream.iterate_eq
{α : Type u}
(f : α → α)
(a : α) :
stream.iterate f a = a::stream.iterate f (f a)
theorem
stream.nth_succ_iterate
{α : Type u}
(n : ℕ)
(f : α → α)
(a : α) :
(stream.iterate f a).nth n.succ = (stream.iterate f (f a)).nth n
theorem
stream.nth_of_bisim
{α : Type u}
(R : stream α → stream α → Prop)
(bisim : stream.is_bisimulation R)
{s₁ s₂ : stream α}
(n : ℕ) :
R s₁ s₂ → s₁.nth n = s₂.nth n ∧ R (stream.drop (n + 1) s₁) (stream.drop (n + 1) s₂)
theorem
stream.map_iterate
{α : Type u}
(f : α → α)
(a : α) :
stream.iterate f (f a) = stream.map f (stream.iterate f a)
theorem
stream.corec_def
{α : Type u}
{β : Type v}
(f : α → β)
(g : α → α)
(a : α) :
stream.corec f g a = stream.map f (stream.iterate g a)
theorem
stream.corec_eq
{α : Type u}
{β : Type v}
(f : α → β)
(g : α → α)
(a : α) :
stream.corec f g a = f a::stream.corec f g (g a)
theorem
stream.corec_id_f_eq_iterate
{α : Type u}
(f : α → α)
(a : α) :
stream.corec id f a = stream.iterate f a
theorem
stream.corec'_eq
{α : Type u}
{β : Type v}
(f : α → β × α)
(a : α) :
stream.corec' f a = (f a).fst::stream.corec' f (f a).snd
theorem
stream.unfolds_eq
{α : Type u}
{β : Type v}
(g : α → β)
(f : α → α)
(a : α) :
stream.unfolds g f a = g a::stream.unfolds g f (f a)
theorem
stream.nth_unfolds_head_tail
{α : Type u}
(n : ℕ)
(s : stream α) :
(stream.unfolds stream.head stream.tail s).nth n = s.nth n
theorem
stream.map_append_stream
{α : Type u}
{β : Type v}
(f : α → β)
(l : list α)
(s : stream α) :
stream.map f (l ++ₛ s) = list.map f l ++ₛ stream.map f s
theorem
stream.drop_append_stream
{α : Type u}
(l : list α)
(s : stream α) :
stream.drop l.length (l ++ₛ s) = s
@[simp]
theorem
stream.take_succ
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.take n.succ s = s.head :: stream.take n s.tail
@[simp]
theorem
stream.nth_take_succ
{α : Type u}
(n : ℕ)
(s : stream α) :
(stream.take n.succ s).nth n = option.some (s.nth n)
theorem
stream.append_take_drop
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.take n s ++ₛ stream.drop n s = s
theorem
stream.take_theorem
{α : Type u}
(s₁ s₂ : stream α) :
(∀ (n : ℕ), stream.take n s₁ = stream.take n s₂) → s₁ = s₂
@[protected]
theorem
stream.cycle_g_cons
{α : Type u}
(a a₁ : α)
(l₁ : list α)
(a₀ : α)
(l₀ : list α) :
stream.cycle_g (a, a₁ :: l₁, a₀, l₀) = (a₁, l₁, a₀, l₀)
theorem
stream.cycle_eq
{α : Type u}
(l : list α)
(h : l ≠ list.nil) :
stream.cycle l h = l ++ₛ stream.cycle l h
theorem
stream.mem_cycle
{α : Type u}
{a : α}
{l : list α}
(h : l ≠ list.nil) :
a ∈ l → a ∈ stream.cycle l h
theorem
stream.cycle_singleton
{α : Type u}
(a : α)
(h : [a] ≠ list.nil) :
stream.cycle [a] h = stream.const a
theorem
stream.inits_core_eq
{α : Type u}
(l : list α)
(s : stream α) :
stream.inits_core l s = l::stream.inits_core (l ++ [s.head]) s.tail
theorem
stream.cons_nth_inits_core
{α : Type u}
(a : α)
(n : ℕ)
(l : list α)
(s : stream α) :
a :: (stream.inits_core l s).nth n = (stream.inits_core (a :: l) s).nth n
theorem
stream.homomorphism
{α : Type u}
{β : Type v}
(f : α → β)
(a : α) :
stream.pure f ⊛ stream.pure a = stream.pure (f a)
theorem
stream.interchange
{α : Type u}
{β : Type v}
(fs : stream (α → β))
(a : α) :
fs ⊛ stream.pure a = stream.pure (λ (f : α → β), f a) ⊛ fs
theorem
stream.map_eq_apply
{α : Type u}
{β : Type v}
(f : α → β)
(s : stream α) :
stream.map f s = stream.pure f ⊛ s