Library NARIncomp
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 Coq.Program.Equality.
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.InterfaceLanguage.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.EntityLanguage.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.ProtAuxResults.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.NARMisc.
Theorem incomingNet_urgent (n n' : Network) (v : list BaseType) (i : nat) (d : Delay) :
reachableNet n -> incomingNet v i n -> ~n -ND- d -ND> n'. Admitted.
Theorem incomp_incomingNet_bad (n n' : Network) (a : ActDiscNet) (l l' : Position) (i : nat)
(m m' : Mode) :
n -NA- a -NA> n' -> inPosNet l i n -> currModeNet m i n ->
incomingNet [baseMode m', basePosition l'] i n ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n' \/
msgBadPathNet i n'.
introz U.
destruct U2.
link_netentdiscfwd_tac e' a' Y. destr_ent_inter e' p' l'' k' li' lo' ln'.
left. eapply incoming_ent_net. repeat constructor. apply H0. my_applys_eq Y.
symmetry. apply Y0.
destruct e' as [p' l'' h' k'].
link_entinterdisc_tac v r Q;destruct h' as [li' lo' ln'];
try (
match goal with [TRI : _ -i- ?act -i> _ |- _] =>
assert (forall d : Delay, act <> d) as ANE end; [intro d;
unfold not; intro CON; inversion CON | ]);
try solve
[lets W : inList_inter_pres_input ANE H0 Q; elim_intro W W1 W2;[left; eapply incoming_ent_net;
repeat constructor; [apply W1 | apply Y] | inversion W2]].
left. eapply incoming_ent_net. repeat constructor. apply H0. my_applys_eq Y.
rewrite <- Q. reflexivity.
lets II : inList_inter_pres_input ANE H0 Q. elim_intro II IN EQ. left.
eapply incoming_ent_net. repeat constructor. apply IN. apply Y.
inversion EQ.
invertClearAs1 EQ EB. rewrite EB in Q0.
right. doappsnd econstructor Y. lets GM : gotMsg_state Q0.
lets CX : U1. rewrite currMode_ent_ex in CX. decompExAnd CX e EA EM.
lets EU : entInNetUnique EA H. rewrite EU in EM.
lets MB : mbpMsg GM EM U3.
replace l'' with l. rewrite <- H3. eapply MB.
eapply inPos_unique. rewrite <- inPos_pres_disc. apply U0. apply U.
econstructor. apply Y. Qed.
Theorem incomp_incomingNet_abort (n n' : Network) (a : ActDiscNet) (l l' : Position) (i : nat)
(m m' : Mode) : n -NA- a -NA> n' -> inPosNet l i n -> nextModeNet m i n ->
incomingNet [baseMode m', basePosition l'] i n ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n' \/ msgAbortPathNet i n'.
Admitted.
Theorem msgAbort_not_nextSince (n n' : Network) (a : ActDiscNet)
(i : nat) (rn : reachableNet n) :
msgAbortPathNet i n -> n -NA- a -NA> n' ->
msgAbortPathNet i n' \/ ~nextSinceStateNet i n'. introz U.
inversion U. link_netentdiscfwd_tac e' b U1. left. econstructor.
apply H. rewrite U2. assumption.
link_entsoftdisc_tac;
lets MSI : minet H0; lets MSI' : minet U1;
lets NME : msgAbort_modeState_eq U MSI U0;
lets MIU : mState_in_net_unique MSI' NME; subst.
left. econstructor;[ | apply U1].
ent_disc_pres_pos_tac. subst.
eapply msgAbort_inter_irrel. eassumption.
remember (currModeMState k0) as CMM.
inversion H; ent_disc_pres_pos_tac; try unfold_all r'; subst.
inversion H6; subst.
link_partripdiscex_tac_norm.
lets LPT : link_par_triple_discW_3 H1. elim_intro LPT EQP EXP.
left. subst. econstructor;[ | apply U1].
eapply mapMsg; try eassumption. econstructor. eassumption.
reflexivity.
ex_flat. lets GMN : gotMessage_next H3 H2. ex_flat.
assert (gotMsgStateEnt m'' l' ([|p1 $||$ p2 $||$ p3, l, h0, k0|])) as GME.
constructor. assumption.
assert (gotRangeStateEnt m'' x1 ([|p1' $||$ p2' $||$ p3', l, h, k0|])) as GRE.
do 2 constructor. assumption.
lets GGE : gotMsg_gotRange_track_ent GME GRE U3.
exand_flat. left. econstructor;[ | eassumption].
eapply mapGrng. econstructor. eassumption. reflexivity.
rewrite AND2. unfold not. intros. apply H8.
assumption. eassumption. rewrite AND2. assumption.
inversion H6; subst.
link_partripdiscex_tac_norm.
lets LPT : link_par_triple_discW_3 H1. elim_intro LPT EQP EXP.
left. subst. econstructor;[ | apply U1].
eapply mapGrng; try eassumption. econstructor. eassumption.
reflexivity.
ex_flat. lets GMN : gotRange_next H3 H2. ex_flat.
assert (gotRangeStateEnt m'' r ([|p1 $||$ p2 $||$ p3, l, h0, k0|])) as GRE.
constructor. assumption.
assert (currPincCheckStateEnt x1 m'' r ([|p1' $||$ p2' $||$ p3', l, h, k0|])) as CPC.
do 2 constructor. assumption.
lets GGE : gotRange_currPincCheck_track_ent GRE CPC U3.
exand_flat. left. econstructor. eapply mapCuco. econstructor.
eapply currPincCheck_cond_false. apply H8. rewrite <- AND2.
eassumption. eassumption. assumption. eassumption.
inversion H5; subst.
link_partripdiscex_tac_norm.
lets LPT : link_par_triple_discW_3 H1. elim_intro LPT EQP EXP.
left. subst. econstructor;[ | apply U1].
eapply mapCuco; try eassumption. econstructor. eassumption.
ex_flat. lets GMN : currComp_next H3 H2.
assert (currCompStateEnt m'' r ([|p1 $||$ p2 $||$ p3, l, h0, k0|])) as CCE.
constructor. assumption. elim_intro GMN ENP LSP.
ex_flat.
assert (nextPincCheckStateEnt x1 m'' r ([|p1' $||$ p2' $||$ p3', l, h, k0|])) as NPC.
do 2 constructor. assumption.
lets GGE : currComp_nextPincCheck_track_ent CCE NPC U3.
exand_flat. left. econstructor;[ | apply U1]. eapply mapAbort.
econstructor. eapply nextPincCheck_cond_true. eassumption.
rewrite H7 in AND2. inversion AND2. assumption.
assert (listeningStateEnt ([|p1' $||$ p2' $||$ p3', l, h, k0|])) as LSE.
do 2 constructor. assumption.
assert (unstable k0) as USK. eapply nextMode_unstable. eassumption.
lets USO : unstable_stable_out_not USK. false. apply USO.
econstructor. lets CLT : currComp_listening_track_ent CCE LSE U3.
and_flat. eassumption.
This case is almost identical to the case for notifAbortPath_not_nextSince.
inversion H3; subst. link_partripdiscex_tac_norm. swapRename H1 H2.
lets LPT : link_par_triple_discW_3 H2. elim_intro LPT EQP EXP.
left. subst. econstructor;[ | apply U1].
eapply mapAbort. econstructor. eassumption.
ex_flat. lets CON : abortOvlp_next H4 H1. right.
assert (p3 <> p3') as PNE3. unfold not. intros. subst.
false. eapply listening_abort_contra; eassumption.
assert (p1 $||$ p2 $||$ p3 <> p1' $||$ p2' $||$ p3') as PNE.
unfold not. intro. inversion H5. subst. apply PNE3. reflexivity.
lets LEP : link_ent_proc_neq_disc PNE U3. andflat LEP.
or_flat; ex_flat; and_flat; try link_partripneq_tac;
try (lets CLT : abortOvlp_listening_track H1 CON AND1; inversion CLT); subst.
reach_net_prot_tac. link_partriptau_tac c v LPT;
try (lets CLT : abortOvlp_listening_track H1 CON LPT1;
inversion CLT; subst).
subst; contradict PNE3; reflexivity.
subst; contradict PNE3; reflexivity.
false. eapply bc_abort_in_not. apply LPT.
inversion RPT. assumption.
inversion RPT.
lets OAI : ovlp_abort_in_notNextSince LPT H9. unfold not. intro. apply OAI.
inversion H11. entnetuniq2 EN n'. subst. inversion H12. inversion H6.
assumption.
false. eapply inter_abort_in_not. eassumption.
false. eapply modeState_abort_in_not; eassumption.
lets CLT : abortOvlp_listening_track H1 CON AND; inversion CLT. Qed.
Theorem instant_incomp_abort (n : Network) (t : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
nextSince m t i n p -> inPosNet l i n -> 0 < t ->
received [baseMode m', basePosition l'] zeroTime i n p ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n \/
msgAbortPathNet i n.
intros U U0 LT U1 U2.
dependent induction U1.
left. eapply incoming_ent_net. eapply input_incomingEnt.
apply H1. assumption.
dependent destruction U. false. eapply Rlt_not_le. apply LT. simpl. apply Rle_refl.
assert (inPosNet l i n) as IP. inposdp.
assert ({| time := zeroNonneg |} = zeroTime) as TZ. reflexivity.
lets IHdisc : IHU1 U IP TZ U2. clear IHU1.
elim_intro IHdisc IN MA.
assert (nextModeNet m i n) as NM. eapply nextSince_next. apply U.
lets II : incomp_incomingNet_abort w IP NM IN U2. apply II.
lets MN : msgAbort_not_nextSince p MA w. elim_intro MN MP NS.
right. assumption.
false.
false. eapply Rle_not_lt. apply Req_le. apply x. eapply Rplus_lt_weaken_rl.
timeNonneg. delPos. Qed.
lets LPT : link_par_triple_discW_3 H2. elim_intro LPT EQP EXP.
left. subst. econstructor;[ | apply U1].
eapply mapAbort. econstructor. eassumption.
ex_flat. lets CON : abortOvlp_next H4 H1. right.
assert (p3 <> p3') as PNE3. unfold not. intros. subst.
false. eapply listening_abort_contra; eassumption.
assert (p1 $||$ p2 $||$ p3 <> p1' $||$ p2' $||$ p3') as PNE.
unfold not. intro. inversion H5. subst. apply PNE3. reflexivity.
lets LEP : link_ent_proc_neq_disc PNE U3. andflat LEP.
or_flat; ex_flat; and_flat; try link_partripneq_tac;
try (lets CLT : abortOvlp_listening_track H1 CON AND1; inversion CLT); subst.
reach_net_prot_tac. link_partriptau_tac c v LPT;
try (lets CLT : abortOvlp_listening_track H1 CON LPT1;
inversion CLT; subst).
subst; contradict PNE3; reflexivity.
subst; contradict PNE3; reflexivity.
false. eapply bc_abort_in_not. apply LPT.
inversion RPT. assumption.
inversion RPT.
lets OAI : ovlp_abort_in_notNextSince LPT H9. unfold not. intro. apply OAI.
inversion H11. entnetuniq2 EN n'. subst. inversion H12. inversion H6.
assumption.
false. eapply inter_abort_in_not. eassumption.
false. eapply modeState_abort_in_not; eassumption.
lets CLT : abortOvlp_listening_track H1 CON AND; inversion CLT. Qed.
Theorem instant_incomp_abort (n : Network) (t : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
nextSince m t i n p -> inPosNet l i n -> 0 < t ->
received [baseMode m', basePosition l'] zeroTime i n p ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n \/
msgAbortPathNet i n.
intros U U0 LT U1 U2.
dependent induction U1.
left. eapply incoming_ent_net. eapply input_incomingEnt.
apply H1. assumption.
dependent destruction U. false. eapply Rlt_not_le. apply LT. simpl. apply Rle_refl.
assert (inPosNet l i n) as IP. inposdp.
assert ({| time := zeroNonneg |} = zeroTime) as TZ. reflexivity.
lets IHdisc : IHU1 U IP TZ U2. clear IHU1.
elim_intro IHdisc IN MA.
assert (nextModeNet m i n) as NM. eapply nextSince_next. apply U.
lets II : incomp_incomingNet_abort w IP NM IN U2. apply II.
lets MN : msgAbort_not_nextSince p MA w. elim_intro MN MP NS.
right. assumption.
false.
false. eapply Rle_not_lt. apply Req_le. apply x. eapply Rplus_lt_weaken_rl.
timeNonneg. delPos. Qed.
If a message was received some non-zero time t' ago and for longer than this time
we have been pending transition to a mode which threatens to be incompatible with
the received mode, given our current position & adjusting for time, the we get a
contradiction.
Theorem incomp_abort (n : Network) (t t' : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
nextSince m t i n p -> inPosNet l i n ->
received [baseMode m', basePosition l'] t' i n p -> zeroTime < t' -> t' < t ->
dist2d l l' -nn- speedMax *nn* msgLatency + speedMax*t' < possIncDist m m' ->
False.
intros U0 U1 U2 U3 U4 U5.
assert (0 < t). eapply Rle_lt_trans;[ |apply U4]. timeNonneg.
generalize dependent t. generalize dependent l.
dependent induction U2; intros l0 Y0 Y1 u U4 W0 W1.
contradict U3. apply Rlt_irrefl.
dependent destruction U4. eapply Rlt_irrefl. eapply Rlt_trans. apply U3.
assumption. assert (inPosNet l0 i n) as IP. inposdp.
eapply IHU2; try assumption. apply IP. assumption. apply U4. assumption. assumption.
dependent destruction U4. lets IPX : inPos_del_bound_bkwd Y0 w.
decompEx2 IPX l IP DI.
assert (t < t0) as TT. simpl in W0. Rplus_lt_tac.
assert (0 < t0) as TG. eapply Rle_lt_trans;[ |apply TT]. timeNonneg.
assert (zeroTime <= t) as TZ. timeNonneg. apply Rle_lt_or_eq_dec in TZ.
elim_intro TZ TZ1 TZ2.
eapply IHU2; try assumption. apply IP.
eapply Rle_lt_trans;[ | apply Y1].
lets DT : dist_tri_ineq l l0 l'.
simpl. rewrite Rmult_plus_distr_l. Rplus3_swap_2_3_free.
apply Rplus_le_compat; [ | apply Rle_refl].
eapply Rle_trans. eapply Rle_subNonnegTot_r.
rewrite <- addNonnegFact in DT. apply DT. rewrite Rplus_comm.
eapply Rle_trans. apply addNonneg_subNonnegTot_le_assoc.
rewrite addNonnegFact. Rplus_le_tac.
eassumption. assumption. assumption.
apply timeEqR in TZ2. rewrite <- TZ2 in U2.
assert (dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m') as DP.
eapply Rle_lt_trans;[ | apply Y1]. lets DT : dist_tri_ineq l l0 l'.
simpl. rewrite Rmult_plus_distr_l. Rplus3_swap_2_3_free.
apply Rplus_le_weaken_rr. apply Rmult_le_0_compat; apply cond_nonneg.
eapply Rle_trans. eapply Rle_subNonnegTot_r.
rewrite <- addNonnegFact in DT. apply DT. rewrite Rplus_comm.
eapply Rle_trans. apply addNonneg_subNonnegTot_le_assoc.
rewrite addNonnegFact. Rplus_le_tac.
lets IC : instant_incomp_abort U4 IP TG U2 DP.
elim_intro IC IN MA. eapply incomingNet_urgent. apply p. apply IN. apply w.
eapply msgAbortPathNet_urgent. eassumption. apply MA. apply w. Qed.
Theorem instant_incomp_tfs (n : Network) (t : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n -> 0 < t ->
received [baseMode m', basePosition l'] zeroTime i n p ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n \/
msgBadPathNet i n \/ tfs m zeroTime i n p.
intros H H0 U. intros.
dependent induction H1.
left. eapply incoming_ent_net. eapply input_incomingEnt. apply H3. assumption.
assert (inPosNet l i n) as Z. eapply inPos_pres_disc. apply w. assumption.
dependent destruction H.
invertClearAs3 H0 e F1 F2. invertClearAs3 H1 e' F3 F4.
lets K : switchCurr_switchListen_net_link F1 F3 F2 F4 w.
invertClearAs2 K K1 K2.
lets II : instant_incomp_abort H Z U H3 H4.
elim_intro II IN MA. left.
apply incoming_net_ent in IN. invertClearAs2 IN e0 IN2. invertClearAs2 IN2 IE X.
invertClear IE. destruct e' as [P' l0' h' K']. eapply incoming_ent_net.
constructor. apply H0. my_applys_eq F4. f_equal; try reflexivity.
simpl in K2. rewrite <- K2. replace e with e0. rewrite <- H1. reflexivity.
eapply entInNetUnique. apply X. assumption.
assert (switchStateNet i n) as SS. econstructor. apply switchCurr_switch_ent.
apply F1. assumption. rewrite <- (paused_switch_net n i p) in SS.
false. eapply msgAbort_paused_disj_net. apply MA. assumption.
assert ({| time := zeroNonneg |} = zeroTime) as V. reflexivity.
lets IH : IHreceived H Z V H3. clear IHreceived.
assert (currModeNet m i n) as J. eapply currSince_curr. apply H.
decompose [or] IH; clear IH.
lets IIB : incomp_incomingNet_bad w Z J H4 H3. elim_intro IIB IB1 IB2.
left. assumption. right. left. assumption.
lets MD : msgBad_disc_net p w H5 J. elim_intro MD MD1 MD2. right. left. assumption.
right. right. apply MD2.
right. right. apply tfs_zero_disc_pres. assumption.
assert (0 < t0 + d) as Q. apply Rplus_lt_weaken_rl. timeNonneg.
delPos. rewrite <- x in Q. false. eapply Rlt_irrefl. apply Q. Qed.
Theorem incomp_tfs (n : Network) (t t' : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n ->
received [baseMode m', basePosition l'] t' i n p ->
zeroTime < t' -> t' < t ->
dist2d l l' -nn- speedMax*nn*msgLatency + speedMax*t' < possIncDist m m' ->
tfs m t' i n p. intros.
assert (speedMax * t' < possIncDist m m') as TLP. eapply Rle_lt_trans;
[ | apply H4]. Rplus_le_tac. apply cond_nonneg.
generalize dependent t. generalize dependent l.
induction H1; intros; rename t into t'.
contradict H2. apply Rlt_irrefl.
assert (inPosNet l i n). erewrite inPos_pres_disc. apply H0. apply w.
dependent destruction H. apply False_ind. eapply incomp_abort. apply H.
apply H7. apply H1. assumption. assumption. assumption.
addHyp (IHreceived H2 TLP l H6 H4 t H H5). clear IHreceived.
constructor. assumption. apply tfs_rel_state in H7. addHyp (tfsStateNet_dec i n').
appDisj H8. apply False_ind. eapply tfsState_not_currSince. apply w.
apply H7. assumption. apply H.
dependent destruction H.
assert (0 <= t'). timeNonneg. apply Rle_lt_or_eq_dec in H5.
invertClear H5.
addHyp (inPos_del_bound_bkwd n n' d l i H0 w). decompose [ex] H5. clear H5.
rename x into l1. invertClear H7.
addHyp (dist_tri_ineq l1 l l').
apply subNonnegTot_plus_lt_Rminus in H4.
addHyp (Rplus_le_lt_compat (dist2d l1 l) (speedMax * d)
(dist2d l l' - speedMax * msgLatency + speedMax * (t' +dt+ d))
(possIncDist m m') H8 H4).
replace (nonneg (dist2d l1 l) +
(nonneg (dist2d l l') - nonneg speedMax * nonneg (time msgLatency) +
nonneg speedMax * pos (delay (t' +dt+ d)))) with (nonneg (dist2d l1 l) +
nonneg (dist2d l l') - nonneg speedMax * nonneg (time msgLatency) +
nonneg speedMax * (nonneg t') + nonneg speedMax * pos(delay d)) in H9;
[ |simpl;ring]. replace (nonneg speedMax * pos (delay d) + possIncDist m m')
with (possIncDist m m' + nonneg speedMax * pos (delay d)) in H9;[ |ring].
apply Rplus_lt_reg_r in H9.
apply (Rplus_le_compat_r (-speedMax*msgLatency + speedMax*t')) in H7.
assert (nonneg (dist2d l1 l') - nonneg speedMax * nonneg (time msgLatency) +
nonneg speedMax * nonneg (time t') < possIncDist m m'). eapply Rle_lt_trans.
eapply Rle_trans;[ | apply H7]. apply Req_le. ring.
eapply Rle_lt_trans;[ | apply H9]. apply Req_le. ring.
constructor. apply IHreceived with (t := t) (l := l1); try assumption.
eapply Rplus_lt_reg_l. eapply Rlt_le_trans. my_applys_eq TLP.
simpl. rewrite Rmult_plus_distr_l.
Admitted.
(m m' : Mode) (p : reachableNet n) :
nextSince m t i n p -> inPosNet l i n ->
received [baseMode m', basePosition l'] t' i n p -> zeroTime < t' -> t' < t ->
dist2d l l' -nn- speedMax *nn* msgLatency + speedMax*t' < possIncDist m m' ->
False.
intros U0 U1 U2 U3 U4 U5.
assert (0 < t). eapply Rle_lt_trans;[ |apply U4]. timeNonneg.
generalize dependent t. generalize dependent l.
dependent induction U2; intros l0 Y0 Y1 u U4 W0 W1.
contradict U3. apply Rlt_irrefl.
dependent destruction U4. eapply Rlt_irrefl. eapply Rlt_trans. apply U3.
assumption. assert (inPosNet l0 i n) as IP. inposdp.
eapply IHU2; try assumption. apply IP. assumption. apply U4. assumption. assumption.
dependent destruction U4. lets IPX : inPos_del_bound_bkwd Y0 w.
decompEx2 IPX l IP DI.
assert (t < t0) as TT. simpl in W0. Rplus_lt_tac.
assert (0 < t0) as TG. eapply Rle_lt_trans;[ |apply TT]. timeNonneg.
assert (zeroTime <= t) as TZ. timeNonneg. apply Rle_lt_or_eq_dec in TZ.
elim_intro TZ TZ1 TZ2.
eapply IHU2; try assumption. apply IP.
eapply Rle_lt_trans;[ | apply Y1].
lets DT : dist_tri_ineq l l0 l'.
simpl. rewrite Rmult_plus_distr_l. Rplus3_swap_2_3_free.
apply Rplus_le_compat; [ | apply Rle_refl].
eapply Rle_trans. eapply Rle_subNonnegTot_r.
rewrite <- addNonnegFact in DT. apply DT. rewrite Rplus_comm.
eapply Rle_trans. apply addNonneg_subNonnegTot_le_assoc.
rewrite addNonnegFact. Rplus_le_tac.
eassumption. assumption. assumption.
apply timeEqR in TZ2. rewrite <- TZ2 in U2.
assert (dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m') as DP.
eapply Rle_lt_trans;[ | apply Y1]. lets DT : dist_tri_ineq l l0 l'.
simpl. rewrite Rmult_plus_distr_l. Rplus3_swap_2_3_free.
apply Rplus_le_weaken_rr. apply Rmult_le_0_compat; apply cond_nonneg.
eapply Rle_trans. eapply Rle_subNonnegTot_r.
rewrite <- addNonnegFact in DT. apply DT. rewrite Rplus_comm.
eapply Rle_trans. apply addNonneg_subNonnegTot_le_assoc.
rewrite addNonnegFact. Rplus_le_tac.
lets IC : instant_incomp_abort U4 IP TG U2 DP.
elim_intro IC IN MA. eapply incomingNet_urgent. apply p. apply IN. apply w.
eapply msgAbortPathNet_urgent. eassumption. apply MA. apply w. Qed.
Theorem instant_incomp_tfs (n : Network) (t : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n -> 0 < t ->
received [baseMode m', basePosition l'] zeroTime i n p ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n \/
msgBadPathNet i n \/ tfs m zeroTime i n p.
intros H H0 U. intros.
dependent induction H1.
left. eapply incoming_ent_net. eapply input_incomingEnt. apply H3. assumption.
assert (inPosNet l i n) as Z. eapply inPos_pres_disc. apply w. assumption.
dependent destruction H.
invertClearAs3 H0 e F1 F2. invertClearAs3 H1 e' F3 F4.
lets K : switchCurr_switchListen_net_link F1 F3 F2 F4 w.
invertClearAs2 K K1 K2.
lets II : instant_incomp_abort H Z U H3 H4.
elim_intro II IN MA. left.
apply incoming_net_ent in IN. invertClearAs2 IN e0 IN2. invertClearAs2 IN2 IE X.
invertClear IE. destruct e' as [P' l0' h' K']. eapply incoming_ent_net.
constructor. apply H0. my_applys_eq F4. f_equal; try reflexivity.
simpl in K2. rewrite <- K2. replace e with e0. rewrite <- H1. reflexivity.
eapply entInNetUnique. apply X. assumption.
assert (switchStateNet i n) as SS. econstructor. apply switchCurr_switch_ent.
apply F1. assumption. rewrite <- (paused_switch_net n i p) in SS.
false. eapply msgAbort_paused_disj_net. apply MA. assumption.
assert ({| time := zeroNonneg |} = zeroTime) as V. reflexivity.
lets IH : IHreceived H Z V H3. clear IHreceived.
assert (currModeNet m i n) as J. eapply currSince_curr. apply H.
decompose [or] IH; clear IH.
lets IIB : incomp_incomingNet_bad w Z J H4 H3. elim_intro IIB IB1 IB2.
left. assumption. right. left. assumption.
lets MD : msgBad_disc_net p w H5 J. elim_intro MD MD1 MD2. right. left. assumption.
right. right. apply MD2.
right. right. apply tfs_zero_disc_pres. assumption.
assert (0 < t0 + d) as Q. apply Rplus_lt_weaken_rl. timeNonneg.
delPos. rewrite <- x in Q. false. eapply Rlt_irrefl. apply Q. Qed.
Theorem incomp_tfs (n : Network) (t t' : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n ->
received [baseMode m', basePosition l'] t' i n p ->
zeroTime < t' -> t' < t ->
dist2d l l' -nn- speedMax*nn*msgLatency + speedMax*t' < possIncDist m m' ->
tfs m t' i n p. intros.
assert (speedMax * t' < possIncDist m m') as TLP. eapply Rle_lt_trans;
[ | apply H4]. Rplus_le_tac. apply cond_nonneg.
generalize dependent t. generalize dependent l.
induction H1; intros; rename t into t'.
contradict H2. apply Rlt_irrefl.
assert (inPosNet l i n). erewrite inPos_pres_disc. apply H0. apply w.
dependent destruction H. apply False_ind. eapply incomp_abort. apply H.
apply H7. apply H1. assumption. assumption. assumption.
addHyp (IHreceived H2 TLP l H6 H4 t H H5). clear IHreceived.
constructor. assumption. apply tfs_rel_state in H7. addHyp (tfsStateNet_dec i n').
appDisj H8. apply False_ind. eapply tfsState_not_currSince. apply w.
apply H7. assumption. apply H.
dependent destruction H.
assert (0 <= t'). timeNonneg. apply Rle_lt_or_eq_dec in H5.
invertClear H5.
addHyp (inPos_del_bound_bkwd n n' d l i H0 w). decompose [ex] H5. clear H5.
rename x into l1. invertClear H7.
addHyp (dist_tri_ineq l1 l l').
apply subNonnegTot_plus_lt_Rminus in H4.
addHyp (Rplus_le_lt_compat (dist2d l1 l) (speedMax * d)
(dist2d l l' - speedMax * msgLatency + speedMax * (t' +dt+ d))
(possIncDist m m') H8 H4).
replace (nonneg (dist2d l1 l) +
(nonneg (dist2d l l') - nonneg speedMax * nonneg (time msgLatency) +
nonneg speedMax * pos (delay (t' +dt+ d)))) with (nonneg (dist2d l1 l) +
nonneg (dist2d l l') - nonneg speedMax * nonneg (time msgLatency) +
nonneg speedMax * (nonneg t') + nonneg speedMax * pos(delay d)) in H9;
[ |simpl;ring]. replace (nonneg speedMax * pos (delay d) + possIncDist m m')
with (possIncDist m m' + nonneg speedMax * pos (delay d)) in H9;[ |ring].
apply Rplus_lt_reg_r in H9.
apply (Rplus_le_compat_r (-speedMax*msgLatency + speedMax*t')) in H7.
assert (nonneg (dist2d l1 l') - nonneg speedMax * nonneg (time msgLatency) +
nonneg speedMax * nonneg (time t') < possIncDist m m'). eapply Rle_lt_trans.
eapply Rle_trans;[ | apply H7]. apply Req_le. ring.
eapply Rle_lt_trans;[ | apply H9]. apply Req_le. ring.
constructor. apply IHreceived with (t := t) (l := l1); try assumption.
eapply Rplus_lt_reg_l. eapply Rlt_le_trans. my_applys_eq TLP.
simpl. rewrite Rmult_plus_distr_l.
Admitted.
This page has been generated by coqdoc