proposition: Lemma comp_is_F_bisimulation_strong (S1 S2 S3:F_coalgebra) (R12:S1.(states)->S2.(states)->Prop) (R23:S2.(states)->S3.(states)->Prop): is_F_bisimulation _ _ R12 -> is_F_bisimulation _ _ R23 -> is_F_bisimulation_strong _ _ (fun x=>(fun z=>{y | R12 x y/\ R23 y z})).
proof: Proof. intros [gamma1 hyp1] [gamma2 hyp2]. set (RS12:={s1s2 : states S1 * states S2 | R12 (fst s1s2) (snd s1s2)}). set (RS23:={s2s3 : states S2 * states S3 | R23 (fst s2s3) (snd s2s3)}). set (r2:=fun r:RS12 => (snd (proj1_sig r))). set (r3:=fun r:RS23 => (fst (proj1_sig r))). set (R12_is_bisim:=exist (fun gamma=> forall s1s2_h , lift_F_ _ _ (fun z : RS12 =>fst(proj1_sig z))(gamma s1s2_h) = S1.(transition) (fst (proj1_sig s1s2_h)) /\ lift_F_ _ _ (fun z : RS12 =>snd(proj1_sig z))(gamma s1s2_h) = S2.(transition) (snd (proj1_sig s1s2_h))) gamma1 hyp1). set (R23_is_bisim:=exist (fun gamma=> forall s2s3_h , lift_F_ _ _ (fun z :RS23 =>fst(proj1_sig z))(gamma s2s3_h) = S2.(transition) (fst (proj1_sig s2s3_h)) /\ lift_F_ _ _ (fun z :RS23 =>snd(proj1_sig z))(gamma s2s3_h) = S3.(transition) (snd (proj1_sig s2s3_h))) gamma2 hyp2). set (X:=weak_pullback _ _ _ r2 r3). set (R12_o_R23:={s1s3 : S1.(states) * S3.(states) & {s2 | R12 (fst s1s3) s2 /\ R23 s2 (snd s1s3)}}). set (i:=fun s1s3h:R12_o_R23 => i_comp_pullback S1 S2 S3 R12 R23 s1s3h). set (j:=fun xyyz:X => j_comp_pullback S1 S2 S3 R12 R23 xyyz). set (alpha_X:=fun xyyz:X => bisim_pullback_structure _ _ _ _ _ R12_is_bisim R23_is_bisim xyyz). set (Fj__alpha_X__i:=fun s1s3h:R12_o_R23 => lift_F_ _ _ j (alpha_X (i s1s3h))). exists Fj__alpha_X__i. intros s1s3_h. split. set (r1:=fun r:RS12 => (fst (proj1_sig r))). assert (triangle1:forall z,fst (projT1 z) = r1 (fst (proj1_sig (i z)))). clear; intros [[s1 s3] [s2 [hyp1 hyp2]]]; trivial. rewrite triangle1. assert (square2:forall x, lift_F_ (weak_pullback_Rel S1 S2 S3 R12 R23) _ (fun x0=>r1 (fst (proj1_sig x0))) (alpha_X x) = S1.(transition) (r1 (fst (proj1_sig x)))) . clear. intros x. rewrite <- lift_F_compose with (Y:=RS12). destruct (hyp1 (fst (proj1_sig x))) as [hyp121 _]. unfold r1 at 2; rewrite <- hyp121. assert (alpha_X_coalg:forall x, lift_F_ (weak_pullback_Rel S1 S2 S3 R12 R23) _ (fun x0=> fst (proj1_sig x0)) (alpha_X x) = gamma1 (fst (proj1_sig x))); [ clear; intros x; unfold alpha_X; rewrite <- bisim_pullback_structure_prop1; reflexivity|]. rewrite alpha_X_coalg; reflexivity. rewrite <- square2. unfold Fj__alpha_X__i. rewrite lift_F_compose. apply lift_F_extensionality. intros [[ [[s1 s2] hyp12] [[s2' s3] hyp23]] hyp]; reflexivity... set (r4:=fun r:RS23 => (snd (proj1_sig r))). assert (triangle1':forall z,snd (projT1 z) = r4 (snd (proj1_sig (i z)))). clear; intros [[s1 s3] [s2 [hyp1 hyp2]]]; trivial. rewrite triangle1'. assert (square2':forall x, lift_F_ (weak_pullback_Rel S1 S2 S3 R12 R23) _ (fun x0=>r4 (snd (proj1_sig x0))) (alpha_X x) = S3.(transition) (r4 (snd (proj1_sig x)))) . clear. intros x. rewrite <- lift_F_compose with (Y:=RS23). destruct (hyp2 (snd (proj1_sig x))) as [_ hyp232]. unfold r4 at 2; rewrite <- hyp232. assert (alpha_X_coalg':forall x, lift_F_ (weak_pullback_Rel S1 S2 S3 R12 R23) _ (fun x0=> snd (proj1_sig x0)) (alpha_X x) = gamma2 (snd (proj1_sig x))); [ clear; intros x; unfold alpha_X; rewrite <- bisim_pullback_structure_prop2; reflexivity|]. rewrite alpha_X_coalg'; reflexivity. rewrite <- square2'. unfold Fj__alpha_X__i. rewrite lift_F_compose. apply lift_F_extensionality. intros [[ [[s1 s2] hyp12] [[s2' s3] hyp23]] hyp]; reflexivity. Qed.
imports: ExtensionalFunctor Setoid