Equations
- stream.drop n s = λ (i : ℕ), s (i + n)
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.nth n (stream.drop m s) = stream.nth (n + m) s
theorem
stream.drop_drop
{α : Type u}
(n m : ℕ)
(s : stream α) :
stream.drop n (stream.drop m s) = stream.drop (n + m) s
theorem
stream.nth_succ
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.nth n.succ s = stream.nth n s.tail
theorem
stream.drop_succ
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.drop n.succ s = stream.drop n s.tail
@[ext]
theorem
stream.ext
{α : Type u}
{s₁ s₂ : stream α} :
(∀ (n : ℕ), stream.nth n s₁ = stream.nth n s₂) → s₁ = s₂
Equations
- stream.all p s = ∀ (n : ℕ), p (stream.nth n s)
Equations
- stream.any p s = ∃ (n : ℕ), p (stream.nth n s)
theorem
stream.all_def
{α : Type u}
(p : α → Prop)
(s : stream α) :
stream.all p s = ∀ (n : ℕ), p (stream.nth n s)
theorem
stream.any_def
{α : Type u}
(p : α → Prop)
(s : stream α) :
stream.any p s = ∃ (n : ℕ), p (stream.nth n s)
Equations
- stream.mem a s = stream.any (λ (b : α), a = b) s
@[instance]
Equations
- stream.has_mem = {mem := stream.mem α}
theorem
stream.mem_of_nth_eq
{α : Type u}
{n : ℕ}
{s : stream α}
{a : α} :
a = stream.nth n s → a ∈ s
Equations
- stream.map f s = λ (n : ℕ), f (stream.nth n s)
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.nth_map
{α : Type u}
{β : Type v}
(f : α → β)
(n : ℕ)
(s : stream α) :
stream.nth n (stream.map f s) = f (stream.nth 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.exists_of_mem_map
{α : Type u}
{β : Type v}
{f : α → β}
{b : β}
{s : stream α} :
b ∈ stream.map f s → (∃ (a : α), a ∈ s ∧ f a = b)
Equations
- stream.zip f s₁ s₂ = λ (n : ℕ), f (stream.nth n s₁) (stream.nth n 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.nth_zip
{α : Type u}
{β : Type v}
{δ : Type w}
(f : α → β → δ)
(n : ℕ)
(s₁ : stream α)
(s₂ : stream β) :
stream.nth n (stream.zip f s₁ s₂) = f (stream.nth n s₁) (stream.nth n s₂)
theorem
stream.head_zip
{α : Type u}
{β : Type v}
{δ : Type w}
(f : α → β → δ)
(s₁ : stream α)
(s₂ : stream β) :
(stream.zip f s₁ s₂).head = f s₁.head s₂.head
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.zip_eq
{α : Type u}
{β : Type v}
{δ : Type w}
(f : α → β → δ)
(s₁ : stream α)
(s₂ : stream β) :
stream.zip f s₁ s₂ = f s₁.head s₂.head :: 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
Equations
- stream.iterate f a = λ (n : ℕ), n.rec_on a (λ (n : ℕ) (r : α), f r)
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_zero_iterate
{α : Type u}
(f : α → α)
(a : α) :
stream.nth 0 (stream.iterate f a) = a
theorem
stream.nth_succ_iterate
{α : Type u}
(n : ℕ)
(f : α → α)
(a : α) :
stream.nth n.succ (stream.iterate f a) = stream.nth n (stream.iterate f (f a))
theorem
stream.nth_of_bisim
{α : Type u}
(R : stream α → stream α → Prop)
(bisim : stream.is_bisimulation R)
{s₁ s₂ : stream α}
(n : ℕ) :
R s₁ s₂ → stream.nth n s₁ = stream.nth n s₂ ∧ R (stream.drop (n + 1) s₁) (stream.drop (n + 1) s₂)
theorem
stream.eq_of_bisim
{α : Type u}
(R : stream α → stream α → Prop)
(bisim : stream.is_bisimulation R)
{s₁ s₂ : stream α} :
R s₁ s₂ → s₁ = s₂
theorem
stream.map_iterate
{α : Type u}
(f : α → α)
(a : α) :
stream.iterate f (f a) = stream.map f (stream.iterate f a)
Equations
- stream.corec f g = λ (a : α), stream.map f (stream.iterate g a)
Equations
- stream.corec_on a f g = stream.corec f g 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
Equations
- stream.corec' f = stream.corec (prod.fst ∘ f) (prod.snd ∘ f)
theorem
stream.corec'_eq
{α : Type u}
{β : Type v}
(f : α → β × α)
(a : α) :
stream.corec' f a = (f a).fst :: stream.corec' f (f a).snd
Equations
- stream.unfolds g f a = stream.corec g f a
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.nth n (stream.unfolds stream.head stream.tail s) = stream.nth n s
theorem
stream.nth_interleave_left
{α : Type u}
(n : ℕ)
(s₁ s₂ : stream α) :
stream.nth (2 * n) (s₁⋈s₂) = stream.nth n s₁
theorem
stream.nth_interleave_right
{α : Type u}
(n : ℕ)
(s₁ s₂ : stream α) :
stream.nth (2 * n + 1) (s₁⋈s₂) = stream.nth n s₂
theorem
stream.nth_even
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.nth n s.even = stream.nth (2 * n) s
theorem
stream.nth_odd
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.nth n s.odd = stream.nth (2 * n + 1) s
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
Equations
- stream.approx (n + 1) s = s.head :: stream.approx n s.tail
- stream.approx 0 s = list.nil
theorem
stream.approx_succ
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.approx n.succ s = s.head :: stream.approx n s.tail
theorem
stream.nth_approx
{α : Type u}
(n : ℕ)
(s : stream α) :
(stream.approx n.succ s).nth n = option.some (stream.nth n s)
theorem
stream.append_approx_drop
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.approx n s++ₛstream.drop n s = s
theorem
stream.take_theorem
{α : Type u}
(s₁ s₂ : stream α) :
(∀ (n : ℕ), stream.approx n s₁ = stream.approx n s₂) → s₁ = s₂
Equations
- stream.cycle (a :: l) h = stream.corec cycle_f cycle_g (a, l, a, l)
- stream.cycle list.nil h = absurd stream.cycle._main._proof_1 h
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
Equations
- s.tails = stream.corec id stream.tail s.tail
theorem
stream.nth_tails
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.nth n s.tails = stream.drop n s.tail
Equations
- s.inits = stream.inits_core [s.head] s.tail
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.nth n (stream.inits_core l s) = stream.nth n (stream.inits_core (a :: l) s)
theorem
stream.nth_inits
{α : Type u}
(n : ℕ)
(s : stream α) :
stream.nth n s.inits = stream.approx n.succ s
Equations
- f⊛s = λ (n : ℕ), stream.nth n f (stream.nth n s)
theorem
stream.composition
{α : Type u}
{β : Type v}
{δ : Type w}
(g : stream (β → δ))
(f : stream (α → β))
(s : stream α) :
stream.pure function.comp⊛g⊛f⊛s = g⊛(f⊛s)
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