Possibly infinite lists

This file provides Stream'.Seq α, a type representing possibly infinite lists (referred here as sequences). It is encoded as an infinite stream of options such that if f n = none, then f m = none for all m ≥ n.

Main definitions

• Seq α: The type of possibly infinite lists (sequences) encoded as streams of options. It is encoded as Stream' (Option α) such that if f n = none, then f m = none for all m ≥ n. It has two "constructors": nil and cons, and a destructor destruct.
• Seq1 α: The type of nonempty sequences
• Seq.get?: Extract the nth element of a sequence (if it exists).
• Seq.corec: Corecursion principle for Seq α as a coinductive type.
• Seq.Terminates: Predicate for when a sequence is finite.

One can convert between sequences and other types: List, Stream', MLList using corresponding functions defined in this file.

There are also a number of operations and predicates on sequences mirroring those on lists: Seq.map, Seq.zip, Seq.zipWith, Seq.unzip, Seq.fold, Seq.update, Seq.drop, Seq.splitAt, Seq.append, Seq.join, Seq.enum, Seq.Pairwire, as well as a cases principle Seq.recOn which allows one to reason about sequences by cases (nil and cons).

Main statements

• eq_of_bisim: Bisimulation principle for sequences.

def Stream'.IsSeq {α : Type u} (s : Stream' (Option α)) : Prop

A stream s : Option α is a sequence if s.get n = none implies s.get (n + 1) = none.

def Stream'.Seq (α : Type u) : Type u

Seq α is the type of possibly infinite lists (referred here as sequences). It is encoded as an infinite stream of options such that if f n = none, then f m = none for all m ≥ n.

def Stream'.Seq1 (α : Type u_1) : Type u_1

Seq1 α is the type of nonempty sequences.

def Stream'.Seq.get? {α : Type u} : Seq α → ℕ → Option α

Get the nth element of a sequence (if it exists)

@[simp]

theorem Stream'.Seq.val_eq_get {α : Type u} (s : Seq α) (n : ℕ) : ↑s n = s.get? n

@[simp]

theorem Stream'.Seq.get?_mk {α : Type u} (f : Stream' (Option α)) (hf : f.IsSeq) : get? ⟨f, hf⟩ = f

theorem Stream'.Seq.le_stable {α : Type u} (s : Seq α) {m n : ℕ} (h : m ≤ n) : s.get? m = none → s.get? n = none

theorem Stream'.Seq.ge_stable {α : Type u} (s : Seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n) (s_nth_eq_some : s.get? n = some aₙ) : ∃ (aₘ : α), s.get? m = some aₘ

If s.get? n = some aₙ for some value aₙ, then there is also some value aₘ such that s.get? = some aₘ for m ≤ n.

theorem Stream'.Seq.ext {α : Type u} {s t : Seq α} (h : ∀ (n : ℕ), s.get? n = t.get? n) : s = t

theorem Stream'.Seq.ext_iff {α : Type u} {s t : Seq α} : s = t ↔ ∀ (n : ℕ), s.get? n = t.get? n

Constructors

def Stream'.Seq.nil {α : Type u} : Seq α

The empty sequence

instance Stream'.Seq.instInhabited {α : Type u} : Inhabited (Seq α)

def Stream'.Seq.cons {α : Type u} (a : α) (s : Seq α) : Seq α

Prepend an element to a sequence

@[simp]

theorem Stream'.Seq.val_cons {α : Type u} (s : Seq α) (x : α) : ↑(cons x s) = Stream'.cons (some x) ↑s

@[simp]

theorem Stream'.Seq.get?_nil {α : Type u} (n : ℕ) : nil.get? n = none

@[simp]

theorem Stream'.Seq.get?_zero_eq_none {α : Type u} {s : Seq α} : s.get? 0 = none ↔ s = nil

@[simp]

theorem Stream'.Seq.get?_cons_zero {α : Type u} (a : α) (s : Seq α) : (cons a s).get? 0 = some a

@[simp]

theorem Stream'.Seq.get?_cons_succ {α : Type u} (a : α) (s : Seq α) (n : ℕ) : (cons a s).get? (n + 1) = s.get? n

@[simp]

theorem Stream'.Seq.cons_ne_nil {α : Type u} {x : α} {s : Seq α} : cons x s ≠ nil

@[simp]

theorem Stream'.Seq.nil_ne_cons {α : Type u} {x : α} {s : Seq α} : nil ≠ cons x s

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

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

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

@[simp]

theorem Stream'.Seq.cons_eq_cons {α : Type u} {x x' : α} {s s' : Seq α} : cons x s = cons x' s' ↔ x = x' ∧ s = s'

Destructors

def Stream'.Seq.head {α : Type u} (s : Seq α) : Option α

Get the first element of a sequence

def Stream'.Seq.tail {α : Type u} (s : Seq α) : Seq α

Get the tail of a sequence (or nil if the sequence is nil)

def Stream'.Seq.destruct {α : Type u} (s : Seq α) : Option (Seq1 α)

Destructor for a sequence, resulting in either none (for nil) or some (a, s) (for cons a s).

theorem Stream'.Seq.head_eq_destruct {α : Type u} (s : Seq α) : s.head = Prod.fst <$> s.destruct

@[simp]

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

@[simp]

theorem Stream'.Seq.destruct_nil {α : Type u} : nil.destruct = none

@[simp]

theorem Stream'.Seq.destruct_cons {α : Type u} (a : α) (s : Seq α) : (cons a s).destruct = some (a, s)

theorem Stream'.Seq.destruct_eq_none {α : Type u} {s : Seq α} : s.destruct = none → s = nil

theorem Stream'.Seq.destruct_eq_cons {α : Type u} {s : Seq α} {a : α} {s' : Seq α} : s.destruct = some (a, s') → s = cons a s'

@[simp]

theorem Stream'.Seq.head_nil {α : Type u} : nil.head = none

@[simp]

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

@[simp]

theorem Stream'.Seq.tail_nil {α : Type u} : nil.tail = nil

@[simp]

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

theorem Stream'.Seq.head_eq_some {α : Type u} {s : Seq α} {x : α} (h : s.head = some x) : s = cons x s.tail

theorem Stream'.Seq.head_eq_none {α : Type u} {s : Seq α} (h : s.head = none) : s = nil

@[simp]

theorem Stream'.Seq.head_eq_none_iff {α : Type u} {s : Seq α} : s.head = none ↔ s = nil

Recursion and corecursion principles

def Stream'.Seq.recOn {α : Type u} {motive : Seq α → Sort v} (s : Seq α) (nil : motive nil) (cons : (x : α) → (s : Seq α) → motive (cons x s)) : motive s

Recursion principle for sequences, compare with List.recOn.

def Stream'.Seq.omap {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) : Option (α × β) → Option (α × γ)

Functorial action of the functor Option (α × _)

def Stream'.Seq.Corec.f {α : Type u} {β : Type v} (f : β → Option (α × β)) : Option β → Option α × Option β

Corecursor over pairs of Option values

def Stream'.Seq.corec {α : Type u} {β : Type v} (f : β → Option (α × β)) (b : β) : Seq α

Corecursor for Seq α as a coinductive type. Iterates f to produce new elements of the sequence until none is obtained.

@[simp]

theorem Stream'.Seq.corec_eq {α : Type u} {β : Type v} (f : β → Option (α × β)) (b : β) : (corec f b).destruct = omap (corec f) (f b)

theorem Stream'.Seq.corec_nil {α : Type u} {β : Type v} (f : β → Option (α × β)) (b : β) (h : f b = none) : corec f b = nil

theorem Stream'.Seq.corec_cons {α : Type u} {β : Type v} {f : β → Option (α × β)} {b : β} {x : α} {s : β} (h : f b = some (x, s)) : corec f b = cons x (corec f s)

Bisimulation

def Stream'.Seq.BisimO {α : Type u} (R : Seq α → Seq α → Prop) : Option (Seq1 α) → Option (Seq1 α) → Prop

Bisimilarity relation over Option of Seq1 α

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

a relation is bisimilar if it meets the BisimO test

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

If two streams are bisimilar, then they are equal. There are also versions eq_of_bisim' and eq_of_bisim_strong that does not mention IsBisimulation and look more like an induction principles.

theorem Stream'.Seq.eq_of_bisim' {α : Type u} {s₁ s₂ : Seq α} (motive : Seq α → Seq α → Prop) (base : motive s₁ s₂) (step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ (x : α) (s₁' : Seq α) (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂') : s₁ = s₂

Coinductive principle for equality on sequences. This is a version of eq_of_bisim that looks more like an induction principle.

theorem Stream'.Seq.eq_of_bisim_strong {α : Type u} {s₁ s₂ : Seq α} (motive : Seq α → Seq α → Prop) (base : motive s₁ s₂) (step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ (x : α) (s₁' : Seq α) (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂') : s₁ = s₂

Coinductive principle for equality on sequences. This is a version of eq_of_bisim' that requires proving only s₁ = s₂ instead of s₁ = nil ∧ s₂ = nil in step.

theorem Stream'.Seq.coinduction {α : Type u} {s₁ s₂ : Seq α} : s₁.head = s₂.head → (∀ (β : Type u) (fr : Seq α → β), fr s₁ = fr s₂ → fr s₁.tail = fr s₂.tail) → s₁ = s₂

theorem Stream'.Seq.coinduction2 {α : Type u} {β : Type v} (s : Seq α) (f g : Seq α → Seq β) (H : ∀ (s : Seq α), BisimO (fun (s1 s2 : Seq β) => ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct) : f s = g s

Termination

def Stream'.Seq.TerminatedAt {α : Type u} (s : Seq α) (n : ℕ) : Prop

A sequence has terminated at position n if the value at position n equals none.

instance Stream'.Seq.terminatedAtDecidable {α : Type u} (s : Seq α) (n : ℕ) : Decidable (s.TerminatedAt n)

It is decidable whether a sequence terminates at a given position.

def Stream'.Seq.Terminates {α : Type u} (s : Seq α) : Prop

A sequence terminates if there is some position n at which it has terminated.

def Stream'.Seq.length {α : Type u} (s : Seq α) (h : s.Terminates) : ℕ

The length of a terminating sequence.

noncomputable def Stream'.Seq.length' {α : Type u} (s : Seq α) : ℕ∞

The ENat-valued length of a sequence. For non-terminating sequences, it is ⊤.

theorem Stream'.Seq.terminated_stable {α : Type u} (s : Seq α) {m n : ℕ} : m ≤ n → s.TerminatedAt m → s.TerminatedAt n

If a sequence terminated at position n, it also terminated at m ≥ n.

theorem Stream'.Seq.not_terminates_iff {α : Type u} {s : Seq α} : ¬s.Terminates ↔ ∀ (n : ℕ), (s.get? n).isSome = true

theorem Stream'.Seq.terminatedAt_nil {α : Type u} {n : ℕ} : nil.TerminatedAt n

@[simp]

theorem Stream'.Seq.cons_not_terminatedAt_zero {α : Type u} {x : α} {s : Seq α} : ¬(cons x s).TerminatedAt 0

@[simp]

theorem Stream'.Seq.cons_terminatedAt_succ_iff {α : Type u} {x : α} {s : Seq α} {n : ℕ} : (cons x s).TerminatedAt (n + 1) ↔ s.TerminatedAt n

@[simp]

theorem Stream'.Seq.terminates_nil {α : Type u} : nil.Terminates

@[simp]

theorem Stream'.Seq.terminates_cons_iff {α : Type u} {x : α} {s : Seq α} : (cons x s).Terminates ↔ s.Terminates

theorem Stream'.Seq.terminatedAt_zero_iff {α : Type u} {s : Seq α} : s.TerminatedAt 0 ↔ s = nil

Membership

def Stream'.Seq.Mem {α : Type u} (s : Seq α) (a : α) : Prop

member definition for Seq

instance Stream'.Seq.instMembership {α : Type u} : Membership α (Seq α)

theorem Stream'.Seq.get?_mem {α : Type u} {s : Seq α} {n : ℕ} {x : α} (h : s.get? n = some x) : x ∈ s

theorem Stream'.Seq.mem_iff_exists_get? {α : Type u} {s : Seq α} {x : α} : x ∈ s ↔ ∃ (i : ℕ), some x = s.get? i

@[simp]

theorem Stream'.Seq.notMem_nil {α : Type u} (a : α) : a ∉ nil

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

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

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

@[simp]

theorem Stream'.Seq.mem_cons_iff {α : Type u} {a b : α} {s : Seq α} : a ∈ cons b s ↔ a = b ∨ a ∈ s

theorem Stream'.Seq.mem_rec_on {α : Type u} {C : Seq α → Prop} {a : α} {s : Seq α} (M : a ∈ s) (h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')) : C s

Converting from/to other types

def Stream'.Seq.ofList {α : Type u} (l : List α) : Seq α

Embed a list as a sequence

instance Stream'.Seq.coeList {α : Type u} : Coe (List α) (Seq α)

@[simp]

theorem Stream'.Seq.ofList_nil {α : Type u} : ↑[] = nil

@[simp]

theorem Stream'.Seq.ofList_get? {α : Type u} (l : List α) (n : ℕ) : (↑l).get? n = l[n]?

@[simp]

theorem Stream'.Seq.ofList_cons {α : Type u} (a : α) (l : List α) : ↑(a :: l) = cons a ↑l

theorem Stream'.Seq.ofList_injective {α : Type u} : Function.Injective ofList

def Stream'.Seq.ofStream {α : Type u} (s : Stream' α) : Seq α

Embed an infinite stream as a sequence

instance Stream'.Seq.coeStream {α : Type u} : Coe (Stream' α) (Seq α)

def Stream'.Seq.ofMLList {α : Type u} : MLList Id α → Seq α

Embed a MLList α as a sequence. Note that even though this is non-meta, it will produce infinite sequences if used with cyclic MLLists created by meta constructions.

instance Stream'.Seq.coeMLList {α : Type u} : Coe (MLList Id α) (Seq α)

unsafe def Stream'.Seq.toMLList {α : Type u} : Seq α → MLList Id α

Translate a sequence into a MLList.

unsafe def Stream'.Seq.forceToList {α : Type u} (s : Seq α) : List α

Translate a sequence to a list. This function will run forever if run on an infinite sequence.

def Stream'.Seq.take {α : Type u} : ℕ → Seq α → List α

Take the first n elements of the sequence (producing a list)

def Stream'.Seq.toList {α : Type u} (s : Seq α) (h : s.Terminates) : List α

Convert a sequence which is known to terminate into a list

def Stream'.Seq.toStream {α : Type u} (s : Seq α) (h : ¬s.Terminates) : Stream' α

Convert a sequence which is known not to terminate into a stream

def Stream'.Seq.toListOrStream {α : Type u} (s : Seq α) [Decidable s.Terminates] : List α ⊕ Stream' α

Convert a sequence into either a list or a stream depending on whether it is finite or infinite. (Without decidability of the infiniteness predicate, this is not constructively possible.)

def Stream'.Seq.toList' {α : Type u_1} (s : Seq α) : Computation (List α)

Convert a sequence into a list, embedded in a computation to allow for the possibility of infinite sequences (in which case the computation never returns anything).

Operations on sequences

def Stream'.Seq.append {α : Type u} (s₁ s₂ : Seq α) : Seq α

Append two sequences. If s₁ is infinite, then s₁ ++ s₂ = s₁, otherwise it puts s₂ at the location of the nil in s₁.

def Stream'.Seq.map {α : Type u} {β : Type v} (f : α → β) : Seq α → Seq β

Map a function over a sequence.

def Stream'.Seq.join {α : Type u} : Seq (Seq1 α) → Seq α

Flatten a sequence of sequences. (It is required that the sequences be nonempty to ensure productivity; in the case of an infinite sequence of nil, the first element is never generated.)

def Stream'.Seq.drop {α : Type u} (s : Seq α) : ℕ → Seq α

Remove the first n elements from the sequence.

def Stream'.Seq.splitAt {α : Type u} : ℕ → Seq α → List α × Seq α

Split a sequence at n, producing a finite initial segment and an infinite tail.

def Stream'.Seq.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s₁ : Seq α) (s₂ : Seq β) : Seq γ

Combine two sequences with a function

def Stream'.Seq.zip {α : Type u} {β : Type v} : Seq α → Seq β → Seq (α × β)

Pair two sequences into a sequence of pairs

def Stream'.Seq.unzip {α : Type u} {β : Type v} (s : Seq (α × β)) : Seq α × Seq β

Separate a sequence of pairs into two sequences

def Stream'.Seq.nats : Seq ℕ

The sequence of natural numbers some 0, some 1, ...

def Stream'.Seq.enum {α : Type u} (s : Seq α) : Seq (ℕ × α)

Enumerate a sequence by tagging each element with its index.

def Stream'.Seq.fold {α : Type u} {β : Type v} (s : Seq α) (init : β) (f : β → α → β) : Seq β

Folds a sequence using f, producing a sequence of intermediate values, i.e. [init, f init s.head, f (f init s.head) s.tail.head, ...].

def Stream'.Seq.update {α : Type u} (s : Seq α) (n : ℕ) (f : α → α) : Seq α

Applies f to the nth element of the sequence, if it exists, replacing that element with the result.

def Stream'.Seq.set {α : Type u} (s : Seq α) (n : ℕ) (a : α) : Seq α

Sets the value of sequence s at index n to a. If the nth element does not exist (s terminates earlier), the sequence is left unchanged.

def Stream'.Seq.Pairwise {α : Type u} (R : α → α → Prop) (s : Seq α) : Prop

Pairwise R s means that all the elements with earlier indices are R-related to all the elements with later indices.

Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3

For example if R = (· ≠ ·) then it asserts s has no duplicates, and if R = (· < ·) then it asserts that s is (strictly) sorted.