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.

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. Link1 : apply bisim_transitive to Link2 Qstep2. 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 Link1 Eq1. clear Link1 Eq1. Link1 : apply bisim_transitive to Link2 Bis. clear Bis Link2. Link1 : apply bisim_eq_2R to Qstep2 Eq3. clear Qstep2 Eq3. Link1 : apply bisim_symmetric to Bis1. clear Bis1. Link1 : apply bisim_eq_2L to Link3 Eq4. clear Link3 Eq4. Link1 : apply bisim_transitive to Link4 Link2. clear Link4 Link2. 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. Link1 : apply bisim_transitive to Link2 Qstep2. clear Link2 Qstep2. 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. Link1 : apply bisim_transitive to Link2 Sstep2. clear Link2 Sstep2. 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_eq_1R to Link4 Eq4. clear Link4 Eq4. Link1 : apply bisim_eq_2R to Link1 Eq3. clear Link1 Eq3. Link1 : apply bisim_transitive to Link4 Bis1. clear Link4 Bis1. Link1 : apply bisim_symmetric to Bis2. clear Bis2. Link1 : apply bisim_eq_2L to Link4 Eq2. clear Link4 Eq2. Link1 : apply bisim_eq_2R to Link2 Eq1. clear Link2 Eq1. Link1 : apply bisim_transitive to Link5 Link4. clear Link5 Link4. 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. Link1 : apply bisim_transitive to Pstep2 Link1. clear Pstep2 Link1. Link1 : apply bisim_symmetric to Link2. clear Link2. Link1 : apply bisim_transitive to Link1 Sstep2. clear Link1 Sstep2. backchain CH.
Theorem bisim_sound_snd : is_sound_snd bisim_t. Theorem bisim_sound : is_sound bisim_t.