# Library CoinductiveExamples.STREAMS.Alter

Section Alter_I.

Require Import Bool.

Inductive St : Set :=
build : X : Set, (X bool × X) X St.
Definition hd (H : St) := match H with
| build X p yfst (p y)
end.

Definition tl (H : St) :=
match H with
| build X p ybuild X p (snd (p y))
end.

Definition T (R : St St Prop) (z1 z2 : St) :=
hd z1 = hd z2 R (tl z1) (tl z2).

Inductive EqSt : St St Prop :=
buildeq :
R : St St Prop,
( x y : St, R x y T R x y)
s1 s2 : St, R s1 s2 EqSt s1 s2.

Let gen1 := build bool (fun b : boolpair b (negb b)).
Let gen2 := build bool (fun b : boolpair (negb b) (negb b)).

Let alter1 := gen1 true.
Let alter2 := gen2 false.

Definition Invariant (s1 s2 : St) :=
b : bool, s1 = gen1 (negb b) s2 = gen2 b.

Theorem eqalters_I : EqSt alter1 alter2.
apply (buildeq Invariant).

intros.
case H.
intros.
case H0.
intros.
rewrite H1; rewrite H2.
simpl in |- ×.
split.
trivial.
unfold Invariant in |- ×.
(negb x0).
unfold gen1 in |- ×.
unfold gen2 in |- ×.
split.
trivial.
trivial.

unfold Invariant in |- ×.
false.
split.
trivial.
trivial.
Qed.

Inductive SimplerInvariant : St St Prop :=
makeinv : b : bool, SimplerInvariant (gen1 (negb b)) (gen2 b).

Theorem eqalters_I_bis : EqSt alter1 alter2.
apply (buildeq SimplerInvariant).
intros.
case H.
unfold T in |- ×.
intros.
split.
trivial.
apply (makeinv (negb b)).
apply (makeinv false).
Qed.

Inductive Cls : St St Prop :=
cls : Cls alter1 alter2.

Inductive EqSt1 : St St Prop :=
eqst1 :
z1 z2 : St,
hd z1 = hd z2
Cls (tl z1) (tl z2) EqSt1 (tl z1) (tl z2) EqSt1 z1 z2.

Lemma eqalters_body : EqSt1 alter1 alter2.
apply eqst1.
trivial.
right.
apply eqst1.
trivial.
left.
apply cls.
Qed.

Lemma H : z1 z2 : St, EqSt1 z1 z2 T EqSt1 z1 z2.
intros z1 z2 x.
red in |- ×.
case x.
intros z3 z4 H0 H1.
split.
assumption.
case H1.
intro H2.
case H2.
apply eqalters_body.
intros.
assumption.
Qed.

Theorem eqalters_II : EqSt alter1 alter2.
apply (buildeq EqSt1 H).
apply eqalters_body.
Qed.

End Alter_I.

Section Alter_II.

Require Import Streams.

CoFixpoint gen1 : bool Stream bool :=
fun b : boolCons b (gen1 (negb b)).

CoFixpoint gen2 : bool Stream bool :=
fun b : boolCons (negb b) (gen2 (negb b)).

Let alter1 := gen1 false.
Let alter2 := gen2 true.

Theorem eqalters_III : EqSt alter1 alter2.
cofix u.
apply eqst.
trivial.
apply eqst.
trivial.
assumption.
Qed.

End Alter_II.