Documentation

Mathlib.Data.Stream.Init

Streams a.k.a. infinite lists a.k.a. infinite sequences #

Porting note: This file used to be in the core library. It was moved to mathlib and renamed to init to avoid name clashes.

instance Stream'.instInhabitedStream' {α : Type u_1} [inst : Inhabited α] :
Equations
@[simp]
theorem Stream'.nth_zero_cons {α : Type u} (a : α) (s : Stream' α) :
theorem Stream'.head_cons {α : Type u} (a : α) (s : Stream' α) :
theorem Stream'.tail_cons {α : Type u} (a : α) (s : Stream' α) :
theorem Stream'.nth_drop {α : Type u} (n : ) (m : ) (s : Stream' α) :
theorem Stream'.drop_drop {α : Type u} (n : ) (m : ) (s : Stream' α) :
@[simp]
theorem Stream'.nth_succ_cons {α : Type u} (n : ) (s : Stream' α) (x : α) :
@[simp]
theorem Stream'.head_drop {α : Type u_1} (a : Stream' α) (n : ) :
theorem Stream'.ext {α : Type u} {s₁ : Stream' α} {s₂ : Stream' α} :
(∀ (n : ), Stream'.nth s₁ n = Stream'.nth s₂ n) → s₁ = s₂
theorem Stream'.all_def {α : Type u} (p : αProp) (s : Stream' α) :
Stream'.All p s = ((n : ) → p (Stream'.nth s n))
theorem Stream'.any_def {α : Type u} (p : αProp) (s : Stream' α) :
Stream'.Any p s = n, p (Stream'.nth s n)
theorem Stream'.mem_cons {α : Type u} (a : α) (s : Stream' α) :
theorem Stream'.mem_cons_of_mem {α : Type u} {a : α} {s : Stream' α} (b : α) :
a sa Stream'.cons b s
theorem Stream'.eq_or_mem_of_mem_cons {α : Type u} {a : α} {b : α} {s : Stream' α} :
a Stream'.cons b sa = b a s
theorem Stream'.mem_of_nth_eq {α : Type u} {n : } {s : Stream' α} {a : α} :
a = Stream'.nth s na s
theorem Stream'.drop_map {α : Type u} {β : Type v} (f : αβ) (n : ) (s : Stream' α) :
theorem Stream'.nth_map {α : Type u} {β : Type v} (f : αβ) (n : ) (s : Stream' α) :
theorem Stream'.tail_map {α : Type u} {β : Type v} (f : αβ) (s : Stream' α) :
theorem Stream'.head_map {α : Type u} {β : Type v} (f : αβ) (s : Stream' α) :
theorem Stream'.map_eq {α : Type u} {β : Type v} (f : αβ) (s : Stream' α) :
theorem Stream'.map_cons {α : Type u} {β : Type v} (f : αβ) (a : α) (s : Stream' α) :
theorem Stream'.map_id {α : Type u} (s : Stream' α) :
Stream'.map id s = s
theorem Stream'.map_map {α : Type u} {β : Type v} {δ : Type w} (g : βδ) (f : αβ) (s : Stream' α) :
theorem Stream'.map_tail {α : Type u} {β : Type v} (f : αβ) (s : Stream' α) :
theorem Stream'.mem_map {α : Type u} {β : Type v} (f : αβ) {a : α} {s : Stream' α} :
a sf a Stream'.map f s
theorem Stream'.exists_of_mem_map {α : Type u} {β : Type v} {f : αβ} {b : β} {s : Stream' α} :
b Stream'.map f sa, a s f a = b
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 (Stream'.zip f s₁ s₂) n = f (Stream'.nth s₁ n) (Stream'.nth s₂ n)
theorem Stream'.head_zip {α : Type u} {β : Type v} {δ : Type w} (f : αβδ) (s₁ : Stream' α) (s₂ : Stream' β) :
Stream'.head (Stream'.zip f s₁ s₂) = f (Stream'.head s₁) (Stream'.head s₂)
theorem Stream'.tail_zip {α : Type u} {β : Type v} {δ : Type w} (f : αβδ) (s₁ : Stream' α) (s₂ : Stream' β) :
theorem Stream'.zip_eq {α : Type u} {β : Type v} {δ : Type w} (f : αβδ) (s₁ : Stream' α) (s₂ : Stream' β) :
@[simp]
theorem Stream'.nth_enum {α : Type u} (s : Stream' α) (n : ) :
theorem Stream'.mem_const {α : Type u} (a : α) :
theorem Stream'.map_const {α : Type u} {β : Type v} (f : αβ) (a : α) :
theorem Stream'.nth_const {α : Type u} (n : ) (a : α) :
theorem Stream'.head_iterate {α : Type u} (f : αα) (a : α) :
theorem Stream'.tail_iterate {α : Type u} (f : αα) (a : α) :
theorem Stream'.iterate_eq {α : Type u} (f : αα) (a : α) :
theorem Stream'.nth_zero_iterate {α : Type u} (f : αα) (a : α) :
theorem Stream'.nth_succ_iterate {α : Type u} (n : ) (f : αα) (a : α) :
def Stream'.IsBisimulation {α : Type u} (R : Stream' αStream' αProp) :

Streams s₁ and s₂ are defined to be bisimulations if their heads are equal and tails are bisimulations.

Equations
theorem Stream'.nth_of_bisim {α : Type u} (R : Stream' αStream' αProp) (bisim : Stream'.IsBisimulation R) {s₁ : Stream' α} {s₂ : Stream' α} (n : ) :
R s₁ s₂Stream'.nth s₁ n = Stream'.nth s₂ n R (Stream'.drop (n + 1) s₁) (Stream'.drop (n + 1) s₂)
theorem Stream'.eq_of_bisim {α : Type u} (R : Stream' αStream' αProp) (bisim : Stream'.IsBisimulation R) {s₁ : Stream' α} {s₂ : Stream' α} :
R s₁ s₂s₁ = s₂
theorem Stream'.bisim_simple {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) :
Stream'.head s₁ = Stream'.head s₂s₁ = Stream'.tail s₁s₂ = Stream'.tail s₂s₁ = s₂
theorem Stream'.coinduction {α : Type u} {s₁ : Stream' α} {s₂ : Stream' α} :
Stream'.head s₁ = Stream'.head s₂(∀ (β : Type u) (fr : Stream' αβ), fr s₁ = fr s₂fr (Stream'.tail s₁) = fr (Stream'.tail s₂)) → s₁ = s₂
theorem Stream'.map_iterate {α : Type u} (f : αα) (a : α) :
theorem Stream'.corec_def {α : Type u} {β : Type v} (f : αβ) (g : αα) (a : α) :
theorem Stream'.corec_eq {α : Type u} {β : Type v} (f : αβ) (g : αα) (a : α) :
Stream'.corec f g a = Stream'.cons (f a) (Stream'.corec f g (g a))
theorem Stream'.corec_id_f_eq_iterate {α : Type u} (f : αα) (a : α) :
theorem Stream'.corec'_eq {α : Type u} {β : Type v} (f : αβ × α) (a : α) :
Stream'.corec' f a = Stream'.cons (f a).fst (Stream'.corec' f (f a).snd)
theorem Stream'.unfolds_eq {α : Type u} {β : Type v} (g : αβ) (f : αα) (a : α) :
theorem Stream'.nth_unfolds_head_tail {α : Type u} (n : ) (s : Stream' α) :
Stream'.nth (Stream'.unfolds Stream'.head Stream'.tail s) n = Stream'.nth s n
theorem Stream'.unfolds_head_eq {α : Type u} (s : Stream' α) :
Stream'.unfolds Stream'.head Stream'.tail s = s
theorem Stream'.interleave_eq {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) :
theorem Stream'.tail_interleave {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) :
Stream'.tail (s₁ s₂) = s₂ Stream'.tail s₁
theorem Stream'.interleave_tail_tail {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) :
theorem Stream'.nth_interleave_left {α : Type u} (n : ) (s₁ : Stream' α) (s₂ : Stream' α) :
Stream'.nth (s₁ s₂) (2 * n) = Stream'.nth s₁ n
theorem Stream'.nth_interleave_right {α : Type u} (n : ) (s₁ : Stream' α) (s₂ : Stream' α) :
Stream'.nth (s₁ s₂) (2 * n + 1) = Stream'.nth s₂ n
theorem Stream'.mem_interleave_left {α : Type u} {a : α} {s₁ : Stream' α} (s₂ : Stream' α) :
a s₁a s₁ s₂
theorem Stream'.mem_interleave_right {α : Type u} {a : α} {s₁ : Stream' α} (s₂ : Stream' α) :
a s₂a s₁ s₂
theorem Stream'.even_cons_cons {α : Type u} (a₁ : α) (a₂ : α) (s : Stream' α) :
theorem Stream'.even_interleave {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) :
Stream'.even (s₁ s₂) = s₁
theorem Stream'.interleave_even_odd {α : Type u} (s₁ : Stream' α) :
Stream'.even s₁ Stream'.odd s₁ = s₁
theorem Stream'.nth_even {α : Type u} (n : ) (s : Stream' α) :
theorem Stream'.nth_odd {α : Type u} (n : ) (s : Stream' α) :
theorem Stream'.mem_of_mem_even {α : Type u} (a : α) (s : Stream' α) :
a Stream'.even sa s
theorem Stream'.mem_of_mem_odd {α : Type u} (a : α) (s : Stream' α) :
a Stream'.odd sa s
theorem Stream'.nil_append_stream {α : Type u} (s : Stream' α) :
[] ++ₛ s = s
theorem Stream'.cons_append_stream {α : Type u} (a : α) (l : List α) (s : Stream' α) :
a :: l ++ₛ s = Stream'.cons a (l ++ₛ s)
theorem Stream'.append_append_stream {α : Type u} (l₁ : List α) (l₂ : List α) (s : Stream' α) :
l₁ ++ l₂ ++ₛ s = l₁ ++ₛ (l₂ ++ₛ s)
theorem Stream'.map_append_stream {α : Type u} {β : Type v} (f : αβ) (l : List α) (s : Stream' α) :
theorem Stream'.drop_append_stream {α : Type u} (l : List α) (s : Stream' α) :
theorem Stream'.mem_append_stream_right {α : Type u} {a : α} (l : List α) {s : Stream' α} :
a sa l ++ₛ s
theorem Stream'.mem_append_stream_left {α : Type u} {a : α} {l : List α} (s : Stream' α) :
a la l ++ₛ s
@[simp]
theorem Stream'.take_zero {α : Type u} (s : Stream' α) :
@[simp]
theorem Stream'.length_take {α : Type u} (n : ) (s : Stream' α) :
theorem Stream'.take_theorem {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) :
(∀ (n : ), Stream'.take n s₁ = Stream'.take n s₂) → s₁ = s₂
theorem Stream'.cycle_g_cons {α : Type u} (a : α) (a₁ : α) (l₁ : List α) (a₀ : α) (l₀ : List α) :
Stream'.cycleG (a, a₁ :: l₁, a₀, l₀) = (a₁, l₁, a₀, l₀)
theorem Stream'.cycle_eq {α : Type u} (l : List α) (h : l []) :
theorem Stream'.mem_cycle {α : Type u} {a : α} {l : List α} (h : l []) :
a la Stream'.cycle l h
theorem Stream'.cycle_singleton {α : Type u} (a : α) (h : [a] []) :
theorem Stream'.cons_nth_inits_core {α : Type u} (a : α) (n : ) (l : List α) (s : Stream' α) :
theorem Stream'.zip_inits_tails {α : Type u} (s : Stream' α) :
Stream'.zip Stream'.appendStream' (Stream'.inits s) (Stream'.tails s) = Stream'.const s
theorem Stream'.identity {α : Type u} (s : Stream' α) :
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 : α) :
theorem Stream'.interchange {α : Type u} {β : Type v} (fs : Stream' (αβ)) (a : α) :
fs Stream'.pure a = (Stream'.pure fun f => f a) fs
theorem Stream'.map_eq_apply {α : Type u} {β : Type v} (f : αβ) (s : Stream' α) :