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} [Inhabited α] : Inhabited (Stream' α)

Equations

• Stream'.instInhabitedStream' = { default := Stream'.const default }

theorem Stream'.eta {α : Type u} (s : Stream' α) : Stream'.cons (Stream'.head s) (Stream'.tail s) = s

theorem Stream'.ext {α : Type u} {s₁ : Stream' α} {s₂ : Stream' α} : (∀ (n : ℕ), Stream'.get s₁ n = Stream'.get s₂ n) → s₁ = s₂

@[simp]

theorem Stream'.get_zero_cons {α : Type u} (a : α) (s : Stream' α) : Stream'.get (Stream'.cons a s) 0 = a

@[simp]

theorem Stream'.head_cons {α : Type u} (a : α) (s : Stream' α) : Stream'.head (Stream'.cons a s) = a

@[simp]

theorem Stream'.tail_cons {α : Type u} (a : α) (s : Stream' α) : Stream'.tail (Stream'.cons a s) = s

@[simp]

theorem Stream'.get_drop {α : Type u} (n : ℕ) (m : ℕ) (s : Stream' α) : Stream'.get (Stream'.drop m s) n = Stream'.get s (n + m)

theorem Stream'.tail_eq_drop {α : Type u} (s : Stream' α) : Stream'.tail s = Stream'.drop 1 s

@[simp]

theorem Stream'.drop_drop {α : Type u} (n : ℕ) (m : ℕ) (s : Stream' α) : Stream'.drop n (Stream'.drop m s) = Stream'.drop (n + m) s

@[simp]

theorem Stream'.get_tail {α : Type u} {n : ℕ} {s : Stream' α} : Stream'.get (Stream'.tail s) n = Stream'.get s (n + 1)

@[simp]

theorem Stream'.tail_drop' {α : Type u} {i : ℕ} {s : Stream' α} : Stream'.tail (Stream'.drop i s) = Stream'.drop (i + 1) s

@[simp]

theorem Stream'.drop_tail' {α : Type u} {i : ℕ} {s : Stream' α} : Stream'.drop i (Stream'.tail s) = Stream'.drop (i + 1) s

theorem Stream'.tail_drop {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.tail (Stream'.drop n s) = Stream'.drop n (Stream'.tail s)

theorem Stream'.get_succ {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.get s (Nat.succ n) = Stream'.get (Stream'.tail s) n

@[simp]

theorem Stream'.get_succ_cons {α : Type u} (n : ℕ) (s : Stream' α) (x : α) : Stream'.get (Stream'.cons x s) (Nat.succ n) = Stream'.get s n

@[simp]

theorem Stream'.drop_zero {α : Type u} {s : Stream' α} : Stream'.drop 0 s = s

theorem Stream'.drop_succ {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.drop (Nat.succ n) s = Stream'.drop n (Stream'.tail s)

theorem Stream'.head_drop {α : Type u} (a : Stream' α) (n : ℕ) : Stream'.head (Stream'.drop n a) = Stream'.get a n

theorem Stream'.cons_injective2 {α : Type u} : Function.Injective2 Stream'.cons

theorem Stream'.cons_injective_left {α : Type u} (s : Stream' α) : Function.Injective fun (x : α) => Stream'.cons x s

theorem Stream'.cons_injective_right {α : Type u} (x : α) : Function.Injective (Stream'.cons x)

theorem Stream'.all_def {α : Type u} (p : α → Prop) (s : Stream' α) : Stream'.All p s = ∀ (n : ℕ), p (Stream'.get s n)

theorem Stream'.any_def {α : Type u} (p : α → Prop) (s : Stream' α) : Stream'.Any p s = ∃ (n : ℕ), p (Stream'.get s n)

@[simp]

theorem Stream'.mem_cons {α : Type u} (a : α) (s : Stream' α) : a ∈ Stream'.cons a s

theorem Stream'.mem_cons_of_mem {α : Type u} {a : α} {s : Stream' α} (b : α) : a ∈ s → a ∈ Stream'.cons b s

theorem Stream'.eq_or_mem_of_mem_cons {α : Type u} {a : α} {b : α} {s : Stream' α} : a ∈ Stream'.cons b s → a = b ∨ a ∈ s

theorem Stream'.mem_of_get_eq {α : Type u} {n : ℕ} {s : Stream' α} {a : α} : a = Stream'.get s n → a ∈ 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)

@[simp]

theorem Stream'.get_map {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (s : Stream' α) : Stream'.get (Stream'.map f s) n = f (Stream'.get s n)

theorem Stream'.tail_map {α : Type u} {β : Type v} (f : α → β) (s : Stream' α) : Stream'.tail (Stream'.map f s) = Stream'.map f (Stream'.tail s)

@[simp]

theorem Stream'.head_map {α : Type u} {β : Type v} (f : α → β) (s : Stream' α) : Stream'.head (Stream'.map f s) = f (Stream'.head s)

theorem Stream'.map_eq {α : Type u} {β : Type v} (f : α → β) (s : Stream' α) : Stream'.map f s = Stream'.cons (f (Stream'.head s)) (Stream'.map f (Stream'.tail s))

theorem Stream'.map_cons {α : Type u} {β : Type v} (f : α → β) (a : α) (s : Stream' α) : Stream'.map f (Stream'.cons a s) = Stream'.cons (f a) (Stream'.map f s)

@[simp]

theorem Stream'.map_id {α : Type u} (s : Stream' α) : Stream'.map id s = s

@[simp]

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

@[simp]

theorem Stream'.map_tail {α : Type u} {β : Type v} (f : α → β) (s : Stream' α) : Stream'.map f (Stream'.tail s) = Stream'.tail (Stream'.map f s)

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

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₂)

@[simp]

theorem Stream'.get_zip {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (n : ℕ) (s₁ : Stream' α) (s₂ : Stream' β) : Stream'.get (Stream'.zip f s₁ s₂) n = f (Stream'.get s₁ n) (Stream'.get 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' β) : Stream'.tail (Stream'.zip f s₁ s₂) = Stream'.zip f (Stream'.tail s₁) (Stream'.tail s₂)

theorem Stream'.zip_eq {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : Stream' α) (s₂ : Stream' β) : Stream'.zip f s₁ s₂ = Stream'.cons (f (Stream'.head s₁) (Stream'.head s₂)) (Stream'.zip f (Stream'.tail s₁) (Stream'.tail s₂))

@[simp]

theorem Stream'.get_enum {α : Type u} (s : Stream' α) (n : ℕ) : Stream'.get (Stream'.enum s) n = (n, Stream'.get s n)

theorem Stream'.enum_eq_zip {α : Type u} (s : Stream' α) : Stream'.enum s = Stream'.zip Prod.mk Stream'.nats s

@[simp]

theorem Stream'.mem_const {α : Type u} (a : α) : a ∈ Stream'.const a

theorem Stream'.const_eq {α : Type u} (a : α) : Stream'.const a = Stream'.cons a (Stream'.const a)

@[simp]

theorem Stream'.tail_const {α : Type u} (a : α) : Stream'.tail (Stream'.const a) = Stream'.const a

@[simp]

theorem Stream'.map_const {α : Type u} {β : Type v} (f : α → β) (a : α) : Stream'.map f (Stream'.const a) = Stream'.const (f a)

@[simp]

theorem Stream'.get_const {α : Type u} (n : ℕ) (a : α) : Stream'.get (Stream'.const a) n = a

@[simp]

theorem Stream'.drop_const {α : Type u} (n : ℕ) (a : α) : Stream'.drop n (Stream'.const a) = Stream'.const a

@[simp]

theorem Stream'.head_iterate {α : Type u} (f : α → α) (a : α) : Stream'.head (Stream'.iterate f a) = a

theorem Stream'.get_succ_iterate' {α : Type u} (n : ℕ) (f : α → α) (a : α) : Stream'.get (Stream'.iterate f a) (Nat.succ n) = f (Stream'.get (Stream'.iterate f a) n)

theorem Stream'.tail_iterate {α : Type u} (f : α → α) (a : α) : Stream'.tail (Stream'.iterate f a) = Stream'.iterate f (f a)

theorem Stream'.iterate_eq {α : Type u} (f : α → α) (a : α) : Stream'.iterate f a = Stream'.cons a (Stream'.iterate f (f a))

@[simp]

theorem Stream'.get_zero_iterate {α : Type u} (f : α → α) (a : α) : Stream'.get (Stream'.iterate f a) 0 = a

theorem Stream'.get_succ_iterate {α : Type u} (n : ℕ) (f : α → α) (a : α) : Stream'.get (Stream'.iterate f a) (Nat.succ n) = Stream'.get (Stream'.iterate f (f a)) n

def Stream'.IsBisimulation {α : Type u} (R : Stream' α → Stream' α → Prop) : Prop

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

Equations

• Stream'.IsBisimulation R = ∀ ⦃s₁ s₂ : Stream' α⦄, R s₁ s₂ → Stream'.head s₁ = Stream'.head s₂ ∧ R (Stream'.tail s₁) (Stream'.tail s₂)

theorem Stream'.get_of_bisim {α : Type u} (R : Stream' α → Stream' α → Prop) (bisim : Stream'.IsBisimulation R) {s₁ : Stream' α} {s₂ : Stream' α} (n : ℕ) : R s₁ s₂ → Stream'.get s₁ n = Stream'.get 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₂

@[simp]

theorem Stream'.iterate_id {α : Type u} (a : α) : Stream'.iterate id a = Stream'.const a

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 = Stream'.cons (f a) (Stream'.corec f g (g a))

theorem Stream'.corec_id_id_eq_const {α : Type u} (a : α) : Stream'.corec id id a = Stream'.const 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 = Stream'.cons (f a).1 (Stream'.corec' f (f a).2)

theorem Stream'.unfolds_eq {α : Type u} {β : Type v} (g : α → β) (f : α → α) (a : α) : Stream'.unfolds g f a = Stream'.cons (g a) (Stream'.unfolds g f (f a))

theorem Stream'.get_unfolds_head_tail {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.get (Stream'.unfolds Stream'.head Stream'.tail s) n = Stream'.get 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' α) : s₁ ⋈ s₂ = Stream'.cons (Stream'.head s₁) (Stream'.cons (Stream'.head s₂) (Stream'.tail s₁ ⋈ Stream'.tail s₂))

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' α) : Stream'.tail s₁ ⋈ Stream'.tail s₂ = Stream'.tail (Stream'.tail (s₁ ⋈ s₂))

theorem Stream'.get_interleave_left {α : Type u} (n : ℕ) (s₁ : Stream' α) (s₂ : Stream' α) : Stream'.get (s₁ ⋈ s₂) (2 * n) = Stream'.get s₁ n

theorem Stream'.get_interleave_right {α : Type u} (n : ℕ) (s₁ : Stream' α) (s₂ : Stream' α) : Stream'.get (s₁ ⋈ s₂) (2 * n + 1) = Stream'.get 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'.odd_eq {α : Type u} (s : Stream' α) : Stream'.odd s = Stream'.even (Stream'.tail s)

@[simp]

theorem Stream'.head_even {α : Type u} (s : Stream' α) : Stream'.head (Stream'.even s) = Stream'.head s

theorem Stream'.tail_even {α : Type u} (s : Stream' α) : Stream'.tail (Stream'.even s) = Stream'.even (Stream'.tail (Stream'.tail s))

theorem Stream'.even_cons_cons {α : Type u} (a₁ : α) (a₂ : α) (s : Stream' α) : Stream'.even (Stream'.cons a₁ (Stream'.cons a₂ s)) = Stream'.cons a₁ (Stream'.even s)

theorem Stream'.even_tail {α : Type u} (s : Stream' α) : Stream'.even (Stream'.tail s) = Stream'.odd s

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'.get_even {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.get (Stream'.even s) n = Stream'.get s (2 * n)

theorem Stream'.get_odd {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.get (Stream'.odd s) n = Stream'.get s (2 * n + 1)

theorem Stream'.mem_of_mem_even {α : Type u} (a : α) (s : Stream' α) : a ∈ Stream'.even s → a ∈ s

theorem Stream'.mem_of_mem_odd {α : Type u} (a : α) (s : Stream' α) : a ∈ Stream'.odd s → a ∈ 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' α) : 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 (List.length l) (l ++ₛ s) = s

theorem Stream'.append_stream_head_tail {α : Type u} (s : Stream' α) : [Stream'.head s] ++ₛ Stream'.tail s = s

theorem Stream'.mem_append_stream_right {α : Type u} {a : α} (l : List α) {s : Stream' α} : a ∈ s → a ∈ l ++ₛ s

theorem Stream'.mem_append_stream_left {α : Type u} {a : α} {l : List α} (s : Stream' α) : a ∈ l → a ∈ l ++ₛ s

@[simp]

theorem Stream'.take_zero {α : Type u} (s : Stream' α) : Stream'.take 0 s = []

theorem Stream'.take_succ {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.take (Nat.succ n) s = Stream'.head s :: Stream'.take n (Stream'.tail s)

@[simp]

theorem Stream'.take_succ_cons {α : Type u} {a : α} (n : ℕ) (s : Stream' α) : Stream'.take (n + 1) (Stream'.cons a s) = a :: Stream'.take n s

theorem Stream'.take_succ' {α : Type u} {s : Stream' α} (n : ℕ) : Stream'.take (n + 1) s = Stream'.take n s ++ [Stream'.get s n]

@[simp]

theorem Stream'.length_take {α : Type u} (n : ℕ) (s : Stream' α) : List.length (Stream'.take n s) = n

@[simp]

theorem Stream'.take_take {α : Type u} {s : Stream' α} {m : ℕ} {n : ℕ} : List.take m (Stream'.take n s) = Stream'.take (min n m) s

@[simp]

theorem Stream'.concat_take_get {α : Type u} {n : ℕ} {s : Stream' α} : Stream'.take n s ++ [Stream'.get s n] = Stream'.take (n + 1) s

theorem Stream'.get?_take {α : Type u} {s : Stream' α} {k : ℕ} {n : ℕ} : k < n → List.get? (Stream'.take n s) k = some (Stream'.get s k)

theorem Stream'.get?_take_succ {α : Type u} (n : ℕ) (s : Stream' α) : List.get? (Stream'.take (Nat.succ n) s) n = some (Stream'.get s n)

@[simp]

theorem Stream'.dropLast_take {α : Type u} {n : ℕ} {xs : Stream' α} : List.dropLast (Stream'.take n xs) = Stream'.take (n - 1) xs

@[simp]

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₁ : 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 ≠ []) : Stream'.cycle l h = l ++ₛ Stream'.cycle l h

theorem Stream'.mem_cycle {α : Type u} {a : α} {l : List α} (h : l ≠ []) : a ∈ l → a ∈ Stream'.cycle l h

@[simp]

theorem Stream'.cycle_singleton {α : Type u} (a : α) : Stream'.cycle [a] ⋯ = Stream'.const a

theorem Stream'.tails_eq {α : Type u} (s : Stream' α) : Stream'.tails s = Stream'.cons (Stream'.tail s) (Stream'.tails (Stream'.tail s))

@[simp]

theorem Stream'.get_tails {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.get (Stream'.tails s) n = Stream'.drop n (Stream'.tail s)

theorem Stream'.tails_eq_iterate {α : Type u} (s : Stream' α) : Stream'.tails s = Stream'.iterate Stream'.tail (Stream'.tail s)

theorem Stream'.inits_core_eq {α : Type u} (l : List α) (s : Stream' α) : Stream'.initsCore l s = Stream'.cons l (Stream'.initsCore (l ++ [Stream'.head s]) (Stream'.tail s))

theorem Stream'.tail_inits {α : Type u} (s : Stream' α) : Stream'.tail (Stream'.inits s) = Stream'.initsCore [Stream'.head s, Stream'.head (Stream'.tail s)] (Stream'.tail (Stream'.tail s))

theorem Stream'.inits_tail {α : Type u} (s : Stream' α) : Stream'.inits (Stream'.tail s) = Stream'.initsCore [Stream'.head (Stream'.tail s)] (Stream'.tail (Stream'.tail s))

theorem Stream'.cons_get_inits_core {α : Type u} (a : α) (n : ℕ) (l : List α) (s : Stream' α) : a :: Stream'.get (Stream'.initsCore l s) n = Stream'.get (Stream'.initsCore (a :: l) s) n

@[simp]

theorem Stream'.get_inits {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.get (Stream'.inits s) n = Stream'.take (Nat.succ n) s

theorem Stream'.inits_eq {α : Type u} (s : Stream' α) : Stream'.inits s = Stream'.cons [Stream'.head s] (Stream'.map (List.cons (Stream'.head s)) (Stream'.inits (Stream'.tail s)))

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' α) : Stream'.pure id ⊛ s = 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 fun (f : α → β) => f a) ⊛ fs

theorem Stream'.map_eq_apply {α : Type u} {β : Type v} (f : α → β) (s : Stream' α) : Stream'.map f s = Stream'.pure f ⊛ s

theorem Stream'.get_nats (n : ℕ) : Stream'.get Stream'.nats n = n

theorem Stream'.nats_eq : Stream'.nats = Stream'.cons 0 (Stream'.map Nat.succ Stream'.nats)