Library ProcEquiv
This file was written by Colm Bhandal, PhD student, Foundations and Methods group,
School of Computer Science and Statistics, Trinity College, Dublin, Ireland.
*************************** Standard Imports
*************************** Specialised Imports
Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.GenTacs.
Single step equivlance on process terms is defined as a bisimulation.
CoInductive bisimulation p q : Prop :=
bisimWitness :
(forall a p', p -P- a -P> p' ->
exists q', q -P- a -P> q' /\ bisimulation p' q') ->
(forall a q', q -P- a -P> q' ->
exists p', p -P- a -P> p' /\ bisimulation p' q') ->
bisimulation p q.
Notation "p ~p~ q" := (bisimulation p q) (at level 70).
bisimWitness :
(forall a p', p -P- a -P> p' ->
exists q', q -P- a -P> q' /\ bisimulation p' q') ->
(forall a q', q -P- a -P> q' ->
exists p', p -P- a -P> p' /\ bisimulation p' q') ->
bisimulation p q.
Notation "p ~p~ q" := (bisimulation p q) (at level 70).
The siumlation relation is reflexive.
CoFixpoint bisim_refl p : p ~p~ p.
The siumlation relation is transitive.
CoFixpoint bisim_trans p1 p2 p3 : p1 ~p~ p2 -> p2 ~p~ p3 ->
p1 ~p~ p3.
CoFixpoint bisim_symm p q : p ~p~ q -> q ~p~ p.
Qed.
Ltac plus_le_left_red := match goal with [Q : ?a + ?b = ?a + ?c |-
?b = ?c] => replace b with (a + b - a);[ | ring];
rewrite Q; ring end.
Require Import ComhCoq.Extras.LibTactics.
Open Scope R_scope.
p1 ~p~ p3.
CoFixpoint bisim_symm p q : p ~p~ q -> q ~p~ p.
Qed.
Ltac plus_le_left_red := match goal with [Q : ?a + ?b = ?a + ?c |-
?b = ?c] => replace b with (a + b - a);[ | ring];
rewrite Q; ring end.
Require Import ComhCoq.Extras.LibTactics.
Open Scope R_scope.
If a is in the sort relation for d, p, and p is capable of doing a delay
of d, then there is some d' < d and p' such that p can delay to this p' by
d' and the resulting p' is capable of doing the action a.
Lemma sort_del a d p : sort a d p -> timedActEnabled p d ->
(exists p' d', p -PD- d' -PD> p' /\ d' < d /\ discActEnabled p' a)
\/ discActEnabled p a.
Lemma bisim_dae p q a : p ~p~ q -> discActEnabled p a ->
discActEnabled q a.
Lemma bisim_del_sort p q a d : p ~p~ q -> timedActEnabled p d ->
sort a d p -> sort a d q.
CoFixpoint choice_bisim_symm p1 p2 : p1 $+$ p2 ~p~ p2 $+$ p1.
CoFixpoint par_bisim_symm p1 p2 : p1 $||$ p2 ~p~ p2 $||$ p1.
CoFixpoint choice_bism_unit_r p : p $+$ nilProc ~p~ p.
CoFixpoint choice_bism_unit_l p : nilProc $+$ p ~p~ p.
CoFixpoint choice_bisim_context p1 p2 p1' p2' :
p1 ~p~ p1' -> p2 ~p~ p2' ->
p1 $+$ p2 ~p~ p1' $+$ p2'. Qed.
Ltac bisim_disc_tac_parm U V :=
apply stepPDisc in V; apply U in V; ex_flat; and_flat;
match goal with [U1 : _ -P- _ -P> _ |- _] => inversion U1; subst end.
Ltac bisim_disc_tac :=
match goal with
| [U : ?p ~p~ ?q, V : ?p -PA- _ -PA> _ |- _] =>
bisim_disc_tac_parm U V
| [U : ?p ~p~ ?q, V : ?q -PA- _ -PA> _ |- _] =>
bisim_disc_tac_parm U V
end.
Ltac bisim_timed_tac_parm U V :=
apply stepPTimed in V; apply U in V; ex_flat; and_flat;
match goal with [U1 : _ -P- _ -P> _ |- _] => inversion U1; subst end.
Ltac bisim_timed_tac :=
match goal with
| [U : ?p ~p~ ?q, V : ?p -PD- _ -PD> _ |- _] =>
bisim_timed_tac_parm U V
| [U : ?p ~p~ ?q, V : ?q -PD- _ -PD> _ |- _] =>
bisim_timed_tac_parm U V
end.
Lemma cond_bisim_lift_true p q b : p ~p~ q -> evalBoolExp b true ->
b $> p ~p~ b $> q.
CoFixpoint par_bisim_context p p' q :
p ~p~ p' -> p $||$ q ~p~ p' $||$ q.
Qed.
Corollary par_bisim_context2 p q q' :
q ~p~ q' -> p $||$ q ~p~ p $||$ q'.
Corollary par_bisim_context_strong p p' q q' :
p ~p~ p' -> q ~p~ q' -> p $||$ q ~p~ p' $||$ q'.
Corollary par_bisim_triple p1 p1' p2 p2' p3 p3' :
p1 ~p~ p1' -> p2 ~p~ p2' -> p3 ~p~ p3' ->
p1 $||$ p2 $||$ p3 ~p~ p1' $||$ p2' $||$ p3'.
Lemma cond_bisim_true p b : evalBoolExp b true ->
b $> p ~p~ p.
Theorem evalBoolExpFalseTot : forall (e : BoolExp),
evalBoolExp e false <-> evalBoolExpFunTot e = false.
CoFixpoint cond_bisim_false p b : evalBoolExpFunTot b = false ->
b $> p ~p~ nilProc.
Lemma if_then_bisim_true b p q :
evalBoolExp b true -> b $> p $+$ !~b $> q ~p~ p.
Lemma if_then_bisim_false b p q :
evalBoolExp b false -> b $> p $+$ !~b $> q ~p~ q.
(exists p' d', p -PD- d' -PD> p' /\ d' < d /\ discActEnabled p' a)
\/ discActEnabled p a.
Lemma bisim_dae p q a : p ~p~ q -> discActEnabled p a ->
discActEnabled q a.
Lemma bisim_del_sort p q a d : p ~p~ q -> timedActEnabled p d ->
sort a d p -> sort a d q.
CoFixpoint choice_bisim_symm p1 p2 : p1 $+$ p2 ~p~ p2 $+$ p1.
CoFixpoint par_bisim_symm p1 p2 : p1 $||$ p2 ~p~ p2 $||$ p1.
CoFixpoint choice_bism_unit_r p : p $+$ nilProc ~p~ p.
CoFixpoint choice_bism_unit_l p : nilProc $+$ p ~p~ p.
CoFixpoint choice_bisim_context p1 p2 p1' p2' :
p1 ~p~ p1' -> p2 ~p~ p2' ->
p1 $+$ p2 ~p~ p1' $+$ p2'. Qed.
Ltac bisim_disc_tac_parm U V :=
apply stepPDisc in V; apply U in V; ex_flat; and_flat;
match goal with [U1 : _ -P- _ -P> _ |- _] => inversion U1; subst end.
Ltac bisim_disc_tac :=
match goal with
| [U : ?p ~p~ ?q, V : ?p -PA- _ -PA> _ |- _] =>
bisim_disc_tac_parm U V
| [U : ?p ~p~ ?q, V : ?q -PA- _ -PA> _ |- _] =>
bisim_disc_tac_parm U V
end.
Ltac bisim_timed_tac_parm U V :=
apply stepPTimed in V; apply U in V; ex_flat; and_flat;
match goal with [U1 : _ -P- _ -P> _ |- _] => inversion U1; subst end.
Ltac bisim_timed_tac :=
match goal with
| [U : ?p ~p~ ?q, V : ?p -PD- _ -PD> _ |- _] =>
bisim_timed_tac_parm U V
| [U : ?p ~p~ ?q, V : ?q -PD- _ -PD> _ |- _] =>
bisim_timed_tac_parm U V
end.
Lemma cond_bisim_lift_true p q b : p ~p~ q -> evalBoolExp b true ->
b $> p ~p~ b $> q.
CoFixpoint par_bisim_context p p' q :
p ~p~ p' -> p $||$ q ~p~ p' $||$ q.
Qed.
Corollary par_bisim_context2 p q q' :
q ~p~ q' -> p $||$ q ~p~ p $||$ q'.
Corollary par_bisim_context_strong p p' q q' :
p ~p~ p' -> q ~p~ q' -> p $||$ q ~p~ p' $||$ q'.
Corollary par_bisim_triple p1 p1' p2 p2' p3 p3' :
p1 ~p~ p1' -> p2 ~p~ p2' -> p3 ~p~ p3' ->
p1 $||$ p2 $||$ p3 ~p~ p1' $||$ p2' $||$ p3'.
Lemma cond_bisim_true p b : evalBoolExp b true ->
b $> p ~p~ p.
Theorem evalBoolExpFalseTot : forall (e : BoolExp),
evalBoolExp e false <-> evalBoolExpFunTot e = false.
CoFixpoint cond_bisim_false p b : evalBoolExpFunTot b = false ->
b $> p ~p~ nilProc.
Lemma if_then_bisim_true b p q :
evalBoolExp b true -> b $> p $+$ !~b $> q ~p~ p.
Lemma if_then_bisim_false b p q :
evalBoolExp b false -> b $> p $+$ !~b $> q ~p~ q.
This page has been generated by coqdoc