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 y ⇒ fst (p y)
                          end.


Definition tl (H : St) :=
  match H with
  | build X p y ⇒ build 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 : bool ⇒ pair b (negb b)).
Let gen2 := build bool (fun b : bool ⇒ pair (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 : bool ⇒ Cons b (gen1 (negb b)).

CoFixpoint gen2 : bool → Stream bool :=
  fun b : bool ⇒ Cons (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.