Library ProtAuxResults
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
Require Import ComhCoq.Extras.LibTactics.
Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.ProtAuxDefs.
Require Import Bool.
Require Import ComhCoq.EntityLanguage.
Require Import ComhCoq.ProcEquiv.
Ltac invert_def := match goal with [ U : def _ = (_, _) |- _] =>
invertClear U; subst end.
Ltac invert_trans := match goal with [P : _ -PA- _ -PA> _ |- _]
=> invertClear P; subst end.
Lemma subProc_id_eq p : subProcTerm idSubst p = p.
Ltac clean_proc_trans := match goal with [U : _ -PA- _ -PA> _ |- _] =>
clean_proc_hyp U end.
Given some application process in the context, this tactic performs inversion and
some cleanup on this until it is in the form of a process body as the source.
Ltac invert_app_trans := match goal with
| [U : _ $( _ )$ -PA- _ -PA> _ |- _] => invertClear U; invert_def; clean_proc_trans
| [U : liftNameProc _ -PA- _ -PA> _ |- _] => invertClear U; invert_def; clean_proc_trans
end.
Lemma dae_outPfx c l v p :
evalExpLists l v -> discActEnabled (c $<l>$! p) (c;! v).
Lemma dae_inPfx c l v p :
length l = length v -> discActEnabled (c $<l>$? p) (c;? v).
Ltac update_eval := match goal with [H : ?e |_| ?m |- update _ ?x ?e ?x |_| ?m]
=> rewrite updateAppEq; apply H end.
Ltac lift_act_sum p1 p2 :=
match goal with
| [V : p1 -PA- ?a -PA> ?p' |- _] => apply (stepDpChoiceL p1 p2) in V
| [V : p2 -PA- ?a -PA> ?p' |- _] => apply (stepDpChoiceR p1 p2) in V
end.
Fixpoint genBaseList (n : nat) : list BaseType :=
match n with
| 0 => []
| S n' => (baseTime zeroTime) :: (genBaseList n')
end.
Ltac lift_act_then b p := match goal with
[V1 : p -PA- ?a -PA> ?p', V2 : evalBoolExpFunTot b = true |- _] =>
let V := fresh in rename V1 into V;
lets V1 : stepDpThen V V2; clear V end.
Lemma stepDpApp_alt : forall (n : Name) (l2 : list Exp) (p' : ProcTerm) (a : DiscAct),
stepDiscProc (subProcTerm (listsToSub (fst (def n)) l2) (snd (def n))) a p' ->
stepDiscProc (app n l2) a p'.
Ltac lift_act_app h l2 :=
match goal with
| [V : (subProcTerm (listsToSub (fst (def h)) l2) (snd (def h))) -PA- _ -PA> _ |- _] =>
apply stepDpApp_alt in V
end.
Lemma genBaseList_length A (l : list A) :
length (genBaseList (length l)) = length l.
Ltac gen_disc_acts p :=
match p with
| ?c $< ?l >$? ?p' => let V := fresh in
assert (p -PA- c ;? genBaseList (length l) -PA>
subProcTerm (listsToSub l (listBaselistExp (genBaseList (length l)))) p');
[constructor; reflexivity | ]; remove_resets_hyp V; remove_updates_hyp V
| ?c $< ?l >$! ?p' =>
let EEL := fresh in let EELEQ := fresh in
remember (evalExpListsFun l) as EEL eqn:EELEQ;
destruct EEL; try solve [inversion EELEQ];
match type of EELEQ with
| Some ?l' = _ =>
symmetry in EELEQ; assert (p -PA- c ;! l' -PA> p');
[apply evalExpListsFunRel in EELEQ; econstructor;
eassumption | ]; inversion EELEQ; subst
| _ => idtac
end; clear EELEQ
| ?b $> ?p' =>
let EEL := fresh in let EELEQ := fresh in
remember (evalBoolExpFunTot b) as EEL eqn:EELEQ;
destruct EEL; try solve [inversion EELEQ];
match type of EELEQ with
| true = _ =>
symmetry in EELEQ; gen_disc_acts p'; lift_act_then b p'; clear EELEQ
| _ => false
end
| ?p1 $+$ ?p2 => gen_disc_acts p1; gen_disc_acts p2; repeat lift_act_sum p1 p2
| ?h $( ?l2 )$ => gen_disc_acts (subProcTerm (listsToSub (fst (def h)) l2) (snd (def h)));
repeat lift_act_app h l2
| subProcTerm ?s ?p' =>
let p'' := fresh "p" in let Hp1 := fresh "Hp1" in
let Hp2 := fresh "Hp2" in
remember p as p'' eqn:Hp1; lets Hp2 : Hp1; simpl in Hp2;
remove_resets_hyp Hp2; remove_updates_hyp Hp2;
match type of Hp2 with _ = ?q => gen_disc_acts q end;
symmetry in Hp2; subst_all Hp2; subst_all Hp1
| $< ?e >$ ?p' => idtac
end.
Lemma bisim_disc_match p p' q a : p ~p~ q -> p -PA- a -PA> p' ->
exists q', q -PA- a -PA> q'.
Ltac invert_trans_rich := invert_trans; try invert_def; clean_proc_trans.
Ltac bisim_contra_rec V1 :=
match type of V1 with ?p ~p~ ?q =>
match goal with [V2 : p -PA- _ -PA> _ |- _] =>
eapply bisim_disc_match in V2; [ | apply V1];
let q' := fresh "q'" in let TR := fresh in
invertClearAs2 V2 q' TR; first [
solve [clear - TR; repeat invert_trans_rich]
| bisim_contra_rec V1]
end
end.
Ltac bisim_contra V1 :=
match type of V1 with ?p ~p~ ?q =>
gen_disc_acts p; bisim_contra_rec V1
end.
Ltac bisim_trans_tac BT :=
match goal with
| [V : ?p ~p~ ?x, V1 : ?p ~p~ ?y |- _] =>
assert (x ~p~ y) as BT; [eapply bisim_trans; [apply bisim_symm | ];
eassumption | ]
| [V : ?x ~p~ ?p, V1 : ?p ~p~ ?y |- _] =>
assert (x ~p~ y) as BT; [eapply bisim_trans; eassumption | ]
end.
Ltac invert_steps := repeat
(match goal with [V : _ -P- _ -P> _ |- _] =>
invertClear V end; subst).
Lemma bisim_dae p q a : p ~p~ q -> discActEnabled p a ->
discActEnabled q a.
Ltac activation_pre_tac :=
let U := fresh in
intro U; eapply bisim_dae; [apply bisim_symm; apply U | ];
match goal with [ |- discActEnabled ?p ?a] =>
match p with
| ?p' => unfold p'
| ?p' ?x1 => unfold p'
| ?p' ?x1 ?x2 => unfold p'
| ?p' ?x1 ?x2 ?x3 => unfold p'
| ?p' ?x1 ?x2 ?x3 ?x4 => unfold p'
| ?p' ?x1 ?x2 ?x3 ?x4 ?x5 => unfold p'
end
end.
Ltac activation_post_tac :=
match goal with
[ |- discActEnabled ?p ?a] =>
match p with
| _ $< _ >$ ? _ => apply dae_inPfx; reflexivity
| _ $< _ >$ ! _ => apply dae_outPfx; constructor
| ?p1 $+$ ?p2 => first [solve [apply daeSumL; activation_post_tac] |
solve [apply daeSumR; activation_post_tac]]
end
end; repeat constructor.
Ltac activation_tac := activation_pre_tac; activation_post_tac.
Lemma bcReady_outProc_out m l p :
bcReadyState m l p -> discActEnabled p (chanOutProc ;! [baseMode m, basePosition l]).
Lemma tfsStart_mCurr_in (p : ProcTerm) (m : Mode) : tfsStartState p ->
discActEnabled p (chanMCurr ;? [baseMode m]).
Lemma tfsNext_mStable_out (p : ProcTerm) (m : Mode) : tfsNextState m p ->
discActEnabled p (chanMStable *!).
Lemma tfsNext_mNext_out (p : ProcTerm) (m : Mode) : tfsNextState m p ->
discActEnabled p (chanMNext ;! ([baseMode (failSafeSucc m)])).
Lemma switchCurr_mCurr_out (p : ProcTerm) : switchCurrState p ->
discActEnabled p (chanMCurr *!).
Lemma switchListen_unpause_out (p : ProcTerm) : switchListenState p ->
discActEnabled p (chanUnpause *!).
Lemma tfsCurr_bad_in (p : ProcTerm) : tfsCurrState p ->
discActEnabled p (chanBad *?).
Lemma tfsCurr_abort_in (p : ProcTerm) : tfsCurrState p ->
discActEnabled p (chanAbort *?).
Lemma tfsCurr_mCurr_out (p : ProcTerm) : tfsCurrState p ->
discActEnabled p (chanMCurr *!).
Lemma tfsListen_bad_in (p : ProcTerm) : tfsListenState p ->
discActEnabled p (chanBad *?).
Lemma tfsListen_abort_in (p : ProcTerm) : tfsListenState p ->
discActEnabled p (chanAbort *?).
Lemma tfsListen_unpause_out (p : ProcTerm) : tfsListenState p ->
discActEnabled p (chanUnpause *!).
Lemma dormant_bad_in (p : ProcTerm) : dormantState p ->
discActEnabled p (chanBad *?).
Lemma dormant_abort_in (p : ProcTerm) : dormantState p ->
discActEnabled p (chanAbort *?).
Lemma dormant_mNext_in (p : ProcTerm) (m : Mode) : dormantState p ->
discActEnabled p (chanMNext ;? [baseMode m]).
Lemma switchBc_wake_out m p : switchBcState m p ->
discActEnabled p (chanWake ;! [baseMode m]).
Lemma sleeping_wake_in m p : sleepingState p ->
discActEnabled p (chanWake ;? [baseMode m]).
Lemma bcWait_wake_in m m' x p : bcWaitState m' x p ->
discActEnabled p (chanWake ;? [baseMode m]).
Lemma ovAbort_stable_out p : ovAbortState p -> discActEnabled p (chanMStable *!).
Lemma tfsBc_trans_out p : tfsBcState p -> discActEnabled p (chanTrans *!).
Lemma bcWait_trans_in p m x : bcWaitState m x p -> discActEnabled p (chanTrans *?).
Lemma sleep_trans_in p : sleepingState p -> discActEnabled p (chanTrans *?).
Lemma paused_unpause_in p : pausedState p -> discActEnabled p (chanUnpause *?).
Lemma paused_unpause_in_sort d p : pausedState p -> sort (chanUnpause *?) d p.
Lemma switchListen_unpause_out_sort d p : switchListenState p -> sort (chanUnpause *!) d p.
Lemma tfsListen_unpause_out_sort d p : tfsListenState p -> sort (chanUnpause *!) d p.
Theorem listener_outProc_out_not (p p' : ProcTerm) (v : list BaseType) :
listenerState p -> p -PA- chanOutProc ;! v -PA> p' -> False.
| [U : _ $( _ )$ -PA- _ -PA> _ |- _] => invertClear U; invert_def; clean_proc_trans
| [U : liftNameProc _ -PA- _ -PA> _ |- _] => invertClear U; invert_def; clean_proc_trans
end.
Lemma dae_outPfx c l v p :
evalExpLists l v -> discActEnabled (c $<l>$! p) (c;! v).
Lemma dae_inPfx c l v p :
length l = length v -> discActEnabled (c $<l>$? p) (c;? v).
Ltac update_eval := match goal with [H : ?e |_| ?m |- update _ ?x ?e ?x |_| ?m]
=> rewrite updateAppEq; apply H end.
Ltac lift_act_sum p1 p2 :=
match goal with
| [V : p1 -PA- ?a -PA> ?p' |- _] => apply (stepDpChoiceL p1 p2) in V
| [V : p2 -PA- ?a -PA> ?p' |- _] => apply (stepDpChoiceR p1 p2) in V
end.
Fixpoint genBaseList (n : nat) : list BaseType :=
match n with
| 0 => []
| S n' => (baseTime zeroTime) :: (genBaseList n')
end.
Ltac lift_act_then b p := match goal with
[V1 : p -PA- ?a -PA> ?p', V2 : evalBoolExpFunTot b = true |- _] =>
let V := fresh in rename V1 into V;
lets V1 : stepDpThen V V2; clear V end.
Lemma stepDpApp_alt : forall (n : Name) (l2 : list Exp) (p' : ProcTerm) (a : DiscAct),
stepDiscProc (subProcTerm (listsToSub (fst (def n)) l2) (snd (def n))) a p' ->
stepDiscProc (app n l2) a p'.
Ltac lift_act_app h l2 :=
match goal with
| [V : (subProcTerm (listsToSub (fst (def h)) l2) (snd (def h))) -PA- _ -PA> _ |- _] =>
apply stepDpApp_alt in V
end.
Lemma genBaseList_length A (l : list A) :
length (genBaseList (length l)) = length l.
Ltac gen_disc_acts p :=
match p with
| ?c $< ?l >$? ?p' => let V := fresh in
assert (p -PA- c ;? genBaseList (length l) -PA>
subProcTerm (listsToSub l (listBaselistExp (genBaseList (length l)))) p');
[constructor; reflexivity | ]; remove_resets_hyp V; remove_updates_hyp V
| ?c $< ?l >$! ?p' =>
let EEL := fresh in let EELEQ := fresh in
remember (evalExpListsFun l) as EEL eqn:EELEQ;
destruct EEL; try solve [inversion EELEQ];
match type of EELEQ with
| Some ?l' = _ =>
symmetry in EELEQ; assert (p -PA- c ;! l' -PA> p');
[apply evalExpListsFunRel in EELEQ; econstructor;
eassumption | ]; inversion EELEQ; subst
| _ => idtac
end; clear EELEQ
| ?b $> ?p' =>
let EEL := fresh in let EELEQ := fresh in
remember (evalBoolExpFunTot b) as EEL eqn:EELEQ;
destruct EEL; try solve [inversion EELEQ];
match type of EELEQ with
| true = _ =>
symmetry in EELEQ; gen_disc_acts p'; lift_act_then b p'; clear EELEQ
| _ => false
end
| ?p1 $+$ ?p2 => gen_disc_acts p1; gen_disc_acts p2; repeat lift_act_sum p1 p2
| ?h $( ?l2 )$ => gen_disc_acts (subProcTerm (listsToSub (fst (def h)) l2) (snd (def h)));
repeat lift_act_app h l2
| subProcTerm ?s ?p' =>
let p'' := fresh "p" in let Hp1 := fresh "Hp1" in
let Hp2 := fresh "Hp2" in
remember p as p'' eqn:Hp1; lets Hp2 : Hp1; simpl in Hp2;
remove_resets_hyp Hp2; remove_updates_hyp Hp2;
match type of Hp2 with _ = ?q => gen_disc_acts q end;
symmetry in Hp2; subst_all Hp2; subst_all Hp1
| $< ?e >$ ?p' => idtac
end.
Lemma bisim_disc_match p p' q a : p ~p~ q -> p -PA- a -PA> p' ->
exists q', q -PA- a -PA> q'.
Ltac invert_trans_rich := invert_trans; try invert_def; clean_proc_trans.
Ltac bisim_contra_rec V1 :=
match type of V1 with ?p ~p~ ?q =>
match goal with [V2 : p -PA- _ -PA> _ |- _] =>
eapply bisim_disc_match in V2; [ | apply V1];
let q' := fresh "q'" in let TR := fresh in
invertClearAs2 V2 q' TR; first [
solve [clear - TR; repeat invert_trans_rich]
| bisim_contra_rec V1]
end
end.
Ltac bisim_contra V1 :=
match type of V1 with ?p ~p~ ?q =>
gen_disc_acts p; bisim_contra_rec V1
end.
Ltac bisim_trans_tac BT :=
match goal with
| [V : ?p ~p~ ?x, V1 : ?p ~p~ ?y |- _] =>
assert (x ~p~ y) as BT; [eapply bisim_trans; [apply bisim_symm | ];
eassumption | ]
| [V : ?x ~p~ ?p, V1 : ?p ~p~ ?y |- _] =>
assert (x ~p~ y) as BT; [eapply bisim_trans; eassumption | ]
end.
Ltac invert_steps := repeat
(match goal with [V : _ -P- _ -P> _ |- _] =>
invertClear V end; subst).
Lemma bisim_dae p q a : p ~p~ q -> discActEnabled p a ->
discActEnabled q a.
Ltac activation_pre_tac :=
let U := fresh in
intro U; eapply bisim_dae; [apply bisim_symm; apply U | ];
match goal with [ |- discActEnabled ?p ?a] =>
match p with
| ?p' => unfold p'
| ?p' ?x1 => unfold p'
| ?p' ?x1 ?x2 => unfold p'
| ?p' ?x1 ?x2 ?x3 => unfold p'
| ?p' ?x1 ?x2 ?x3 ?x4 => unfold p'
| ?p' ?x1 ?x2 ?x3 ?x4 ?x5 => unfold p'
end
end.
Ltac activation_post_tac :=
match goal with
[ |- discActEnabled ?p ?a] =>
match p with
| _ $< _ >$ ? _ => apply dae_inPfx; reflexivity
| _ $< _ >$ ! _ => apply dae_outPfx; constructor
| ?p1 $+$ ?p2 => first [solve [apply daeSumL; activation_post_tac] |
solve [apply daeSumR; activation_post_tac]]
end
end; repeat constructor.
Ltac activation_tac := activation_pre_tac; activation_post_tac.
Lemma bcReady_outProc_out m l p :
bcReadyState m l p -> discActEnabled p (chanOutProc ;! [baseMode m, basePosition l]).
Lemma tfsStart_mCurr_in (p : ProcTerm) (m : Mode) : tfsStartState p ->
discActEnabled p (chanMCurr ;? [baseMode m]).
Lemma tfsNext_mStable_out (p : ProcTerm) (m : Mode) : tfsNextState m p ->
discActEnabled p (chanMStable *!).
Lemma tfsNext_mNext_out (p : ProcTerm) (m : Mode) : tfsNextState m p ->
discActEnabled p (chanMNext ;! ([baseMode (failSafeSucc m)])).
Lemma switchCurr_mCurr_out (p : ProcTerm) : switchCurrState p ->
discActEnabled p (chanMCurr *!).
Lemma switchListen_unpause_out (p : ProcTerm) : switchListenState p ->
discActEnabled p (chanUnpause *!).
Lemma tfsCurr_bad_in (p : ProcTerm) : tfsCurrState p ->
discActEnabled p (chanBad *?).
Lemma tfsCurr_abort_in (p : ProcTerm) : tfsCurrState p ->
discActEnabled p (chanAbort *?).
Lemma tfsCurr_mCurr_out (p : ProcTerm) : tfsCurrState p ->
discActEnabled p (chanMCurr *!).
Lemma tfsListen_bad_in (p : ProcTerm) : tfsListenState p ->
discActEnabled p (chanBad *?).
Lemma tfsListen_abort_in (p : ProcTerm) : tfsListenState p ->
discActEnabled p (chanAbort *?).
Lemma tfsListen_unpause_out (p : ProcTerm) : tfsListenState p ->
discActEnabled p (chanUnpause *!).
Lemma dormant_bad_in (p : ProcTerm) : dormantState p ->
discActEnabled p (chanBad *?).
Lemma dormant_abort_in (p : ProcTerm) : dormantState p ->
discActEnabled p (chanAbort *?).
Lemma dormant_mNext_in (p : ProcTerm) (m : Mode) : dormantState p ->
discActEnabled p (chanMNext ;? [baseMode m]).
Lemma switchBc_wake_out m p : switchBcState m p ->
discActEnabled p (chanWake ;! [baseMode m]).
Lemma sleeping_wake_in m p : sleepingState p ->
discActEnabled p (chanWake ;? [baseMode m]).
Lemma bcWait_wake_in m m' x p : bcWaitState m' x p ->
discActEnabled p (chanWake ;? [baseMode m]).
Lemma ovAbort_stable_out p : ovAbortState p -> discActEnabled p (chanMStable *!).
Lemma tfsBc_trans_out p : tfsBcState p -> discActEnabled p (chanTrans *!).
Lemma bcWait_trans_in p m x : bcWaitState m x p -> discActEnabled p (chanTrans *?).
Lemma sleep_trans_in p : sleepingState p -> discActEnabled p (chanTrans *?).
Lemma paused_unpause_in p : pausedState p -> discActEnabled p (chanUnpause *?).
Lemma paused_unpause_in_sort d p : pausedState p -> sort (chanUnpause *?) d p.
Lemma switchListen_unpause_out_sort d p : switchListenState p -> sort (chanUnpause *!) d p.
Lemma tfsListen_unpause_out_sort d p : tfsListenState p -> sort (chanUnpause *!) d p.
Theorem listener_outProc_out_not (p p' : ProcTerm) (v : list BaseType) :
listenerState p -> p -PA- chanOutProc ;! v -PA> p' -> False.
A process in the listening state is listening on the channel AN.
Lemma listening_AN_prot p v :
listeningStateProt p -> discActEnabled p (chanAN ;? v).
Lemma goMsg_gotRange_track m m' l r p p' a :
gotMsgState m l p -> gotRangeState m' r p' ->
p -PA- a -PA> p' -> exists l',
a = chanPos ;? [basePosition l'] /\
r = mkDistance (dist2d l l' -nn- speedMax *nn* msgLatency).
Lemma currOK_listening_track m p p' a : currOKState m p ->
listeningState p' -> p -PA- a -PA> p' -> a = (chanMStable *?).
Lemma abortOvlp_listening_track (p p' : ProcTerm) (a : DiscAct) :
abortOvlpState p -> listeningState p' -> p -PA- a -PA> p' ->
a = chanAbort;! [].
Ltac backtrack_pre p TR2 :=
let TR1 := fresh "TR" in
let SP1 := fresh "SP" in let SP2 := fresh "SP" in
intros TR1 SP1 SP2; cbv in SP2; apply stepPDisc in TR1;
lets TR2 : TR1;
invertClear SP1; match goal with [V : _ p |- _] =>
apply V in TR1 end; exand_flat.
listeningStateProt p -> discActEnabled p (chanAN ;? v).
Lemma goMsg_gotRange_track m m' l r p p' a :
gotMsgState m l p -> gotRangeState m' r p' ->
p -PA- a -PA> p' -> exists l',
a = chanPos ;? [basePosition l'] /\
r = mkDistance (dist2d l l' -nn- speedMax *nn* msgLatency).
Lemma currOK_listening_track m p p' a : currOKState m p ->
listeningState p' -> p -PA- a -PA> p' -> a = (chanMStable *?).
Lemma abortOvlp_listening_track (p p' : ProcTerm) (a : DiscAct) :
abortOvlpState p -> listeningState p' -> p -PA- a -PA> p' ->
a = chanAbort;! [].
Ltac backtrack_pre p TR2 :=
let TR1 := fresh "TR" in
let SP1 := fresh "SP" in let SP2 := fresh "SP" in
intros TR1 SP1 SP2; cbv in SP2; apply stepPDisc in TR1;
lets TR2 : TR1;
invertClear SP1; match goal with [V : _ p |- _] =>
apply V in TR1 end; exand_flat.
Given a context already pre-processed by backtrack_pre, this tactic
attempts to generate a contradiction via bisimilarities that are set up.
TR2 is just a hypothesis that needs to be cleared.
Ltac backtrack_post TR2 :=
clear TR2; let BT := fresh "BT" in
bisim_trans_tac BT; invert_steps;
repeat invert_trans; try bisim_contra BT;
try (apply bisim_symm in BT; bisim_contra BT).
Ltac backtrack_weed p := let TR := fresh in
backtrack_pre p TR; backtrack_post TR.
Theorem tfsNext_prev (p p' : ProcTerm) (a : DiscAct) (m : Mode) :
p -PA- a -PA> p' -> overlapState p -> tfsNextState m p' ->
tfsStartState p.
Theorem ovWait_prev (p p' : ProcTerm) (a : DiscAct) (m : Mode) (t x y : Time) :
p -PA- a -PA> p' -> overlapState p -> ovWaitState m t x y p' ->
initStateProt m p \/ exists l,
ovReadyState m (addTime t (period m)) l p /\ x = t
/\ y = period m /\ a = (chanOutProc ;! [baseMode m, basePosition l]).
Theorem ovReady_prev (p p' : ProcTerm) (a : DiscAct) (m : Mode) (t : Time) (l : Position) :
p -PA- a -PA> p' -> overlapState p -> ovReadyState m t l p' ->
exists x, ovWaitState m t x zeroTime p.
Theorem switchBc_prev (p p' : ProcTerm) (a : DiscAct) (m : Mode) :
p -PA- a -PA> p' -> overlapState p -> switchBcState m p' ->
exists t, exists y, ovWaitState m t zeroTime y p.
Theorem switchCurr_prev (p p' : ProcTerm) (a : DiscAct) :
p -PA- a -PA> p' -> overlapState p -> switchCurrState p' ->
exists m, switchBcState m p.
clear TR2; let BT := fresh "BT" in
bisim_trans_tac BT; invert_steps;
repeat invert_trans; try bisim_contra BT;
try (apply bisim_symm in BT; bisim_contra BT).
Ltac backtrack_weed p := let TR := fresh in
backtrack_pre p TR; backtrack_post TR.
Theorem tfsNext_prev (p p' : ProcTerm) (a : DiscAct) (m : Mode) :
p -PA- a -PA> p' -> overlapState p -> tfsNextState m p' ->
tfsStartState p.
Theorem ovWait_prev (p p' : ProcTerm) (a : DiscAct) (m : Mode) (t x y : Time) :
p -PA- a -PA> p' -> overlapState p -> ovWaitState m t x y p' ->
initStateProt m p \/ exists l,
ovReadyState m (addTime t (period m)) l p /\ x = t
/\ y = period m /\ a = (chanOutProc ;! [baseMode m, basePosition l]).
Theorem ovReady_prev (p p' : ProcTerm) (a : DiscAct) (m : Mode) (t : Time) (l : Position) :
p -PA- a -PA> p' -> overlapState p -> ovReadyState m t l p' ->
exists x, ovWaitState m t x zeroTime p.
Theorem switchBc_prev (p p' : ProcTerm) (a : DiscAct) (m : Mode) :
p -PA- a -PA> p' -> overlapState p -> switchBcState m p' ->
exists t, exists y, ovWaitState m t zeroTime y p.
Theorem switchCurr_prev (p p' : ProcTerm) (a : DiscAct) :
p -PA- a -PA> p' -> overlapState p -> switchCurrState p' ->
exists m, switchBcState m p.
Tactics
This is an activation-esque pre-tactic that instead of proving a dae,
matches to an actual transition, possibly with an eVar.
Ltac activation_trans_pre := match goal with [U : _ ?p |- ?p -PA- _ -PA> _] =>
inversion U; try (econstructor; [reflexivity | ]); remove_resets;
remove_updates end.
Ltac fwd_track_pre := intros; repeat eexists_safe;
match goal with [ |- ?P /\ _] => assert P end.
inversion U; try (econstructor; [reflexivity | ]); remove_resets;
remove_updates end.
Ltac fwd_track_pre := intros; repeat eexists_safe;
match goal with [ |- ?P /\ _] => assert P end.
Results
Theorem currOK_next (p p' : ProcTerm) (a : DiscAct) (m'' : Mode) :
p -PA- a -PA> p' -> currOKState m'' p ->
(exists m, nextEqState m m'' p') \/
listeningState p'.
Theorem rangeBad_next (p p' : ProcTerm) (a : DiscAct) (m'' : Mode) :
p -PA- a -PA> p' -> rangeBadState m'' p ->
(exists m, currEqState m m'' p').
Theorem gotMessage_next (p p' : ProcTerm)
(a : DiscAct) (m'' : Mode) (l : Position) :
p -PA- a -PA> p' -> gotMsgState m'' l p ->
(exists r, gotRangeState m'' r p').
Theorem gotRange_next (p p' : ProcTerm)
(a : DiscAct) (m'' : Mode) (r : Distance) :
p -PA- a -PA> p' -> gotRangeState m'' r p ->
(exists m, currPincCheckState m m'' r p').
Theorem currComp_next (p p' : ProcTerm)
(a : DiscAct) (m'' : Mode) (r : Distance) :
p -PA- a -PA> p' -> currCompState m'' r p ->
(exists m, nextPincCheckState m m'' r p') \/
listeningState p'.
Theorem badOvlp_next (p p' : ProcTerm) (a : DiscAct) :
p -PA- a -PA> p' -> badOvlpState p -> listeningState p'.
Theorem abortOvlp_next (p p' : ProcTerm) (a : DiscAct) :
p -PA- a -PA> p' -> abortOvlpState p -> listeningState p'.
Lemma tfsStart_next (p p' : ProcTerm) (a : DiscAct) :
p -PA- a -PA> p' -> tfsStartState p ->
exists m, tfsNextState m p'.
Lemma currEq_cond_true m m'' p :
m = m'' -> currEqState m m'' p -> badOvlpState p.
Lemma currEq_cond_false m m'' p :
m <> m'' -> currEqState m m'' p -> currOKState m'' p.
Lemma nextEq_cond_true m' m'' p :
m' = m'' -> nextEqState m' m'' p -> abortOvlpState p.
Lemma nextEq_cond_false m' m'' p :
m' <> m'' -> nextEqState m' m'' p -> listeningState p.
Lemma currPincCheck_cond_true m m'' (r : Distance) p :
possiblyIncompatible m m'' r -> currPincCheckState m m'' r p ->
badOvlpState p.
Lemma currPincCheck_cond_false m m'' (r : Distance) p :
~possiblyIncompatible m m'' r ->
currPincCheckState m m'' r p -> currCompState m'' r p.
Lemma nextPincCheck_cond_true m m'' (r : Distance) p :
possiblyIncompatible m m'' r ->
nextPincCheckState m m'' r p -> abortOvlpState p.
Lemma nextPincCheck_cond_false m m'' (r : Distance) p :
~possiblyIncompatible m m'' r ->
nextPincCheckState m m'' r p -> listeningState p.
Ltac existentialise_evals_del H :=
let y1 := fresh in let y2 := fresh in
let y3 := fresh in let y4 := fresh in let U := fresh in
match type of H with
| ?P /\ ?Q =>
match P with
| (((?e1 |_| ?v1 /\ ?e2 |_| ?v2) /\
?e3 |_| ?v3) /\ ?e4 |_| ?v4) =>
match Q with ?f ?e1 ?e2 ?e3 ?e4 -PD- ?d -PD> ?p' =>
assert (exists y1 y2 y3 y4, f y1 y2 y3 y4 -PD- d -PD> p'
/\ (((y1 |_| v1 /\ y2 |_| v2) /\
y3 |_| v3) /\ y4 |_| v4)) as U;
[repeat eexists; apply H | clear H]; rename U into H
end
| ((?e1 |_| ?v1 /\ ?e2 |_| ?v2) /\
?e3 |_| ?v3) =>
match Q with ?f ?e1 ?e2 ?e3 -PD- ?d -PD> ?p' =>
assert (exists y1 y2 y3, f y1 y2 y3 -PD- d -PD> p'
/\ ((y1 |_| v1 /\ y2 |_| v2) /\
y3 |_| v3)) as U;
[repeat eexists; apply H | clear H]; rename U into H
end
| (?e1 |_| ?v1 /\ ?e2 |_| ?v2) =>
match Q with ?f ?e1 ?e2 -PD- ?d -PD> ?p' =>
assert (exists y1 y2, f y1 y2 -PD- d -PD> p'
/\ (y1 |_| v1 /\ y2 |_| v2)) as U;
[repeat eexists; apply H | clear H]; rename U into H
end
| ?e1 |_| ?v1 =>
match Q with ?f ?e1 -PD- ?d -PD> ?p' =>
assert (exists y1, f y1 y2 -PD- d -PD> p'
/\ y1 |_| v1) as U;
[repeat eexists; apply H | clear H]; rename U into H
end
end
| _ => idtac
end.
Ltac invert_trans_del := match goal with [P : _ -PD- _ -PD> _ |- _]
=> invertClear P; subst end.
Lemma ovWait_del_pres m t x y p p' d :
ovWaitState m t x y p -> p -PD- d -PD> p' ->
ovWaitState m t x y p'.
Lemma ovReady_del_pres m t l p p' d :
ovReadyState m t l p -> p -PD- d -PD> p' ->
ovReadyState m t l p'.
Lemma switchBc_del_pres m p p' d :
switchBcState m p -> p -PD- d -PD> p' ->
switchBcState m p'.
Lemma switchCurr_del_pres p p' d :
switchCurrState p -> p -PD- d -PD> p' ->
switchCurrState p'.
Theorem del_pres_nextSinceState (p p' : ProcTerm) (d : Delay) :
nextSinceState p -> p -PD- d -PD> p' -> nextSinceState p'.
Theorem del_pres_tfsState (p p' : ProcTerm) (d : Delay):
tfsState p -> p -PD- d -PD> p' -> tfsState p'.
Lemma link_par_triple_discEx (p1 p2 p3 p' : ProcTerm) (a : DiscAct) :
p1 $||$ p2 $||$ p3 -PA- a -PA> p' -> exists p1' p2' p3',
p' = p1' $||$ p2' $||$ p3'.
Ltac link_partripdiscex_tac U p1' p2' p3' :=
match goal with
[H : ?p1 $||$ ?p2 $||$ ?p3 -PA- ?a -PA> ?p' |- _] =>
let Q1 := fresh in lets Q1 : link_par_triple_discEx H;
let U1 := fresh U in decompEx3 Q1 p1' p2' p3' U1
end.
Ltac link_partripdiscex_tac2 p1' p2' p3' :=
match goal with
[H : ?p1 $||$ ?p2 $||$ ?p3 -PA- ?a -PA> ?p' |- _] =>
let Q1 := fresh in lets Q1 : link_par_triple_discEx H;
let U1 := fresh in decompEx3 Q1 p1' p2' p3' U1;
rewrite U1 in H; clear U1
end.
Lemma link_par_triple_delEx (p1 p2 p3 p' : ProcTerm) (d : Delay) :
p1 $||$ p2 $||$ p3 -PD- d -PD> p' -> exists p1' p2' p3',
p' = p1' $||$ p2' $||$ p3'.
Ltac link_partripdelex_tac U p1' p2' p3' :=
match goal with
[H : ?p1 $||$ ?p2 $||$ ?p3 -PD- ?d -PD> ?p' |- _] =>
let Q1 := fresh in lets Q1 : link_par_triple_delEx H;
let U1 := fresh U in decompEx3 Q1 p1' p2' p3' U1
end.
Ltac link_partripdelex_tac2 p1' p2' p3' :=
match goal with
[H : ?p1 $||$ ?p2 $||$ ?p3 -PD- ?d -PD> ?p' |- _] =>
let Q1 := fresh in lets Q1 : link_par_triple_delEx H;
let U1 := fresh in decompEx3 Q1 p1' p2' p3' U1;
rewrite U1 in H; clear U1
end.
Lemma link_par_triple_out (p1 p2 p3 p1' p2' p3' : ProcTerm)
(c : Channel) (v : list BaseType) :
p1 $||$ p2 $||$ p3 -PA- c ;! v -PA> p1' $||$ p2' $||$ p3' ->
(p1 -PA- c ;! v -PA> p1' /\ p2 = p2' /\ p3 = p3' \/
p2 -PA- c ;! v -PA> p2' /\ p1 = p1' /\ p3 = p3' \/
p3 -PA- c ;! v -PA> p3' /\ p1 = p1' /\ p2 = p2').
Ltac link_partripout_tac U :=
match goal with
[H : ?p1 $||$ ?p2 $||$ ?p3 -PA- ?c ;! ?v -PA> ?p1' $||$ ?p2' $||$ ?p3' |- _] =>
let H1 := fresh in lets H1 : link_par_triple_out H;
let H2 := fresh in elimOr3 H1 H2; andflat U
end.
Lemma link_par_triple_in (p1 p2 p3 p1' p2' p3' : ProcTerm)
(c : Channel) (v : list BaseType) :
p1 $||$ p2 $||$ p3 -PA- c ;? v -PA> p1' $||$ p2' $||$ p3' ->
(p1 -PA- c ;? v -PA> p1' /\ p2 = p2' /\ p3 = p3' \/
p2 -PA- c ;? v -PA> p2' /\ p1 = p1' /\ p3 = p3' \/
p3 -PA- c ;? v -PA> p3' /\ p1 = p1' /\ p2 = p2').
Ltac link_partripin_tac U :=
match goal with
[H : ?p1 $||$ ?p2 $||$ ?p3 -PA- ?c ;? ?v -PA> ?p1' $||$ ?p2' $||$ ?p3' |- _] =>
let H1 := fresh in lets H1 : link_par_triple_in H;
let H2 := fresh in elimOr3 H1 H2; andflat U
end.
Lemma link_reach_triple_tau (p1 p2 p3 p1' p2' p3' : ProcTerm) :
p1 $||$ p2 $||$ p3 -PA- tauAct -PA> p1' $||$ p2' $||$ p3' ->
protocolState (p1 $||$ p2 $||$ p3) -> exists c v,
(p1 -PA- c ;! v -PA> p1' /\ p2 -PA- c ;? v -PA> p2' /\ p3 = p3') \/
(p1 -PA- c ;? v -PA> p1' /\ p2 -PA- c ;! v -PA> p2' /\ p3 = p3') \/
(p1 -PA- c ;! v -PA> p1' /\ p3 -PA- c ;? v -PA> p3' /\ p2 = p2') \/
(p1 -PA- c ;? v -PA> p1' /\ p3 -PA- c ;! v -PA> p3' /\ p2 = p2') \/
(p2 -PA- c ;! v -PA> p2' /\ p3 -PA- c ;? v -PA> p3' /\ p1 = p1') \/
(p2 -PA- c ;? v -PA> p2' /\ p3 -PA- c ;! v -PA> p3' /\ p1 = p1').
Ltac link_partriptau_tac c v U :=
match goal with
[H : ?p1 $||$ ?p2 $||$ ?p3 -PA- tauAct -PA> ?p1' $||$ ?p2' $||$ ?p3',
H0 : protocolState (?p1 $||$ ?p2 $||$ ?p3) |- _] =>
let H1 := fresh in lets H1 : link_reach_triple_tau H H0;
let Q1 := fresh in decompEx2 H1 c v Q1;
let H2 := fresh in elimOr6 Q1 H2; andflat U
end.
Lemma link_par_triple_del (p1 p2 p3 p1' p2' p3' : ProcTerm)
(d : Delay) :
p1 $||$ p2 $||$ p3 -PD- d -PD> p1' $||$ p2' $||$ p3' ->
(p1 -PD- d -PD> p1' /\ p2 -PD- d-PD> p2' /\ p3 -PD- d -PD> p3').
Ltac link_partripdel_tac U :=
match goal with
[H : ?p1 $||$ ?p2 $||$ ?p3 -PD- ?d -PD> ?p1' $||$ ?p2' $||$ ?p3' |- _] =>
let Q1 := fresh in lets Q1 : link_par_triple_del H; andflat U
end.
Theorem paused_switch (p : ProcTerm) :
reachableProt p ->
(pausedStateProt p <-> switchStateProt p).
Theorem reachableProt_triple (p : ProcTerm) :
reachableProt p -> protocolState p.
Ltac reachprot U :=
match goal with
[H : reachableProt ?p |- _] => let U1 := fresh U in
lets U1 : reachableProt_triple H
end.
Theorem bc_outProc_out (p p' : ProcTerm) (m : Mode) (l : Position) :
p -PA- chanOutProc ;! [baseMode m, basePosition l] -PA> p' -> broadcastState p ->
bcReadyState m l p /\ bcWaitState m (period m) p'.
Theorem ovlp_outProc_out (p p' : ProcTerm) (m : Mode) (l : Position) :
p -PA- chanOutProc ;! [baseMode m, basePosition l] -PA> p' -> overlapState p ->
exists t f, ovReadyState m t l p /\
ovWaitState m (minusTime t (period m) f) (minusTime t (period m) f) (period m) p'.
Theorem prot_outProc_in_not (p p' : ProcTerm) (v : list BaseType) :
p -PA- chanOutProc ;? v -PA> p' -> protocolState p -> False.
Theorem bc_mCurr_out_not (p p' : ProcTerm) :
p -PA- chanMCurr ;! [] -PA> p' -> broadcastState p -> False.
Theorem bc_abort_in_not (p p' : ProcTerm) :
p -PA- chanAbort*? -PA> p' -> broadcastState p -> False.
Theorem listen_mCurr_out_not (p p' : ProcTerm) :
p -PA- chanMCurr ;! [] -PA> p' -> listenerState p -> False.
Theorem ovlp_mCurr_out (p p' : ProcTerm) :
p -PA- chanMCurr ;! [] -PA> p' -> overlapState p ->
(switchCurrState p /\ switchListenState p') \/
(tfsCurrState p /\ tfsBcState p').
Lemma bc_abort_out_not (p p' : ProcTerm) :
p -PA- chanAbort;! [] -PA> p' -> broadcastState p -> False.
Lemma ovlp_abort_out_not (p p' : ProcTerm) :
p -PA- chanAbort;! [] -PA> p' -> overlapState p -> False.
Theorem ovlp_abort_in (p p' : ProcTerm) (m : Mode) :
p -PA- chanAbort*? -PA> p' -> overlapState p ->
(dormantState p /\ dormantState p') \/
ovAbortState p' \/
(tfsCurrState p /\ tfsCurrState p') \/
(tfsListenState p /\ tfsListenState p').
Theorem bc_mStable_out_not (p p' : ProcTerm) :
p -PA- chanMStable*! -PA> p' -> broadcastState p -> False.
Theorem ovlp_mStable_out_not (p p' : ProcTerm) :
p -PA- chanMStable*! -PA> p' -> overlapState p -> False.
Lemma gotMsg_state p p' m l :
p -PA- chanInProc;? [baseMode m, basePosition l] -PA> p' -> gotMsgStateProt m l p'.
Lemma link_ent_soft_disc p p' l l' h h' k k' a :
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
p = p' \/ exists b, p -PA- b -PA> p'.
Destructs any entities into constituent parts, looks for a
discrete entity transition in the goal, extracts a process transition
or a process equality from this.
Ltac link_entsoftdisc_tac :=
destrEnts_norm; match goal with
[V : [|_, _, _, _|] -EA- _ ->> [|_, _, _, _|] |- _] =>
let U := fresh in let U1 := fresh "LES" in
let U2 := fresh "LES" in
lets U : link_ent_soft_disc V; elim_intro U U1 U2; [ | ex_flat];subst end.
Ltac link_partripdiscex_tac_subst p1' p2' p3' :=
match goal with
[H : ?p1 $||$ ?p2 $||$ ?p3 -PA- ?a -PA> ?p' |- _] =>
let Q1 := fresh in lets Q1 : link_par_triple_discEx H;
let U1 := fresh in decompEx3 Q1 p1' p2' p3' U1; subst
end.
Ltac link_partripdiscex_tac_norm :=
let p1' := fresh "p1'" in let p2' := fresh "p2'" in
let p3' := fresh "p3'" in
link_partripdiscex_tac_subst p1' p2' p3'.
destrEnts_norm; match goal with
[V : [|_, _, _, _|] -EA- _ ->> [|_, _, _, _|] |- _] =>
let U := fresh in let U1 := fresh "LES" in
let U2 := fresh "LES" in
lets U : link_ent_soft_disc V; elim_intro U U1 U2; [ | ex_flat];subst end.
Ltac link_partripdiscex_tac_subst p1' p2' p3' :=
match goal with
[H : ?p1 $||$ ?p2 $||$ ?p3 -PA- ?a -PA> ?p' |- _] =>
let Q1 := fresh in lets Q1 : link_par_triple_discEx H;
let U1 := fresh in decompEx3 Q1 p1' p2' p3' U1; subst
end.
Ltac link_partripdiscex_tac_norm :=
let p1' := fresh "p1'" in let p2' := fresh "p2'" in
let p3' := fresh "p3'" in
link_partripdiscex_tac_subst p1' p2' p3'.
If a parallel process triple can do an action, then the first component is either
preserved or it too can do some action.
Lemma link_par_triple_discW_1 p1 p1' p2 p2' p3 p3' a :
p1 $||$ p2 $||$ p3 -PA- a -PA> p1' $||$ p2' $||$ p3' ->
p1 = p1' \/ exists a', p1 -PA- a' -PA> p1'.
p1 $||$ p2 $||$ p3 -PA- a -PA> p1' $||$ p2' $||$ p3' ->
p1 = p1' \/ exists a', p1 -PA- a' -PA> p1'.
If a parallel process triple can do an action, then the second component is either
preserved or it too can do some action.
Lemma link_par_triple_discW_2 p1 p1' p2 p2' p3 p3' a :
p1 $||$ p2 $||$ p3 -PA- a -PA> p1' $||$ p2' $||$ p3' ->
p2 = p2' \/ exists a', p2 -PA- a' -PA> p2'.
p1 $||$ p2 $||$ p3 -PA- a -PA> p1' $||$ p2' $||$ p3' ->
p2 = p2' \/ exists a', p2 -PA- a' -PA> p2'.
If a parallel process triple can do an action, then the third component is either
preserved or it too can do some action.
Lemma link_par_triple_discW_3 p1 p1' p2 p2' p3 p3' a :
p1 $||$ p2 $||$ p3 -PA- a -PA> p1' $||$ p2' $||$ p3' ->
p3 = p3' \/ exists a', p3 -PA- a' -PA> p3'.
Lemma link_par_triple_out_neq1 p1 p1' p2 p2' p3 p3' c v :
p1 <> p1' ->
p1 $||$ p2 $||$ p3 -PA- c ;! v -PA> p1' $||$ p2' $||$ p3' ->
p1 -PA- c ;! v -PA> p1' /\ p2 = p2' /\ p3 = p3'.
Lemma link_par_triple_out_neq2 p1 p1' p2 p2' p3 p3' c v :
p2 <> p2' ->
p1 $||$ p2 $||$ p3 -PA- c ;! v -PA> p1' $||$ p2' $||$ p3' ->
p2 -PA- c ;! v -PA> p2' /\ p1 = p1' /\ p3 = p3'.
Lemma link_par_triple_out_neq3 p1 p1' p2 p2' p3 p3' c v :
p3 <> p3' ->
p1 $||$ p2 $||$ p3 -PA- c ;! v -PA> p1' $||$ p2' $||$ p3' ->
p3 -PA- c ;! v -PA> p3' /\ p1 = p1' /\ p2 = p2'.
Lemma link_par_triple_in_neq1 p1 p1' p2 p2' p3 p3' c v :
p1 <> p1' ->
p1 $||$ p2 $||$ p3 -PA- c ;? v -PA> p1' $||$ p2' $||$ p3' ->
p1 -PA- c ;? v -PA> p1' /\ p2 = p2' /\ p3 = p3'.
Lemma link_par_triple_in_neq2 p1 p1' p2 p2' p3 p3' c v :
p2 <> p2' ->
p1 $||$ p2 $||$ p3 -PA- c ;? v -PA> p1' $||$ p2' $||$ p3' ->
p2 -PA- c ;? v -PA> p2' /\ p1 = p1' /\ p3 = p3'.
Lemma link_par_triple_in_neq3 p1 p1' p2 p2' p3 p3' c v :
p3 <> p3' ->
p1 $||$ p2 $||$ p3 -PA- c ;? v -PA> p1' $||$ p2' $||$ p3' ->
p3 -PA- c ;?v -PA> p3' /\ p1 = p1' /\ p2 = p2'.
Ltac link_partripneq_out_tac :=
let LPO := fresh "LPO" in
match goal with
[V : ?p1 $||$ ?p2 $||$ ?p3 -PA- ?c ;! ?v -PA> ?p1' $||$ ?p2' $||$ ?p3' |- _] =>
match goal with
| [V1 : p1 <> p1' |- _ ] => lets LPO : link_par_triple_out_neq1 V1 V
| [V1 : p2 <> p2' |- _ ] => lets LPO : link_par_triple_out_neq2 V1 V
| [V1 : p3 <> p3' |- _ ] => lets LPO : link_par_triple_out_neq3 V1 V
end;
and_flat
end.
Ltac link_partripneq_in_tac :=
let LPO := fresh "LPO" in
match goal with
[V : ?p1 $||$ ?p2 $||$ ?p3 -PA- ?c ;? ?v -PA> ?p1' $||$ ?p2' $||$ ?p3' |- _] =>
match goal with
| [V1 : p1 <> p1' |- _ ] => lets LPO : link_par_triple_in_neq1 V1 V
| [V1 : p2 <> p2' |- _ ] => lets LPO : link_par_triple_in_neq2 V1 V
| [V1 : p3 <> p3' |- _ ] => lets LPO : link_par_triple_in_neq3 V1 V
end;
and_flat
end.
Ltac link_partripneq_tac := first [link_partripneq_in_tac | link_partripneq_out_tac].
Lemma ovlp_abort_in_notNextSince p p' :
p -PA- chanAbort;? [] -PA> p' -> overlapState p -> ~ nextSinceState p'.
Lemma listening_abort_contra p :
listeningState p -> abortOvlpState p -> False.
p1 $||$ p2 $||$ p3 -PA- a -PA> p1' $||$ p2' $||$ p3' ->
p3 = p3' \/ exists a', p3 -PA- a' -PA> p3'.
Lemma link_par_triple_out_neq1 p1 p1' p2 p2' p3 p3' c v :
p1 <> p1' ->
p1 $||$ p2 $||$ p3 -PA- c ;! v -PA> p1' $||$ p2' $||$ p3' ->
p1 -PA- c ;! v -PA> p1' /\ p2 = p2' /\ p3 = p3'.
Lemma link_par_triple_out_neq2 p1 p1' p2 p2' p3 p3' c v :
p2 <> p2' ->
p1 $||$ p2 $||$ p3 -PA- c ;! v -PA> p1' $||$ p2' $||$ p3' ->
p2 -PA- c ;! v -PA> p2' /\ p1 = p1' /\ p3 = p3'.
Lemma link_par_triple_out_neq3 p1 p1' p2 p2' p3 p3' c v :
p3 <> p3' ->
p1 $||$ p2 $||$ p3 -PA- c ;! v -PA> p1' $||$ p2' $||$ p3' ->
p3 -PA- c ;! v -PA> p3' /\ p1 = p1' /\ p2 = p2'.
Lemma link_par_triple_in_neq1 p1 p1' p2 p2' p3 p3' c v :
p1 <> p1' ->
p1 $||$ p2 $||$ p3 -PA- c ;? v -PA> p1' $||$ p2' $||$ p3' ->
p1 -PA- c ;? v -PA> p1' /\ p2 = p2' /\ p3 = p3'.
Lemma link_par_triple_in_neq2 p1 p1' p2 p2' p3 p3' c v :
p2 <> p2' ->
p1 $||$ p2 $||$ p3 -PA- c ;? v -PA> p1' $||$ p2' $||$ p3' ->
p2 -PA- c ;? v -PA> p2' /\ p1 = p1' /\ p3 = p3'.
Lemma link_par_triple_in_neq3 p1 p1' p2 p2' p3 p3' c v :
p3 <> p3' ->
p1 $||$ p2 $||$ p3 -PA- c ;? v -PA> p1' $||$ p2' $||$ p3' ->
p3 -PA- c ;?v -PA> p3' /\ p1 = p1' /\ p2 = p2'.
Ltac link_partripneq_out_tac :=
let LPO := fresh "LPO" in
match goal with
[V : ?p1 $||$ ?p2 $||$ ?p3 -PA- ?c ;! ?v -PA> ?p1' $||$ ?p2' $||$ ?p3' |- _] =>
match goal with
| [V1 : p1 <> p1' |- _ ] => lets LPO : link_par_triple_out_neq1 V1 V
| [V1 : p2 <> p2' |- _ ] => lets LPO : link_par_triple_out_neq2 V1 V
| [V1 : p3 <> p3' |- _ ] => lets LPO : link_par_triple_out_neq3 V1 V
end;
and_flat
end.
Ltac link_partripneq_in_tac :=
let LPO := fresh "LPO" in
match goal with
[V : ?p1 $||$ ?p2 $||$ ?p3 -PA- ?c ;? ?v -PA> ?p1' $||$ ?p2' $||$ ?p3' |- _] =>
match goal with
| [V1 : p1 <> p1' |- _ ] => lets LPO : link_par_triple_in_neq1 V1 V
| [V1 : p2 <> p2' |- _ ] => lets LPO : link_par_triple_in_neq2 V1 V
| [V1 : p3 <> p3' |- _ ] => lets LPO : link_par_triple_in_neq3 V1 V
end;
and_flat
end.
Ltac link_partripneq_tac := first [link_partripneq_in_tac | link_partripneq_out_tac].
Lemma ovlp_abort_in_notNextSince p p' :
p -PA- chanAbort;? [] -PA> p' -> overlapState p -> ~ nextSinceState p'.
Lemma listening_abort_contra p :
listeningState p -> abortOvlpState p -> False.
This page has been generated by coqdoc