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.

theorem Stream'.ext {α : Type u} {s₁ : Stream' α} {s₂ : Stream' α} :
(∀ (n : ), Stream'.nth s₁ n = Stream'.nth s₂ n) → s₁ = s₂
@[simp]
theorem Stream'.nth_zero_cons {α : Type u} (a : α) (s : Stream' α) :
@[simp]
theorem Stream'.head_cons {α : Type u} (a : α) (s : Stream' α) :
@[simp]
theorem Stream'.tail_cons {α : Type u} (a : α) (s : Stream' α) :
@[simp]
theorem Stream'.nth_drop {α : Type u} (n : ) (m : ) (s : Stream' α) :
@[simp]
theorem Stream'.drop_drop {α : Type u} (n : ) (m : ) (s : Stream' α) :
@[simp]
theorem Stream'.nth_tail {α : Type u} {n : } {s : Stream' α} :
@[simp]
theorem Stream'.tail_drop' {α : Type u} {i : } {s : Stream' α} :
@[simp]
theorem Stream'.drop_tail' {α : Type u} {i : } {s : Stream' α} :
theorem Stream'.nth_succ {α : Type u} (n : ) (s : Stream' α) :
@[simp]
theorem Stream'.nth_succ_cons {α : Type u} (n : ) (s : Stream' α) (x : α) :
@[simp]
theorem Stream'.drop_zero {α : Type u} {s : Stream' α} :
theorem Stream'.head_drop {α : Type u} (a : Stream' α) (n : ) :
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)
@[simp]
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' α) :
@[simp]
theorem Stream'.nth_map {α : Type u} {β : Type v} (f : αβ) (n : ) (s : Stream' α) :
theorem Stream'.tail_map {α : Type u} {β : Type v} (f : αβ) (s : Stream' α) :
@[simp]
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' α) :
@[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' α) :
@[simp]
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₂)
@[simp]
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 : ) :
@[simp]
theorem Stream'.mem_const {α : Type u} (a : α) :
@[simp]
@[simp]
theorem Stream'.map_const {α : Type u} {β : Type v} (f : αβ) (a : α) :
@[simp]
theorem Stream'.nth_const {α : Type u} (n : ) (a : α) :
@[simp]
theorem Stream'.drop_const {α : Type u} (n : ) (a : α) :
@[simp]
theorem Stream'.head_iterate {α : Type u} (f : αα) (a : α) :
theorem Stream'.nth_succ_iterate' {α : Type u} (n : ) (f : αα) (a : α) :
theorem Stream'.tail_iterate {α : Type u} (f : αα) (a : α) :
theorem Stream'.iterate_eq {α : Type u} (f : αα) (a : α) :
@[simp]
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.

Instances For
    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₂
    @[simp]
    theorem Stream'.iterate_id {α : Type u} (a : α) :
    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'.take_succ_cons {α : Type u} {a : α} (n : ) (s : Stream' α) :
    theorem Stream'.take_succ' {α : Type u} {s : Stream' α} (n : ) :
    @[simp]
    theorem Stream'.length_take {α : Type u} (n : ) (s : Stream' α) :
    @[simp]
    theorem Stream'.take_take {α : Type u} {s : Stream' α} {m : } {n : } :
    @[simp]
    theorem Stream'.concat_take_nth {α : Type u} {n : } {s : Stream' α} :
    theorem Stream'.get?_take {α : Type u} {s : Stream' α} {k : } {n : } :
    k < nList.get? (Stream'.take n s) k = some (Stream'.nth s k)
    theorem Stream'.get?_take_succ {α : Type u} (n : ) (s : Stream' α) :
    @[simp]
    theorem Stream'.dropLast_take {α : Type u} {n : } {xs : Stream' α} :
    @[simp]
    theorem Stream'.append_take_drop {α : 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
    @[simp]
    theorem Stream'.cycle_singleton {α : Type u} (a : α) :
    Stream'.cycle [a] (_ : ¬[a] = []) = Stream'.const a
    @[simp]
    theorem Stream'.cons_nth_inits_core {α : Type u} (a : α) (n : ) (l : List α) (s : Stream' α) :
    @[simp]
    theorem Stream'.nth_inits {α : Type u} (n : ) (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' α) :