# Reasoning

[View pic_bisim.thm]

Click on a command or tactic to see a detailed view of its use.

```Kind name,label,proc type.

Import "pic_core". [View pic_core]

%%% Bisimulation up to bisimilarity

Define bisim_t : proc -> proc -> proc -> proc -> prop by
bisim_t P1 P2 Q1 Q2 :=
bisim_up_to refl_t P1 P2 /\ bisim_up_to refl_t Q1 Q2.

Define is_sound_fst : (proc -> proc -> proc -> proc -> prop) -> prop by
is_sound_fst Tech := forall P Q,
(exists R S, bisim_up_to refl_t P R /\ bisim_up_to Tech R S /\ bisim_up_to refl_t S Q)
-> bisim_up_to refl_t P Q.

Define is_sound_snd : (proc -> proc -> proc -> proc -> prop) -> prop by
is_sound_snd Tech := forall P Q, bisim_up_to Tech P Q ->
exists R S, bisim_up_to refl_t P R /\ bisim_up_to Tech R S /\ bisim_up_to refl_t S Q.

Theorem bisim_t_reflexive : forall P, bisim_t P P P P.
intros. unfold. backchain bisim_reflexive. backchain bisim_reflexive.
Theorem bisim_sound_fst : is_sound_fst bisim_t.
unfold. coinduction. intros. case H1.
rename H2 to Left. rename H3 to Middle. rename H4 to Right.
unfold.
intros Pstep.
Left1 : case Left. Rstep : apply Left1 to Pstep. clear Left1 Left2 Left3 Left4 Left5 Left6.
case Rstep1.
Middle1 : case Middle. Sstep : apply Middle1 to Rstep. clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Sstep : case Sstep1.
Right1 : case Right. Qstep : apply Right1 to Sstep. clear Right1 Right2 Right3 Right4 Right5 Right6.
case Qstep1.
witness Q6. split. search.
witness P3. witness Q6. split. search.
Link1 : apply bisim_transitive to Rstep2 Sstep1.
Link1 : apply bisim_symmetric to Sstep3.
clear Rstep2 Sstep1 Sstep3 Qstep2 Link2.
backchain CH.

intros Pstep.
Left1 : case Left. Rstep : apply Left2 to Pstep. clear Left1 Left2 Left3 Left4 Left5 Left6.
Middle1 : case Middle. Sstep : apply Middle2 to Rstep. clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Right1 : case Right. Qstep : apply Right2 to Sstep. clear Right1 Right2 Right3 Right4 Right5 Right6.
witness Q5. split. search.
witness P1. witness Q5. intros. split. search.
clear Pstep Qstep Rstep Sstep.
Rstep : apply Rstep1 with N = N. clear Rstep1.
Sstep : apply Sstep1 with N = N. clear Sstep1.
Qstep : apply Qstep1 with N = N. clear Qstep1.
Eq1 : case Rstep. Eq1 : case Qstep. Bis : case Sstep.
Link1 : apply bisim_eq_1R to Rstep2 Eq2. clear Rstep2 Eq2.
Link1 : apply bisim_eq_2R to Qstep2 Eq3. clear Qstep2 Eq3.
Link1 : apply bisim_symmetric to Bis1. clear Bis1.
backchain CH.

intros Pstep.
Left1 : case Left. Rstep : apply Left3 to Pstep. clear Left1 Left2 Left3 Left4 Left5 Left6.
Middle1 : case Middle. Sstep : apply Middle3 to Rstep. clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Right1 : case Right. Qstep : apply Right3 to Sstep. clear Right1 Right2 Right3 Right4 Right5 Right6.
witness Q5. split. search.
witness P1. witness Q5. intros. split. search.
clear Pstep Qstep Rstep Sstep.
case Rstep1. case Qstep1. Sstep1 : case Sstep1.
Link1 : apply bisim_transitive to Rstep2 Sstep1. clear Rstep2 Sstep1.
Link1 : apply bisim_symmetric to Sstep3. clear Sstep3.
backchain CH.

intros Qstep.
Right1 : case Right. Sstep : apply Right4 to Qstep. clear Right1 Right2 Right3 Right4 Right5 Right6.
Middle1 : case Middle. Rstep : apply Middle4 to Sstep. clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Left1 : case Left. Pstep : apply Left4 to Rstep. clear Left1 Left2 Left3 Left4 Left5 Left6.
witness P5. split. search.
witness P5. witness Q1. split. search.
clear Pstep Qstep Rstep Sstep.
case Sstep1. case Pstep1. Rstep1 : case Rstep1.
Link1 : apply bisim_transitive to Pstep2 Rstep1. clear Pstep2 Rstep1.
Link1 : apply bisim_symmetric to Rstep3. clear Rstep3.
backchain CH.

intros Qstep.
Right1 : case Right. Sstep : apply Right5 to Qstep. clear Right1 Right2 Right3 Right4 Right5 Right6.
Middle1 : case Middle. Rstep : apply Middle5 to Sstep. clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Left1 : case Left. Pstep : apply Left5 to Rstep. clear Left1 Left2 Left3 Left4 Left5 Left6.
witness P5. split. search.
witness P5. witness Q1. intros. split. search.
clear Pstep Qstep Rstep Sstep.
Link1 : apply Sstep1 with N = N. Eq1 : case Link1. clear Sstep1.
Link1 : apply Rstep1 with N = N. Bis1 : case Link1. clear Rstep1.
Link1 : apply Pstep1 with N = N. Eq1 : case Link1. clear Pstep1.
Link1 : apply bisim_symmetric to Bis2. clear Bis2.
backchain CH.

intros Qstep.
Right1 : case Right. Sstep : apply Right6 to Qstep. clear Right1 Right2 Right3 Right4 Right5 Right6.
Middle1 : case Middle. Rstep : apply Middle6 to Sstep. clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Left1 : case Left. Pstep : apply Left6 to Rstep. clear Left1 Left2 Left3 Left4 Left5 Left6.
witness P5. split. search.
witness P5. witness Q1. intros. split. search.
clear Pstep Qstep Rstep Sstep.
case Sstep1. Link1 : case Rstep1. case Pstep1.
backchain CH.

Theorem bisim_sound_snd : is_sound_snd bisim_t.
unfold. intros.
witness P. witness Q. split.
backchain bisim_reflexive.
search.
backchain bisim_reflexive.
Theorem bisim_sound : is_sound bisim_t.
Fst : apply bisim_sound_fst. Fst : case Fst.
Snd : apply bisim_sound_snd. Snd : case Snd.
unfold. intros PQ.
apply Snd to PQ. backchain Fst.
```