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.

Equations
theorem Stream'.eta {α : Type u} (s : Stream' α) :
Stream'.cons s.head s.tail = s
theorem Stream'.ext {α : Type u} {s₁ : Stream' α} {s₂ : Stream' α} :
(∀ (n : ), s₁.get n = s₂.get n)s₁ = s₂
@[simp]
theorem Stream'.get_zero_cons {α : Type u} (a : α) (s : Stream' α) :
(Stream'.cons a s).get 0 = a
@[simp]
theorem Stream'.head_cons {α : Type u} (a : α) (s : Stream' α) :
(Stream'.cons a s).head = a
@[simp]
theorem Stream'.tail_cons {α : Type u} (a : α) (s : Stream' α) :
(Stream'.cons a s).tail = s
@[simp]
theorem Stream'.get_drop {α : Type u} (n : ) (m : ) (s : Stream' α) :
(Stream'.drop m s).get n = s.get (n + m)
theorem Stream'.tail_eq_drop {α : Type u} (s : Stream' α) :
s.tail = Stream'.drop 1 s
@[simp]
theorem Stream'.drop_drop {α : Type u} (n : ) (m : ) (s : Stream' α) :
@[simp]
theorem Stream'.get_tail {α : Type u} {n : } {s : Stream' α} :
s.tail.get n = s.get (n + 1)
@[simp]
theorem Stream'.tail_drop' {α : Type u} {i : } {s : Stream' α} :
(Stream'.drop i s).tail = Stream'.drop (i + 1) s
@[simp]
theorem Stream'.drop_tail' {α : Type u} {i : } {s : Stream' α} :
Stream'.drop i s.tail = Stream'.drop (i + 1) s
theorem Stream'.tail_drop {α : Type u} (n : ) (s : Stream' α) :
(Stream'.drop n s).tail = Stream'.drop n s.tail
theorem Stream'.get_succ {α : Type u} (n : ) (s : Stream' α) :
s.get n.succ = s.tail.get n
@[simp]
theorem Stream'.get_succ_cons {α : Type u} (n : ) (s : Stream' α) (x : α) :
(Stream'.cons x s).get n.succ = s.get n
@[simp]
theorem Stream'.drop_zero {α : Type u} {s : Stream' α} :
theorem Stream'.drop_succ {α : Type u} (n : ) (s : Stream' α) :
Stream'.drop n.succ s = Stream'.drop n s.tail
theorem Stream'.head_drop {α : Type u} (a : Stream' α) (n : ) :
(Stream'.drop n a).head = a.get n
theorem Stream'.cons_injective_left {α : Type u} (s : Stream' α) :
Function.Injective fun (x : α) => Stream'.cons x s
theorem Stream'.all_def {α : Type u} (p : αProp) (s : Stream' α) :
Stream'.All p s = ∀ (n : ), p (s.get n)
theorem Stream'.any_def {α : Type u} (p : αProp) (s : Stream' α) :
Stream'.Any p s = ∃ (n : ), p (s.get 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_get_eq {α : Type u} {n : } {s : Stream' α} {a : α} :
a = s.get na s
theorem Stream'.drop_map {α : Type u} {β : Type v} (f : αβ) (n : ) (s : Stream' α) :
@[simp]
theorem Stream'.get_map {α : Type u} {β : Type v} (f : αβ) (n : ) (s : Stream' α) :
(Stream'.map f s).get n = f (s.get n)
theorem Stream'.tail_map {α : Type u} {β : Type v} (f : αβ) (s : Stream' α) :
(Stream'.map f s).tail = Stream'.map f s.tail
@[simp]
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 = Stream'.cons (f s.head) (Stream'.map f s.tail)
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' α) :
Stream'.map f s.tail = (Stream'.map f s).tail
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 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'.zip f s₁ s₂).get n = f (s₁.get n) (s₂.get n)
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₂ = Stream'.cons (f s₁.head s₂.head) (Stream'.zip f s₁.tail s₂.tail)
@[simp]
theorem Stream'.get_enum {α : Type u} (s : Stream' α) (n : ) :
s.enum.get n = (n, s.get n)
theorem Stream'.enum_eq_zip {α : Type u} (s : Stream' α) :
s.enum = Stream'.zip Prod.mk Stream'.nats s
@[simp]
theorem Stream'.mem_const {α : Type u} (a : α) :
@[simp]
theorem Stream'.tail_const {α : Type u} (a : α) :
@[simp]
theorem Stream'.map_const {α : Type u} {β : Type v} (f : αβ) (a : α) :
@[simp]
theorem Stream'.get_const {α : Type u} (n : ) (a : α) :
(Stream'.const a).get n = a
@[simp]
theorem Stream'.drop_const {α : Type u} (n : ) (a : α) :
@[simp]
theorem Stream'.head_iterate {α : Type u} (f : αα) (a : α) :
(Stream'.iterate f a).head = a
theorem Stream'.get_succ_iterate' {α : Type u} (n : ) (f : αα) (a : α) :
(Stream'.iterate f a).get n.succ = f ((Stream'.iterate f a).get n)
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 : α) :
@[simp]
theorem Stream'.get_zero_iterate {α : Type u} (f : αα) (a : α) :
(Stream'.iterate f a).get 0 = a
theorem Stream'.get_succ_iterate {α : Type u} (n : ) (f : αα) (a : α) :
(Stream'.iterate f a).get n.succ = (Stream'.iterate f (f a)).get n
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
Instances For
    theorem Stream'.get_of_bisim {α : Type u} (R : Stream' αStream' αProp) (bisim : Stream'.IsBisimulation R) {s₁ : Stream' α} {s₂ : Stream' α} (n : ) :
    R s₁ s₂s₁.get n = s₂.get 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' α) :
    s₁.head = s₂.heads₁ = s₁.tails₂ = s₂.tails₁ = s₂
    theorem Stream'.coinduction {α : Type u} {s₁ : Stream' α} {s₂ : Stream' α} :
    s₁.head = s₂.head(∀ (β : Type u) (fr : Stream' αβ), fr s₁ = fr s₂fr s₁.tail = fr s₂.tail)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 : α) :
    theorem Stream'.unfolds_eq {α : Type u} {β : Type v} (g : αβ) (f : αα) (a : α) :
    theorem Stream'.get_unfolds_head_tail {α : Type u} (n : ) (s : Stream' α) :
    (Stream'.unfolds Stream'.head Stream'.tail s).get n = s.get 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 s₁.head (Stream'.cons s₂.head (s₁.tail s₂.tail))
    theorem Stream'.tail_interleave {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) :
    (s₁ s₂).tail = s₂ s₁.tail
    theorem Stream'.interleave_tail_tail {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) :
    s₁.tail s₂.tail = (s₁ s₂).tail.tail
    theorem Stream'.get_interleave_left {α : Type u} (n : ) (s₁ : Stream' α) (s₂ : Stream' α) :
    (s₁ s₂).get (2 * n) = s₁.get n
    theorem Stream'.get_interleave_right {α : Type u} (n : ) (s₁ : Stream' α) (s₂ : Stream' α) :
    (s₁ s₂).get (2 * n + 1) = s₂.get 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' α) :
    s.odd = s.tail.even
    @[simp]
    theorem Stream'.head_even {α : Type u} (s : Stream' α) :
    s.even.head = s.head
    theorem Stream'.tail_even {α : Type u} (s : Stream' α) :
    s.even.tail = s.tail.tail.even
    theorem Stream'.even_cons_cons {α : Type u} (a₁ : α) (a₂ : α) (s : Stream' α) :
    (Stream'.cons a₁ (Stream'.cons a₂ s)).even = Stream'.cons a₁ s.even
    theorem Stream'.even_tail {α : Type u} (s : Stream' α) :
    s.tail.even = s.odd
    theorem Stream'.even_interleave {α : Type u} (s₁ : Stream' α) (s₂ : Stream' α) :
    (s₁ s₂).even = s₁
    theorem Stream'.interleave_even_odd {α : Type u} (s₁ : Stream' α) :
    s₁.even s₁.odd = s₁
    theorem Stream'.get_even {α : Type u} (n : ) (s : Stream' α) :
    s.even.get n = s.get (2 * n)
    theorem Stream'.get_odd {α : Type u} (n : ) (s : Stream' α) :
    s.odd.get n = s.get (2 * n + 1)
    theorem Stream'.mem_of_mem_even {α : Type u} (a : α) (s : Stream' α) :
    a s.evena s
    theorem Stream'.mem_of_mem_odd {α : Type u} (a : α) (s : Stream' α) :
    a s.odda 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' α) :
    Stream'.drop l.length (l ++ₛ s) = s
    theorem Stream'.append_stream_head_tail {α : Type u} (s : Stream' α) :
    [s.head] ++ₛ s.tail = s
    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' α) :
    theorem Stream'.take_succ {α : Type u} (n : ) (s : Stream' α) :
    Stream'.take n.succ s = s.head :: Stream'.take n s.tail
    @[simp]
    theorem Stream'.take_succ_cons {α : Type u} {a : α} (n : ) (s : Stream' α) :
    theorem Stream'.take_succ' {α : Type u} {s : Stream' α} (n : ) :
    Stream'.take (n + 1) s = Stream'.take n s ++ [s.get n]
    @[simp]
    theorem Stream'.length_take {α : Type u} (n : ) (s : Stream' α) :
    (Stream'.take n s).length = n
    @[simp]
    theorem Stream'.take_take {α : Type u} {s : Stream' α} {m : } {n : } :
    @[simp]
    theorem Stream'.concat_take_get {α : Type u} {n : } {s : Stream' α} :
    Stream'.take n s ++ [s.get n] = Stream'.take (n + 1) s
    theorem Stream'.get?_take {α : Type u} {s : Stream' α} {k : } {n : } :
    k < n(Stream'.take n s).get? k = some (s.get k)
    theorem Stream'.get?_take_succ {α : Type u} (n : ) (s : Stream' α) :
    (Stream'.take n.succ s).get? n = some (s.get n)
    @[simp]
    theorem Stream'.dropLast_take {α : Type u} {n : } {xs : Stream' α} :
    (Stream'.take n xs).dropLast = Stream'.take (n - 1) xs
    @[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 : α) :
    theorem Stream'.tails_eq {α : Type u} (s : Stream' α) :
    s.tails = Stream'.cons s.tail s.tail.tails
    @[simp]
    theorem Stream'.get_tails {α : Type u} (n : ) (s : Stream' α) :
    s.tails.get n = Stream'.drop n s.tail
    theorem Stream'.tails_eq_iterate {α : Type u} (s : Stream' α) :
    s.tails = Stream'.iterate Stream'.tail s.tail
    theorem Stream'.inits_core_eq {α : Type u} (l : List α) (s : Stream' α) :
    theorem Stream'.tail_inits {α : Type u} (s : Stream' α) :
    s.inits.tail = Stream'.initsCore [s.head, s.tail.head] s.tail.tail
    theorem Stream'.inits_tail {α : Type u} (s : Stream' α) :
    s.tail.inits = Stream'.initsCore [s.tail.head] s.tail.tail
    theorem Stream'.cons_get_inits_core {α : Type u} (a : α) (n : ) (l : List α) (s : Stream' α) :
    a :: (Stream'.initsCore l s).get n = (Stream'.initsCore (a :: l) s).get n
    @[simp]
    theorem Stream'.get_inits {α : Type u} (n : ) (s : Stream' α) :
    s.inits.get n = Stream'.take n.succ s
    theorem Stream'.inits_eq {α : Type u} (s : Stream' α) :
    s.inits = Stream'.cons [s.head] (Stream'.map (List.cons s.head) s.tail.inits)
    theorem Stream'.zip_inits_tails {α : Type u} (s : Stream' α) :
    Stream'.zip Stream'.appendStream' s.inits s.tails = 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' α) :
    theorem Stream'.get_nats (n : ) :
    Stream'.nats.get n = n