Section dyn_def.

Variables A B : Set.

CoInductive str : Set :=  SCons : A -> str -> str.

Variable P : B -> bool.
Variable h : B -> A.
Variable g g' : B -> B.

(* function to define:
   dyn x = if P x then Scons (h x) (dyn (g x)) else dyn (g' x)
*)
Inductive eventually_dyn (x: B) : Prop :=
  ev_dyn1 : P x = true -> eventually_dyn x
| ev_dyn2 : P x = false -> eventually_dyn (g' x) -> eventually_dyn x.

Lemma eventually_dyn_inv : forall x, eventually_dyn x -> P x = false -> eventually_dyn (g' x).
intros x T; case T; clear T.
intros T; rewrite T; intros; discriminate.
intros _ H' _; exact H'.
Defined.

Fixpoint pre_dyn (x:B)(d:eventually_dyn x) {struct d} : A*B :=
  match P x as b return P x = b -> A*B with
    true => fun t => (h x, g x)
  | false => fun t => pre_dyn (g' x) (eventually_dyn_inv x d t)
  end (refl_equal (P x)).

CoInductive infinite_dyn (x : B): Prop :=
  di : forall d: eventually_dyn x, infinite_dyn (snd (pre_dyn x d)) -> infinite_dyn x.

Lemma infinite_eventually_dyn : forall x, infinite_dyn x -> eventually_dyn x.
intros x i; case i; intros; assumption.
Qed.

Scheme eventually_dyn_inv2 := Induction for eventually_dyn Sort Prop.

Lemma pre_dyn_prf_irrelevant :
 forall x e1 e2, pre_dyn x e1 = pre_dyn x e2.
intros x e1; induction e1 using eventually_dyn_inv2.
intros e2; case e2.
simpl; destruct (P x); try discriminate; auto.
intros e0; elimtype False.
rewrite e0 in e; discriminate.
intros e2; case e2.
intros e0; elimtype False.
rewrite e0 in e; discriminate.
intros e0 d; simpl.
destruct (P x); try discriminate; auto.
Qed.

Lemma infinite_always_dyn : 
  forall x, infinite_dyn x-> forall e:eventually_dyn x, infinite_dyn (snd (pre_dyn x e)).
intros x i; case i.
intros d q e; rewrite (pre_dyn_prf_irrelevant x e d); auto.
Qed.

CoFixpoint dyn (x:B)(i:infinite_dyn x) : str :=
  SCons (fst (pre_dyn x (infinite_eventually_dyn x i)))
     (dyn _ (infinite_always_dyn x i (infinite_eventually_dyn x i))).

CoInductive bisimilar_s:  str -> str -> Prop :=
 bisim: forall (a : A) (s s' : str),
   bisimilar_s s s' -> bisimilar_s (SCons a s)(SCons a s').

Definition str_decompose (s : str) : str :=
   match s with SCons x s' => SCons x s' end.

Lemma st_dec_eq: forall (s : str),  s = str_decompose s.
intros s; case s; auto.
Qed.

Lemma dyn_prf_irrelevant :
  forall x x' (i:infinite_dyn x) (i':infinite_dyn x'), x = x' ->
  bisimilar_s (dyn x i) (dyn x' i').
cofix dpi.
intros x x' i i' xx'; rewrite (st_dec_eq (dyn x i)); 
  rewrite (st_dec_eq (dyn x' i')); simpl.
assert (pp' : pre_dyn x (infinite_eventually_dyn x i) = pre_dyn x' (infinite_eventually_dyn x' i')).
generalize i'; clear i'; rewrite <- xx'; intros i'.
rewrite (pre_dyn_prf_irrelevant x (infinite_eventually_dyn x i)(infinite_eventually_dyn x i')); auto.
pattern (pre_dyn x (infinite_eventually_dyn x i)) at 1; rewrite pp'.
apply bisim.
apply dpi; rewrite pp'; auto.
Qed.

Lemma dyn_step1 : forall x, P x = true -> infinite_dyn x -> infinite_dyn (g x).
intros x q d; inversion d.
generalize H; case d0; simpl.
intros t'; generalize (refl_equal (P x)); pattern (P x) at 2 3; rewrite q.
auto.
intros t'; rewrite q in t'; discriminate.
Qed.

Lemma dyn_step2 : forall x, P x = false -> infinite_dyn x -> infinite_dyn (g' x).
intros x q d; inversion d.
generalize H; case d0; simpl.
intros t'; elimtype False; rewrite q in t'; discriminate.
intros _; generalize (refl_equal (P x)); pattern (P x) at 2 3; rewrite q.
intros _ d1 i; apply di with d1; auto.
Qed.

Theorem dyn_equation :
  forall x i, bisimilar_s (dyn x i)
    (match P x as b return P x = b -> infinite_dyn x -> str with
    | true => fun t i => SCons (h x) (dyn (g x) (dyn_step1 x t i))
    | false => fun t i => dyn (g' x) (dyn_step2 x t i)
    end (refl_equal (P x)) i).
intros x i; rewrite (st_dec_eq (dyn x i)); simpl str_decompose.
pattern (infinite_eventually_dyn x i) at 1; case (infinite_eventually_dyn x i).
intros t; simpl.
generalize (refl_equal (P x)); pattern (P x) at 2 3 8; rewrite t.
intros t'; apply bisim.
apply dyn_prf_irrelevant; clear t'.
case (infinite_eventually_dyn x i); intros t'.
simpl; generalize (refl_equal (P x)); pattern (P x) at 2 3; rewrite t; auto.
elimtype False; rewrite t in t'; discriminate.

intros t; simpl.
generalize (refl_equal (P x)); pattern (P x) at 2 3 7; rewrite t.
intros t' e; rewrite (st_dec_eq (dyn (g' x)(dyn_step2 x t' i))).
simpl.
pattern (pre_dyn _ (infinite_eventually_dyn (g' x)(dyn_step2 x t' i))) at
1; rewrite (pre_dyn_prf_irrelevant _ (infinite_eventually_dyn (g' x)(dyn_step2 x t' i)) e).
apply bisim; apply dyn_prf_irrelevant; apply f_equal with (f := @snd A B).
case (infinite_eventually_dyn x i); intros t''.
elimtype False; rewrite t in t''; discriminate.
simpl.
intros e'; generalize (refl_equal (P x)); pattern (P x) at 2 3; rewrite t.
intros _; apply pre_dyn_prf_irrelevant.
Qed.

End dyn_def.