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 slicesdef 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)
In the end, I just didn't want inductive finite lists.
No comments:
Post a Comment