Coinductive lists (sequences) without using thunks

seq.lean

universes u v w

variable {α : Type u}

class seq_ty (α : Type u) :=
(data : Type v)
(destruct : data → option (α × data))

structure seq (α : Type u) : Type (max u (v+1)) :=
(pfx : list α)
(ty : seq_ty.{u v} α)
(ini : ty.data)

def destruct : Π (s : seq α), option (α × seq α)
| ⟨[], σ, v⟩ := match @seq_ty.destruct _ σ v with
  | some (a, v') := some (a, ⟨[], σ, v'⟩)
  | none := none
  end
| ⟨a::l, σ, v⟩ := some (a, ⟨l, σ, v⟩)

def head (s : seq α) : option α :=
match destruct s with some (a, s') := some a | none := none end

def tail (s : seq α) : option (seq α) :=
match destruct s with some (a, s') := some s' | none := none end

def of_list (l : list α) : seq α :=
⟨l, ⟨unit, λ_, none⟩, ()⟩

def nil : seq α := of_list []

def cons (a : α) : seq α → seq α
| ⟨l, σ, i⟩ := ⟨a :: l, σ, i⟩

def iterates (f : α → α) (a : α) : seq α :=
⟨[], ⟨α, λa', some (a', f a')⟩, a⟩

def iota (i : nat) : seq nat :=
iterates nat.succ i

def nth : seq α → nat → option α
| s 0     := head s
| s (n+1) := match destruct s with some (a, t) := nth t n | none := none end

def seq_eq_aux (r : seq α → seq α → Prop) : Π (d d' : option (α × seq α)), Prop
| (some (a, v)) (some (b, w)) := a = b ∧ r v w
| none          none          := true
| _             _             := false

def seq_eq (s t : seq α) : Prop :=
∃ (r : seq α → seq α → Prop), (∀ {s t}, r s t → seq_eq_aux r (destruct s) (destruct t)) ∧ r s t

def seq_eq_destruct {s t : seq α} : seq_eq s t → seq_eq_aux seq_eq (destruct s) (destruct t)
| ⟨r, h1, h2⟩ := match destruct s, destruct t, h1 h2, h2 with
  | some (a, v), some (b, w), ⟨ab, h'⟩, h2 := ⟨ab, ⟨r, @h1, h'⟩⟩
  | none, none, _, _ := trivial
  end

def seq_eq_nth : ∀ {s t : seq α} (h : seq_eq s t) n, nth s n = nth t n
| s t h 0 := by dsimp[nth, head]; exact match destruct s, destruct t, seq_eq_destruct h with
  | some (a, v), some (b, w), ⟨ab, h'⟩ := by dsimp[head]; rw ab
  | none, none, _ := rfl
  end
| s t h (n+1) := by dsimp[nth]; exact match destruct s, destruct t, seq_eq_destruct h with
  | some (a, v), some (b, w), ⟨ab, h'⟩ := by dsimp[nth]; exact seq_eq_nth h' n
  | none, none, _ := rfl
  end

def seq_eq_iff_nth {s t : seq α} : seq_eq s t ↔ ∀ n, nth s n = nth t n :=
⟨seq_eq_nth, λal, ⟨λs t, ∀ n, nth s n = nth t n, λs t al,
  match destruct s, destruct t, (by note t' := al 0; dsimp[nth, head] at t'; exact t'), (λn, by note t' := al (n+1); dsimp[nth] at t'; exact t') with
  | some (a, v), some (b, w), h0, hn := by dsimp[head] at h0; injection h0 with h0; exact ⟨h0, hn⟩
  | some (a, v), none,        h0, hn := by dsimp[head] at h0; contradiction
  | none,        some (b, w), h0, hn := by dsimp[head] at h0; contradiction
  | none,        none,        h0, hn := trivial
  end, al⟩⟩