Require Export List. Section E_Trees. Variables A1 A2 B1 B2 : Set. Variables (P : A1 -> Prop)(P1 : B1 -> Prop) (P_dec : forall x, ({ P x }) + ({ ~ P x })) (P1_dec : forall x, ({ P1 x }) + ({ ~ P1 x })). CoInductive ETrees (A B : Set) : Set := | A_node : A -> ETrees A B -> ETrees A B | B_node : B -> ETrees A B -> ETrees A B -> ETrees A B. Definition ETree_decomp (A B : Set) (t: ETrees A B) : ETrees A B := match t with A_node a t1 => A_node A B a t1 | B_node a t1 t2 => (B_node A B a t1 t2) end. Lemma ETree_decompose : forall (A B: Set) (t: ETrees A B), t = ETree_decomp A B t. Proof. destruct t; trivial. Qed. Ltac ETree_unfold term := apply trans_equal with (1 := ETree_decompose term). (* Non-guarded function: Variables (h1 : A1 -> A2) (h2: B1 -> A2) (h1': A1 -> A1) (h2' : B1 -> B1) (h3: ETrees A1 B1 -> ETrees A1 B1). CoFixpoint etree_filter (t: ETrees A1 B1) : ETrees A2 B2 := match t with |A_node a t1 => match P_dec a with |left _ => (A_node (h1 a) (etree_filter (A_node (h1' a) t1 ))) |right ht => etree_filter (h3 (A_node a t1)) end |B_node b t1 t2 => match P1_dec b with |left _ => (A_node (h2 b) (etree_filter (B_node (h2' b) t1 t2))) |right ht' => etree_filter (h3 (B_node b t1 t2)) end end. *) Variables (h1 : A1+B1 -> A2) (h2: A1+B1 -> A1*B1 ) (h3: ETrees A1 B1 -> ETrees A1 B1). Inductive eventually_t: ETrees A1 B1 -> Prop := | ev_rB: forall x t t1 , ~P1 x -> eventually_t (h3 (B_node A1 B1 x t t1)) -> eventually_t (B_node A1 B1 x t t1) | ev_bB: forall x t t1, P1 x -> eventually_t (B_node A1 B1 x t t1) | ev_rA: forall x t, ~P x -> eventually_t (h3 (A_node A1 B1 x t)) -> eventually_t (A_node A1 B1 x t) | ev_bA: forall x t, P x -> eventually_t (A_node A1 B1 x t). Lemma eventually_t_inv: forall t : ETrees A1 B1, eventually_t t -> forall (x : A1) (t' : ETrees A1 B1), t = (A_node A1 B1 x t') -> ~ P x -> eventually_t (h3 (A_node A1 B1 x t')). intros t h; case h. intros. discriminate H1. intros. discriminate H0. intros. injection H1. intros. subst x0 t'; assumption. intros. elim H1. injection H0. intros. subst x0; assumption. Defined. Lemma eventually_t_inv': forall t : ETrees A1 B1, eventually_t t -> forall (x : B1) (t' t1 : ETrees A1 B1), t = (B_node A1 B1 x t' t1) -> ~P1 x -> eventually_t (h3 (B_node A1 B1 x t' t1)). intros t h; case h. intros. injection H1. intros. subst x0 t' t2; assumption. intros. elim H1. injection H0. intros. subst x0; assumption. intros. discriminate H1. intros. discriminate H0. Defined. Fixpoint pre_filter_t (t : ETrees A1 B1)(h: eventually_t t ){struct h}: A2 * ETrees A1 B1 := match t as b return t = b -> A2*(ETrees A1 B1) with |A_node x t' => fun heq : t = (A_node A1 B1 x t') => match P_dec x with |left _ => ((h1 (inl B1 x)),(A_node A1 B1 (fst (h2 (inl B1 x))) t')) |right hn => pre_filter_t (h3 (A_node A1 B1 x t'))(eventually_t_inv t h x t' heq hn) end |B_node x t' t1 => fun heq' : t = (@B_node A1 B1 x t' t1) => match P1_dec x with |left _ => ((h1 (inr A1 x)),(B_node A1 B1 (snd (h2 (inr A1 x))) t' t1)) |right hn' => pre_filter_t (h3 (B_node A1 B1 x t' t1)) (eventually_t_inv' t h x t' t1 heq' hn') end end (@refl_equal (ETrees A1 B1) t). CoInductive infinite_t: ETrees A1 B1 -> Prop := cf: forall (t:ETrees A1 B1) (h:eventually_t t), infinite_t(snd (pre_filter_t t h)) -> infinite_t t. Lemma infinite_eventually_t : forall t, infinite_t t -> eventually_t t. intros t H; case H; auto. Qed. Scheme eventually_t_ind2 := Induction for eventually_t Sort Prop. Lemma pre_filter_t_prf_irrelevant : forall t (h h':eventually_t t), pre_filter_t t h = pre_filter_t t h'. induction h using eventually_t_ind2. idtac "inversion on h0, by hand"; intros h0; (apply (eventually_t_ind2 (fun t' h0' => t' = (B_node A1 B1 x t t1) -> pre_filter_t (B_node A1 B1 x t t1) (ev_rB x t t1 n h) = pre_filter_t t' h0'))); auto; try (intros; discriminate). intros x1 t3 t4 n0 H4 _ q; injection q; intros q1 q2 q3. generalize H4 n0. rewrite q3; rewrite q2; rewrite q1; intros. simpl; case (P1_dec x);[intro B; case n1;exact B | intro; apply IHh]. intros x1 t3 t4 p q; injection q; intros q1 q2 q3; elimtype False; rewrite q3 in p; case n;exact p. intros h0; (apply (eventually_t_ind2 (fun t' h0' => t' = (B_node A1 B1 x t t1) -> pre_filter_t (B_node A1 B1 x t t1) (ev_bB x t t1 p) = pre_filter_t t' h0'))); auto; try (intros; discriminate). intros a b c n e _ q; injection q; intros q1 q2 q3; elimtype False; rewrite q3 in n; auto. intros x0 t0 t2 p0 q; injection q; intros q1 q2 q3; generalize p0; rewrite q1; rewrite q2; rewrite q3; simpl. intros p1; case (P1_dec x);[auto | intros n; elimtype False; case n;exact p]. intros h0; (apply (eventually_t_ind2 (fun t' h0' => t' = (A_node A1 B1 x t) -> (pre_filter_t (A_node A1 B1 x t) (ev_rA x t n h)) = pre_filter_t t' h0'))); auto; try (intros;discriminate). intros x0 t0 n0 e _ q; injection q; intros q1 q2. generalize n0 e; rewrite q1; rewrite q2; simpl. case (P_dec x); [intros A; case n; auto | auto]. intros x0 t0 p q; injection q; intros q1 q2. generalize p; rewrite q1; rewrite q2; simpl; auto. intros p0; case (P_dec x); [auto | intros A; elimtype False; case A; auto]. intros h0; (apply (eventually_t_ind2 (fun t' h0' => t' = (A_node A1 B1 x t) -> pre_filter_t (A_node A1 B1 x t) (ev_bA x t p) = pre_filter_t t' h0'))); auto; try (intros;discriminate). intros x0 t0 n e _ q; injection q; intros q1 q2; generalize n e; rewrite q1; rewrite q2. intros n0; case n0; auto. intros x0 t0 p0 q;injection q; intros q1 q2; generalize p0; rewrite q1; rewrite q2; simpl; case (P_dec x); auto. intros n; case n; auto. Qed. Lemma infinite_always_t : forall (t : ETrees A1 B1) (h : infinite_t t), infinite_t (snd(pre_filter_t t (infinite_eventually_t t h))). intros t h; case h. intros t0 h0; case h0. intros. rewrite (pre_filter_t_prf_irrelevant (B_node A1 B1 x t1 t2)(infinite_eventually_t (B_node A1 B1 x t1 t2) (cf (B_node A1 B1 x t1 t2) (ev_rB x t1 t2 n e) i)) (ev_rB x t1 t2 n e)); auto. intros. rewrite (pre_filter_t_prf_irrelevant (B_node A1 B1 x t1 t2) (infinite_eventually_t (B_node A1 B1 x t1 t2) (cf (B_node A1 B1 x t1 t2) (ev_bB x t1 t2 p) i)) (ev_bB x t1 t2 p)); auto. intros. rewrite (pre_filter_t_prf_irrelevant (A_node A1 B1 x t1) (infinite_eventually_t (A_node A1 B1 x t1) (cf (A_node A1 B1 x t1) (ev_rA x t1 n e) i)) (ev_rA x t1 n e)); auto. intros. rewrite (pre_filter_t_prf_irrelevant (A_node A1 B1 x t1) (infinite_eventually_t (A_node A1 B1 x t1) (cf (A_node A1 B1 x t1) (ev_bA x t1 p) i)) (ev_bA x t1 p)); auto. Qed. CoFixpoint e_filter(t:ETrees A1 B1): forall (h:infinite_t t), ETrees A2 B2 := match t return infinite_t t -> ETrees A2 B2 with | A_node x t' => fun h' : infinite_t (A_node A1 B1 x t') => A_node A2 B2 (fst (pre_filter_t (A_node A1 B1 x t') (infinite_eventually_t (A_node A1 B1 x t') h'))) (e_filter (snd (pre_filter_t (A_node A1 B1 x t')(infinite_eventually_t (A_node A1 B1 x t') h'))) (infinite_always_t (A_node A1 B1 x t') h')) | B_node x t' t2 => fun h' : infinite_t(B_node A1 B1 x t' t2) => A_node A2 B2 (fst (pre_filter_t (B_node A1 B1 x t' t2) (infinite_eventually_t (B_node A1 B1 x t' t2) h'))) (e_filter (snd (pre_filter_t (B_node A1 B1 x t' t2)(infinite_eventually_t (B_node A1 B1 x t' t2) h'))) (infinite_always_t (B_node A1 B1 x t' t2) h')) end. Lemma t_step1 : forall t x, P x -> infinite_t(A_node A1 B1 x t) -> infinite_t(A_node A1 B1 (fst (h2 (inl B1 x))) t). intros t x hp hf; inversion hf. generalize H; clear H; dependent inversion h. simpl. case (P_dec x). intros; auto. intros; elim n; auto. simpl. case P_dec. intros; auto. intros; elim n; assumption. Qed. Lemma t_step1' : forall t t' x, P1 x -> infinite_t(B_node A1 B1 x t t') -> infinite_t(B_node A1 B1 (snd (h2 (inr A1 x))) t t'). intros t t' x hp hf; inversion hf. generalize H; clear H; dependent inversion h. simpl. case (P1_dec x). intros; auto. intros; elim n; auto. simpl. case P1_dec. intros; auto. intros; elim n; assumption. Qed. Lemma t_step2 : forall t x, ~P x -> infinite_t(A_node A1 B1 x t) -> infinite_t(h3 (A_node A1 B1 x t)). intros t x hp hf; inversion hf. generalize H; clear H; dependent inversion h. simpl. case (P_dec x). intro; elim hp; auto. intros _ H'. apply cf with e; assumption. simpl. case P_dec. intros; elim hp; auto. intros; elim hp; auto. Qed. Lemma t_step2' : forall t t' x, ~P1 x -> infinite_t(B_node A1 B1 x t t') -> infinite_t(h3 (B_node A1 B1 x t t')). intros t t' x hp hf; inversion hf. generalize H; clear H; dependent inversion h. simpl. case (P1_dec x). intros; elim hp; auto. intros _ H'. apply cf with e; assumption. simpl. case P1_dec. intros; elim hp; auto. intros; elim hp; auto. Qed. CoInductive bisimilar: ETrees A2 B2 -> ETrees A2 B2 -> Prop := |bisim1: forall (a: A2) (t t': ETrees A2 B2), bisimilar t t' -> bisimilar (A_node A2 B2 a t)(A_node A2 B2 a t') |bisim2: forall (b: B2) (t t' t1 t1': ETrees A2 B2) , bisimilar t t' -> bisimilar t1 t1' -> bisimilar (B_node A2 B2 b t t1) (B_node A2 B2 b t' t1'). Require Import Relation_Definitions. Require Import Relation_Operators. Require Import Operators_Properties. Theorem Bisim_refl: forall (t: ETrees A2 B2), bisimilar t t. cofix H. intros. case t. intros. apply bisim1. apply H. intros. apply bisim2. apply H. apply H. Qed. Theorem Bisim_trans: forall (l u v : ETrees A2 B2), bisimilar l u -> bisimilar u v -> bisimilar l v. cofix H. intros l u v. case l; case u; case v. intros. assert (a1 = a0). inversion H0; auto. assert (a = a0). inversion H1; auto. assert (a1 = a). apply trans_equal with a0; auto. rewrite H4. apply bisim1. apply H with e0. Guarded. inversion H0; assumption. inversion H1; assumption. intros; inversion H1. intros; inversion H1. intros; inversion H0. intros; inversion H0. intros; inversion H0. intros; inversion H1. intros. assert (b1 = b0). inversion H0; auto. assert (b = b0). inversion H1; auto. assert (b1 = b). apply trans_equal with b0; auto. rewrite H4. apply bisim2. apply H with e1. Guarded. inversion H0; assumption. inversion H1; assumption. apply H with e2. inversion H0; assumption. inversion H1; assumption. Qed. Theorem Bisim_sym: forall (l v: ETrees A2 B2), bisimilar l v -> bisimilar v l. cofix H. intros l v ; case l; case v. intros. assert (a = a0). inversion H0; auto. rewrite H1; apply bisim1. apply H. inversion H0; assumption. intros. inversion H0. intros; inversion H0. intros. assert (b = b0). inversion H0; auto. rewrite H1; apply bisim2. apply H. inversion H0; assumption. apply H. inversion H0; assumption. Qed. Lemma filter_prf_irrelevant : forall t t' (h : infinite_t t) (h':infinite_t t'), t = t' -> bisimilar (e_filter t h) (e_filter t' h'). cofix H. intros t t'; case t; case t'. intros a e a0 e0 h h' Htt'; injection Htt'; clear Htt'; intros Htt' Haa'. rewrite (ETree_decompose A2 B2 (e_filter (A_node A1 B1 a0 e0) h)); simpl. rewrite (ETree_decompose A2 B2 (e_filter (A_node A1 B1 a e) h')); simpl. assert (pre_filter_t (A_node A1 B1 a0 e0)(infinite_eventually_t (A_node A1 B1 a0 e0) h) = pre_filter_t (A_node A1 B1 a e) (infinite_eventually_t (A_node A1 B1 a e) h')). generalize h'; clear h'; rewrite <- Haa'; rewrite <- Htt'; intros h'. rewrite (pre_filter_t_prf_irrelevant (A_node A1 B1 a0 e0) (infinite_eventually_t (A_node A1 B1 a0 e0) h) (infinite_eventually_t (A_node A1 B1 a0 e0) h')); auto. pattern ((pre_filter_t (A_node A1 B1 a0 e0) (infinite_eventually_t (A_node A1 B1 a0 e0) h))) at 1; rewrite H0. apply bisim1. apply H. rewrite H0; auto. intros. inversion H0. intros. inversion H0. intros b e e0 b0 e1 e2 h h' Htt'; injection Htt'; clear Htt'; intros Htt' Hee Hbb'. rewrite (ETree_decompose A2 B2 (e_filter (B_node A1 B1 b0 e1 e2) h)); simpl. rewrite (ETree_decompose A2 B2 (e_filter (B_node A1 B1 b e e0) h')); simpl. assert (pre_filter_t (B_node A1 B1 b0 e1 e2)(infinite_eventually_t (B_node A1 B1 b0 e1 e2) h) = pre_filter_t (B_node A1 B1 b e e0) (infinite_eventually_t (B_node A1 B1 b e e0) h')). generalize h' h; clear h' h; rewrite <- Hbb'; rewrite Hee; rewrite <- Htt'; intros h' h. rewrite (pre_filter_t_prf_irrelevant (B_node A1 B1 b0 e e2) (infinite_eventually_t (B_node A1 B1 b0 e e2) h) (infinite_eventually_t (B_node A1 B1 b0 e e2) h')); auto. pattern (pre_filter_t (B_node A1 B1 b0 e1 e2) (infinite_eventually_t (B_node A1 B1 b0 e1 e2) h)) at 1; rewrite H0. apply bisim1. apply H. rewrite H0; auto. Qed. Lemma misc3A: forall (x: A1) (t: ETrees A1 B1) (H: eventually_t(A_node A1 B1 x t)), P x -> (h1 (inl B1 x), A_node A1 B1 (fst (h2 (inl B1 x))) t) = (pre_filter_t (A_node A1 B1 x t) H). intros x t h h0. dependent inversion h. contradiction. apply trans_equal with (pre_filter_t (A_node A1 B1 x t) h). apply sym_equal. unfold pre_filter_t. dependent inversion h; case P_dec; auto; intro; contradiction. rewrite (pre_filter_t_prf_irrelevant (A_node A1 B1 x t) (h)(ev_bA x t p)); auto. Qed. Lemma misc3B: forall (x: B1) (t t1: ETrees A1 B1) (H: eventually_t(B_node A1 B1 x t t1)), P1 x -> (h1 (inr A1 x), B_node A1 B1 (snd (h2 (inr A1 x))) t t1) = (pre_filter_t (B_node A1 B1 x t t1) H). intros x t t1 h h0. dependent inversion h. contradiction. apply trans_equal with (pre_filter_t (B_node A1 B1 x t t1) h). apply sym_equal. unfold pre_filter_t. dependent inversion h; case P1_dec; auto; intro; contradiction. rewrite (pre_filter_t_prf_irrelevant (B_node A1 B1 x t t1) (h)(ev_bB x t t1 p)); auto. Qed. Lemma misc3A': forall (x:A1) (t: ETrees A1 B1) (H: eventually_t(A_node A1 B1 x t)), P x -> h1 (inl B1 x) = fst (pre_filter_t (A_node A1 B1 x t) H). intros. assert ((h1 (inl B1 x), A_node A1 B1 (fst (h2 (inl B1 x))) t) = pre_filter_t (A_node A1 B1 x t) H). apply misc3A; assumption. rewrite <- H1; auto. Qed. Lemma misc3A'': forall (x: A1) (t: ETrees A1 B1) (H: eventually_t(A_node A1 B1 x t)), P x -> snd (pre_filter_t (A_node A1 B1 x t) H) = A_node A1 B1 (fst (h2 (inl B1 x))) t. intros x t h h0. assert ((h1 (inl B1 x), A_node A1 B1 (fst (h2 (inl B1 x))) t) = pre_filter_t (A_node A1 B1 x t) h). apply misc3A; assumption. rewrite <- H; auto. Qed. Lemma misc3B': forall (x: B1) (t t1: ETrees A1 B1) (H: eventually_t(B_node A1 B1 x t t1)), P1 x -> h1 (inr A1 x) = fst(pre_filter_t (B_node A1 B1 x t t1) H). intros. assert ((h1 (inr A1 x), B_node A1 B1 (snd (h2 (inr A1 x))) t t1) = pre_filter_t (B_node A1 B1 x t t1) H). apply misc3B; assumption. rewrite <- H1; auto. Qed. Lemma misc3B'': forall (x: B1) (t t1: ETrees A1 B1) (H: eventually_t(B_node A1 B1 x t t1)), P1 x -> B_node A1 B1 (snd (h2 (inr A1 x))) t t1 = snd(pre_filter_t (B_node A1 B1 x t t1) H). intros. assert ((h1 (inr A1 x), B_node A1 B1 (snd (h2 (inr A1 x))) t t1) = pre_filter_t (B_node A1 B1 x t t1) H). apply misc3B; assumption. rewrite <- H1; auto. Qed. Lemma misc5: forall t (i: infinite_t t), (e_filter t i) = ( A_node A2 B2 (fst (pre_filter_t t (infinite_eventually_t t i))) (e_filter (snd (pre_filter_t t (infinite_eventually_t t i))) (infinite_always_t t i))). intros. case i; clear t i; intros. rewrite (ETree_decompose A2 B2 (e_filter t (cf t h i))); simpl. generalize (cf t h i). case t. intros; auto. intros; auto. Qed. Lemma case_neg: forall x t (h : infinite_t(A_node A1 B1 x t)) (n: ~ P x), bisimilar (e_filter (A_node A1 B1 x t) h) (e_filter (h3 (A_node A1 B1 x t)) (t_step2 t x n h)). intros. assert (infinite_t (h3 (A_node A1 B1 x t))). apply t_step2; assumption. apply Bisim_trans with (e_filter (h3 (A_node A1 B1 x t)) H). dependent inversion H; rewrite (ETree_decompose A2 B2 (e_filter (A_node A1 B1 x t) h)); simpl. apply Bisim_trans with (e_filter (h3 (A_node A1 B1 x t)) H). generalize H; generalize h. intros i' i0. generalize (refl_equal (A_node A1 B1 x t)). generalize (infinite_always_t (A_node A1 B1 x t) i'). pattern (A_node A1 B1 x t) at 1 2 3 5 6, (infinite_eventually_t (A_node A1 B1 x t) i'); case (infinite_eventually_t (A_node A1 B1 x t) i');try (intros; discriminate). intros a t2 n0 e i'' q'; injection q'; intros q1 q2. simpl; simpl in i''. generalize i''; case (P_dec a). intros A; case n0; auto. intros _; clear i''; generalize e i0. rewrite q1; rewrite q2. clear e i0 i; intros e i i0. apply Bisim_trans with ( A_node A2 B2 (fst (pre_filter_t (h3 (A_node A1 B1 x t)) (infinite_eventually_t (h3 (A_node A1 B1 x t)) i))) (e_filter (snd (pre_filter_t (h3 (A_node A1 B1 x t)) (infinite_eventually_t (h3 (A_node A1 B1 x t)) i))) (infinite_always_t (h3 (A_node A1 B1 x t)) i))). assert (pre_filter_t (h3 (A_node A1 B1 x t)) e = pre_filter_t (h3 (A_node A1 B1 x t)) (infinite_eventually_t (h3 (A_node A1 B1 x t)) i)). apply pre_filter_t_prf_irrelevant. pattern (pre_filter_t (h3 (A_node A1 B1 x t)) e) at 1; rewrite H1. apply bisim1. apply filter_prf_irrelevant. rewrite (pre_filter_t_prf_irrelevant (h3 (A_node A1 B1 x t)) e (infinite_eventually_t (h3 (A_node A1 B1 x t)) i)); auto. apply Bisim_sym. rewrite misc5; apply bisim1; apply Bisim_refl. intros a t2 p i1 q'; injection q'; intros q1 q2. assert (P x). rewrite <- q2; assumption. contradiction. apply filter_prf_irrelevant; auto. apply filter_prf_irrelevant; auto. Qed. Lemma case_neg2: forall b t t1 (h : infinite_t(B_node A1 B1 b t t1)) (n: ~ P1 b), bisimilar (e_filter (B_node A1 B1 b t t1) h) (e_filter (h3 (B_node A1 B1 b t t1)) (t_step2' t t1 b n h)). intros. assert (infinite_t (h3 (B_node A1 B1 b t t1))). apply t_step2'; assumption. apply Bisim_trans with (e_filter (h3 (B_node A1 B1 b t t1)) H). dependent inversion H; rewrite (ETree_decompose A2 B2 (e_filter (B_node A1 B1 b t t1) h)); simpl. apply Bisim_trans with (e_filter (h3 (B_node A1 B1 b t t1)) H). generalize H; generalize h. intros i' i0. generalize (refl_equal (B_node A1 B1 b t t1)). generalize (infinite_always_t (B_node A1 B1 b t t1) i'). pattern (B_node A1 B1 b t t1) at 1 2 3 5 6, (infinite_eventually_t (B_node A1 B1 b t t1) i'); case (infinite_eventually_t (B_node A1 B1 b t t1) i');try (intros; discriminate). intros x t2 t3 n0 e i'' q'; injection q'; intros q1 q2 q3. simpl; simpl in i''. generalize i''; case (P1_dec x). intros A; case n0; auto. intros _; clear i''; generalize e i0. rewrite q1; rewrite q2; rewrite q3. clear e i0 i; intros e i i0. apply Bisim_trans with ( A_node A2 B2 (fst (pre_filter_t (h3 (B_node A1 B1 b t t1)) (infinite_eventually_t (h3 (B_node A1 B1 b t t1)) i))) (e_filter (snd (pre_filter_t (h3 (B_node A1 B1 b t t1)) (infinite_eventually_t (h3 (B_node A1 B1 b t t1)) i))) (infinite_always_t (h3 (B_node A1 B1 b t t1)) i))). assert (pre_filter_t (h3 (B_node A1 B1 b t t1)) e = pre_filter_t (h3 (B_node A1 B1 b t t1)) (infinite_eventually_t (h3 (B_node A1 B1 b t t1)) i)). apply pre_filter_t_prf_irrelevant. pattern (pre_filter_t (h3 (B_node A1 B1 b t t1)) e) at 1; rewrite H1. apply bisim1. apply filter_prf_irrelevant. rewrite (pre_filter_t_prf_irrelevant (h3 (B_node A1 B1 b t t1)) e (infinite_eventually_t (h3 (B_node A1 B1 b t t1)) i)); auto. apply Bisim_sym. rewrite misc5; apply bisim1; apply Bisim_refl. intros x t2 t3 p i1 q'; injection q'; intros q1 q2 q3. assert (P1 b). rewrite <- q3; assumption. contradiction. apply filter_prf_irrelevant; auto. apply filter_prf_irrelevant; auto. Qed. Theorem filter_equation : forall (t : ETrees A1 B1) (h : infinite_t t), bisimilar (e_filter t h) (match t as t0 return (infinite_t t0 -> ETrees A2 B2) with | A_node x t' => fun h0 : infinite_t (A_node A1 B1 x t') => match P_dec x return (ETrees A2 B2) with | left hp => A_node A2 B2 (h1 (@inl A1 B1 x)) (e_filter (A_node A1 B1 (fst(h2 (@inl A1 B1 x))) t') (t_step1 t' x hp h0)) | right hp => e_filter (h3 (A_node A1 B1 x t')) (t_step2 t' x hp h0) end | B_node x t' t2 => fun h0 : infinite_t (B_node A1 B1 x t' t2) => match P1_dec x return (ETrees A2 B2) with | left hp => A_node A2 B2 (h1 (@inr A1 B1 x)) (e_filter (B_node A1 B1 (@snd A1 B1 (h2 (@inr A1 B1 x))) t' t2) (t_step1' t' t2 x hp h0)) | right hp => e_filter (h3 (B_node A1 B1 x t' t2)) (t_step2' t' t2 x hp h0) end end h). intros t h. case h; intros. induction h0 using eventually_t_ind2. case P1_dec. intro. contradiction. intro. apply case_neg2. case P1_dec. intro. rewrite (ETree_decompose A2 B2 (e_filter (B_node A1 B1 x t0 t1) (cf (B_node A1 B1 x t0 t1) (ev_bB x t0 t1 p) i))); simpl. assert ((h1(inr A1 x)) = (fst (pre_filter_t (B_node A1 B1 x t0 t1) (infinite_eventually_t (B_node A1 B1 x t0 t1) (cf (B_node A1 B1 x t0 t1) (ev_bB x t0 t1 p) i))))). assert (eventually_t(B_node A1 B1 x t0 t1)). apply ev_bB; assumption. assert (infinite_t(B_node A1 B1 x t0 t1)). apply cf with H. assert (pre_filter_t (B_node A1 B1 x t0 t1) H = pre_filter_t (B_node A1 B1 x t0 t1) (ev_bB x t0 t1 p)). rewrite (pre_filter_t_prf_irrelevant (B_node A1 B1 x t0 t1) (H) (ev_bB x t0 t1 p)); auto. rewrite H0; assumption. apply trans_equal with (fst (pre_filter_t (B_node A1 B1 x t0 t1) H)). generalize p0. apply misc3B'; auto. rewrite (pre_filter_t_prf_irrelevant (B_node A1 B1 x t0 t1) (H) (infinite_eventually_t (B_node A1 B1 x t0 t1) (cf (B_node A1 B1 x t0 t1) (ev_bB x t0 t1 p) i))); auto. rewrite <- H. apply bisim1. apply filter_prf_irrelevant. inversion i. assert (eventually_t(B_node A1 B1 x t0 t1)). apply ev_bB; assumption. apply trans_equal with (snd (pre_filter_t (B_node A1 B1 x t0 t1) H2)). rewrite (pre_filter_t_prf_irrelevant (B_node A1 B1 x t0 t1) (infinite_eventually_t (B_node A1 B1 x t0 t1) (cf (B_node A1 B1 x t0 t1) (ev_bB x t0 t1 p) i)) (H2)); auto. apply sym_equal. apply misc3B''; auto. intro; contradiction. case P_dec. intro; contradiction. intro. apply case_neg. case P_dec. intro. rewrite (ETree_decompose A2 B2 (e_filter (A_node A1 B1 x t0) (cf (A_node A1 B1 x t0) (ev_bA x t0 p) i))); simpl. assert ((h1(inl B1 x)) = (fst (pre_filter_t (A_node A1 B1 x t0) (infinite_eventually_t (A_node A1 B1 x t0) (cf (A_node A1 B1 x t0) (ev_bA x t0 p) i))))). assert (eventually_t(A_node A1 B1 x t0)). apply ev_bA; assumption. assert (infinite_t(A_node A1 B1 x t0)). apply cf with H. assert (pre_filter_t (A_node A1 B1 x t0) H = pre_filter_t (A_node A1 B1 x t0) (ev_bA x t0 p)). rewrite (pre_filter_t_prf_irrelevant (A_node A1 B1 x t0) (H) (ev_bA x t0 p)); auto. rewrite H0; assumption. apply trans_equal with (fst (pre_filter_t (A_node A1 B1 x t0) H)). generalize p0. apply misc3A'; auto. rewrite (pre_filter_t_prf_irrelevant (A_node A1 B1 x t0) (H) (infinite_eventually_t (A_node A1 B1 x t0) (cf (A_node A1 B1 x t0) (ev_bA x t0 p) i))); auto. rewrite <- H. apply bisim1. apply filter_prf_irrelevant. inversion i. assert (eventually_t(A_node A1 B1 x t0)). apply ev_bA; assumption. apply trans_equal with (snd (pre_filter_t (A_node A1 B1 x t0) H2)). rewrite (pre_filter_t_prf_irrelevant (A_node A1 B1 x t0) (infinite_eventually_t (A_node A1 B1 x t0) (cf (A_node A1 B1 x t0) (ev_bA x t0 p) i)) (H2)); auto. apply misc3A''; auto. intro; contradiction. Qed. End E_Trees.