proposition: Lemma inverse_image_F_bisimulation_is_F_bisimulation (S1 S2:F_coalgebra) (f:S1.(states)->S2.(states)) (R:S2.(states)->S2.(states)->Prop): (forall s1, lift_F_ _ _ f (S1.(transition) s1) = S2.(transition) (f s1)) -> is_F_bisimulation _ _ R -> is_F_bisimulation S1 S1 (fun x y=>R (f x) (f y)).
proof: Proof. intros hypf hypR. set (R_:=fun x y=>R (f x) (f y)). set (G_f:=fun x y=>y=f(x)). set (G_f_min:=fun x y=>x=f(y)). set (R_o_G_f_min := fun x y=>R x (f y)). set (G_f_o_R_o_G_f_min := fun x z=>{y | G_f x y/\ R_o_G_f_min y z}). set (R_o_G_f_min_str := fun x z=>{y | R x y/\ G_f_min y z}). assert (hyp_G_f := graph_morphism_is_F_bisimulation S1 S2 f hypf :is_F_bisimulation S1 S2 G_f). apply relation_equivalence_bisimulation_strong with G_f_o_R_o_G_f_min. apply comp_is_F_bisimulation_strong; trivial. apply relation_equivalence_bisimulation_strong with R_o_G_f_min_str. apply comp_is_F_bisimulation_strong; trivial. apply inv_is_F_bisimulation; trivial. intros x y hyp_R; exists (f y); split; try red; trivial. intros x y [y0 [hyp1 hyp2]]; red in hyp2; subst y0; trivial. intros x y hyp_R_; exists (f x); split; red; trivial. intros x y [y0 [hyp1 hyp2]]; red in hyp1, hyp2; subst R_; simpl; subst y0; trivial. Qed.
imports: ExtensionalFunctor Setoid