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.

ink

instance Stream'.instInhabitedStream' {α : Type u_1} [inst : Inhabited α] : Inhabited (Stream' α)

Equations

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Stream'.mem_of_nth_eq {α : Type u} {n : ℕ} {s : Stream' α} {a : α} : a = Stream'.nth s n → a ∈ s

ink

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)

ink

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

ink

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

ink

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

ink

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

ink

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)

ink

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

ink

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

ink

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

ink

theorem Stream'.mem_map {α : Type u} {β : Type v} (f : α → β) {a : α} {s : Stream' α} : a ∈ s → f a ∈ Stream'.map f s

ink

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

ink

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

ink

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)

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Stream'.eq_of_bisim {α : Type u} (R : Stream' α → Stream' α → Prop) (bisim : Stream'.IsBisimulation R) {s₁ : Stream' α} {s₂ : Stream' α} : R s₁ s₂ → s₁ = s₂

ink

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₂

ink

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₂

ink

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

ink

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

ink

theorem Stream'.corec_def {α : Type u} {β : Type v} (f : α → β) (g : α → α) (a : α) : Stream'.corec f g a = Stream'.map f (Stream'.iterate g a)

ink

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

ink

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

ink

theorem Stream'.corec_id_f_eq_iterate {α : Type u} (f : α → α) (a : α) : Stream'.corec id f a = Stream'.iterate f a

ink

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)

ink

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

ink

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

ink

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

ink

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

ink

theorem Stream'.tail_interleave {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) : Stream'.tail (s₁ ⋈ s₂) = s₂ ⋈ Stream'.tail s₁

ink

theorem Stream'.interleave_tail_tail {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) : Stream'.tail s₁ ⋈ Stream'.tail s₂ = Stream'.tail (Stream'.tail (s₁ ⋈ s₂))

ink

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

ink

theorem Stream'.nth_interleave_right {α : Type u} (n : ℕ) (s₁ : Stream' α) (s₂ : Stream' α) : Stream'.nth (s₁ ⋈ s₂) (2 * n + 1) = Stream'.nth s₂ n

ink

theorem Stream'.mem_interleave_left {α : Type u} {a : α} {s₁ : Stream' α} (s₂ : Stream' α) : a ∈ s₁ → a ∈ s₁ ⋈ s₂

ink

theorem Stream'.mem_interleave_right {α : Type u} {a : α} {s₁ : Stream' α} (s₂ : Stream' α) : a ∈ s₂ → a ∈ s₁ ⋈ s₂

ink

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

ink

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

ink

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

ink

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)

ink

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

ink

theorem Stream'.even_interleave {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) : Stream'.even (s₁ ⋈ s₂) = s₁

ink

theorem Stream'.interleave_even_odd {α : Type u} (s₁ : Stream' α) : Stream'.even s₁ ⋈ Stream'.odd s₁ = s₁

ink

theorem Stream'.nth_even {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.nth (Stream'.even s) n = Stream'.nth s (2 * n)

ink

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

ink

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

ink

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

ink

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

ink

theorem Stream'.cons_append_stream {α : Type u} (a : α) (l : List α) (s : Stream' α) : a :: l ++ₛ s = Stream'.cons a (l ++ₛ s)

ink

theorem Stream'.append_append_stream {α : Type u} (l₁ : List α) (l₂ : List α) (s : Stream' α) : l₁ ++ l₂ ++ₛ s = l₁ ++ₛ (l₂ ++ₛ s)

ink

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

ink

theorem Stream'.drop_append_stream {α : Type u} (l : List α) (s : Stream' α) : Stream'.drop (List.length l) (l ++ₛ s) = s

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

theorem Stream'.append_take_drop {α : Type u} (n : ℕ) (s : Stream' α) : Stream'.take n s ++ₛ Stream'.drop n s = s

ink

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

ink

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

ink

theorem Stream'.cycle_eq {α : Type u} (l : List α) (h : l ≠ []) : Stream'.cycle l h = l ++ₛ Stream'.cycle l h

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Stream'.zip_inits_tails {α : Type u} (s : Stream' α) : Stream'.zip Stream'.appendStream' (Stream'.inits s) (Stream'.tails s) = Stream'.const s

ink

theorem Stream'.identity {α : Type u} (s : Stream' α) : Stream'.pure id ⊛ s = s

ink

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)

ink

theorem Stream'.homomorphism {α : Type u} {β : Type v} (f : α → β) (a : α) : Stream'.pure f ⊛ Stream'.pure a = Stream'.pure (f a)

ink

theorem Stream'.interchange {α : Type u} {β : Type v} (fs : Stream' (α → β)) (a : α) : fs ⊛ Stream'.pure a = (Stream'.pure fun f => f a) ⊛ fs

ink

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

ink

theorem Stream'.nth_nats (n : ℕ) : Stream'.nth Stream'.nats n = n

ink

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