Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
! This file was ported from Lean 3 source module data.stream.init
! leanprover-community/mathlib commit 207cfac9fcd06138865b5d04f7091e46d9320432
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Std.Tactic.Ext
import Mathlib.Data.Stream.Defs
import Mathlib.Logic.Function.Basic
import Mathlib.Init.Data.List.Basic
import Mathlib.Data.List.Basic
/-!
# 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. -/
open Nat Function Option
namespace Stream'
variable { α : Type u } { β : Type v } { δ : Type w }
instance [ Inhabited : Sort ?u.14 → Sort (max1?u.14) α ] : Inhabited : Sort ?u.17 → Sort (max1?u.17) ( Stream' α ) :=
⟨ Stream'.const default ⟩
protected theorem eta ( s : Stream' α ) : ( head s :: tail s ) = s :=
funext : ∀ {α : Sort ?u.1149} {β : α → Sort ?u.1148f g : (x : α ) → β x }, (∀ (x : α ), f x = g x ) → f = g fun i => by cases i <;> rfl
#align stream.eta Stream'.eta
@[ ext ]
protected theorem ext { s₁ s₂ : Stream' α } : (∀ n , nth s₁ n = nth s₂ n ) → s₁ = s₂ :=
fun h => funext : ∀ {α : Sort ?u.1286} {β : α → Sort ?u.1285f g : (x : α ) → β x }, (∀ (x : α ), f x = g x ) → f = g h
#align stream.ext Stream'.ext
@[ simp ]
theorem nth_zero_cons ( a : α ) ( s : Stream' α ) : nth ( a :: s ) 0 = a :=
rfl : ∀ {α : Sort ?u.2247} {a : α }, a = a
#align stream.nth_zero_cons Stream'.nth_zero_cons
@[ simp ]
theorem head_cons ( a : α ) ( s : Stream' α ) : head ( a :: s ) = a :=
rfl : ∀ {α : Sort ?u.3204} {a : α }, a = a
#align stream.head_cons Stream'.head_cons
@[ simp ]
theorem tail_cons ( a : α ) ( s : Stream' α ) : tail ( a :: s ) = s :=
rfl : ∀ {α : Sort ?u.4163} {a : α }, a = a
#align stream.tail_cons Stream'.tail_cons
@[ simp ]
theorem nth_drop ( n m : Nat ) ( s : Stream' α ) : nth ( drop m s ) n = nth s ( n + m ) :=
rfl : ∀ {α : Sort ?u.4284} {a : α }, a = a
#align stream.nth_drop Stream'.nth_drop
theorem tail_eq_drop ( s : Stream' α ) : tail s = drop 1 s :=
rfl : ∀ {α : Sort ?u.4363} {a : α }, a = a
#align stream.tail_eq_drop Stream'.tail_eq_drop
@[ simp ]
theorem drop_drop ( n m : Nat ) ( s : Stream' α ) : drop n ( drop m s ) = drop ( n + m ) s := by
ext ; simp [ Nat.add_assoc : ∀ (n m k : ℕ ), n + m + k = n + (m + k ]
#align stream.drop_drop Stream'.drop_drop
@[ simp ] theorem nth_tail { s : Stream' α } : s . tail . nth n = s . nth ( n + 1 ) := rfl : ∀ {α : Sort ?u.4707} {a : α }, a = a
@[ simp ] theorem tail_drop' { s : Stream' α } : tail ( drop i s ) = s . drop ( i + 1 ) := by
ext ; simp [ add_comm , add_assoc , add_left_comm ]
@[ simp ] theorem drop_tail' { s : Stream' α } : drop i ( tail s ) = s . drop ( i + 1 ) := rfl : ∀ {α : Sort ?u.5329} {a : α }, a = a
theorem tail_drop ( n : Nat ) ( s : Stream' α ) : tail ( drop n s ) = drop n ( tail s ) := by simp
#align stream.tail_drop Stream'.tail_drop
theorem nth_succ ( n : Nat ) ( s : Stream' α ) : nth s ( succ n ) = nth ( tail s ) n :=
rfl : ∀ {α : Sort ?u.5561} {a : α }, a = a
#align stream.nth_succ Stream'.nth_succ
@[ simp ]
theorem nth_succ_cons ( n : Nat ) ( s : Stream' α ) ( x : α ) : nth ( x :: s ) n . succ = nth s n :=
rfl : ∀ {α : Sort ?u.6518} {a : α }, a = a
#align stream.nth_succ_cons Stream'.nth_succ_cons
@[ simp ] theorem drop_zero { s : Stream' α } : s . drop 0 = s := rfl : ∀ {α : Sort ?u.6606} {a : α }, a = a
theorem drop_succ ( n : Nat ) ( s : Stream' α ) : drop ( succ n ) s = drop n ( tail s ) :=
rfl : ∀ {α : Sort ?u.6671} {a : α }, a = a
#align stream.drop_succ Stream'.drop_succ
theorem head_drop ( a : Stream' α ) ( n : ℕ ) : ( a . drop n ). head = a . nth n := by simp
#align stream.head_drop Stream'.head_drop
theorem cons_injective2 : Function.Injective2 : {α : Sort ?u.6882} → {β : Sort ?u.6881} → {γ : Sort ?u.6880} → (α → β → γ Prop ( cons : α → Stream' α → Stream' α ) := fun x y s t h =>
⟨ by rw [ ← nth_zero_cons x s , h , nth_zero_cons ] ,
Stream'.ext fun n => by rw [ ← nth_succ_cons n _ x , h , nth_succ_cons ] ⟩
#align stream.cons_injective2 Stream'.cons_injective2
theorem cons_injective_left ( s : Stream' α ) : Function.Injective : {α : Sort ?u.7030} → {β : Sort ?u.7029} → (α → β Prop fun x => cons x s :=
cons_injective2 . left _
#align stream.cons_injective_left Stream'.cons_injective_left
theorem cons_injective_right ( x : α ) : Function.Injective : {α : Sort ?u.7097} → {β : Sort ?u.7096} → (α → β Prop ( cons x ) :=
cons_injective2 . right _
#align stream.cons_injective_right Stream'.cons_injective_right
theorem all_def ( p : α → Prop ) ( s : Stream' α ) : All p s = ∀ n , p ( nth s n ) :=
rfl : ∀ {α : Sort ?u.7184} {a : α }, a = a
#align stream.all_def Stream'.all_def
theorem any_def ( p : α → Prop ) ( s : Stream' α ) : Any p s = ∃ n , p ( nth s n ) :=
rfl : ∀ {α : Sort ?u.7230} {a : α }, a = a
#align stream.any_def Stream'.any_def
@[ simp ]
theorem mem_cons ( a : α ) ( s : Stream' α ) : a ∈ a :: s :=
Exists.intro : ∀ {α : Sort ?u.8183} {p : α → Prop w : α ), p w Exists p 0 rfl : ∀ {α : Sort ?u.8203} {a : α }, a = a
#align stream.mem_cons Stream'.mem_cons
theorem mem_cons_of_mem : ∀ {α : Type u} {a : α } {s : Stream' α b : α ), a ∈ s a ∈ b :: s mem_cons_of_mem { a : α } { s : Stream' α } ( b : α ) : a ∈ s → a ∈ b :: s := fun ⟨ n , h : (fun b => a = b ) (nth s n h ⟩ =>
Exists.intro : ∀ {α : Sort ?u.9245} {p : α → Prop w : α ), p w Exists p ( succ n ) ( by rw [ nth_succ , tail_cons , (fun b => a = b ) (nth s n h : (fun b => a = b ) (nth s n h ] )
#align stream.mem_cons_of_mem Stream'.mem_cons_of_mem : ∀ {α : Type u} {a : α } {s : Stream' α b : α ), a ∈ s a ∈ b :: s
theorem eq_or_mem_of_mem_cons : ∀ {α : Type u} {a b : α } {s : Stream' α a ∈ b :: s a = b ∨ a ∈ s eq_or_mem_of_mem_cons { a b : α } { s : Stream' α } : ( a ∈ b :: s ) → a = b ∨ a ∈ s :=
fun ⟨ n , h : (fun b => a = b ) (nth (b :: s n h ⟩ => by
cases' n with n'
· left
exact h
· right
rw [ nth_succ , tail_cons ] at h
exact ⟨ n' , h ⟩
#align stream.eq_or_mem_of_mem_cons Stream'.eq_or_mem_of_mem_cons : ∀ {α : Type u} {a b : α } {s : Stream' α a ∈ b :: s a = b ∨ a ∈ s
theorem mem_of_nth_eq : ∀ {n : ℕ } {s : Stream' α a : α }, a = nth s n a ∈ s mem_of_nth_eq { n : Nat } { s : Stream' α } { a : α } : a = nth s n → a ∈ s := fun h =>
Exists.intro : ∀ {α : Sort ?u.10674} {p : α → Prop w : α ), p w Exists p n h
#align stream.mem_of_nth_eq Stream'.mem_of_nth_eq : ∀ {α : Type u} {n : ℕ } {s : Stream' α a : α }, a = nth s n a ∈ s
section Map
variable ( f : α → β )
theorem drop_map ( n : Nat ) ( s : Stream' α ) : drop n ( map f s ) = map f ( drop n s ) :=
Stream'.ext fun _ => rfl : ∀ {α : Sort ?u.10763} {a : α }, a = a
#align stream.drop_map Stream'.drop_map
@[ simp ]
theorem nth_map ( n : Nat ) ( s : Stream' α ) : nth ( map f s ) n = f ( nth s n ) :=
rfl : ∀ {α : Sort ?u.10842} {a : α }, a = a
#align stream.nth_map Stream'.nth_map
theorem tail_map ( s : Stream' α ) : tail ( map f s ) = map f ( tail s ) := rfl : ∀ {α : Sort ?u.10921} {a : α }, a = a
#align stream.tail_map Stream'.tail_map
@[ simp ]
theorem head_map ( s : Stream' α ) : head ( map f s ) = f ( head s ) :=
rfl : ∀ {α : Sort ?u.10988} {a : α }, a = a
#align stream.head_map Stream'.head_map
theorem map_eq ( s : Stream' α ) : map f s = f ( head s ):: map f ( tail s ) := by
rw [ ← Stream'.eta ( map f s ), tail_map , head_map ]
#align stream.map_eq Stream'.map_eq
theorem map_cons ( a : α ) ( s : Stream' α ) : map f ( a :: s ) = f a :: map f s := by
rw [ ← Stream'.eta ( map f ( a :: s )), map_eq ] ; rfl
#align stream.map_cons Stream'.map_cons
@[ simp ]
theorem map_id ( s : Stream' α ) : map id : {α : Sort ?u.14847} → α → α s = s :=
rfl : ∀ {α : Sort ?u.14860} {a : α }, a = a
#align stream.map_id Stream'.map_id
@[ simp ]
theorem map_map ( g : β → δ ) ( f : α → β ) ( s : Stream' α ) : map g ( map f s ) = map ( g ∘ f ) s :=
rfl : ∀ {α : Sort ?u.14954} {a : α }, a = a
#align stream.map_map Stream'.map_map
@[ simp ]
theorem map_tail ( s : Stream' α ) : map f ( tail s ) = tail ( map f s ) :=
rfl : ∀ {α : Sort ?u.15056} {a : α }, a = a
#align stream.map_tail Stream'.map_tail
theorem mem_map { a : α } { s : Stream' α } : a ∈ s → f a ∈ map f s := fun ⟨ n , h : (fun b => a = b ) (nth s n h ⟩ =>
Exists.intro : ∀ {α : Sort ?u.15227} {p : α → Prop w : α ), p w Exists p n ( by (fun b => f a = b ) (nth (map f s n rw [ (fun b => f a = b ) (nth (map f s n nth_map , (fun b => f a = b ) (f (nth s n (fun b => f a = b ) (nth (map f s n h : (fun b => a = b ) (nth s n h (fun b => f (nth s n = b ) (f (nth s n ] )
#align stream.mem_map Stream'.mem_map : ∀ {α : Type u} {β : Type v} (f : α → β a : α } {s : Stream' α a ∈ s f a ∈ map f s
theorem exists_of_mem_map : ∀ {α : Type u} {β : Type v} {f : α → β b : β } {s : Stream' α b ∈ map f s ∃ a , a ∈ s ∧ f a = b exists_of_mem_map { f } { b : β } { s : Stream' α } : b ∈ map f s → ∃ a , a ∈ s ∧ f a = b :=
fun ⟨ n , h : (fun b_1 => b = b_1 ) (nth (map f s n h ⟩ => ⟨ nth s n , ⟨ n , rfl : ∀ {α : Sort ?u.15510} {a : α }, a = a ⟩, h : (fun b_1 => b = b_1 ) (nth (map f s n h . symm : ∀ {α : Sort ?u.15516} {a b : α }, a = b b = a ⟩
#align stream.exists_of_mem_map Stream'.exists_of_mem_map : ∀ {α : Type u} {β : Type v} {f : α → β b : β } {s : Stream' α b ∈ map f s ∃ a , a ∈ s ∧ f a = b
end Map
section Zip
variable ( f : α → β → δ )
theorem drop_zip ( n : Nat ) ( s₁ : Stream' α ) ( s₂ : Stream' β ) :
drop n ( zip f s₁ s₂ ) = zip f ( drop n s₁ ) ( drop n s₂ ) :=
Stream'.ext fun _ => rfl : ∀ {α : Sort ?u.15709} {a : α }, a = a
#align stream.drop_zip Stream'.drop_zip
@[ simp ]
theorem nth_zip ( n : Nat ) ( s₁ : Stream' α ) ( s₂ : Stream' β ) :
nth ( zip f s₁ s₂ ) n = f ( nth s₁ n ) ( nth s₂ n ) :=
rfl : ∀ {α : Sort ?u.15823} {a : α }, a = a
#align stream.nth_zip Stream'.nth_zip
theorem head_zip ( s₁ : Stream' α ) ( s₂ : Stream' β ) : head ( zip f s₁ s₂ ) = f ( head s₁ ) ( head s₂ ) :=
rfl : ∀ {α : Sort ?u.15918} {a : α }, a = a
#align stream.head_zip Stream'.head_zip
theorem tail_zip ( s₁ : Stream' α ) ( s₂ : Stream' β ) :
tail ( zip f s₁ s₂ ) = zip f ( tail s₁ ) ( tail s₂ ) :=
rfl : ∀ {α : Sort ?u.16004} {a : α }, a = a
#align stream.tail_zip Stream'.tail_zip
theorem zip_eq ( s₁ : Stream' α ) ( s₂ : Stream' β ) :
zip f s₁ s₂ = f ( head s₁ ) ( head s₂ ):: zip f ( tail s₁ ) ( tail s₂ ) := by
rw [ ← Stream'.eta ( zip f s₁ s₂ ) ] ; rfl
#align stream.zip_eq Stream'.zip_eq
@[ simp ]
theorem nth_enum ( s : Stream' α ) ( n : ℕ ) : nth ( enum s ) n = ( n , s . nth n ) :=
rfl : ∀ {α : Sort ?u.17192} {a : α }, a = a
#align stream.nth_enum Stream'.nth_enum
theorem enum_eq_zip ( s : Stream' α ) : enum s = zip Prod.mk : {α : Type ?u.17246} → {β : Type ?u.17245} → α → β → α × β nats s :=
rfl : ∀ {α : Sort ?u.17264} {a : α }, a = a
#align stream.enum_eq_zip Stream'.enum_eq_zip
end Zip
@[ simp ]
theorem mem_const ( a : α ) : a ∈ const a :=
Exists.intro : ∀ {α : Sort ?u.17320} {p : α → Prop w : α ), p w Exists p 0 rfl : ∀ {α : Sort ?u.17340} {a : α }, a = a
#align stream.mem_const Stream'.mem_const : ∀ {α : Type u} (a : α ), a ∈ const a
theorem const_eq ( a : α ) : const a = a :: const a := by
apply Stream'.ext ; intro n
cases n <;> rfl
#align stream.const_eq Stream'.const_eq
@[ simp ]
theorem tail_const ( a : α ) : tail ( const a ) = const a :=
suffices tail ( a :: const a ) = const a by rwa [ ← const_eq ] at this
rfl : ∀ {α : Sort ?u.19332} {a : α }, a = a
#align stream.tail_const Stream'.tail_const
@[ simp ]
theorem map_const ( f : α → β ) ( a : α ) : map f ( const a ) = const ( f a ) :=
rfl : ∀ {α : Sort ?u.19448} {a : α }, a = a
#align stream.map_const Stream'.map_const
@[ simp ]
theorem nth_const ( n : Nat ) ( a : α ) : nth ( const a ) n = a :=
rfl : ∀ {α : Sort ?u.19502} {a : α }, a = a
#align stream.nth_const Stream'.nth_const : ∀ {α : Type u} (n : ℕ ) (a : α ), nth (const a n = a
@[ simp ]
theorem drop_const ( n : Nat ) ( a : α ) : drop n ( const a ) = const a :=
Stream'.ext fun _ => rfl : ∀ {α : Sort ?u.19562} {a : α }, a = a
#align stream.drop_const Stream'.drop_const
@[ simp ]
theorem head_iterate ( f : α → α ) ( a : α ) : head ( iterate f a ) = a :=
rfl : ∀ {α : Sort ?u.19619} {a : α }, a = a
#align stream.head_iterate Stream'.head_iterate : ∀ {α : Type u} (f : α → α a : α ), head (iterate f a = a
theorem nth_succ_iterate' ( n : Nat ) ( f : α → α ) ( a : α ) :
nth ( iterate f a ) ( succ n ) = f ( nth ( iterate f a ) n ) := rfl : ∀ {α : Sort ?u.19695} {a : α }, a = a
theorem tail_iterate ( f : α → α ) ( a : α ) : tail ( iterate f a ) = iterate f ( f a ) := by
ext n
rw [ nth_tail ]
induction' n with n' ih
· rfl
· rw [ nth_succ_iterate' , ih , nth_succ_iterate' ]
#align stream.tail_iterate Stream'.tail_iterate
theorem iterate_eq ( f : α → α ) ( a : α ) : iterate f a = a :: iterate f ( f a ) := by
rw [ ← Stream'.eta ( iterate f a ) ]
rw [ tail_iterate ] ; rfl
#align stream.iterate_eq Stream'.iterate_eq
@[ simp ]
theorem nth_zero_iterate : ∀ {α : Type u} (f : α → α a : α ), nth (iterate f a 0 = a nth_zero_iterate ( f : α → α ) ( a : α ) : nth ( iterate f a ) 0 = a :=
rfl : ∀ {α : Sort ?u.20995} {a : α }, a = a
#align stream.nth_zero_iterate Stream'.nth_zero_iterate : ∀ {α : Type u} (f : α → α a : α ), nth (iterate f a 0 = a
theorem nth_succ_iterate ( n : Nat ) ( f : α → α ) ( a : α ) :
nth ( iterate f a ) ( succ n ) = nth ( iterate f ( f a )) n := by rw [ nth_succ , tail_iterate ]
#align stream.nth_succ_iterate Stream'.nth_succ_iterate
section Bisim
variable ( R : Stream' α → Stream' α → Prop )
/-- equivalence relation -/
local infixl :50 " ~ " => R
/-- Streams `s₁` and `s₂` are defined to be bisimulations if
their heads are equal and tails are bisimulations. -/
def IsBisimulation :=
∀ ⦃ s₁ s₂ ⦄, s₁ ~ s₂ →
head s₁ = head s₂ ∧ tail s₁ ~ tail s₂
#align stream.is_bisimulation Stream'.IsBisimulation
theorem nth_of_bisim ( bisim : IsBisimulation R ) :
∀ { s₁ s₂ } ( n ), s₁ ~ s₂ → nth s₁ n = nth s₂ n ∧ drop ( n + 1 ) s₁ ~ drop ( n + 1 ) s₂
| _, _, 0 , h => bisim h
| _, _, n + 1, h =>
match bisim h with
| ⟨_, trel ⟩ => nth_of_bisim bisim n trel
#align stream.nth_of_bisim Stream'.nth_of_bisim
-- If two streams are bisimilar, then they are equal
theorem eq_of_bisim ( bisim : IsBisimulation R ) : ∀ { s₁ s₂ }, s₁ ~ s₂ → s₁ = s₂ := fun r =>
Stream'.ext fun n => And.left : ∀ {a b : Prop }, a ∧ b a ( nth_of_bisim R bisim n r )
#align stream.eq_of_bisim Stream'.eq_of_bisim
end Bisim
theorem bisim_simple ( s₁ s₂ : Stream' α ) :
head s₁ = head s₂ → s₁ = tail s₁ → s₂ =