Library NARTop
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 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.NetworkLanguage.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.NARInsuff.
Require Import ComhCoq.NARMisc.
Require Import ComhCoq.NARMsgPosition.
Require Import ComhCoq.NAROvlpTime.
Theorem currSince_lower_bound (n : Network) (t : Time) (m : Mode)
(i : nat) (p : reachableNet n) : currSince m t i n p ->
msgLatency + Rmax adaptNotif transMax < t.
intros. induction H.
apply (nextSince_switchCurr_lower n m i t p H H0).
assumption. apply Rplus_lt_weaken_rr. apply Rlt_le. delPos.
assumption. Qed.
Lemma maxAnTrans_positive : 0 <= Rmax adaptNotif transMax.
eapply Rle_trans;[ |apply Rmax_l]. timeNonneg. Qed.
Theorem nextSince_fst_deliv_suff (n : Network) (t : Time) (m : Mode)
(i : nat) (l : Position) (p : reachableNet n) :
nextSince m t i n p -> inPosNet l i n ->
forall q : msgLatency + Rmax adaptNotif transMax < t,
let s := (Rplus_lt_weaken_lr msgLatency (Rmax adaptNotif transMax)
t q maxAnTrans_positive) in
let s' := Rlt_le msgLatency t s in
exists l0 l1 r,
delivered ([-[baseMode m, basePosition l0], l1, r-]) (minusTime t msgLatency s') i n p /\
sufficient m r /\ dist2d l l0 <= speedMax*t.
intros U0 U1 q. simpl.
assert (msgLatency < t) as MT. eapply Rplus_lt_weaken_lr. apply q.
apply maxAnTrans_positive. lets FX : fst_delivered U0 U1 MT. decompEx3 FX l0 l1 r FD.
decompAnd2 FD DE DI.
exists l0 l1 r. splits;[my_applys_eq DE | | apply DI]. timering.
assert (adaptNotif < t - msgLatency) as AT. apply Rplus_lt_swap_ll in q.
eapply Rle_lt_trans;[ |apply q]. apply Rmax_l.
assert (t - msgLatency < t). apply Rplus_lt_swap_rr. Rplus_lt_tac.
apply msgLatency_positive.
eapply deliv_next_suff. apply U0. apply DE. simpl. assumption. apply H.
Qed.
Lemma ovWait_del_pres_bkwd_net_strong n n' d m t x y i :
n -ND- d -ND> n' -> ovWaitStateNet m t x y i n' ->
ovWaitStateNet m t (x +dt+ d) (y +dt+ d) i n. Admitted.
Lemma init_ovWait_track_net m m' t' i x y n n' a :
initStateNet m i n -> ovWaitStateNet m' t' x y i n' ->
n -NA- a -NA> n' -> m = m' /\ x = t' /\ y = zeroTime.
Admitted.
Theorem ovWait_sent (n : Network) (m : Mode) (t x y : Time) (i : nat) (p : reachableNet n) :
ovWaitStateNet m t x y i n -> 0 < y ->
exists l q,
sent [baseMode m, basePosition l] (minusTime (period m) y q) i n p.
introz U. genDep2 x y. induction p; intros y U0 x U.
Admitted.
Theorem nextSince_periodic_sent (n : Network) (m : Mode) (t t' : Time)
(i : nat) (p : reachableNet n) :
nextSince m t i n p -> t' < t ->
exists t'' l,
t' < (time t'') <= t' + period m /\ t'' <= t /\
sent [baseMode m, basePosition l] t'' i n p.
intros. gen t'.
induction H; intros.
contradict H2. apply Rle_not_lt. simpl. timeNonneg.
lets IH : IHnextSince H1. clear IHnextSince. decompEx2 IH t'' l W.
andflat Y. exists t'' l. splits; try assumption. split; assumption.
constructor. assumption.
lets NR : nextSince_rel_state H.
lets ND : nextSince_del_ovWait w NR. decompEx4 ND m0 t0 x y OS. assert (m0 = m) as ME.
eapply nextSince_ovWait_modes_eq. apply OS. apply H.
lets RO : Rle_or_lt d t'. elim_intro RO DT TD.
assert (exists t'', nonneg t' = (time t'') + d) as TX. apply RlePlusExistsR in DT.
invertClearAs2 DT dt TE. decompAnd2 TE TP TL. rewrite Rplus_comm in TP.
exists (mkTime (mknonnegreal dt TL)). apply TP. invertClearAs2 TX t'' TE.
assert (t'' < t) as TL. rewrite TE in H0. simpl in H0. Rplus_lt_tac.
apply IHnextSince in TL. clear IHnextSince. decompEx2 TL u l TA.
andflat T.
exists (u +dt+ d) l.
splits. rewrite TE. simpl.
split. Rplus_lt_tac. Rplus3_swap_2_3 t'' d (period m). Rplus_le_tac. simpl. Rplus_le_tac.
constructor. assumption.
assert (zeroTime < (delToTime (y +dt+ d))) as YD. simpl. replace 0 with (0 + 0).
apply Rplus_le_lt_compat. timeNonneg. delPos. ring.
lets SX : ovWait_sent p OS YD. decompEx2 SX l q SE.
assert (y <= period m0) as YL. simpl in q. eapply Rplus_le_weaken_lr.
apply q. apply Rlt_le. delPos.
exists (minusTime (period m0) y YL) l. simpl in q, YD. simpl. splits.
split. simpl. eapply Rlt_le_trans. apply TD. Rplus_le_tac.
simpl. rewrite Rplus_comm. rewrite ME.
Rminus_plus_zero (period m) y. Rplus_le_tac. apply Rplus_le_swap_rr.
replace 0 with (0 + 0). apply Rplus_le_compat; timeNonneg. ring.
rewrite <- ME in H. lets ON : ovWait_nextSince_time OS H. simpl in ON.
apply Rminus_le_swap_lr. my_applys_eq ON. ring. generalize dependent YL.
rewrite <- ME. intro YL. lets SD : sentDel p w SE. my_applys_eq SD.
timering. Qed.
Theorem tfsBc_not_currSince (n : Network) (m : Mode) (t : Time)
(i : nat) (p : reachableNet n) :
tfsBcStateNet i n -> currSince m t i n p -> False. Admitted.
Theorem currSince_bc_state (n : Network) (m : Mode) (t : Time)
(i : nat) (p : reachableNet n) : currSince m t i n p ->
(exists x, bcWaitStateNet m x i n) \/
(exists l, bcReadyStateNet m l i n). Admitted.
If we're currSince & we can delay, then we're in the bcWait state.
Corollary currSince_del_bcWait (n n' : Network) (m : Mode) (t : Time)
(i : nat) (d : Delay) (p : reachableNet n) :
n -ND- d -ND> n' -> currSince m t i n p ->
exists x, bcWaitStateNet m (delToTime (x +dt+ d)) i n. Admitted.
Theorem bcWait_currSince_time (n : Network) (m : Mode) (x t: Time)
(i : nat) (p : reachableNet n) :
bcWaitStateNet m x i n -> currSince m t i n p -> period m - x <= t.
Admitted.
Theorem bcWait_sent (n : Network) (m : Mode) (x : Time)
(i : nat) (p : reachableNet n) :
bcWaitStateNet m x i n -> zeroTime < x ->
exists l q,
sent [baseMode m, basePosition l] (minusTime (period m) x q) i n p.
intros. gen x.
induction p; intros.
false. eapply initial_not_bcWait_net. apply i0. apply H.
assert (x <> zeroTime) as Q. unfold not. intro F. rewrite F in H0.
contradiction (Rlt_irrefl zeroTime).
lets BB : bcWait_bktrk_net p H s. decompOr3 BB W1 W2 W3.
apply IHp in W1. decompEx2 W1 l q V. exists l q. constructor. assumption.
assumption. andflat Y. contradiction Q. invertClearAs2 W3 l L.
andflat Y. rewrite <- Y1. exists l (Rle_refl x). constructor. my_applys_eq Y2.
timering.
lets BD : bcWaitNet_del_bkwd s H. assert (zeroTime < x +dt+ d) as ZL.
apply Rplus_lt_weaken_rl. timeNonneg. simpl.
delPos. lets IH : IHp BD ZL. decompEx2 IH l q SE. assert (x <= period m) as q0.
simpl in q. eapply Rplus_le_weaken_lr. apply q. apply Rlt_le. delPos. exists l q0.
eapply sentDel in SE. my_applys_eq SE. timering. Qed.
Theorem currSince_periodic_sent (n : Network) (m : Mode) (t t' : Time)
(i : nat) (p : reachableNet n) :
currSince m t i n p -> t' < t ->
exists t'' l, t' < (time t'') /\ t'' <= t' + period m /\ t'' <= t /\
sent [baseMode m, basePosition l] t'' i n p.
intros. generalize dependent t'. induction H; intros.
addHyp (nextSince_periodic_sent n m t t' i p H H2). decompose [ex] H3.
rename x into t''. rename x0 into l. exists t''. exists l. decompose [and] H5.
clear H5. repeat (split; try assumption). constructor. assumption.
apply IHcurrSince in H1. decompose [ex] H1. clear H1. decompose [and] H3.
clear H3. rename x into t''. rename x0 into l. exists t''. exists l.
clear IHcurrSince. repeat (split; try assumption). constructor. assumption.
addHyp (Rle_or_lt d t'). invertClear H1.
assert (exists t'', nonneg t' = (time t'') + d). apply RlePlusExistsR in H2.
invertClear H2. rename x into t''. invertClear H1. rewrite Rplus_comm in H2.
exists (mkTime (mknonnegreal t'' H3)). apply H2. invertClear H1. rename x into t''.
assert (t'' < t). rewrite H3 in H0. simpl in H0. eapply Rplus_lt_reg_r in H0.
assumption.
apply IHcurrSince in H1. clear IHcurrSince. decompose [ex] H1. clear H1.
rename x into u. rename x0 into l. decompose [and] H5. clear H5.
exists (u +dt+ d). exists l.
split. rewrite H3. apply Rplus_lt_compat_r. assumption. split. rewrite Rplus_comm.
rewrite H3. rewrite <- Rplus_assoc. apply Rplus_le_compat_r. rewrite Rplus_comm.
assumption. split. apply Rplus_le_compat_r. assumption.
constructor. assumption.
addHyp (currSince_del_bcWait n n' m t i d p w H). invertClear H1.
assert (zeroTime < (delToTime (x +dt+ d))). simpl. replace 0 with (0 + 0).
apply Rplus_le_lt_compat. timeNonneg. delPos. ring.
addHyp (bcWait_sent n m (x +dt+ d) i p H3 H1). decompose [ex] H4. clear H4.
rename x1 into Q. rename x0 into l.
assert (x <= period m). simpl in Q. eapply Rplus_le_weaken_lr. apply Q.
apply Rlt_le. delPos. exists (minusTime (period m) x H4). exists l. split.
eapply Rlt_le_trans. apply H2. simpl. simpl in Q. apply Rplus_le_swap_lr.
rewrite Rplus_comm. assumption. split.
simpl. rewrite Rplus_comm.
apply Rminus_le_weaken_lr. timeNonneg. apply Rplus_le_weaken_rr. timeNonneg.
apply Rle_refl. split. simpl. addHyp (bcWait_currSince_time n m (x +dt+ d) t i p H3 H).
simpl in H5. apply Rminus_le_swap_lr. eapply Rle_trans;[ |apply H5].
apply Req_le. ring.
replace (minusTime (nonneg (time (period m))) (nonneg (time x)) H4)
with (delToTime (minusTime (nonneg (time (period m)))
(nonneg (time (delToTime (x +dt+ d)))) Q +dt+ d)).
constructor. assumption. apply timeEqR. simpl. ring. Qed.
Theorem currSince_fst_deliv_suff (n : Network) (m : Mode) (t : Time)
(i : nat) (l : Position) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n ->
exists q,
let s := (Rplus_lt_weaken_lr msgLatency (Rmax adaptNotif transMax) t q
maxAnTrans_positive) in
let s' := Rlt_le msgLatency t s in
exists r l0 l1,
delivered ([-[baseMode m, basePosition l0], l1, r-]) (minusTime t msgLatency s') i n p /\
sufficient m r /\ dist2d l l0 <= speedMax*t.
intro. generalize dependent l. induction H; intros.
addHyp (nextSince_switchCurr_lower n m i t p H H0).
assert (msgLatency + adaptNotif < t). eapply Rle_lt_trans;[ |apply H3].
apply Rplus_le_compat. apply Rle_refl. apply Rmax_l.
addHyp (inPos_pres_disc n n' a l i w). rewrite <- H5 in H2.
addHyp (nextSince_fst_deliv_suff n t m i l p H H2 H3). cbv zeta in H6.
decompose [ex] H6. clear H6. rename x into l0. rename x0 into l1. rename x1 into r.
decompose [and] H7. clear H7. exists H3. exists r. exists l0. exists l1.
repeat (split; try assumption).
constructor. assumption.
addHyp (inPos_pres_disc n n' a l i w). rewrite <- H2 in H1.
apply IHcurrSince in H1. clear IHcurrSince. cbv zeta in H1.
decompose [ex] H1. clear H1. rename x into q. rename x0 into r. rename x1 into l0.
rename x2 into l1. decompose [and] H4. clear H4. exists q. exists r. exists l0. exists l1.
repeat (split; try assumption). constructor. assumption.
addHyp (inPos_del_bound_bkwd n n' d l i H0 w). invertClear H1. rename x into l0.
invertClear H2.
apply IHcurrSince in H1. clear IHcurrSince. cbv zeta in H1. decompose [ex] H1.
clear H1. rename x0 into r. rename x1 into l1. rename x2 into l2.
decompose [and] H4. clear H4.
assert (msgLatency + Rmax adaptNotif transMax < t +dt+ d) as q. apply Rplus_lt_weaken_rr.
apply Rlt_le. delPos. assumption.
exists q. exists r. exists l1. exists l2. split.
replace (minusTime (nonneg (time (delToTime (t +dt+ d)))) (nonneg (time msgLatency))
(Rlt_le (nonneg (time msgLatency)) (nonneg (time (delToTime (t +dt+ d))))
(Rplus_lt_weaken_lr (nonneg (time msgLatency))
(Rmax (nonneg (time adaptNotif)) (nonneg (time transMax)))
(nonneg (time (delToTime (t +dt+ d)))) q maxAnTrans_positive))) with
(delToTime (minusTime (nonneg (time t)) (nonneg (time msgLatency))
(Rlt_le (nonneg (time msgLatency)) (nonneg (time t))
(Rplus_lt_weaken_lr (nonneg (time msgLatency))
(Rmax (nonneg (time adaptNotif)) (nonneg (time transMax)))
(nonneg (time t)) x maxAnTrans_positive)) +dt+ d)). constructor. assumption. apply timeEqR. simpl. ring.
split. assumption.
eapply Rle_trans. eapply dist_tri_ineq. simpl. rewrite Rmult_plus_distr_l.
rewrite Rplus_comm. apply Rplus_le_compat. apply H6. rewrite distSymmetric in H3.
apply H3. Qed.
Theorem pre_del_suff (n : Network) (m : Mode) (t : Time)
(i : nat) (l : Position) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n -> ~failSafe m ->
exists t' r l0 l1,
delivered ([-[baseMode m, basePosition l0], l1, r-]) t' i n p /\
sufficient m r /\ t' [:] (preDeliveredInterval m) /\ t' < t /\
dist2d l l0 <= speedMax*(msgLatency+ t'). intros.
match goal with [ H : ~failSafe m |- _ ] => rename H into Q end.
remember (preDeliveredInterval m) as h. unfold preDeliveredInterval in Heqh.
remember (msgLatency + Rmax adaptNotif transMax + period m + trans m) as u.
addHyp (Rle_or_le t u). invertClear H1.
addHyp (currSince_fst_deliv_suff n m t i l p H H0). simpl in H1. decompose [ex] H1.
clear H1. decompose [and] H4. clear H4. rename x0 into r. rename x1 into l0.
rename x2 into l1. remember (minusTime t msgLatency (Rlt_le msgLatency t
(Rplus_lt_weaken_lr msgLatency (Rmax adaptNotif transMax) t x maxAnTrans_positive)))
as t'.
foldDist l l0 H6. assert (nonneg t = t' + msgLatency). rewrite Heqt'. simpl. ring.
rewrite H3 in H6. rewrite Rplus_comm in H6.
assert (t' < t). rewrite H3. apply Rlt_plus_r.
apply msgLatency_positive.
exists t' r l0 l1. split. assumption. split. assumption. split;[ |split;assumption].
rewrite Heqh. replace (nonneg (time t')) with (nonneg (time t') +
nonneg (time msgLatency) - nonneg (time msgLatency));[ | ring]. split.
addHyp (currSince_lower_bound n t m i p H). apply Rplus_lt_swap_ll in H7.
rewrite H3 in H7. simpl. assumption.
simpl. rewrite Hequ in H2. rewrite Rplus_assoc in H2. rewrite Rplus_assoc in H2.
apply Rplus_le_swap_rl in H2. rewrite H3 in H2. rewrite Rplus_assoc. assumption.
assert (nonneg (time msgLatency) +
Rmax (nonneg (time adaptNotif)) (nonneg (time transMax)) + nonneg (time (trans m)) < t).
eapply Rlt_le_trans;[ |apply H2]. rewrite Hequ. apply Rplus_lt_compat_r.
rewrite Rplus_assoc. repeat (apply Rplus_lt_compat_l). apply Rlt_plus_r.
apply period_positive.
remember (msgLatency +t+ (timeMax adaptNotif transMax) +t+ trans m) as w.
assert (nonneg (time msgLatency) + Rmax (nonneg (time adaptNotif))
(nonneg (time transMax)) + nonneg (time (trans m)) =
nonneg ((msgLatency +t+ timeMax adaptNotif transMax) +t+ trans m)). simpl.
ring. rewrite H3 in H1. rewrite <- Heqw in H1.
addHyp (currSince_periodic_sent n m t w i p H H1). decompose [ex] H4.
clear H4. decompose [and] H6. clear H6. rename x0 into l0. rename x into t'.
assert (t' <= u). rewrite Hequ. eapply Rle_trans. apply H7. rewrite Heqw.
rewrite <- H3. rewrite Rplus_assoc. rewrite Rplus_comm. rewrite Rplus_assoc.
rewrite Rplus_comm. apply Rplus_le_compat_r. rewrite Rplus_comm. apply Rle_refl.
rewrite Hequ in H6.
addHyp (sent_pos_bound n m t' i l l0 p H9 H0).
assert (msgLatency < t'). eapply Rle_lt_trans;[ |apply H4]. rewrite Heqw.
rewrite <- H3. rewrite Rplus_assoc. apply Rle_plus_r. apply Rle_zero_plus.
rewrite <- timeMax_RMax. timeNonneg.
timeNonneg.
addHyp (sent_delivered n [baseMode m, basePosition l0] t' i p H9 H10).
decompose [ex] H11. clear H11. rename x0 into l1. rename x into r.
remember (minusTime (nonneg (time t')) (nonneg (time msgLatency))
(Rlt_le (nonneg (time msgLatency)) (nonneg (time t')) H10)) as t''.
assert ((Rmax adaptNotif transMax) + trans m < t'').
rewrite Heqt''. simpl. apply Rplus_lt_swap_ll. rewrite <- Rplus_assoc.
rewrite H3. rewrite <- Heqw. assumption.
assert (t'' <= (Rmax adaptNotif transMax) + period m + trans m).
rewrite Heqt''. simpl. apply Rplus_le_swap_rl. repeat rewrite <- Rplus_assoc.
assumption.
assert (t'' [:] preDeliveredInterval m). split;simpl.
eapply Rle_lt_trans;[ | apply H11]. apply Rle_plus_r. timeNonneg.
assumption.
assert (t'' < t). rewrite Heqt''. simpl. eapply Rlt_le_trans;[ |apply H5].
apply Rplus_lt_swap_rr. apply Rlt_plus_r. apply msgLatency_positive.
assert (nonneg t' = msgLatency + t''). rewrite Heqt''. simpl. ring.
rewrite H16 in H8.
exists t'' r l0 l1. rewrite Heqh. repeat (split;try assumption).
addHyp (suffDec m r). appDisj H17. assumption.
assert (adaptNotif < t''). eapply Rle_lt_trans;[ |apply H11].
apply Rplus_le_weaken_rr. timeNonneg. apply Rmax_l.
addHyp (insuff_react n m l0 l1 r t t'' i p H H13 H17 H15 n0 Q).
decompExAnd H18 x LT TF. lets TB : tfs_bound TF.
assert (minusTime t'' adaptNotif (Rlt_le adaptNotif t'' H17) <= trans m) as C1.
eapply Rle_trans. apply LT. assumption.
assert (adaptNotif + trans m < t''). eapply Rle_lt_trans;[ |apply H11].
apply Rplus_le_compat_r. apply Rmax_l.
simpl in C1. apply Rplus_lt_swap_ll in H18.
apply False_ind. apply (Rlt_irrefl (t'' - adaptNotif)). eapply Rle_lt_trans.
apply C1. assumption. Qed.
(i : nat) (d : Delay) (p : reachableNet n) :
n -ND- d -ND> n' -> currSince m t i n p ->
exists x, bcWaitStateNet m (delToTime (x +dt+ d)) i n. Admitted.
Theorem bcWait_currSince_time (n : Network) (m : Mode) (x t: Time)
(i : nat) (p : reachableNet n) :
bcWaitStateNet m x i n -> currSince m t i n p -> period m - x <= t.
Admitted.
Theorem bcWait_sent (n : Network) (m : Mode) (x : Time)
(i : nat) (p : reachableNet n) :
bcWaitStateNet m x i n -> zeroTime < x ->
exists l q,
sent [baseMode m, basePosition l] (minusTime (period m) x q) i n p.
intros. gen x.
induction p; intros.
false. eapply initial_not_bcWait_net. apply i0. apply H.
assert (x <> zeroTime) as Q. unfold not. intro F. rewrite F in H0.
contradiction (Rlt_irrefl zeroTime).
lets BB : bcWait_bktrk_net p H s. decompOr3 BB W1 W2 W3.
apply IHp in W1. decompEx2 W1 l q V. exists l q. constructor. assumption.
assumption. andflat Y. contradiction Q. invertClearAs2 W3 l L.
andflat Y. rewrite <- Y1. exists l (Rle_refl x). constructor. my_applys_eq Y2.
timering.
lets BD : bcWaitNet_del_bkwd s H. assert (zeroTime < x +dt+ d) as ZL.
apply Rplus_lt_weaken_rl. timeNonneg. simpl.
delPos. lets IH : IHp BD ZL. decompEx2 IH l q SE. assert (x <= period m) as q0.
simpl in q. eapply Rplus_le_weaken_lr. apply q. apply Rlt_le. delPos. exists l q0.
eapply sentDel in SE. my_applys_eq SE. timering. Qed.
Theorem currSince_periodic_sent (n : Network) (m : Mode) (t t' : Time)
(i : nat) (p : reachableNet n) :
currSince m t i n p -> t' < t ->
exists t'' l, t' < (time t'') /\ t'' <= t' + period m /\ t'' <= t /\
sent [baseMode m, basePosition l] t'' i n p.
intros. generalize dependent t'. induction H; intros.
addHyp (nextSince_periodic_sent n m t t' i p H H2). decompose [ex] H3.
rename x into t''. rename x0 into l. exists t''. exists l. decompose [and] H5.
clear H5. repeat (split; try assumption). constructor. assumption.
apply IHcurrSince in H1. decompose [ex] H1. clear H1. decompose [and] H3.
clear H3. rename x into t''. rename x0 into l. exists t''. exists l.
clear IHcurrSince. repeat (split; try assumption). constructor. assumption.
addHyp (Rle_or_lt d t'). invertClear H1.
assert (exists t'', nonneg t' = (time t'') + d). apply RlePlusExistsR in H2.
invertClear H2. rename x into t''. invertClear H1. rewrite Rplus_comm in H2.
exists (mkTime (mknonnegreal t'' H3)). apply H2. invertClear H1. rename x into t''.
assert (t'' < t). rewrite H3 in H0. simpl in H0. eapply Rplus_lt_reg_r in H0.
assumption.
apply IHcurrSince in H1. clear IHcurrSince. decompose [ex] H1. clear H1.
rename x into u. rename x0 into l. decompose [and] H5. clear H5.
exists (u +dt+ d). exists l.
split. rewrite H3. apply Rplus_lt_compat_r. assumption. split. rewrite Rplus_comm.
rewrite H3. rewrite <- Rplus_assoc. apply Rplus_le_compat_r. rewrite Rplus_comm.
assumption. split. apply Rplus_le_compat_r. assumption.
constructor. assumption.
addHyp (currSince_del_bcWait n n' m t i d p w H). invertClear H1.
assert (zeroTime < (delToTime (x +dt+ d))). simpl. replace 0 with (0 + 0).
apply Rplus_le_lt_compat. timeNonneg. delPos. ring.
addHyp (bcWait_sent n m (x +dt+ d) i p H3 H1). decompose [ex] H4. clear H4.
rename x1 into Q. rename x0 into l.
assert (x <= period m). simpl in Q. eapply Rplus_le_weaken_lr. apply Q.
apply Rlt_le. delPos. exists (minusTime (period m) x H4). exists l. split.
eapply Rlt_le_trans. apply H2. simpl. simpl in Q. apply Rplus_le_swap_lr.
rewrite Rplus_comm. assumption. split.
simpl. rewrite Rplus_comm.
apply Rminus_le_weaken_lr. timeNonneg. apply Rplus_le_weaken_rr. timeNonneg.
apply Rle_refl. split. simpl. addHyp (bcWait_currSince_time n m (x +dt+ d) t i p H3 H).
simpl in H5. apply Rminus_le_swap_lr. eapply Rle_trans;[ |apply H5].
apply Req_le. ring.
replace (minusTime (nonneg (time (period m))) (nonneg (time x)) H4)
with (delToTime (minusTime (nonneg (time (period m)))
(nonneg (time (delToTime (x +dt+ d)))) Q +dt+ d)).
constructor. assumption. apply timeEqR. simpl. ring. Qed.
Theorem currSince_fst_deliv_suff (n : Network) (m : Mode) (t : Time)
(i : nat) (l : Position) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n ->
exists q,
let s := (Rplus_lt_weaken_lr msgLatency (Rmax adaptNotif transMax) t q
maxAnTrans_positive) in
let s' := Rlt_le msgLatency t s in
exists r l0 l1,
delivered ([-[baseMode m, basePosition l0], l1, r-]) (minusTime t msgLatency s') i n p /\
sufficient m r /\ dist2d l l0 <= speedMax*t.
intro. generalize dependent l. induction H; intros.
addHyp (nextSince_switchCurr_lower n m i t p H H0).
assert (msgLatency + adaptNotif < t). eapply Rle_lt_trans;[ |apply H3].
apply Rplus_le_compat. apply Rle_refl. apply Rmax_l.
addHyp (inPos_pres_disc n n' a l i w). rewrite <- H5 in H2.
addHyp (nextSince_fst_deliv_suff n t m i l p H H2 H3). cbv zeta in H6.
decompose [ex] H6. clear H6. rename x into l0. rename x0 into l1. rename x1 into r.
decompose [and] H7. clear H7. exists H3. exists r. exists l0. exists l1.
repeat (split; try assumption).
constructor. assumption.
addHyp (inPos_pres_disc n n' a l i w). rewrite <- H2 in H1.
apply IHcurrSince in H1. clear IHcurrSince. cbv zeta in H1.
decompose [ex] H1. clear H1. rename x into q. rename x0 into r. rename x1 into l0.
rename x2 into l1. decompose [and] H4. clear H4. exists q. exists r. exists l0. exists l1.
repeat (split; try assumption). constructor. assumption.
addHyp (inPos_del_bound_bkwd n n' d l i H0 w). invertClear H1. rename x into l0.
invertClear H2.
apply IHcurrSince in H1. clear IHcurrSince. cbv zeta in H1. decompose [ex] H1.
clear H1. rename x0 into r. rename x1 into l1. rename x2 into l2.
decompose [and] H4. clear H4.
assert (msgLatency + Rmax adaptNotif transMax < t +dt+ d) as q. apply Rplus_lt_weaken_rr.
apply Rlt_le. delPos. assumption.
exists q. exists r. exists l1. exists l2. split.
replace (minusTime (nonneg (time (delToTime (t +dt+ d)))) (nonneg (time msgLatency))
(Rlt_le (nonneg (time msgLatency)) (nonneg (time (delToTime (t +dt+ d))))
(Rplus_lt_weaken_lr (nonneg (time msgLatency))
(Rmax (nonneg (time adaptNotif)) (nonneg (time transMax)))
(nonneg (time (delToTime (t +dt+ d)))) q maxAnTrans_positive))) with
(delToTime (minusTime (nonneg (time t)) (nonneg (time msgLatency))
(Rlt_le (nonneg (time msgLatency)) (nonneg (time t))
(Rplus_lt_weaken_lr (nonneg (time msgLatency))
(Rmax (nonneg (time adaptNotif)) (nonneg (time transMax)))
(nonneg (time t)) x maxAnTrans_positive)) +dt+ d)). constructor. assumption. apply timeEqR. simpl. ring.
split. assumption.
eapply Rle_trans. eapply dist_tri_ineq. simpl. rewrite Rmult_plus_distr_l.
rewrite Rplus_comm. apply Rplus_le_compat. apply H6. rewrite distSymmetric in H3.
apply H3. Qed.
Theorem pre_del_suff (n : Network) (m : Mode) (t : Time)
(i : nat) (l : Position) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n -> ~failSafe m ->
exists t' r l0 l1,
delivered ([-[baseMode m, basePosition l0], l1, r-]) t' i n p /\
sufficient m r /\ t' [:] (preDeliveredInterval m) /\ t' < t /\
dist2d l l0 <= speedMax*(msgLatency+ t'). intros.
match goal with [ H : ~failSafe m |- _ ] => rename H into Q end.
remember (preDeliveredInterval m) as h. unfold preDeliveredInterval in Heqh.
remember (msgLatency + Rmax adaptNotif transMax + period m + trans m) as u.
addHyp (Rle_or_le t u). invertClear H1.
addHyp (currSince_fst_deliv_suff n m t i l p H H0). simpl in H1. decompose [ex] H1.
clear H1. decompose [and] H4. clear H4. rename x0 into r. rename x1 into l0.
rename x2 into l1. remember (minusTime t msgLatency (Rlt_le msgLatency t
(Rplus_lt_weaken_lr msgLatency (Rmax adaptNotif transMax) t x maxAnTrans_positive)))
as t'.
foldDist l l0 H6. assert (nonneg t = t' + msgLatency). rewrite Heqt'. simpl. ring.
rewrite H3 in H6. rewrite Rplus_comm in H6.
assert (t' < t). rewrite H3. apply Rlt_plus_r.
apply msgLatency_positive.
exists t' r l0 l1. split. assumption. split. assumption. split;[ |split;assumption].
rewrite Heqh. replace (nonneg (time t')) with (nonneg (time t') +
nonneg (time msgLatency) - nonneg (time msgLatency));[ | ring]. split.
addHyp (currSince_lower_bound n t m i p H). apply Rplus_lt_swap_ll in H7.
rewrite H3 in H7. simpl. assumption.
simpl. rewrite Hequ in H2. rewrite Rplus_assoc in H2. rewrite Rplus_assoc in H2.
apply Rplus_le_swap_rl in H2. rewrite H3 in H2. rewrite Rplus_assoc. assumption.
assert (nonneg (time msgLatency) +
Rmax (nonneg (time adaptNotif)) (nonneg (time transMax)) + nonneg (time (trans m)) < t).
eapply Rlt_le_trans;[ |apply H2]. rewrite Hequ. apply Rplus_lt_compat_r.
rewrite Rplus_assoc. repeat (apply Rplus_lt_compat_l). apply Rlt_plus_r.
apply period_positive.
remember (msgLatency +t+ (timeMax adaptNotif transMax) +t+ trans m) as w.
assert (nonneg (time msgLatency) + Rmax (nonneg (time adaptNotif))
(nonneg (time transMax)) + nonneg (time (trans m)) =
nonneg ((msgLatency +t+ timeMax adaptNotif transMax) +t+ trans m)). simpl.
ring. rewrite H3 in H1. rewrite <- Heqw in H1.
addHyp (currSince_periodic_sent n m t w i p H H1). decompose [ex] H4.
clear H4. decompose [and] H6. clear H6. rename x0 into l0. rename x into t'.
assert (t' <= u). rewrite Hequ. eapply Rle_trans. apply H7. rewrite Heqw.
rewrite <- H3. rewrite Rplus_assoc. rewrite Rplus_comm. rewrite Rplus_assoc.
rewrite Rplus_comm. apply Rplus_le_compat_r. rewrite Rplus_comm. apply Rle_refl.
rewrite Hequ in H6.
addHyp (sent_pos_bound n m t' i l l0 p H9 H0).
assert (msgLatency < t'). eapply Rle_lt_trans;[ |apply H4]. rewrite Heqw.
rewrite <- H3. rewrite Rplus_assoc. apply Rle_plus_r. apply Rle_zero_plus.
rewrite <- timeMax_RMax. timeNonneg.
timeNonneg.
addHyp (sent_delivered n [baseMode m, basePosition l0] t' i p H9 H10).
decompose [ex] H11. clear H11. rename x0 into l1. rename x into r.
remember (minusTime (nonneg (time t')) (nonneg (time msgLatency))
(Rlt_le (nonneg (time msgLatency)) (nonneg (time t')) H10)) as t''.
assert ((Rmax adaptNotif transMax) + trans m < t'').
rewrite Heqt''. simpl. apply Rplus_lt_swap_ll. rewrite <- Rplus_assoc.
rewrite H3. rewrite <- Heqw. assumption.
assert (t'' <= (Rmax adaptNotif transMax) + period m + trans m).
rewrite Heqt''. simpl. apply Rplus_le_swap_rl. repeat rewrite <- Rplus_assoc.
assumption.
assert (t'' [:] preDeliveredInterval m). split;simpl.
eapply Rle_lt_trans;[ | apply H11]. apply Rle_plus_r. timeNonneg.
assumption.
assert (t'' < t). rewrite Heqt''. simpl. eapply Rlt_le_trans;[ |apply H5].
apply Rplus_lt_swap_rr. apply Rlt_plus_r. apply msgLatency_positive.
assert (nonneg t' = msgLatency + t''). rewrite Heqt''. simpl. ring.
rewrite H16 in H8.
exists t'' r l0 l1. rewrite Heqh. repeat (split;try assumption).
addHyp (suffDec m r). appDisj H17. assumption.
assert (adaptNotif < t''). eapply Rle_lt_trans;[ |apply H11].
apply Rplus_le_weaken_rr. timeNonneg. apply Rmax_l.
addHyp (insuff_react n m l0 l1 r t t'' i p H H13 H17 H15 n0 Q).
decompExAnd H18 x LT TF. lets TB : tfs_bound TF.
assert (minusTime t'' adaptNotif (Rlt_le adaptNotif t'' H17) <= trans m) as C1.
eapply Rle_trans. apply LT. assumption.
assert (adaptNotif + trans m < t''). eapply Rle_lt_trans;[ |apply H11].
apply Rplus_le_compat_r. apply Rmax_l.
simpl in C1. apply Rplus_lt_swap_ll in H18.
apply False_ind. apply (Rlt_irrefl (t'' - adaptNotif)). eapply Rle_lt_trans.
apply C1. assumption. Qed.
This page has been generated by coqdoc