Productive weak sequences

This file defines the property of a weak sequence being productive as never stalling – the next output always comes after a finite time. Given a productive weak sequence, a regular sequence (Seq) can be derived from it using toSeq.

class Stream'.WSeq.Productive {α : Type u} (s : WSeq α) : Prop

A weak sequence is productive if it never stalls forever - there are always a finite number of thinks between cons constructors. The sequence itself is allowed to be infinite though.

• get?_terminates (n : ℕ) : (s.get? n).Terminates

theorem Stream'.WSeq.productive_iff {α : Type u} (s : WSeq α) : s.Productive ↔ ∀ (n : ℕ), (s.get? n).Terminates

instance Stream'.WSeq.get?_terminates {α : Type u} (s : WSeq α) [h : s.Productive] (n : ℕ) : (s.get? n).Terminates

instance Stream'.WSeq.head_terminates {α : Type u} (s : WSeq α) [s.Productive] : s.head.Terminates

instance Stream'.WSeq.productive_tail {α : Type u} (s : WSeq α) [s.Productive] : s.tail.Productive

instance Stream'.WSeq.productive_dropn {α : Type u} (s : WSeq α) [s.Productive] (n : ℕ) : (s.drop n).Productive

instance Stream'.WSeq.productive_ofSeq {α : Type u} (s : Seq α) : (↑s).Productive

theorem Stream'.WSeq.productive_congr {α : Type u} {s t : WSeq α} (h : s ~ʷ t) : s.Productive ↔ t.Productive

def Stream'.WSeq.toSeq {α : Type u} (s : WSeq α) [s.Productive] : Seq α

Given a productive weak sequence, we can collapse all the thinks to produce a sequence.

Equations

• s.toSeq = ⟨fun (n : ℕ) => (s.get? n).get, ⋯⟩

theorem Stream'.WSeq.toSeq_ofSeq {α : Type u} (s : Seq α) : (↑s).toSeq = s