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.