Lazy Streams

 I did a small Lean experiment with lazy streams.  It failed, but I wanted to write it down anyway.

inductive Sequence (α : Type u) : Type u

| nil : Sequence α

| cons : α → (Unit → Sequence α) → Sequence α

Let's look at slices

def slice : Nat → Sequence α → List α

| 0, _ => []

| _, .nil => []

| n + 1, .cons a f => a :: slice n (f ())

and prove the following.

theorem sequence_extensionality {α : Type u} (s₁ s₂ : Sequence α) :

 (∀ n : Nat, slice n s₁ = slice n s₂) → s₁ = s₂ := by

    sorry

So far so good. But unfortunately, this models finite lists. On the following, Lean cannot prove termination.

def zeroes : Sequence Nat := Sequence.cons 0 (fun x => zeroes)

Moreover, falsum is trivially inhabited by induction. 

example (x : Sequence Nat) (h : x = .cons 0 (fun _ => x)) : False := by

induction x with

 | nil =>

contradiction

 | cons a f ih =>

     simp only [Sequence.cons.injEq] at h

     apply ih ()

     conv => lhs; rw [h.2]

     dsimp

     rw [h.1]

We could try the following, but it just results in finite lists.

def zeroes : Nat -> Sequence Nat

| 0 => .nil

| n + 1 => .cons 0 (fun _ => zeroes n)

End of experiment for me, I was just interested whether a formalization like this could work.