Last active
May 16, 2017 15:10
-
-
Save gebner/66bab9997d4b37fdb0884f7bcab95418 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment