Skip to content

Instantly share code, notes, and snippets.

@keigoi keigoi/Alt.v
Created Jul 3, 2013

Embed
What would you like to do?
Axiom A :Set.
CoInductive Stream := Cons : A -> Stream -> Stream.
Definition head (s:Stream) : A :=
match s with
Cons x _ => x
end.
Definition tail (s:Stream) : Stream :=
match s with
Cons _ xs => xs
end.
Inductive eq {A:Type} (x:A) : A ->Prop := eq_refl : eq x x.
CoInductive Bisim : Stream -> Stream -> Prop :=
B : forall (s t : Stream), eq (head s) (head t) -> Bisim(tail s) (tail t) -> Bisim s t.
CoFixpoint replicate (x:A) := Cons x (replicate x).
CoFixpoint alt (s t : Stream) :=
match s, t with
Cons x xs, Cons _ ys => Cons x (alt ys xs)
end.
Theorem eq_alt : forall (x:Stream), Bisim x (alt x x).
cofix.
intros.
destruct x.
constructor.
simpl.
constructor.
simpl.
apply eq_alt.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.