coindpred.lean

import data.stream
universes u

/-

coinductive alternating : stream bool → Prop
| f : ∀ s, alternating (ff :: s) → alternating (tt :: ff :: s)
| t : ∀ s, alternating (tt :: s) → alternating (ff :: tt :: s)

-/

inductive alternating.funct (τ : stream bool → Prop) : stream bool → Prop
| f : ∀ s, τ (ff :: s) → alternating.funct (tt :: ff :: s)
| t : ∀ s, τ (tt :: s) → alternating.funct (ff :: tt :: s)

lemma alternating.funct.map {τ₁ τ₂ : stream bool → Prop} (f : ∀ s, τ₁ s → τ₂ s) :
    ∀ {s}, alternating.funct τ₁ s → alternating.funct τ₂ s
| ._ (alternating.funct.f s h) := alternating.funct.f s (f _ h)
| ._ (alternating.funct.t s h) := alternating.funct.t s (f _ h)

def alternating (s : stream bool) : Prop :=
∃ C : stream bool → Prop,
∃ step : ∀ s, C s → alternating.funct C s,
C s

def alternating.corec {C : stream bool → Prop}
    (step : ∀ s, C s → alternating.funct C s)
    (s : stream bool) (start : C s) : alternating s :=
⟨C, step, start⟩

lemma alternating.corec_on (C : stream bool → Prop)
    {s : stream bool} (start : C s)
    (step : ∀ s, C s → alternating.funct C s) : alternating s :=
alternating.corec step s start

lemma alternating.unfold {s : stream bool} : alternating s → alternating.funct alternating s
| ⟨C, step, start⟩ := alternating.funct.map (λ s h, alternating.corec_on C h step) (step _ start)

@[elab_as_eliminator]
lemma alternating.cases_on {C : stream bool → Prop}
    {s : stream bool} (p : alternating s)
    (cf : ∀ s, alternating (ff :: s) → C (tt :: ff :: s))
    (ct : ∀ s, alternating (tt :: s) → C (ff :: tt :: s)) :
    C s :=
by apply alternating.funct.cases_on (alternating.unfold p); assumption

lemma alternating.f (s : stream bool) (h : alternating (ff :: s)) : alternating (tt :: ff :: s) :=
alternating.corec_on (λ s', s' = tt :: ff :: s ∨ alternating s') (or.inl rfl)
begin
intros s' h', cases h',
case or.inl h' {subst h', apply alternating.funct.f, right, assumption},
case or.inr h' {apply alternating.funct.map _ (alternating.unfold h'), intros, apply or.inr, assumption},
end

lemma alternating.t (s : stream bool) (h : alternating (tt :: s)) : alternating (ff :: tt :: s) :=
alternating.corec_on (λ s', s' = ff :: tt :: s ∨ alternating s') (or.inl rfl)
begin
intros s' h', cases h',
case or.inl h' {subst h', apply alternating.funct.t, right, assumption},
case or.inr h' {apply alternating.funct.map _ (alternating.unfold h'), intros, apply or.inr, assumption},
end

namespace ex

def alt : bool → stream bool :=
stream.iterate bnot

lemma alt_eq (i) : alt i = i :: alt (bnot i) :=
begin change stream.iterate _ _ = _, rw stream.iterate_eq, refl end

lemma alternating_alt (i) : alternating (alt i) :=
alternating.corec_on (λ s, ∃ i, s = alt i)
    (show ∃ j, alt i = alt j, from ⟨_, rfl⟩)
    (take s : stream bool, assume h : ∃ j, s = alt j,
     begin
        cases h with j h, subst h,
        rw alt_eq, rw alt_eq,
        cases j; constructor; existsi _,
        {change tt :: alt (bnot tt) = _, rw -alt_eq},
        {change ff :: alt (bnot ff) = _, rw -alt_eq},
     end)

end ex

/-

coinductive bisim {α : Type u} : stream α → stream α → Prop
| cons : ∀ hd s₁ s₂, bisim s₁ s₂ → bisim (hd :: s₁) (hd :: s₂)

-/

inductive bisim.funct {α : Type u} (τ : stream α → stream α → Prop) : stream α → stream α → Prop
| cons : ∀ hd s₁ s₂, τ s₁ s₂ → bisim.funct (hd :: s₁) (hd :: s₂)

lemma bisim.funct.map {α : Type u} {τ₁ τ₂ : stream α → stream α → Prop}
    (f : ∀ s₁ s₂, τ₁ s₁ s₂ → τ₂ s₁ s₂) :
    ∀ {s₁ s₂ : stream α}, bisim.funct τ₁ s₁ s₂ → bisim.funct τ₂ s₁ s₂
| ._ ._ (bisim.funct.cons hd s₁ s₂ h) := bisim.funct.cons hd s₁ s₂ (f _ _ h)

def bisim {α} (s₁ s₂ : stream α) : Prop :=
∃ C : stream α → stream α → Prop,
∃ step : ∀ s₁ s₂, C s₁ s₂ → bisim.funct C s₁ s₂,
C s₁ s₂

def bisim.corec {α} {C : stream α → stream α → Prop}
    (step : ∀ s₁ s₂, C s₁ s₂ → bisim.funct C s₁ s₂)
    (s₁ s₂ : stream α) (start : C s₁ s₂) : bisim s₁ s₂ :=
⟨C, step, start⟩

lemma bisim.corec_on {α} (C : stream α → stream α → Prop)
    {s₁ s₂ : stream α} (start : C s₁ s₂)
    (step : ∀ s₁ s₂, C s₁ s₂ → bisim.funct C s₁ s₂) : bisim s₁ s₂ :=
bisim.corec step s₁ s₂ start

lemma bisim.unfold {α} {s₁ s₂ : stream α} : bisim s₁ s₂ → bisim.funct bisim s₁ s₂
| ⟨C, step, start⟩ := bisim.funct.map (λ s₁ s₂ h, bisim.corec_on C h step) (step _ _ start)

@[elab_as_eliminator]
lemma bisim.cases_on {α} {C : stream α → stream α → Prop}
    {s₁ s₂ : stream α} (p : bisim s₁ s₂)
    (ccons : ∀ hd s₁ s₂, bisim s₁ s₂ → C (hd :: s₁) (hd :: s₂)) :
    C s₁ s₂ :=
by apply bisim.funct.cases_on (bisim.unfold p); assumption

lemma bisim.cons {α : Type u} (hd) (s₁ s₂ : stream α) (h : bisim s₁ s₂) : bisim (hd :: s₁) (hd :: s₂) :=
bisim.corec_on (λ s₁' s₂', (s₁' = hd :: s₁ ∧ s₂' = hd :: s₂) ∨ bisim s₁' s₂') (or.inl ⟨rfl,rfl⟩)
begin
intros s₁' s₂' h', cases h',
case or.inl h' {cases h' with h' h', subst h', subst h', apply bisim.funct.cons, right, assumption},
case or.inr h' {apply bisim.funct.map _ (bisim.unfold h'), intros, apply or.inr, assumption},
end

namespace ex

lemma eq_of_bisim {α} {s₁ s₂ : stream α} (h : bisim s₁ s₂) : s₁ = s₂ :=
begin
apply funext, intro i,
induction i with i generalizing s₁ s₂,
case nat.zero { change s₁ 0 = s₂ 0, apply bisim.cases_on h, intros, refl },
case nat.succ i { apply bisim.cases_on h, intros, simph [stream.cons], apply ih_1, assumption }
end

lemma bisim_of_eq {α} {s₁ s₂ : stream α} (h : s₁ = s₂) : bisim s₁ s₂ :=
begin
apply bisim.corec_on (λ s₁ s₂, s₁ = s₂) h,
clear h s₁ s₂, intros s₁ s₂ h,
subst h, rw -stream.eta s₁, constructor, refl,
end

end ex