Library Examples
Require Import SfLib.
Require Import LibTactics.
Require Import BisimTheory.
Module ExampleTactics.
Import Stepping.
Ltac cc n:= match n with
| 1 ⇒ constructor 1 | 2 ⇒ constructor 2 | 3 ⇒ constructor 3
| 4 ⇒ constructor 4 | 5 ⇒ constructor 5 | 6 ⇒ constructor 6
| 7 ⇒ constructor 7 | 8 ⇒ constructor 8 | 9 ⇒ constructor 9
| 10 ⇒ constructor 10 | 11 ⇒ constructor 11 | 12 ⇒ constructor 12
| 13 ⇒ constructor 13 | 14 ⇒ constructor 14 | 15 ⇒ constructor 15
| 16 ⇒ constructor 16 | 17 ⇒ constructor 17 | 18 ⇒ constructor 18
| 19 ⇒ constructor 19 | 20 ⇒ constructor 20 | 21 ⇒ constructor 21
| 22 ⇒ constructor 22 | 23 ⇒ constructor 23 | 24 ⇒ constructor 24
| 25 ⇒ constructor 25 | 26 ⇒ constructor 26 | 27 ⇒ constructor 27
| 28 ⇒ constructor 28 | 29 ⇒ constructor 29 | 30 ⇒ constructor 30
end.
Ltac try_each_step prove_step_star Nconstrs max_steps constrID:= match constrID with
| S ?constrID' ⇒ solve
[ eapply @step_tcons; [cc constrID | prove_step_star Nconstrs max_steps ]
| eapply @step_lcons; [cc constrID | prove_step_star Nconstrs max_steps ]
| try_each_step prove_step_star Nconstrs max_steps constrID']
end.
Ltac prove_step_star Nconstrs max_steps := match max_steps with
| S ?max_steps' ⇒ match goal with
| |- @step_star _ ?S nil ?S ⇒ apply @step_nil
| |- @step_star _ ?S1 ?la ?S2 ⇒ first
[ eapply @single_tstep; constructor
| eapply @single_lstep; constructor
| try_each_step prove_step_star Nconstrs max_steps' Nconstrs ]
| _ ⇒ auto
end
end.
Ltac sstt Nconstrs max_steps RconstrID:= match RconstrID with
| S ?RconstrID' ⇒ solve
[ split; [| cc RconstrID]; prove_step_star Nconstrs max_steps
| split; [| cc RconstrID]; prove_step_star Nconstrs max_steps
| sstt Nconstrs max_steps RconstrID']
end.
Tactic Notation "tt" constr(Nconstrs) constr(max_steps) constr(m) := eexists; sstt Nconstrs max_steps m.
Ltac inv := match goal with
| [ H: @tstep _ _ _ |- _ ] ⇒ inverts H
| [ H: @lstep _ _ _ _ |- _ ] ⇒ inverts H
| [ H: @step_star _ _ _ _ |- _ ] ⇒ inverts H
end.
Ltac ssel Nsteps Nconstrs S:=
∃ S; split; [prove_step_star Nconstrs Nsteps | constructor].
Ltac sselL Nsteps Nconstrs a := left; ∃ a; split; auto; [prove_step_star Nconstrs Nsteps|constructor].
Ltac sselR Nsteps Nconstrs a := right; ∃ a; split; prove_step_star Nconstrs Nsteps.
End ExampleTactics.
Module SeqParBackwardSimulationFailsContrasimulationHolds.
Inductive state := p0 | p1 | p2 | p3 | p4 | p5 | p6
| q0 | q1 | q2 | q3 | q4 | q5 | q6 | q7.
Inductive tstep : state→state→Prop :=
| s_p01: tstep p0 p1
| s_p02: tstep p0 p2
| s_q01: tstep q0 q1
| s_q02: tstep q0 q2
| s_q73: tstep q7 q3
| s_q74: tstep q7 q4.
Inductive lstep : state→nat→state→Prop :=
| s_p13: lstep p1 0 p3
| s_p35: lstep p3 1 p5
| s_p24: lstep p2 0 p4
| s_p46: lstep p4 2 p6
| s_q13: lstep q1 0 q3
| s_q35: lstep q3 1 q5
| s_q07: lstep q0 0 q7
| s_q24: lstep q2 0 q4
| s_q46: lstep q4 2 q6.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state nat lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 9 S.
Tactic Notation "selL" constr(a) := sselL 3 9 a.
Tactic Notation "selR" constr(a) := sselR 3 9 a.
Tactic Notation "tt" constr(m) := tt 9 3 m.
Tactic Notation "ss" := prove_step_star 9 3.
Tactic Notation "ttt" constr(m) := do 2 eexists; split; [| sstt 9 3 m].
Tactic Notation "tttt" constr(m) := do 2 eexists; split; [apply step_nil | sstt 9 3 m].
Inductive RR : state→state→Prop :=
| RR_00: RR p0 q0
| RR_11: RR p1 q1
| RR_22: RR p2 q2
| RR_33: RR p3 q3
| RR_44: RR p4 q4
| RR_55: RR p5 q5
| RR_66: RR p6 q6.
Lemma wsim_forward_true:
∃ R, weak_simulation R ∧ R p0 q0.
Proof.
∃ RR; splits; try solve [apply RR_00]; intros p q; intros.
× split; intros.
+ inverts H; repeat inv; try solve [tt 3].
+ inverts H; repeat inv; try solve [tt 7].
Qed.
Lemma wsim_backward_false:
¬∃ R, weak_simulation R ∧ R q0 p0.
Proof.
intro.
destruct H as [R[??]].
edestruct weak_simulation_lstep with (p':=q7) as [p'[??]]; eauto.
constructor.
repeat inv.
edestruct weak_simulation_step_star with (p':=q6) as [p'[??]]; eauto.
ss.
repeat inv.
edestruct weak_simulation_step_star with (p':=q5) as [p'[??]]; eauto.
ss.
repeat inv.
Qed.
Lemma wbisim_false: ¬wbisimilar p0 q0.
Proof.
intro.
apply wsim_backward_false.
destruct H as [R[??]].
∃ (inv R); split; auto.
apply H.
Qed.
Lemma cssim_false: ¬coupled_similar p0 q0.
Proof.
intro.
apply wsim_backward_false.
destruct H as [R[?[?[?[??]]]]].
∃ R; split; auto.
Qed.
Lemma esim_true: eventually_similar p0 q0.
Proof.
∃ RR; splits; try solve [apply RR_00]; intros p q; intros.
× destruct H0.
× destruct H0.
× split; intros.
+ inverts H; repeat inv; try solve [tt 3].
+ inverts H; repeat inv; try solve [tt 7].
× inverts H; repeat inv; try solve [tttt 7; ss].
ttt 7; ss.
Qed.
Lemma csim_true: contrasimilar p0 q0.
Proof. apply ebisim_csim; apply esim_ebisim1; apply esim_true. Qed.
End Lemmas.
End SeqParBackwardSimulationFailsContrasimulationHolds.
Module ebisim_trans_false.
Inductive state : Set :=
| s1: nat→state
| s2: nat→nat→state
| s1': nat→state
| s0: state.
Inductive tstep : state→state→Prop :=
| s_t2: ∀ n m,
tstep (s2 n m) (s2 (2+n) (2+m))
| s_t1: ∀ n,
tstep (s1 n) (s1 (1+n))
| s_t1': ∀ n,
tstep (s1' n) (s2 (1+n) (2+n)).
Inductive lstep : state→nat→state→Prop :=
| s_sL: ∀ n m,
lstep (s2 n m) n s0
| s_sR: ∀ n m,
lstep (s2 n m) m s0
| s_s1: ∀ n,
lstep (s1 n) n s0
| s_s1': ∀ n,
lstep (s1' n) n s0.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state nat lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Import Stepping.
Existing Instance lts.
Lemma step_star_s0_inv: ∀ la p',
step_star s0 la p' → la=nil ∧ p'=s0.
Proof.
intros.
remember s0 as p.
revert Heqp.
induction H; intros; subst; auto; inverts H.
Qed.
Lemma step_star_s1_tau: ∀ k n,
step_star (s1 n) nil (s1 (k+n)).
Proof.
induction k; intros.
apply step_nil.
replace (S k + n) with (k + (S n)).
eapply step_tcons; eauto.
constructor.
omega.
Qed.
Lemma step_star_s1_inv: ∀ n la p',
step_star (s1 n) la p' →
∃ k,
(la=nil ∧ p'=s1 (k+n)) ∨ (la=[k+n] ∧ p'=s0).
Proof.
intros.
remember (s1 n) as p.
revert n Heqp.
induction H; intros; subst.
× ∃ 0; auto.
× inverts H.
edestruct step_star_s0_inv as [??]; eauto; subst la p''.
∃ 0; auto.
× inverts H.
edestruct IHstep_star as [k[ [??] | [??] ]]; clear IHstep_star; eauto; subst la p'';
∃ (1+k); [left|right]; split; auto; f_equal; omega.
Qed.
Lemma step_star_s2_tau: ∀ k n m,
step_star (s2 n m) nil (s2 (k+k+n) (k+k+m)).
Proof.
induction k; intros.
× apply step_nil.
× eapply step_tsnoc; eauto.
replace (S k + S k + n) with (2 + (k+k+n)).
replace (S k + S k + m) with (2 + (k+k+m)).
constructor.
omega. omega.
Qed.
Lemma step_star_s2_inv: ∀ n m la p',
step_star (s2 n m) la p' →
∃ k,
(la=nil ∧ p'=s2 (k+k+n) (k+k+m)) ∨ (la=[k+k+n] ∧ p'=s0) ∨ (la=[k+k+m]∧p'=s0).
Proof.
intros.
remember (s2 n m) as p.
revert n m Heqp.
induction H; intros; subst.
× ∃ 0; auto.
× inverts H;
edestruct step_star_s0_inv as [??]; eauto; subst la p''; ∃ 0; auto.
× inverts H.
edestruct IHstep_star as [k[ [??] | [ [??] | [??] ]]]; eauto; clear IHstep_star; subst la p''.
+ ∃ (1+k); left; split; auto; f_equal; omega.
+ ∃ (1+k); right; left; split; auto; f_equal; omega.
+ ∃ (1+k); right; right; split; auto; f_equal; omega.
Qed.
Lemma nat_div2: ∀ k, ∃ x, k=x+x ∨ k=1+x+x.
Proof.
intros.
∃ (Div2.div2 k).
destruct (Even.even_or_odd k).
left.
apply Div2.even_double; auto.
right.
apply Div2.odd_double; auto.
Qed.
Lemma esimPQ: ∀ n,
eventually_similar (s2 n (1+n)) (s1 n).
Proof.
intros.
∃ (fun p q ⇒ (∃ n, p=s2 n (1+n) ∧ q=s1 n) ∨ q=p).
splits; eauto; clear n; intros p q; unfold inv in *; intros.
× destruct H0.
× destruct H0.
× destruct H as [ [n[??]] | ?]; subst; split; intros.
+ inverts H.
∃ (s1 (2+n)); split; eauto.
eapply step_tcons. constructor. apply single_tstep; constructor.
+ inverts H; ∃ s0; split; auto.
apply single_lstep; constructor.
eapply step_tcons. constructor. apply single_lstep. constructor.
+ ∃ p'; split; auto. apply single_tstep; auto.
+ ∃ p'; split; auto. apply single_lstep; auto.
× destruct H as [ [n[??]] | ?]; subst; intros.
+ edestruct step_star_s1_inv as [k[ [??] | [??] ]]; eauto; subst la p'.
- destruct (nat_div2 k) as [x[?|?]]; subst.
∃ (s1 (x + x + n)) (s2 (x+x+n) (x+x+(1+n))); splits; eauto.
apply step_nil.
apply step_star_s2_tau.
do 2 eexists; splits.
apply single_tstep. constructor.
apply step_star_s2_tau with (k:=1+x).
left; ∃ (2+x+x+n); split; auto; f_equal; omega.
- ∃ s0 s0; splits; auto.
apply step_nil.
change [k+n] with ([]++[k+n]).
destruct (nat_div2 k) as [x[?|?]]; subst.
eapply step_lsnoc; [| apply s_sL].
apply step_star_s2_tau with (k:=x).
eapply step_lsnoc; [| apply s_sR].
replace (1+x+x+n) with (x+x+(1+n)).
apply step_star_s2_tau.
omega.
+ ∃ p' p'; split; auto. apply step_nil.
Qed.
Lemma esimRQ: ∀ n,
eventually_similar (s1' n) (s1 n).
Proof.
intros.
∃ (fun p q ⇒ (∃ n, p=s1' n∧q=s1 n) ∨ eventually_similar p q).
splits; eauto; clear n; intros p q; unfold inv in *; intros.
× destruct H0.
× destruct H0.
× destruct H as [ [n[??]] | ?]; subst; split; intros.
+ inverts H.
∃ (s1 (1+n)); split.
apply single_tstep; constructor.
right.
apply esimPQ.
+ inverts H.
∃ s0; split; auto.
apply single_lstep; constructor.
right; apply esim_refl.
+ edestruct tstep_esim1 as [q'[??]]; eauto.
+ edestruct lstep_esim1 as [q'[??]]; eauto.
× destruct H as [ [n[??]] | ?]; subst; intros.
+ edestruct step_star_s1_inv as [k[ [??] | [??] ]]; eauto; subst la p'.
- destruct (nat_div2 k) as [x[?|?]]; subst.
do 2 eexists; splits.
apply single_tstep. constructor.
eapply step_tcons. constructor.
apply step_star_s2_tau with (k:=x).
right.
replace (1+(x+x+n)) with (x+x+(1+n)).
replace (x + x + (2 + n)) with (1+(x+x+(1+n))).
apply esimPQ.
omega. omega.
do 2 eexists; splits.
apply step_nil.
eapply step_tcons. constructor.
apply step_star_s2_tau with (k:=x).
right.
replace (x+x+(2+n)) with (1+(x+x+(1+n))).
replace (1+x+x+n) with (x+x+(1+n)).
apply esimPQ.
omega. omega.
- ∃ s0 s0; splits; auto.
apply step_nil.
destruct k.
apply single_lstep; constructor.
eapply step_tcons. constructor.
change [S k+n] with ([]++[S k+n]).
destruct (nat_div2 k) as [x[?|?]]; subst.
eapply step_lsnoc; [| apply s_sL].
replace (S (x+x)+n) with (x+x+(1+n)).
apply step_star_s2_tau.
omega.
eapply step_lsnoc; [| apply s_sR].
replace (S (1+x+x)+n) with (x+x+(2+n)).
apply step_star_s2_tau.
omega.
right. apply esim_refl.
+ edestruct step_star_esim2 as [q''[p''[?[??]]]]; eauto.
∃ p'' q''; splits; eauto.
Qed.
Lemma step_star_s2_out: ∀ n m k p',
step_star (s2 n m) [k] p' → min n m ≤ k.
Proof.
intros.
remember (s2 n m) as p.
remember [k] as la.
revert n m k Heqp Heqla.
induction H; intros; subst.
× false.
× inverts Heqla.
inverts H.
+ apply Min.le_min_l.
+ apply Min.le_min_r.
× inverts H.
specialize (IHstep_star (2+n) (2+m) k).
lapply IHstep_star; intros; auto.
lapply H; intros; auto.
rewrite Min.plus_min_distr_l in H1.
omega.
Qed.
Lemma ebisimPR_false: ∀ n,
¬eventually_bisimilar (s2 n (1+n)) (s1' n).
Proof.
intros; intro.
edestruct tstep_ebisim2 as [p'[q'[?[??]]]]; eauto.
constructor.
edestruct step_star_s2_inv with (p':=p') as [k[ [??] | [ [??] | [??] ] ]]; eauto; try discriminate.
edestruct step_star_s2_inv with (p':=q') as [k'[ [??] | [ [??] | [??] ] ]]; eauto; try discriminate.
subst. clear H3 H5 H1 H0 H.
simpl in ×.
destruct (le_lt_dec k k') as [?|?].
+ edestruct lstep_ebisim1 as [p'[q'[?[??]]]]; eauto.
apply s_sL.
apply step_star_s2_out in H0.
clear -H0 l.
apply NPeano.Nat.min_le_iff in H0.
omega.
+ edestruct lstep_ebisim2 as [p'[q'[?[??]]]]; eauto.
apply s_sL.
apply step_star_s2_out in H.
clear -H l.
apply NPeano.Nat.min_le_iff in H.
omega.
Qed.
Lemma ebisim_trans_false: ∃ p q r,
eventually_bisimilar p q ∧ eventually_bisimilar q r ∧ ¬eventually_bisimilar p r.
Proof.
∃ (s2 0 1) (s1 0) (s1' 0); splits.
apply esim_ebisim1. apply esimPQ.
apply esim_ebisim2. apply esimRQ.
intro. apply ebisimPR_false in H. auto.
Qed.
End Lemmas.
End ebisim_trans_false.
Module ExampleA.
Inductive state : Set := Sa|Sb|Sc|Sd|Se|Sf|Sg|Sh|Si.
Definition label := nat.
Inductive lstep : state→label→state→Prop :=
| lstep_ab: lstep Sa 1 Sb
| lstep_bc: lstep Sb 2 Sc
| lstep_bd: lstep Sb 3 Sd
| lstep_ef: lstep Se 1 Sf
| lstep_eg: lstep Se 1 Sg
| lstep_fh: lstep Sf 2 Sh
| lstep_gi: lstep Sg 3 Si.
Inductive tstep : state→state→Prop := .
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Existing Instance lts.
Import ExampleTactics.
Lemma wbisim_false:
wbisimilar Sa Se → False.
Proof.
intros.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_ab.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_bd.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_bc.
repeat inv.
Qed.
Lemma csim_false:
contrasimilar Sa Se → False.
Proof.
intros.
apply csim_pcsim2 in H.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_ef. clear H.
repeat inv.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_bd. clear H1.
repeat inv.
Qed.
Lemma cssim_false:
coupled_similar Sa Se → False.
Proof.
intros.
apply cssim_pcssim2 in H.
edestruct lstep_pcssim as [p'[??]]; eauto.
apply lstep_ef.
repeat inv.
edestruct flip_pcssim as [p''[??]]; eauto.
repeat inv.
edestruct lstep_pcssim as [q'[??]]; eauto.
apply lstep_bd.
repeat inv.
Qed.
Lemma pbisim_false1:
par_bisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply pbisim_csim; auto.
Qed.
Lemma pbisim_false2:
par_bisimilar Se Sa → False.
Proof.
intros.
eapply csim_false.
apply csim_symm.
apply pbisim_csim; auto.
Qed.
End Lemmas.
End ExampleA.
Module ExampleB.
Inductive state:= Sa|Sb|Sc|Sd|Se|Sf|Sg|Sh|Si.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_ab: lstep Sa 1 Sb
| lstep_ce: lstep Sc 1 Se
| lstep_df: lstep Sd 1 Sf
| lstep_he: lstep Sh 1 Se
| lstep_if: lstep Si 1 Sf.
Inductive tstep : state→state→Prop :=
| tstep_ac: tstep Sa Sc
| tstep_ad: tstep Sa Sd
| tstep_be: tstep Sb Se
| tstep_bf: tstep Sb Sf
| tstep_gh: tstep Sg Sh
| tstep_gi: tstep Sg Si.
Definition is_halted p := p=Se∨p=Sf.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system _ _ lstep tstep is_halted _ _).
Next Obligation.
destruct H as [?|?]; subst p; inverts H0.
Qed.
Next Obligation.
destruct H as [?|?]; subst p; inverts H0.
Qed.
Section Lemmas.
Existing Instance lts.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 6 S.
Tactic Notation "selL" constr(a) := sselL 3 6 a.
Tactic Notation "selR" constr(a) := sselR 3 6 a.
Tactic Notation "tt" constr(m) := tt 6 3 m.
Tactic Notation "ss" := prove_step_star 6 3.
Lemma wbisim_false:
wbisimilar Sa Sg → False.
Proof.
intros.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_ab. clear H.
repeat inv.
edestruct tstep_wbisim1 as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_wbisim1 in H0.
repeat inv.
compute; auto.
edestruct tstep_wbisim1 as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_wbisim1 in H0.
repeat inv.
compute; auto.
Qed.
Lemma csim_false:
coupled_similar Sa Sg → False.
Proof.
intros.
edestruct lstep_pcssim as [q'[??]]; eauto.
apply lstep_ab.
apply cssim_pcssim1; eauto.
repeat inv.
edestruct tstep_pcssim as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_pcssim1 in H2; auto.
repeat inv.
compute; auto.
edestruct tstep_pcssim as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_pcssim1 in H2; auto.
repeat inv.
compute; auto.
Qed.
Import Stepping.
Inductive Rp : state→state→Prop :=
| Rp_ga: Rp Sg Sa
| Rp_ee: Rp Se Se | Rp_ff: Rp Sf Sf
| Rp_cc: Rp Sc Sc | Rp_dd: Rp Sd Sd
| Rp_hc: Rp Sh Sc | Rp_id: Rp Si Sd.
Lemma pbisim_true1:
par_bisimilar Sg Sa.
Proof.
∃ Rp.
split; [| constructor].
splits; auto; intros p q ?; intros.
× destruct H0; subst p; inverts H; ss.
× destruct H0; subst p; inverts H; ss.
× split; intros.
- intros; inverts H; repeat inv; tt 7.
- intros; inverts H; repeat inv; tt 7.
× unfold inv in *; inverts H; repeat inv; try solve [left; tt 7].
selR Se.
Qed.
Lemma pbisim_false2:
par_bisimilar Sa Sg → False.
Proof.
intros.
edestruct lstep_pbisim1 as [q'[??]]; eauto.
apply lstep_ab. clear H.
repeat inv.
edestruct tstep_pbisim1 as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_pbisim1 in H0.
repeat inv.
compute; auto.
edestruct tstep_pbisim1 as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_pbisim1 in H0.
repeat inv.
compute; auto.
Qed.
Lemma csim_true:
contrasimilar Sg Sa.
Proof.
apply pbisim_csim.
apply pbisim_true1.
Qed.
End Lemmas.
End ExampleB.
Module ExampleB_Full.
Inductive state:=
| Pa|Pb|Pc|Pd|Pe
| Qa|Qb|Qc|Qd|Qe|Qf|Qg|Qh|Qi|Qj|Qk|Ql|Qm|Qn|Qo|Qp|Qq
| Sw|Sx|Sy|Sz.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_Swy: lstep Sw 1 Sy
| lstep_Sxz: lstep Sx 1 Sz
| lstep_Qbe: lstep Qb 1 Qe
| lstep_Qfn: lstep Qf 1 Qn
| lstep_Qgo: lstep Qg 1 Qo
| lstep_Qhp: lstep Qh 1 Qp
| lstep_Qjq: lstep Qj 1 Qq.
Inductive tstep : state→state→Prop :=
| tstep_Pab: tstep Pa Pb
| tstep_Pac: tstep Pa Pc
| tstep_Pbd: tstep Pb Pd
| tstep_Pce: tstep Pc Pe
| tstep_Pdw: tstep Pd Sw
| tstep_Pex: tstep Pe Sx
| tstep_Qab: tstep Qa Qb
| tstep_Qac: tstep Qa Qc
| tstep_Qad: tstep Qa Qd
| tstep_Qbf: tstep Qb Qf
| tstep_Qbg: tstep Qb Qg
| tstep_Qch: tstep Qc Qh
| tstep_Qci: tstep Qc Qi
| tstep_Qdj: tstep Qd Qj
| tstep_Qdk: tstep Qd Qk
| tstep_Qel: tstep Qe Ql
| tstep_Qem: tstep Qe Qm
| tstep_Qfw: tstep Qf Sw
| tstep_Qgx: tstep Qg Sx
| tstep_Qhw: tstep Qh Sw
| tstep_Qiw: tstep Qi Sw
| tstep_Qjx: tstep Qj Sx
| tstep_Qkx: tstep Qk Sx
| tstep_Qly: tstep Ql Sy
| tstep_Qmz: tstep Qm Sz
| tstep_Qny: tstep Qn Sy
| tstep_Qoz: tstep Qo Sz
| tstep_Qpy: tstep Qp Sy
| tstep_Qqz: tstep Qq Sz.
Definition is_halted p := p=Sy∨p=Sz.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system _ _ lstep tstep is_halted _ _).
Next Obligation.
destruct H as [?|?]; subst p; inverts H0.
Qed.
Next Obligation.
destruct H as [?|?]; subst p; inverts H0.
Qed.
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 4 29 S.
Tactic Notation "selL" constr(a) := sselL 4 29 a.
Tactic Notation "selR" constr(a) := sselR 4 29 a.
Tactic Notation "tt" constr(m) := tt 29 4 m.
Tactic Notation "ss" := prove_step_star 29 4.
Ltac ss_split S :=
match goal with
| [ |- step_star ?p ?la ?p' ] ⇒ let la1:=fresh "la1" in let la2:= fresh "la2" in let H:=fresh "H" in
evar (la1: list lts_L); evar (la2: list lts_L);
cut (la = la1++la2); subst la1 la2; [intros H; rewrite H; eapply (@step_star_app _ _ _ S); ss | try reflexivity]
| [ |- step_star ?p _ ?p' ] ⇒ eapply (@step_star_app _ _ _ S); ss
end.
Lemma wbisim_false:
wbisimilar Pa Qa → False.
Proof.
intros.
edestruct step_star_wbisim2 with (q:=Qa) (q':=Qe) as [q'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_wbisim2 with (q:=Qe) (q':=Sz) as [q'[??]]; eauto.
ss.
repeat inv.
apply halted_wbisim1 in H2.
repeat inv.
compute; auto.
edestruct step_star_wbisim2 with (q:=Qe) (q':=Sy) as [q'[??]]; eauto.
ss.
repeat inv.
apply halted_wbisim1 in H2.
repeat inv.
compute; auto.
Qed.
Lemma cssim_false:
coupled_similar Pa Qa → False.
Proof.
intros.
apply cssim_pcssim2 in H.
edestruct step_star_pcssim with (p:=Qa) (p':=Qe) as [q'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_pcssim with (p:=Qe) (p':=Sz) as [q'[??]]; eauto.
ss.
repeat inv.
apply halted_pcssim1 in H2; auto.
repeat inv.
compute; auto.
edestruct step_star_pcssim with (p:=Qe) (p':=Sy) as [q'[??]]; eauto.
ss.
repeat inv.
apply halted_pcssim1 in H2; auto.
repeat inv.
compute; auto.
Qed.
Inductive Rp : state→state→Prop :=
| Rp_init: Rp Pa Qa
| Rp_ww: Rp Sw Sw | Rp_xx: Rp Sx Sx | Rp_yy: Rp Sy Sy | Rp_zz: Rp Sz Sz
| Rp_bw: Rp Pb Sw | Rp_cx: Rp Pc Sx
| Rp_dw: Rp Pd Sw | Rp_ex: Rp Pe Sx.
Lemma pbisim_true2:
par_bisimilar Pa Qa.
Proof.
∃ Rp.
split; [| constructor].
splits; intros p q ?; unfold inv in ×.
× intros [?|?]; subst; inverts H; ss.
× intros [?|?]; subst; inverts H; ss.
× split; intros.
- inverts H; repeat inv; try solve [tt 9].
- inverts H; repeat inv; tt 9.
× intros. inverts H; repeat inv; try solve [left; tt 9].
selR Sx.
selR Sy.
selR Sy.
selR Sz.
selR Sw.
selR Sy.
selR Sx.
selR Sz.
selR Sw.
selR Sw.
selR Sy.
selR Sw.
selR Sx.
selR Sx.
selR Sz.
selR Sx.
Qed.
Lemma pbisim_false1:
par_bisimilar Qa Pa → False.
Proof.
intros.
edestruct step_star_pbisim1 with (p:=Qa) (p':=Qe) as [p'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_pbisim1 with (p:=Qe) (p':=Sz) as [p'[??]]; eauto.
ss.
repeat inv.
apply halted_pbisim1 in H2.
repeat inv.
compute; auto.
edestruct step_star_pbisim1 with (p:=Qe) (p':=Sy) as [p'[??]]; eauto.
ss.
repeat inv.
apply halted_pbisim2 in H2.
repeat inv.
compute; auto.
Qed.
Lemma csim_true:
contrasimilar Qa Pa.
Proof.
apply csim_symm.
apply pbisim_csim.
apply pbisim_true2.
Qed.
End Lemmas.
End ExampleB_Full.
Module ExampleB'.
Inductive state:= Sa|Sb|Sc|Sd|Se|Sf|Sg|Sh|Si.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_ab: lstep Sa 1 Sb
| lstep_ce: lstep Sc 1 Se
| lstep_df: lstep Sd 1 Sf.
Inductive tstep : state→state→Prop :=
| tstep_ac: tstep Sa Sc
| tstep_ad: tstep Sa Sd
| tstep_be: tstep Sb Se
| tstep_bf: tstep Sb Sf
| tstep_cg: tstep Sc Sg
| tstep_dh: tstep Sd Sh
| tstep_ic: tstep Si Sc
| tstep_id: tstep Si Sd.
Definition is_halted p := p=Se∨p=Sf∨p=Sg∨p=Sh.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system _ _ lstep tstep is_halted _ _).
Next Obligation.
destruct H as [?|[?|[?|?]]]; subst p; inverts H0.
Qed.
Next Obligation.
destruct H as [?|[?|[?|?]]]; subst p; inverts H0.
Qed.
Section Lemmas.
Existing Instance lts.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 8 S.
Tactic Notation "selL" constr(a) := sselL 3 8 a.
Tactic Notation "selR" constr(a) := sselR 3 8 a.
Tactic Notation "tt" constr(m) := tt 8 3 m.
Tactic Notation "ss" := prove_step_star 8 3.
Lemma wbisim_false:
wbisimilar Sa Si → False.
Proof.
intros.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_ab. clear H.
repeat inv.
edestruct tstep_wbisim1 as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_wbisim1 in H0.
repeat inv.
compute; auto.
edestruct tstep_wbisim1 as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_wbisim1 in H0.
repeat inv.
compute; auto.
Qed.
Lemma cssim_false:
coupled_similar Sa Si → False.
Proof.
intros.
edestruct lstep_pcssim as [q'[??]]; eauto.
apply lstep_ab.
apply cssim_pcssim1; eauto.
repeat inv.
edestruct tstep_pcssim with (p:=Sb) as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_pcssim1 in H2.
repeat inv.
compute; auto.
edestruct tstep_pcssim with (p:=Sb) as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_pcssim1 in H2.
repeat inv.
compute; auto.
Qed.
Import Stepping.
Inductive Rp : state→state→Prop :=
| Rp_ia: Rp Si Sa
| Rp_ee: Rp Se Se | Rp_ff: Rp Sf Sf | Rp_gg: Rp Sg Sg | Rp_hh: Rp Sh Sh
| Rp_cc: Rp Sc Sc | Rp_dd: Rp Sd Sd.
Lemma pbisim_true1:
par_bisimilar Si Sa.
Proof.
∃ Rp.
split; [| constructor].
splits; intros p q ?.
× intros [?|[?|[?|?]]]; subst; inverts H; ss.
× intros [?|[?|[?|?]]]; subst; inverts H; ss.
× split; intros.
- inverts H; repeat inv; tt 7.
- inverts H; repeat inv; tt 7.
× intros.
inverts H; repeat inv; try solve [left; tt 7].
selR Se.
Qed.
Lemma pbisim_false2:
par_bisimilar Sa Si → False.
Proof.
intros.
edestruct lstep_pbisim1 as [q'[??]]; eauto.
apply lstep_ab. clear H.
repeat inv.
edestruct tstep_pbisim1 as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_pbisim1 in H0.
repeat inv.
compute; auto.
edestruct tstep_pbisim1 as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_pbisim1 in H0.
repeat inv.
compute; auto.
Qed.
Lemma csim_true:
contrasimilar Sa Si.
Proof.
apply csim_symm.
apply pbisim_csim.
apply pbisim_true1.
Qed.
End Lemmas.
End ExampleB'.
Module ExampleC.
Inductive state : Set := Sa | Sb | Sc | Sd | Se | Sf | Sg | Sh.
Definition label := nat.
Inductive lstep : state→label→state→Prop :=
| lstep_ab: lstep Sa 1 Sb
| lstep_bc: lstep Sb 2 Sc
| lstep_ef: lstep Se 1 Sf
| lstep_eg: lstep Se 1 Sg
| lstep_fh: lstep Sf 2 Sh.
Inductive tstep : state→state→Prop := .
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Existing Instance lts.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 2 5 S.
Tactic Notation "selL" constr(a) := sselL 2 5 a.
Tactic Notation "selR" constr(a) := sselR 2 5 a.
Tactic Notation "tt" constr(m) := tt 5 2 m.
Tactic Notation "ss" := prove_step_star 5 2.
Lemma wbisim_false:
wbisimilar Sa Se → False.
Proof.
intros.
edestruct lstep_wbisim2 as [q'[??]]; eauto.
apply lstep_eg. clear H.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_bc.
repeat inv.
Qed.
Lemma cssim_false:
coupled_similar Sa Se → False.
Proof.
intros.
edestruct lstep_pcssim as [p'[??]].
apply lstep_eg.
apply cssim_pcssim2; eauto.
repeat inv.
edestruct flip_pcssim as [p'[??]]; eauto.
repeat inv.
edestruct lstep_pcssim with (p:=Sb) as [q'[??]]; eauto.
apply lstep_bc.
repeat inv.
Qed.
Lemma csim_false:
contrasimilar Sa Se → False.
Proof.
intros.
apply csim_pcsim2 in H.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_eg. clear H.
repeat inv.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_bc. clear H1.
repeat inv.
Qed.
Lemma pbisim_false1:
par_bisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply pbisim_csim; auto.
Qed.
Lemma wbisim_false2:
wbisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply wbisim_csim; auto.
Qed.
End Lemmas.
End ExampleC.
Module ExampleD. Inductive state : Set := Sa | Sb | Sc | Sd | Se | Sf | Sg | Sh | Si.
Inductive label : Set := pay_cent | pick_tea | pick_coffee | tea | coffee.
Inductive lstep : state→label→state→Prop :=
| lstep_ab: lstep Sa pay_cent Sb
| lstep_bc: lstep Sb pick_tea Sc
| lstep_bd: lstep Sb pick_coffee Sd
| lstep_ca: lstep Sc tea Sa
| lstep_da: lstep Sd coffee Sa
| lstep_ef: lstep Se pay_cent Sf
| lstep_eg: lstep Se pay_cent Sg
| lstep_fh: lstep Sh pick_tea Sh
| lstep_gi: lstep Sg pick_coffee Si
| lstep_he: lstep Sh tea Se
| lstep_ie: lstep Si coffee Se.
Inductive tstep : state→state→Prop := .
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 11 S.
Tactic Notation "selL" constr(a) := sselL 3 11 a.
Tactic Notation "selR" constr(a) := sselR 3 11 a.
Tactic Notation "tt" constr(m) := tt 11 3 m.
Tactic Notation "ss" := prove_step_star 11 3.
Lemma wbisim_false:
wbisimilar Sa Se → False.
Proof.
intros.
edestruct lstep_wbisim2 as [q'[??]]; eauto.
apply lstep_ef. clear H.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_bc.
repeat inv.
Qed.
Lemma cssim_false:
coupled_similar Sa Se → False.
Proof.
intros.
edestruct lstep_pcssim as [p'[??]].
apply lstep_eg.
apply cssim_pcssim2; eauto.
repeat inv.
edestruct flip_pcssim as [p'[??]]; eauto.
repeat inv.
edestruct lstep_pcssim as [p'[??]]; eauto.
apply lstep_bc.
repeat inv.
Qed.
Lemma csim_false:
contrasimilar Sa Se → False.
Proof.
intros.
apply csim_pcsim2 in H.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_eg. clear H.
repeat inv.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_bc. clear H1.
repeat inv.
Qed.
Lemma pbisim_false1:
par_bisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply pbisim_csim; auto.
Qed.
Lemma par_bisim_false2:
par_bisimilar Se Sa → False.
Proof.
intros.
eapply csim_false.
apply csim_symm.
apply pbisim_csim; auto.
Qed.
End Lemmas.
End ExampleD.
Module ExampleE.
Inductive state : Set := Sa | Sb | Sc | Sd | Se.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_ac: lstep Sa 2 Sc
| lstep_bd: lstep Sb 1 Sd
| lstep_ed: lstep Se 1 Sd
| lstep_ec: lstep Se 2 Sc.
Inductive tstep : state→state→Prop :=
| tstep_ab: tstep Sa Sb.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 2 4 S.
Tactic Notation "selL" constr(a) := sselL 2 4 a.
Tactic Notation "selR" constr(a) := sselR 2 4 a.
Tactic Notation "tt" constr(m) := tt 4 2 m.
Tactic Notation "ss" := prove_step_star 4 2.
Lemma csim_false:
contrasimilar Sa Se → False.
Proof.
intros.
apply csim_pcsim1 in H.
edestruct tstep_pcsim as [q'[??]]; eauto.
apply tstep_ab.
repeat inv.
edestruct lstep_pcsim as [p'[??]]; eauto.
apply lstep_ec.
repeat inv.
Qed.
Lemma wbisim_false:
wbisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply wbisim_csim; auto.
Qed.
Lemma pbisim_false1:
par_bisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply pbisim_csim; auto.
Qed.
Lemma pbisim_false2:
par_bisimilar Se Sa → False.
Proof.
intros.
eapply csim_false.
apply csim_symm.
apply pbisim_csim; auto.
Qed.
Lemma cssim_false:
coupled_similar Sa Se → False.
Proof.
intros.
edestruct tstep_pcssim as [q'[??]].
apply tstep_ab.
apply cssim_pcssim1; eauto.
repeat inv.
edestruct flip_pcssim as [q'[??]]; eauto.
repeat inv.
edestruct lstep_pcssim with (p:=Se) as [p'[??]]; eauto.
apply lstep_ec.
repeat inv.
Qed.
End Lemmas.
End ExampleE.
Module ExampleF.
Inductive state : Set := Sa | Sb | Sc | Sd | Se | Sf | Sg | Sh | Si | Sj | Sk | Sl.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_be: lstep Sb 1 Se
| lstep_cf: lstep Sc 2 Sf
| lstep_dg: lstep Sd 3 Sg
| lstep_ie: lstep Si 1 Se
| lstep_kf: lstep Sk 2 Sf
| lstep_lg: lstep Sl 3 Sg.
Inductive tstep : state→state→Prop :=
| tstep_ab: tstep Sa Sb
| tstep_ac: tstep Sa Sc
| tstep_ad: tstep Sa Sd
| tstep_hi: tstep Sh Si
| tstep_hj: tstep Sh Sj
| tstep_jk: tstep Sj Sk
| tstep_jl: tstep Sj Sl.
Definition is_halted (p:state) := False.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep is_halted _ _).
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 7 S.
Tactic Notation "selL" constr(a) := sselL 3 7 a.
Tactic Notation "selR" constr(a) := sselR 3 7 a.
Tactic Notation "tt" constr(m) := tt 7 3 m.
Tactic Notation "ss" := prove_step_star 7 3.
Lemma wbisim_false:
wbisimilar Sa Sh → False.
Proof.
intros.
edestruct tstep_wbisim2 as [p'[??]]; eauto.
apply tstep_hj.
clear H.
inverts H0.
edestruct step_star_wbisim1 with (p':=Se) as [q'[??]]; eauto.
ss.
repeat inv.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_be.
repeat inv.
edestruct step_star_wbisim2 with (q':=Sg) as [p'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_wbisim2 with (q':=Sf) as [p'[??]]; eauto.
ss.
repeat inv.
Qed.
Inductive Rc1 : state→state→Prop :=
| Rc1_ah: Rc1 Sa Sh | Rc1_bi: Rc1 Sb Si | Rc1_ck: Rc1 Sc Sk | Rc1_dl: Rc1 Sd Sl
| Rc1_ee: Rc1 Se Se | Rc1_ff: Rc1 Sf Sf | Rc1_gg: Rc1 Sg Sg
| Rc1_cj: Rc1 Sc Sj.
Inductive Rc2 : state→state→Prop :=
| Rc2_ah: Rc2 Sa Sh | Rc2_bi: Rc2 Sb Si | Rc2_ck: Rc2 Sc Sk | Rc2_dl: Rc2 Sd Sl
| Rc2_ee: Rc2 Se Se | Rc2_ff: Rc2 Sf Sf | Rc2_gg: Rc2 Sg Sg
| Rc2_aj: Rc2 Sa Sj.
Lemma cssim_true:
coupled_similar Sa Sh.
Proof.
apply coupled_similar_equiv.
∃ Rc1 Rc2.
splits; try solve [constructor]; intros p q; intros.
× inverts H; tt 8.
× inverts H; tt 8.
× destruct H0.
× destruct H0.
× split; intros.
- inverts H; inverts H0; tt 8.
- inverts H; inverts H0; tt 8.
× split; intros.
- inverts H; inverts H0; tt 8.
- inverts H; inverts H0; tt 8.
Qed.
Lemma pbisim_false1:
par_bisimilar Sh Sa → False.
Proof.
intros.
edestruct tstep_pbisim1 as [p'[??]]; eauto.
apply tstep_hj.
clear H.
repeat inv.
edestruct step_star_pbisim2 with (q':=Se)
as [ [q'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
edestruct step_star_pbisim2 with (q':=Se)
as [ [q'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
edestruct step_star_pbisim1 with (p':=Sg)
as [p'[??]]; eauto; [ss | ]; repeat inv.
edestruct step_star_pbisim1 with (p':=Sf)
as [p'[??]]; eauto; [ss | ]; repeat inv.
Qed.
Lemma pbisim_false2:
par_bisimilar Sa Sh → False.
Proof.
intros.
edestruct tstep_pbisim2 as [ [p'[??]] | [pq'[??]] ]; eauto.
apply tstep_hj.
repeat inv.
edestruct step_star_pbisim1 with (p':=Se) as [q'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_pbisim1 with (p':=Se) as [q'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_pbisim2 with (q':=Sg)
as [ [p'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
edestruct step_star_pbisim2 with (q':=Sf)
as [ [p'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
repeat inv.
Qed.
Inductive Rd : state→state→Prop :=
| Rd_ha: Rd Sh Sa | Rd_ah: Rd Sa Sh
| Rd_bi: Rd Sb Si | Rd_cj: Rd Sc Sj | Rd_ck: Rd Sc Sk
| Rd_dl: Rd Sd Sl | Rd_ib: Rd Si Sb | Rd_kc: Rd Sk Sc
| Rd_ld: Rd Sl Sd
| Rd_ee: Rd Se Se | Rd_ff: Rd Sf Sf | Rd_gg: Rd Sg Sg.
Lemma csim_true:
contrasimilar Sa Sh.
Proof.
∃ Rd.
splits; try solve [constructor]; intros p q ?; intros.
- destruct H0.
- inverts H; inverts H0; repeat inv; tt 12.
Qed.
End Lemmas.
End ExampleF.
Module ExampleG.
Inductive state : Set := Sa | Sb | Sc | Sd | Se | Sf | Sg | Sh | Sj.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_be: lstep Sb 1 Se
| lstep_cf: lstep Sc 2 Sf
| lstep_dg: lstep Sd 3 Sg.
Inductive tstep : state→state→Prop :=
| tstep_ab: tstep Sa Sb
| tstep_ac: tstep Sa Sc
| tstep_ad: tstep Sa Sd
| tstep_hb: tstep Sh Sb
| tstep_hj: tstep Sh Sj
| tstep_jc: tstep Sj Sc
| tstep_jd: tstep Sj Sd.
Definition is_halted (p:state) := False.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep is_halted _ _).
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 7 S.
Tactic Notation "selL" constr(a) := sselL 3 7 a.
Tactic Notation "selR" constr(a) := sselR 3 7 a.
Tactic Notation "tt" constr(m) := tt 7 3 m.
Tactic Notation "ss" := prove_step_star 7 3.
Lemma wbisim_false:
wbisimilar Sa Sh → False.
Proof.
intros.
edestruct tstep_wbisim2 as [p'[??]]; eauto.
apply tstep_hj.
clear H.
inverts H0.
edestruct step_star_wbisim1 with (p':=Se) as [q'[??]]; eauto.
ss.
repeat inv.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_be.
repeat inv.
edestruct step_star_wbisim2 with (q':=Sg) as [p'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_wbisim2 with (q':=Sf) as [p'[??]]; eauto.
ss.
repeat inv.
Qed.
Inductive Rc1 : state→state→Prop :=
| Rc1_ah: Rc1 Sa Sh | Rc1_bb: Rc1 Sb Sb | Rc1_cc: Rc1 Sc Sc | Rc1_dd: Rc1 Sd Sd
| Rc1_ee: Rc1 Se Se | Rc1_ff: Rc1 Sf Sf | Rc1_gg: Rc1 Sg Sg
| Rc1_cj: Rc1 Sc Sj.
Inductive Rc2 : state→state→Prop :=
| Rc2_ah: Rc2 Sa Sh | Rc2_bb: Rc2 Sb Sb | Rc2_cc: Rc2 Sc Sc | Rc2_dd: Rc2 Sd Sd
| Rc2_ee: Rc2 Se Se | Rc2_ff: Rc2 Sf Sf | Rc2_gg: Rc2 Sg Sg
| Rc2_aj: Rc2 Sa Sj.
Lemma cssim_true:
coupled_similar Sa Sh.
Proof.
apply coupled_similar_equiv.
∃ Rc1 Rc2.
splits; try solve [constructor]; intros p q; intros.
× inverts H; tt 8.
× inverts H; tt 8.
× destruct H0.
× destruct H0.
× split; intros.
+ inverts H; inverts H0; tt 8.
+ inverts H; inverts H0; tt 8.
× split; intros.
+ inverts H; inverts H0; tt 8.
+ inverts H; inverts H0; tt 8.
Qed.
Lemma pbisim_false1:
par_bisimilar Sh Sa → False.
Proof.
intros.
edestruct tstep_pbisim1 as [q'[??]]; eauto.
apply tstep_hj.
clear H.
repeat inv.
edestruct step_star_pbisim2 with (q':=Se)
as [ [q'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
edestruct step_star_pbisim2 with (q':=Se)
as [ [q'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
edestruct step_star_pbisim1 with (p':=Sg)
as [p'[??]]; eauto; [ss | ]; repeat inv.
edestruct step_star_pbisim1 with (p':=Sf)
as [p'[??]]; eauto; [ss | ]; repeat inv.
Qed.
Inductive Rp : state→state→Prop :=
| Rp_ah: Rp Sa Sh | Rp_bb: Rp Sb Sb | Rp_cc: Rp Sc Sc | Rp_dd: Rp Sd Sd
| Rp_ee: Rp Se Se | Rp_ff: Rp Sf Sf | Rp_gg: Rp Sg Sg.
Lemma pbisim_true2:
par_bisimilar Sa Sh.
Proof.
∃ Rp.
split; [|constructor].
splits; intros p q; intros.
× destruct H0.
× destruct H0.
× split; intros.
- inverts H; repeat inv; tt 8.
- inverts H; repeat inv; tt 8.
× inverts H; repeat inv; try solve [left; tt 8].
right; ∃ Sc; split; ss.
Qed.
Lemma csim_true:
contrasimilar Sa Sh.
Proof.
intros.
apply pbisim_csim.
apply pbisim_true2.
Qed.
End Lemmas.
End ExampleG.
Require Import LibTactics.
Require Import BisimTheory.
Module ExampleTactics.
Import Stepping.
Ltac cc n:= match n with
| 1 ⇒ constructor 1 | 2 ⇒ constructor 2 | 3 ⇒ constructor 3
| 4 ⇒ constructor 4 | 5 ⇒ constructor 5 | 6 ⇒ constructor 6
| 7 ⇒ constructor 7 | 8 ⇒ constructor 8 | 9 ⇒ constructor 9
| 10 ⇒ constructor 10 | 11 ⇒ constructor 11 | 12 ⇒ constructor 12
| 13 ⇒ constructor 13 | 14 ⇒ constructor 14 | 15 ⇒ constructor 15
| 16 ⇒ constructor 16 | 17 ⇒ constructor 17 | 18 ⇒ constructor 18
| 19 ⇒ constructor 19 | 20 ⇒ constructor 20 | 21 ⇒ constructor 21
| 22 ⇒ constructor 22 | 23 ⇒ constructor 23 | 24 ⇒ constructor 24
| 25 ⇒ constructor 25 | 26 ⇒ constructor 26 | 27 ⇒ constructor 27
| 28 ⇒ constructor 28 | 29 ⇒ constructor 29 | 30 ⇒ constructor 30
end.
Ltac try_each_step prove_step_star Nconstrs max_steps constrID:= match constrID with
| S ?constrID' ⇒ solve
[ eapply @step_tcons; [cc constrID | prove_step_star Nconstrs max_steps ]
| eapply @step_lcons; [cc constrID | prove_step_star Nconstrs max_steps ]
| try_each_step prove_step_star Nconstrs max_steps constrID']
end.
Ltac prove_step_star Nconstrs max_steps := match max_steps with
| S ?max_steps' ⇒ match goal with
| |- @step_star _ ?S nil ?S ⇒ apply @step_nil
| |- @step_star _ ?S1 ?la ?S2 ⇒ first
[ eapply @single_tstep; constructor
| eapply @single_lstep; constructor
| try_each_step prove_step_star Nconstrs max_steps' Nconstrs ]
| _ ⇒ auto
end
end.
Ltac sstt Nconstrs max_steps RconstrID:= match RconstrID with
| S ?RconstrID' ⇒ solve
[ split; [| cc RconstrID]; prove_step_star Nconstrs max_steps
| split; [| cc RconstrID]; prove_step_star Nconstrs max_steps
| sstt Nconstrs max_steps RconstrID']
end.
Tactic Notation "tt" constr(Nconstrs) constr(max_steps) constr(m) := eexists; sstt Nconstrs max_steps m.
Ltac inv := match goal with
| [ H: @tstep _ _ _ |- _ ] ⇒ inverts H
| [ H: @lstep _ _ _ _ |- _ ] ⇒ inverts H
| [ H: @step_star _ _ _ _ |- _ ] ⇒ inverts H
end.
Ltac ssel Nsteps Nconstrs S:=
∃ S; split; [prove_step_star Nconstrs Nsteps | constructor].
Ltac sselL Nsteps Nconstrs a := left; ∃ a; split; auto; [prove_step_star Nconstrs Nsteps|constructor].
Ltac sselR Nsteps Nconstrs a := right; ∃ a; split; prove_step_star Nconstrs Nsteps.
End ExampleTactics.
Module SeqParBackwardSimulationFailsContrasimulationHolds.
Inductive state := p0 | p1 | p2 | p3 | p4 | p5 | p6
| q0 | q1 | q2 | q3 | q4 | q5 | q6 | q7.
Inductive tstep : state→state→Prop :=
| s_p01: tstep p0 p1
| s_p02: tstep p0 p2
| s_q01: tstep q0 q1
| s_q02: tstep q0 q2
| s_q73: tstep q7 q3
| s_q74: tstep q7 q4.
Inductive lstep : state→nat→state→Prop :=
| s_p13: lstep p1 0 p3
| s_p35: lstep p3 1 p5
| s_p24: lstep p2 0 p4
| s_p46: lstep p4 2 p6
| s_q13: lstep q1 0 q3
| s_q35: lstep q3 1 q5
| s_q07: lstep q0 0 q7
| s_q24: lstep q2 0 q4
| s_q46: lstep q4 2 q6.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state nat lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 9 S.
Tactic Notation "selL" constr(a) := sselL 3 9 a.
Tactic Notation "selR" constr(a) := sselR 3 9 a.
Tactic Notation "tt" constr(m) := tt 9 3 m.
Tactic Notation "ss" := prove_step_star 9 3.
Tactic Notation "ttt" constr(m) := do 2 eexists; split; [| sstt 9 3 m].
Tactic Notation "tttt" constr(m) := do 2 eexists; split; [apply step_nil | sstt 9 3 m].
Inductive RR : state→state→Prop :=
| RR_00: RR p0 q0
| RR_11: RR p1 q1
| RR_22: RR p2 q2
| RR_33: RR p3 q3
| RR_44: RR p4 q4
| RR_55: RR p5 q5
| RR_66: RR p6 q6.
Lemma wsim_forward_true:
∃ R, weak_simulation R ∧ R p0 q0.
Proof.
∃ RR; splits; try solve [apply RR_00]; intros p q; intros.
× split; intros.
+ inverts H; repeat inv; try solve [tt 3].
+ inverts H; repeat inv; try solve [tt 7].
Qed.
Lemma wsim_backward_false:
¬∃ R, weak_simulation R ∧ R q0 p0.
Proof.
intro.
destruct H as [R[??]].
edestruct weak_simulation_lstep with (p':=q7) as [p'[??]]; eauto.
constructor.
repeat inv.
edestruct weak_simulation_step_star with (p':=q6) as [p'[??]]; eauto.
ss.
repeat inv.
edestruct weak_simulation_step_star with (p':=q5) as [p'[??]]; eauto.
ss.
repeat inv.
Qed.
Lemma wbisim_false: ¬wbisimilar p0 q0.
Proof.
intro.
apply wsim_backward_false.
destruct H as [R[??]].
∃ (inv R); split; auto.
apply H.
Qed.
Lemma cssim_false: ¬coupled_similar p0 q0.
Proof.
intro.
apply wsim_backward_false.
destruct H as [R[?[?[?[??]]]]].
∃ R; split; auto.
Qed.
Lemma esim_true: eventually_similar p0 q0.
Proof.
∃ RR; splits; try solve [apply RR_00]; intros p q; intros.
× destruct H0.
× destruct H0.
× split; intros.
+ inverts H; repeat inv; try solve [tt 3].
+ inverts H; repeat inv; try solve [tt 7].
× inverts H; repeat inv; try solve [tttt 7; ss].
ttt 7; ss.
Qed.
Lemma csim_true: contrasimilar p0 q0.
Proof. apply ebisim_csim; apply esim_ebisim1; apply esim_true. Qed.
End Lemmas.
End SeqParBackwardSimulationFailsContrasimulationHolds.
Module ebisim_trans_false.
Inductive state : Set :=
| s1: nat→state
| s2: nat→nat→state
| s1': nat→state
| s0: state.
Inductive tstep : state→state→Prop :=
| s_t2: ∀ n m,
tstep (s2 n m) (s2 (2+n) (2+m))
| s_t1: ∀ n,
tstep (s1 n) (s1 (1+n))
| s_t1': ∀ n,
tstep (s1' n) (s2 (1+n) (2+n)).
Inductive lstep : state→nat→state→Prop :=
| s_sL: ∀ n m,
lstep (s2 n m) n s0
| s_sR: ∀ n m,
lstep (s2 n m) m s0
| s_s1: ∀ n,
lstep (s1 n) n s0
| s_s1': ∀ n,
lstep (s1' n) n s0.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state nat lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Import Stepping.
Existing Instance lts.
Lemma step_star_s0_inv: ∀ la p',
step_star s0 la p' → la=nil ∧ p'=s0.
Proof.
intros.
remember s0 as p.
revert Heqp.
induction H; intros; subst; auto; inverts H.
Qed.
Lemma step_star_s1_tau: ∀ k n,
step_star (s1 n) nil (s1 (k+n)).
Proof.
induction k; intros.
apply step_nil.
replace (S k + n) with (k + (S n)).
eapply step_tcons; eauto.
constructor.
omega.
Qed.
Lemma step_star_s1_inv: ∀ n la p',
step_star (s1 n) la p' →
∃ k,
(la=nil ∧ p'=s1 (k+n)) ∨ (la=[k+n] ∧ p'=s0).
Proof.
intros.
remember (s1 n) as p.
revert n Heqp.
induction H; intros; subst.
× ∃ 0; auto.
× inverts H.
edestruct step_star_s0_inv as [??]; eauto; subst la p''.
∃ 0; auto.
× inverts H.
edestruct IHstep_star as [k[ [??] | [??] ]]; clear IHstep_star; eauto; subst la p'';
∃ (1+k); [left|right]; split; auto; f_equal; omega.
Qed.
Lemma step_star_s2_tau: ∀ k n m,
step_star (s2 n m) nil (s2 (k+k+n) (k+k+m)).
Proof.
induction k; intros.
× apply step_nil.
× eapply step_tsnoc; eauto.
replace (S k + S k + n) with (2 + (k+k+n)).
replace (S k + S k + m) with (2 + (k+k+m)).
constructor.
omega. omega.
Qed.
Lemma step_star_s2_inv: ∀ n m la p',
step_star (s2 n m) la p' →
∃ k,
(la=nil ∧ p'=s2 (k+k+n) (k+k+m)) ∨ (la=[k+k+n] ∧ p'=s0) ∨ (la=[k+k+m]∧p'=s0).
Proof.
intros.
remember (s2 n m) as p.
revert n m Heqp.
induction H; intros; subst.
× ∃ 0; auto.
× inverts H;
edestruct step_star_s0_inv as [??]; eauto; subst la p''; ∃ 0; auto.
× inverts H.
edestruct IHstep_star as [k[ [??] | [ [??] | [??] ]]]; eauto; clear IHstep_star; subst la p''.
+ ∃ (1+k); left; split; auto; f_equal; omega.
+ ∃ (1+k); right; left; split; auto; f_equal; omega.
+ ∃ (1+k); right; right; split; auto; f_equal; omega.
Qed.
Lemma nat_div2: ∀ k, ∃ x, k=x+x ∨ k=1+x+x.
Proof.
intros.
∃ (Div2.div2 k).
destruct (Even.even_or_odd k).
left.
apply Div2.even_double; auto.
right.
apply Div2.odd_double; auto.
Qed.
Lemma esimPQ: ∀ n,
eventually_similar (s2 n (1+n)) (s1 n).
Proof.
intros.
∃ (fun p q ⇒ (∃ n, p=s2 n (1+n) ∧ q=s1 n) ∨ q=p).
splits; eauto; clear n; intros p q; unfold inv in *; intros.
× destruct H0.
× destruct H0.
× destruct H as [ [n[??]] | ?]; subst; split; intros.
+ inverts H.
∃ (s1 (2+n)); split; eauto.
eapply step_tcons. constructor. apply single_tstep; constructor.
+ inverts H; ∃ s0; split; auto.
apply single_lstep; constructor.
eapply step_tcons. constructor. apply single_lstep. constructor.
+ ∃ p'; split; auto. apply single_tstep; auto.
+ ∃ p'; split; auto. apply single_lstep; auto.
× destruct H as [ [n[??]] | ?]; subst; intros.
+ edestruct step_star_s1_inv as [k[ [??] | [??] ]]; eauto; subst la p'.
- destruct (nat_div2 k) as [x[?|?]]; subst.
∃ (s1 (x + x + n)) (s2 (x+x+n) (x+x+(1+n))); splits; eauto.
apply step_nil.
apply step_star_s2_tau.
do 2 eexists; splits.
apply single_tstep. constructor.
apply step_star_s2_tau with (k:=1+x).
left; ∃ (2+x+x+n); split; auto; f_equal; omega.
- ∃ s0 s0; splits; auto.
apply step_nil.
change [k+n] with ([]++[k+n]).
destruct (nat_div2 k) as [x[?|?]]; subst.
eapply step_lsnoc; [| apply s_sL].
apply step_star_s2_tau with (k:=x).
eapply step_lsnoc; [| apply s_sR].
replace (1+x+x+n) with (x+x+(1+n)).
apply step_star_s2_tau.
omega.
+ ∃ p' p'; split; auto. apply step_nil.
Qed.
Lemma esimRQ: ∀ n,
eventually_similar (s1' n) (s1 n).
Proof.
intros.
∃ (fun p q ⇒ (∃ n, p=s1' n∧q=s1 n) ∨ eventually_similar p q).
splits; eauto; clear n; intros p q; unfold inv in *; intros.
× destruct H0.
× destruct H0.
× destruct H as [ [n[??]] | ?]; subst; split; intros.
+ inverts H.
∃ (s1 (1+n)); split.
apply single_tstep; constructor.
right.
apply esimPQ.
+ inverts H.
∃ s0; split; auto.
apply single_lstep; constructor.
right; apply esim_refl.
+ edestruct tstep_esim1 as [q'[??]]; eauto.
+ edestruct lstep_esim1 as [q'[??]]; eauto.
× destruct H as [ [n[??]] | ?]; subst; intros.
+ edestruct step_star_s1_inv as [k[ [??] | [??] ]]; eauto; subst la p'.
- destruct (nat_div2 k) as [x[?|?]]; subst.
do 2 eexists; splits.
apply single_tstep. constructor.
eapply step_tcons. constructor.
apply step_star_s2_tau with (k:=x).
right.
replace (1+(x+x+n)) with (x+x+(1+n)).
replace (x + x + (2 + n)) with (1+(x+x+(1+n))).
apply esimPQ.
omega. omega.
do 2 eexists; splits.
apply step_nil.
eapply step_tcons. constructor.
apply step_star_s2_tau with (k:=x).
right.
replace (x+x+(2+n)) with (1+(x+x+(1+n))).
replace (1+x+x+n) with (x+x+(1+n)).
apply esimPQ.
omega. omega.
- ∃ s0 s0; splits; auto.
apply step_nil.
destruct k.
apply single_lstep; constructor.
eapply step_tcons. constructor.
change [S k+n] with ([]++[S k+n]).
destruct (nat_div2 k) as [x[?|?]]; subst.
eapply step_lsnoc; [| apply s_sL].
replace (S (x+x)+n) with (x+x+(1+n)).
apply step_star_s2_tau.
omega.
eapply step_lsnoc; [| apply s_sR].
replace (S (1+x+x)+n) with (x+x+(2+n)).
apply step_star_s2_tau.
omega.
right. apply esim_refl.
+ edestruct step_star_esim2 as [q''[p''[?[??]]]]; eauto.
∃ p'' q''; splits; eauto.
Qed.
Lemma step_star_s2_out: ∀ n m k p',
step_star (s2 n m) [k] p' → min n m ≤ k.
Proof.
intros.
remember (s2 n m) as p.
remember [k] as la.
revert n m k Heqp Heqla.
induction H; intros; subst.
× false.
× inverts Heqla.
inverts H.
+ apply Min.le_min_l.
+ apply Min.le_min_r.
× inverts H.
specialize (IHstep_star (2+n) (2+m) k).
lapply IHstep_star; intros; auto.
lapply H; intros; auto.
rewrite Min.plus_min_distr_l in H1.
omega.
Qed.
Lemma ebisimPR_false: ∀ n,
¬eventually_bisimilar (s2 n (1+n)) (s1' n).
Proof.
intros; intro.
edestruct tstep_ebisim2 as [p'[q'[?[??]]]]; eauto.
constructor.
edestruct step_star_s2_inv with (p':=p') as [k[ [??] | [ [??] | [??] ] ]]; eauto; try discriminate.
edestruct step_star_s2_inv with (p':=q') as [k'[ [??] | [ [??] | [??] ] ]]; eauto; try discriminate.
subst. clear H3 H5 H1 H0 H.
simpl in ×.
destruct (le_lt_dec k k') as [?|?].
+ edestruct lstep_ebisim1 as [p'[q'[?[??]]]]; eauto.
apply s_sL.
apply step_star_s2_out in H0.
clear -H0 l.
apply NPeano.Nat.min_le_iff in H0.
omega.
+ edestruct lstep_ebisim2 as [p'[q'[?[??]]]]; eauto.
apply s_sL.
apply step_star_s2_out in H.
clear -H l.
apply NPeano.Nat.min_le_iff in H.
omega.
Qed.
Lemma ebisim_trans_false: ∃ p q r,
eventually_bisimilar p q ∧ eventually_bisimilar q r ∧ ¬eventually_bisimilar p r.
Proof.
∃ (s2 0 1) (s1 0) (s1' 0); splits.
apply esim_ebisim1. apply esimPQ.
apply esim_ebisim2. apply esimRQ.
intro. apply ebisimPR_false in H. auto.
Qed.
End Lemmas.
End ebisim_trans_false.
Module ExampleA.
Inductive state : Set := Sa|Sb|Sc|Sd|Se|Sf|Sg|Sh|Si.
Definition label := nat.
Inductive lstep : state→label→state→Prop :=
| lstep_ab: lstep Sa 1 Sb
| lstep_bc: lstep Sb 2 Sc
| lstep_bd: lstep Sb 3 Sd
| lstep_ef: lstep Se 1 Sf
| lstep_eg: lstep Se 1 Sg
| lstep_fh: lstep Sf 2 Sh
| lstep_gi: lstep Sg 3 Si.
Inductive tstep : state→state→Prop := .
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Existing Instance lts.
Import ExampleTactics.
Lemma wbisim_false:
wbisimilar Sa Se → False.
Proof.
intros.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_ab.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_bd.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_bc.
repeat inv.
Qed.
Lemma csim_false:
contrasimilar Sa Se → False.
Proof.
intros.
apply csim_pcsim2 in H.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_ef. clear H.
repeat inv.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_bd. clear H1.
repeat inv.
Qed.
Lemma cssim_false:
coupled_similar Sa Se → False.
Proof.
intros.
apply cssim_pcssim2 in H.
edestruct lstep_pcssim as [p'[??]]; eauto.
apply lstep_ef.
repeat inv.
edestruct flip_pcssim as [p''[??]]; eauto.
repeat inv.
edestruct lstep_pcssim as [q'[??]]; eauto.
apply lstep_bd.
repeat inv.
Qed.
Lemma pbisim_false1:
par_bisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply pbisim_csim; auto.
Qed.
Lemma pbisim_false2:
par_bisimilar Se Sa → False.
Proof.
intros.
eapply csim_false.
apply csim_symm.
apply pbisim_csim; auto.
Qed.
End Lemmas.
End ExampleA.
Module ExampleB.
Inductive state:= Sa|Sb|Sc|Sd|Se|Sf|Sg|Sh|Si.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_ab: lstep Sa 1 Sb
| lstep_ce: lstep Sc 1 Se
| lstep_df: lstep Sd 1 Sf
| lstep_he: lstep Sh 1 Se
| lstep_if: lstep Si 1 Sf.
Inductive tstep : state→state→Prop :=
| tstep_ac: tstep Sa Sc
| tstep_ad: tstep Sa Sd
| tstep_be: tstep Sb Se
| tstep_bf: tstep Sb Sf
| tstep_gh: tstep Sg Sh
| tstep_gi: tstep Sg Si.
Definition is_halted p := p=Se∨p=Sf.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system _ _ lstep tstep is_halted _ _).
Next Obligation.
destruct H as [?|?]; subst p; inverts H0.
Qed.
Next Obligation.
destruct H as [?|?]; subst p; inverts H0.
Qed.
Section Lemmas.
Existing Instance lts.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 6 S.
Tactic Notation "selL" constr(a) := sselL 3 6 a.
Tactic Notation "selR" constr(a) := sselR 3 6 a.
Tactic Notation "tt" constr(m) := tt 6 3 m.
Tactic Notation "ss" := prove_step_star 6 3.
Lemma wbisim_false:
wbisimilar Sa Sg → False.
Proof.
intros.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_ab. clear H.
repeat inv.
edestruct tstep_wbisim1 as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_wbisim1 in H0.
repeat inv.
compute; auto.
edestruct tstep_wbisim1 as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_wbisim1 in H0.
repeat inv.
compute; auto.
Qed.
Lemma csim_false:
coupled_similar Sa Sg → False.
Proof.
intros.
edestruct lstep_pcssim as [q'[??]]; eauto.
apply lstep_ab.
apply cssim_pcssim1; eauto.
repeat inv.
edestruct tstep_pcssim as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_pcssim1 in H2; auto.
repeat inv.
compute; auto.
edestruct tstep_pcssim as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_pcssim1 in H2; auto.
repeat inv.
compute; auto.
Qed.
Import Stepping.
Inductive Rp : state→state→Prop :=
| Rp_ga: Rp Sg Sa
| Rp_ee: Rp Se Se | Rp_ff: Rp Sf Sf
| Rp_cc: Rp Sc Sc | Rp_dd: Rp Sd Sd
| Rp_hc: Rp Sh Sc | Rp_id: Rp Si Sd.
Lemma pbisim_true1:
par_bisimilar Sg Sa.
Proof.
∃ Rp.
split; [| constructor].
splits; auto; intros p q ?; intros.
× destruct H0; subst p; inverts H; ss.
× destruct H0; subst p; inverts H; ss.
× split; intros.
- intros; inverts H; repeat inv; tt 7.
- intros; inverts H; repeat inv; tt 7.
× unfold inv in *; inverts H; repeat inv; try solve [left; tt 7].
selR Se.
Qed.
Lemma pbisim_false2:
par_bisimilar Sa Sg → False.
Proof.
intros.
edestruct lstep_pbisim1 as [q'[??]]; eauto.
apply lstep_ab. clear H.
repeat inv.
edestruct tstep_pbisim1 as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_pbisim1 in H0.
repeat inv.
compute; auto.
edestruct tstep_pbisim1 as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_pbisim1 in H0.
repeat inv.
compute; auto.
Qed.
Lemma csim_true:
contrasimilar Sg Sa.
Proof.
apply pbisim_csim.
apply pbisim_true1.
Qed.
End Lemmas.
End ExampleB.
Module ExampleB_Full.
Inductive state:=
| Pa|Pb|Pc|Pd|Pe
| Qa|Qb|Qc|Qd|Qe|Qf|Qg|Qh|Qi|Qj|Qk|Ql|Qm|Qn|Qo|Qp|Qq
| Sw|Sx|Sy|Sz.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_Swy: lstep Sw 1 Sy
| lstep_Sxz: lstep Sx 1 Sz
| lstep_Qbe: lstep Qb 1 Qe
| lstep_Qfn: lstep Qf 1 Qn
| lstep_Qgo: lstep Qg 1 Qo
| lstep_Qhp: lstep Qh 1 Qp
| lstep_Qjq: lstep Qj 1 Qq.
Inductive tstep : state→state→Prop :=
| tstep_Pab: tstep Pa Pb
| tstep_Pac: tstep Pa Pc
| tstep_Pbd: tstep Pb Pd
| tstep_Pce: tstep Pc Pe
| tstep_Pdw: tstep Pd Sw
| tstep_Pex: tstep Pe Sx
| tstep_Qab: tstep Qa Qb
| tstep_Qac: tstep Qa Qc
| tstep_Qad: tstep Qa Qd
| tstep_Qbf: tstep Qb Qf
| tstep_Qbg: tstep Qb Qg
| tstep_Qch: tstep Qc Qh
| tstep_Qci: tstep Qc Qi
| tstep_Qdj: tstep Qd Qj
| tstep_Qdk: tstep Qd Qk
| tstep_Qel: tstep Qe Ql
| tstep_Qem: tstep Qe Qm
| tstep_Qfw: tstep Qf Sw
| tstep_Qgx: tstep Qg Sx
| tstep_Qhw: tstep Qh Sw
| tstep_Qiw: tstep Qi Sw
| tstep_Qjx: tstep Qj Sx
| tstep_Qkx: tstep Qk Sx
| tstep_Qly: tstep Ql Sy
| tstep_Qmz: tstep Qm Sz
| tstep_Qny: tstep Qn Sy
| tstep_Qoz: tstep Qo Sz
| tstep_Qpy: tstep Qp Sy
| tstep_Qqz: tstep Qq Sz.
Definition is_halted p := p=Sy∨p=Sz.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system _ _ lstep tstep is_halted _ _).
Next Obligation.
destruct H as [?|?]; subst p; inverts H0.
Qed.
Next Obligation.
destruct H as [?|?]; subst p; inverts H0.
Qed.
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 4 29 S.
Tactic Notation "selL" constr(a) := sselL 4 29 a.
Tactic Notation "selR" constr(a) := sselR 4 29 a.
Tactic Notation "tt" constr(m) := tt 29 4 m.
Tactic Notation "ss" := prove_step_star 29 4.
Ltac ss_split S :=
match goal with
| [ |- step_star ?p ?la ?p' ] ⇒ let la1:=fresh "la1" in let la2:= fresh "la2" in let H:=fresh "H" in
evar (la1: list lts_L); evar (la2: list lts_L);
cut (la = la1++la2); subst la1 la2; [intros H; rewrite H; eapply (@step_star_app _ _ _ S); ss | try reflexivity]
| [ |- step_star ?p _ ?p' ] ⇒ eapply (@step_star_app _ _ _ S); ss
end.
Lemma wbisim_false:
wbisimilar Pa Qa → False.
Proof.
intros.
edestruct step_star_wbisim2 with (q:=Qa) (q':=Qe) as [q'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_wbisim2 with (q:=Qe) (q':=Sz) as [q'[??]]; eauto.
ss.
repeat inv.
apply halted_wbisim1 in H2.
repeat inv.
compute; auto.
edestruct step_star_wbisim2 with (q:=Qe) (q':=Sy) as [q'[??]]; eauto.
ss.
repeat inv.
apply halted_wbisim1 in H2.
repeat inv.
compute; auto.
Qed.
Lemma cssim_false:
coupled_similar Pa Qa → False.
Proof.
intros.
apply cssim_pcssim2 in H.
edestruct step_star_pcssim with (p:=Qa) (p':=Qe) as [q'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_pcssim with (p:=Qe) (p':=Sz) as [q'[??]]; eauto.
ss.
repeat inv.
apply halted_pcssim1 in H2; auto.
repeat inv.
compute; auto.
edestruct step_star_pcssim with (p:=Qe) (p':=Sy) as [q'[??]]; eauto.
ss.
repeat inv.
apply halted_pcssim1 in H2; auto.
repeat inv.
compute; auto.
Qed.
Inductive Rp : state→state→Prop :=
| Rp_init: Rp Pa Qa
| Rp_ww: Rp Sw Sw | Rp_xx: Rp Sx Sx | Rp_yy: Rp Sy Sy | Rp_zz: Rp Sz Sz
| Rp_bw: Rp Pb Sw | Rp_cx: Rp Pc Sx
| Rp_dw: Rp Pd Sw | Rp_ex: Rp Pe Sx.
Lemma pbisim_true2:
par_bisimilar Pa Qa.
Proof.
∃ Rp.
split; [| constructor].
splits; intros p q ?; unfold inv in ×.
× intros [?|?]; subst; inverts H; ss.
× intros [?|?]; subst; inverts H; ss.
× split; intros.
- inverts H; repeat inv; try solve [tt 9].
- inverts H; repeat inv; tt 9.
× intros. inverts H; repeat inv; try solve [left; tt 9].
selR Sx.
selR Sy.
selR Sy.
selR Sz.
selR Sw.
selR Sy.
selR Sx.
selR Sz.
selR Sw.
selR Sw.
selR Sy.
selR Sw.
selR Sx.
selR Sx.
selR Sz.
selR Sx.
Qed.
Lemma pbisim_false1:
par_bisimilar Qa Pa → False.
Proof.
intros.
edestruct step_star_pbisim1 with (p:=Qa) (p':=Qe) as [p'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_pbisim1 with (p:=Qe) (p':=Sz) as [p'[??]]; eauto.
ss.
repeat inv.
apply halted_pbisim1 in H2.
repeat inv.
compute; auto.
edestruct step_star_pbisim1 with (p:=Qe) (p':=Sy) as [p'[??]]; eauto.
ss.
repeat inv.
apply halted_pbisim2 in H2.
repeat inv.
compute; auto.
Qed.
Lemma csim_true:
contrasimilar Qa Pa.
Proof.
apply csim_symm.
apply pbisim_csim.
apply pbisim_true2.
Qed.
End Lemmas.
End ExampleB_Full.
Module ExampleB'.
Inductive state:= Sa|Sb|Sc|Sd|Se|Sf|Sg|Sh|Si.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_ab: lstep Sa 1 Sb
| lstep_ce: lstep Sc 1 Se
| lstep_df: lstep Sd 1 Sf.
Inductive tstep : state→state→Prop :=
| tstep_ac: tstep Sa Sc
| tstep_ad: tstep Sa Sd
| tstep_be: tstep Sb Se
| tstep_bf: tstep Sb Sf
| tstep_cg: tstep Sc Sg
| tstep_dh: tstep Sd Sh
| tstep_ic: tstep Si Sc
| tstep_id: tstep Si Sd.
Definition is_halted p := p=Se∨p=Sf∨p=Sg∨p=Sh.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system _ _ lstep tstep is_halted _ _).
Next Obligation.
destruct H as [?|[?|[?|?]]]; subst p; inverts H0.
Qed.
Next Obligation.
destruct H as [?|[?|[?|?]]]; subst p; inverts H0.
Qed.
Section Lemmas.
Existing Instance lts.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 8 S.
Tactic Notation "selL" constr(a) := sselL 3 8 a.
Tactic Notation "selR" constr(a) := sselR 3 8 a.
Tactic Notation "tt" constr(m) := tt 8 3 m.
Tactic Notation "ss" := prove_step_star 8 3.
Lemma wbisim_false:
wbisimilar Sa Si → False.
Proof.
intros.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_ab. clear H.
repeat inv.
edestruct tstep_wbisim1 as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_wbisim1 in H0.
repeat inv.
compute; auto.
edestruct tstep_wbisim1 as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_wbisim1 in H0.
repeat inv.
compute; auto.
Qed.
Lemma cssim_false:
coupled_similar Sa Si → False.
Proof.
intros.
edestruct lstep_pcssim as [q'[??]]; eauto.
apply lstep_ab.
apply cssim_pcssim1; eauto.
repeat inv.
edestruct tstep_pcssim with (p:=Sb) as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_pcssim1 in H2.
repeat inv.
compute; auto.
edestruct tstep_pcssim with (p:=Sb) as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_pcssim1 in H2.
repeat inv.
compute; auto.
Qed.
Import Stepping.
Inductive Rp : state→state→Prop :=
| Rp_ia: Rp Si Sa
| Rp_ee: Rp Se Se | Rp_ff: Rp Sf Sf | Rp_gg: Rp Sg Sg | Rp_hh: Rp Sh Sh
| Rp_cc: Rp Sc Sc | Rp_dd: Rp Sd Sd.
Lemma pbisim_true1:
par_bisimilar Si Sa.
Proof.
∃ Rp.
split; [| constructor].
splits; intros p q ?.
× intros [?|[?|[?|?]]]; subst; inverts H; ss.
× intros [?|[?|[?|?]]]; subst; inverts H; ss.
× split; intros.
- inverts H; repeat inv; tt 7.
- inverts H; repeat inv; tt 7.
× intros.
inverts H; repeat inv; try solve [left; tt 7].
selR Se.
Qed.
Lemma pbisim_false2:
par_bisimilar Sa Si → False.
Proof.
intros.
edestruct lstep_pbisim1 as [q'[??]]; eauto.
apply lstep_ab. clear H.
repeat inv.
edestruct tstep_pbisim1 as [q'[??]]; eauto.
apply tstep_bf.
repeat inv.
apply halted_pbisim1 in H0.
repeat inv.
compute; auto.
edestruct tstep_pbisim1 as [q'[??]]; eauto.
apply tstep_be.
repeat inv.
apply halted_pbisim1 in H0.
repeat inv.
compute; auto.
Qed.
Lemma csim_true:
contrasimilar Sa Si.
Proof.
apply csim_symm.
apply pbisim_csim.
apply pbisim_true1.
Qed.
End Lemmas.
End ExampleB'.
Module ExampleC.
Inductive state : Set := Sa | Sb | Sc | Sd | Se | Sf | Sg | Sh.
Definition label := nat.
Inductive lstep : state→label→state→Prop :=
| lstep_ab: lstep Sa 1 Sb
| lstep_bc: lstep Sb 2 Sc
| lstep_ef: lstep Se 1 Sf
| lstep_eg: lstep Se 1 Sg
| lstep_fh: lstep Sf 2 Sh.
Inductive tstep : state→state→Prop := .
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Existing Instance lts.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 2 5 S.
Tactic Notation "selL" constr(a) := sselL 2 5 a.
Tactic Notation "selR" constr(a) := sselR 2 5 a.
Tactic Notation "tt" constr(m) := tt 5 2 m.
Tactic Notation "ss" := prove_step_star 5 2.
Lemma wbisim_false:
wbisimilar Sa Se → False.
Proof.
intros.
edestruct lstep_wbisim2 as [q'[??]]; eauto.
apply lstep_eg. clear H.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_bc.
repeat inv.
Qed.
Lemma cssim_false:
coupled_similar Sa Se → False.
Proof.
intros.
edestruct lstep_pcssim as [p'[??]].
apply lstep_eg.
apply cssim_pcssim2; eauto.
repeat inv.
edestruct flip_pcssim as [p'[??]]; eauto.
repeat inv.
edestruct lstep_pcssim with (p:=Sb) as [q'[??]]; eauto.
apply lstep_bc.
repeat inv.
Qed.
Lemma csim_false:
contrasimilar Sa Se → False.
Proof.
intros.
apply csim_pcsim2 in H.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_eg. clear H.
repeat inv.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_bc. clear H1.
repeat inv.
Qed.
Lemma pbisim_false1:
par_bisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply pbisim_csim; auto.
Qed.
Lemma wbisim_false2:
wbisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply wbisim_csim; auto.
Qed.
End Lemmas.
End ExampleC.
Module ExampleD. Inductive state : Set := Sa | Sb | Sc | Sd | Se | Sf | Sg | Sh | Si.
Inductive label : Set := pay_cent | pick_tea | pick_coffee | tea | coffee.
Inductive lstep : state→label→state→Prop :=
| lstep_ab: lstep Sa pay_cent Sb
| lstep_bc: lstep Sb pick_tea Sc
| lstep_bd: lstep Sb pick_coffee Sd
| lstep_ca: lstep Sc tea Sa
| lstep_da: lstep Sd coffee Sa
| lstep_ef: lstep Se pay_cent Sf
| lstep_eg: lstep Se pay_cent Sg
| lstep_fh: lstep Sh pick_tea Sh
| lstep_gi: lstep Sg pick_coffee Si
| lstep_he: lstep Sh tea Se
| lstep_ie: lstep Si coffee Se.
Inductive tstep : state→state→Prop := .
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 11 S.
Tactic Notation "selL" constr(a) := sselL 3 11 a.
Tactic Notation "selR" constr(a) := sselR 3 11 a.
Tactic Notation "tt" constr(m) := tt 11 3 m.
Tactic Notation "ss" := prove_step_star 11 3.
Lemma wbisim_false:
wbisimilar Sa Se → False.
Proof.
intros.
edestruct lstep_wbisim2 as [q'[??]]; eauto.
apply lstep_ef. clear H.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_bc.
repeat inv.
Qed.
Lemma cssim_false:
coupled_similar Sa Se → False.
Proof.
intros.
edestruct lstep_pcssim as [p'[??]].
apply lstep_eg.
apply cssim_pcssim2; eauto.
repeat inv.
edestruct flip_pcssim as [p'[??]]; eauto.
repeat inv.
edestruct lstep_pcssim as [p'[??]]; eauto.
apply lstep_bc.
repeat inv.
Qed.
Lemma csim_false:
contrasimilar Sa Se → False.
Proof.
intros.
apply csim_pcsim2 in H.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_eg. clear H.
repeat inv.
edestruct lstep_pcsim as [q'[??]]; eauto.
apply lstep_bc. clear H1.
repeat inv.
Qed.
Lemma pbisim_false1:
par_bisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply pbisim_csim; auto.
Qed.
Lemma par_bisim_false2:
par_bisimilar Se Sa → False.
Proof.
intros.
eapply csim_false.
apply csim_symm.
apply pbisim_csim; auto.
Qed.
End Lemmas.
End ExampleD.
Module ExampleE.
Inductive state : Set := Sa | Sb | Sc | Sd | Se.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_ac: lstep Sa 2 Sc
| lstep_bd: lstep Sb 1 Sd
| lstep_ed: lstep Se 1 Sd
| lstep_ec: lstep Se 2 Sc.
Inductive tstep : state→state→Prop :=
| tstep_ab: tstep Sa Sb.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep (fun _⇒False) _ _).
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 2 4 S.
Tactic Notation "selL" constr(a) := sselL 2 4 a.
Tactic Notation "selR" constr(a) := sselR 2 4 a.
Tactic Notation "tt" constr(m) := tt 4 2 m.
Tactic Notation "ss" := prove_step_star 4 2.
Lemma csim_false:
contrasimilar Sa Se → False.
Proof.
intros.
apply csim_pcsim1 in H.
edestruct tstep_pcsim as [q'[??]]; eauto.
apply tstep_ab.
repeat inv.
edestruct lstep_pcsim as [p'[??]]; eauto.
apply lstep_ec.
repeat inv.
Qed.
Lemma wbisim_false:
wbisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply wbisim_csim; auto.
Qed.
Lemma pbisim_false1:
par_bisimilar Sa Se → False.
Proof.
intros.
eapply csim_false.
apply pbisim_csim; auto.
Qed.
Lemma pbisim_false2:
par_bisimilar Se Sa → False.
Proof.
intros.
eapply csim_false.
apply csim_symm.
apply pbisim_csim; auto.
Qed.
Lemma cssim_false:
coupled_similar Sa Se → False.
Proof.
intros.
edestruct tstep_pcssim as [q'[??]].
apply tstep_ab.
apply cssim_pcssim1; eauto.
repeat inv.
edestruct flip_pcssim as [q'[??]]; eauto.
repeat inv.
edestruct lstep_pcssim with (p:=Se) as [p'[??]]; eauto.
apply lstep_ec.
repeat inv.
Qed.
End Lemmas.
End ExampleE.
Module ExampleF.
Inductive state : Set := Sa | Sb | Sc | Sd | Se | Sf | Sg | Sh | Si | Sj | Sk | Sl.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_be: lstep Sb 1 Se
| lstep_cf: lstep Sc 2 Sf
| lstep_dg: lstep Sd 3 Sg
| lstep_ie: lstep Si 1 Se
| lstep_kf: lstep Sk 2 Sf
| lstep_lg: lstep Sl 3 Sg.
Inductive tstep : state→state→Prop :=
| tstep_ab: tstep Sa Sb
| tstep_ac: tstep Sa Sc
| tstep_ad: tstep Sa Sd
| tstep_hi: tstep Sh Si
| tstep_hj: tstep Sh Sj
| tstep_jk: tstep Sj Sk
| tstep_jl: tstep Sj Sl.
Definition is_halted (p:state) := False.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep is_halted _ _).
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 7 S.
Tactic Notation "selL" constr(a) := sselL 3 7 a.
Tactic Notation "selR" constr(a) := sselR 3 7 a.
Tactic Notation "tt" constr(m) := tt 7 3 m.
Tactic Notation "ss" := prove_step_star 7 3.
Lemma wbisim_false:
wbisimilar Sa Sh → False.
Proof.
intros.
edestruct tstep_wbisim2 as [p'[??]]; eauto.
apply tstep_hj.
clear H.
inverts H0.
edestruct step_star_wbisim1 with (p':=Se) as [q'[??]]; eauto.
ss.
repeat inv.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_be.
repeat inv.
edestruct step_star_wbisim2 with (q':=Sg) as [p'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_wbisim2 with (q':=Sf) as [p'[??]]; eauto.
ss.
repeat inv.
Qed.
Inductive Rc1 : state→state→Prop :=
| Rc1_ah: Rc1 Sa Sh | Rc1_bi: Rc1 Sb Si | Rc1_ck: Rc1 Sc Sk | Rc1_dl: Rc1 Sd Sl
| Rc1_ee: Rc1 Se Se | Rc1_ff: Rc1 Sf Sf | Rc1_gg: Rc1 Sg Sg
| Rc1_cj: Rc1 Sc Sj.
Inductive Rc2 : state→state→Prop :=
| Rc2_ah: Rc2 Sa Sh | Rc2_bi: Rc2 Sb Si | Rc2_ck: Rc2 Sc Sk | Rc2_dl: Rc2 Sd Sl
| Rc2_ee: Rc2 Se Se | Rc2_ff: Rc2 Sf Sf | Rc2_gg: Rc2 Sg Sg
| Rc2_aj: Rc2 Sa Sj.
Lemma cssim_true:
coupled_similar Sa Sh.
Proof.
apply coupled_similar_equiv.
∃ Rc1 Rc2.
splits; try solve [constructor]; intros p q; intros.
× inverts H; tt 8.
× inverts H; tt 8.
× destruct H0.
× destruct H0.
× split; intros.
- inverts H; inverts H0; tt 8.
- inverts H; inverts H0; tt 8.
× split; intros.
- inverts H; inverts H0; tt 8.
- inverts H; inverts H0; tt 8.
Qed.
Lemma pbisim_false1:
par_bisimilar Sh Sa → False.
Proof.
intros.
edestruct tstep_pbisim1 as [p'[??]]; eauto.
apply tstep_hj.
clear H.
repeat inv.
edestruct step_star_pbisim2 with (q':=Se)
as [ [q'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
edestruct step_star_pbisim2 with (q':=Se)
as [ [q'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
edestruct step_star_pbisim1 with (p':=Sg)
as [p'[??]]; eauto; [ss | ]; repeat inv.
edestruct step_star_pbisim1 with (p':=Sf)
as [p'[??]]; eauto; [ss | ]; repeat inv.
Qed.
Lemma pbisim_false2:
par_bisimilar Sa Sh → False.
Proof.
intros.
edestruct tstep_pbisim2 as [ [p'[??]] | [pq'[??]] ]; eauto.
apply tstep_hj.
repeat inv.
edestruct step_star_pbisim1 with (p':=Se) as [q'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_pbisim1 with (p':=Se) as [q'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_pbisim2 with (q':=Sg)
as [ [p'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
edestruct step_star_pbisim2 with (q':=Sf)
as [ [p'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
repeat inv.
Qed.
Inductive Rd : state→state→Prop :=
| Rd_ha: Rd Sh Sa | Rd_ah: Rd Sa Sh
| Rd_bi: Rd Sb Si | Rd_cj: Rd Sc Sj | Rd_ck: Rd Sc Sk
| Rd_dl: Rd Sd Sl | Rd_ib: Rd Si Sb | Rd_kc: Rd Sk Sc
| Rd_ld: Rd Sl Sd
| Rd_ee: Rd Se Se | Rd_ff: Rd Sf Sf | Rd_gg: Rd Sg Sg.
Lemma csim_true:
contrasimilar Sa Sh.
Proof.
∃ Rd.
splits; try solve [constructor]; intros p q ?; intros.
- destruct H0.
- inverts H; inverts H0; repeat inv; tt 12.
Qed.
End Lemmas.
End ExampleF.
Module ExampleG.
Inductive state : Set := Sa | Sb | Sc | Sd | Se | Sf | Sg | Sh | Sj.
Definition label:= nat.
Inductive lstep : state→label→state→Prop :=
| lstep_be: lstep Sb 1 Se
| lstep_cf: lstep Sc 2 Sf
| lstep_dg: lstep Sd 3 Sg.
Inductive tstep : state→state→Prop :=
| tstep_ab: tstep Sa Sb
| tstep_ac: tstep Sa Sc
| tstep_ad: tstep Sa Sd
| tstep_hb: tstep Sh Sb
| tstep_hj: tstep Sh Sj
| tstep_jc: tstep Sj Sc
| tstep_jd: tstep Sj Sd.
Definition is_halted (p:state) := False.
Program Definition lts : labeled_transition_system :=
(Build_labeled_transition_system state label lstep tstep is_halted _ _).
Section Lemmas.
Existing Instance lts.
Import Stepping.
Import ExampleTactics.
Tactic Notation "sel" constr(S) := ssel 3 7 S.
Tactic Notation "selL" constr(a) := sselL 3 7 a.
Tactic Notation "selR" constr(a) := sselR 3 7 a.
Tactic Notation "tt" constr(m) := tt 7 3 m.
Tactic Notation "ss" := prove_step_star 7 3.
Lemma wbisim_false:
wbisimilar Sa Sh → False.
Proof.
intros.
edestruct tstep_wbisim2 as [p'[??]]; eauto.
apply tstep_hj.
clear H.
inverts H0.
edestruct step_star_wbisim1 with (p':=Se) as [q'[??]]; eauto.
ss.
repeat inv.
repeat inv.
edestruct lstep_wbisim1 as [q'[??]]; eauto.
apply lstep_be.
repeat inv.
edestruct step_star_wbisim2 with (q':=Sg) as [p'[??]]; eauto.
ss.
repeat inv.
edestruct step_star_wbisim2 with (q':=Sf) as [p'[??]]; eauto.
ss.
repeat inv.
Qed.
Inductive Rc1 : state→state→Prop :=
| Rc1_ah: Rc1 Sa Sh | Rc1_bb: Rc1 Sb Sb | Rc1_cc: Rc1 Sc Sc | Rc1_dd: Rc1 Sd Sd
| Rc1_ee: Rc1 Se Se | Rc1_ff: Rc1 Sf Sf | Rc1_gg: Rc1 Sg Sg
| Rc1_cj: Rc1 Sc Sj.
Inductive Rc2 : state→state→Prop :=
| Rc2_ah: Rc2 Sa Sh | Rc2_bb: Rc2 Sb Sb | Rc2_cc: Rc2 Sc Sc | Rc2_dd: Rc2 Sd Sd
| Rc2_ee: Rc2 Se Se | Rc2_ff: Rc2 Sf Sf | Rc2_gg: Rc2 Sg Sg
| Rc2_aj: Rc2 Sa Sj.
Lemma cssim_true:
coupled_similar Sa Sh.
Proof.
apply coupled_similar_equiv.
∃ Rc1 Rc2.
splits; try solve [constructor]; intros p q; intros.
× inverts H; tt 8.
× inverts H; tt 8.
× destruct H0.
× destruct H0.
× split; intros.
+ inverts H; inverts H0; tt 8.
+ inverts H; inverts H0; tt 8.
× split; intros.
+ inverts H; inverts H0; tt 8.
+ inverts H; inverts H0; tt 8.
Qed.
Lemma pbisim_false1:
par_bisimilar Sh Sa → False.
Proof.
intros.
edestruct tstep_pbisim1 as [q'[??]]; eauto.
apply tstep_hj.
clear H.
repeat inv.
edestruct step_star_pbisim2 with (q':=Se)
as [ [q'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
edestruct step_star_pbisim2 with (q':=Se)
as [ [q'[??]] | [pq'[??]] ]; eauto; [ss | | ]; repeat inv.
edestruct step_star_pbisim1 with (p':=Sg)
as [p'[??]]; eauto; [ss | ]; repeat inv.
edestruct step_star_pbisim1 with (p':=Sf)
as [p'[??]]; eauto; [ss | ]; repeat inv.
Qed.
Inductive Rp : state→state→Prop :=
| Rp_ah: Rp Sa Sh | Rp_bb: Rp Sb Sb | Rp_cc: Rp Sc Sc | Rp_dd: Rp Sd Sd
| Rp_ee: Rp Se Se | Rp_ff: Rp Sf Sf | Rp_gg: Rp Sg Sg.
Lemma pbisim_true2:
par_bisimilar Sa Sh.
Proof.
∃ Rp.
split; [|constructor].
splits; intros p q; intros.
× destruct H0.
× destruct H0.
× split; intros.
- inverts H; repeat inv; tt 8.
- inverts H; repeat inv; tt 8.
× inverts H; repeat inv; try solve [left; tt 8].
right; ∃ Sc; split; ss.
Qed.
Lemma csim_true:
contrasimilar Sa Sh.
Proof.
intros.
apply pbisim_csim.
apply pbisim_true2.
Qed.
End Lemmas.
End ExampleG.