Library NARInsuff
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.EntityLanguage.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.NARMisc.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.ProtAuxResults.
Lemma tfs_state_rel i n (p : reachableNet n) :
tfsStateNet i n -> exists m t, tfs m t i n p.
Admitted.
Lemma tfs_currModeNet m1 m2 t i n p : tfs m1 t i n p ->
currModeNet m2 i n -> ~failSafe m2 -> m1 = m2.
Admitted.
Lemma currModeNet_notifBad_pres_bkwd m i n n' a
(rn : reachableNet n) (w : n -NA- a -NA> n') :
currModeNet m i n' -> notifBadPathNet i n ->
~failSafe m ->
currModeNet m i n \/
exists t, tfs m t i n' (reachNetDisc n n' a rn w). introz U.
lets CPB : currMode_pres_bkwd w U. ex_flat.
lets EDM : eqDecMode x m. elim_intro EDM EQ NEQ.
subst. left. assumption.
lets CSS : currModeNet_switch_states rn w H U NEQ.
lets NBC : notifBadPathNet_cases U0 H.
elim_intro CSS SW TF. and_flat.
lets PS : paused_switch_net i rn.
assert (switchStateNet i n) as SSN. inversion AND.
inversion H0. inversion H2. subst.
econstructor; [do 2 econstructor | ].
eapply switCurSt. eassumption. eassumption.
rewrite <- PS in SSN.
Admitted.
Lemma currEq_eq_badOvlp_net m m'' i n :
m = m'' -> currEqStateNet m m'' i n -> badOvlpStateNet i n.
introz U. subst. inversion U0. inversion H.
inversion H1. subst. econstructor; [do 2 econstructor | ];
[ | eassumption].
Admitted.
Theorem delivered_incomingNetNotif (n : Network) (v : list BaseType) (r : Distance)
(l : Position) (t : Time) (i : nat) (p : reachableNet n) :
delivered ([-v, l, r-]) t i n p -> forall q : t < adaptNotif,
incomingNetNotif ((baseDistance r)::v) (minusTime adaptNotif t (Rlt_le t adaptNotif q)) i n.
intros H q.
induction H.
lets OI : outNet_incomingNetNotif w. my_applys_eq OI. apply timeEqR. simpl. ring.
lets IH : IHdelivered q. clear IHdelivered.
lets ID : incomingNetNotif_disc_pres w IH. apply ID. apply RltMinusBothSides. assumption.
assert (t < adaptNotif) as Q. eapply Rplus_lt_weaken_lr. apply q. apply Rlt_le. delPos.
lets IH : IHdelivered Q. clear IHdelivered.
lets Q1 : incomingNetNotif_del p w IH.
invertClearAs2 Q1 p1 Q2. my_applys_eq Q2. apply timeEqR. simpl. ring. Qed.
Theorem insuff_incomingNotif_abort (n n' : Network) (a : ActDiscNet) (m : Mode)
(r : Distance) (l : Position) (i : nat) :
nextModeNet m i n -> n -NA- a -NA> n' -> ~sufficient m r ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n' \/
notifAbortPathNet i n'. Admitted.
Theorem nextSince_next (n : Network) (m : Mode) (t : Time) (i : nat) (p : reachableNet n) :
nextSince m t i n p -> nextModeNet m i n.
introz U. induction U.
eapply ovWaitState_nextMode_net.
eapply reachNetDisc. apply p. apply w. apply H1.
Admitted.
Theorem notifAbort_not_nextSince (n n' : Network)
(a : ActDiscNet) (i : nat) (rn : reachableNet n) :
notifAbortPathNet i n -> n -NA- a -NA> n' ->
notifAbortPathNet 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 : notifAbort_modeState_eq U MSI U0;
lets MIU : mState_in_net_unique MSI' NME; subst.
left. econstructor;[ | apply U1]. inversion H.
econstructor; eassumption. eapply napCuok; eassumption.
eapply napAbort; eassumption.
inversion H; 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 napRng. econstructor. eassumption. reflexivity.
assumption. assumption.
ex_flat. lets RBN : rangeBad_next H3 H2. ex_flat.
left. econstructor. eapply napCuok. econstructor.
eapply currEq_cond_false. apply H8. my_applys_eq H4.
remember ([|p1' $||$ p2' $||$ p3', l, h, k0|]) as e'.
replace (currModeMState k0) with (currModeEnt e').
assert (currEqStateEnt x1 m' e'). subst.
Admitted.
Theorem instant_insuff_abort (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t : Time) (i : nat) (p : reachableNet n) :
delivered ([-[baseMode m, basePosition l], l0, r-]) adaptNotif i n p -> ~sufficient m r ->
nextSince m t i n p -> adaptNotif < t ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n \/
notifAbortPathNet i n.
intros H H0 H1 H2.
dependent induction H. false. apply (Rlt_irrefl adaptNotif).
eapply Rle_lt_trans. rewrite <- x. apply Rle_refl. apply adaptNotif_positive.
dependent destruction H1. false. eapply Rlt_not_le. apply H4. simpl. timeNonneg.
lets IHdisc : IHdelivered H0 H1 H3. reflexivity.
elim_intro IHdisc D1 D2.
assert (nextModeNet m i n) as Q. eapply nextSince_next. apply H1.
eapply insuff_incomingNotif_abort. apply Q.
apply w. assumption. assumption.
lets G : notifAbort_not_nextSince p D2 w. elim_intro G G1 G2.
right. assumption.
false.
assert (t0 < adaptNotif) as Q. rewrite <- x. simpl. Rplus_lt_tac. delPos.
lets W : delivered_incomingNetNotif H Q.
left. lets E : incomingNetNotif_del p w W. invertClearAs2 E Z1 Z2.
my_applys_eq Z2. apply timeEqR. simpl. rewrite <- x. simpl. ring. Qed.
Theorem insuff_incomingNotif_bad (n n' : Network) (a : ActDiscNet) (m : Mode)
(r : Distance) (l : Position) (i : nat) :
currModeNet m i n -> n -NA- a -NA> n' -> ~sufficient m r ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n' \/
notifBadPathNet i n'. Admitted.
If the badOvlp state holds at a particular reachable state,
and in the next state listening holds, then the next state is tfs for some
time t, with the mode parameter equal to the current mode.
Theorem badOvlp_listening_tfs n n' a i m
(rn : reachableNet n) (w : n -NA- a -NA> n') :
badOvlpStateNet i n -> listeningStateNet i n' ->
currModeNet m i n ->
exists t, tfs m t i n' (reachNetDisc n n' a rn w).
Admitted.
Theorem notifBad_pres_tfs (m : Mode) (n n' : Network)
(a : ActDiscNet) (i : nat) (rn : reachableNet n)
(w : n -NA- a -NA> n') :
notifBadPathNet i n -> currModeNet m i n' -> ~failSafe m ->
notifBadPathNet i n' \/ (exists t, tfs m t i n' (reachNetDisc n n' a rn w)).
introz U.
lets CPB : currModeNet_notifBad_pres_bkwd U0 U U1.
elim_intro CPB CMN TFD.
lets NBC : notifBadPathNet_cases U CMN. or_flat. ex_flat.
lets RNN : rangeBad_next_net w OR CMN. left. or_flat.
eapply rangeBad_notifBad_net; eassumption.
ex_flat.
assert (badOvlpStateNet i n') as BOS. eapply currEq_eq_badOvlp_net.
reflexivity. eassumption. apply badOvlp_notifBad_net; assumption.
lets BNN : badOvlp_next_net w OR0. or_flat.
left. apply badOvlp_notifBad_net; assumption.
right. eapply badOvlp_listening_tfs; eassumption.
right. apply TFD. Qed.
Lemma tfs_pres_not_currSince m t i n n' p a
(w : n -NA- a -NA> n') : tfs m t i n p ->
tfs m t i n' (reachNetDisc n n' a p w) \/
(forall m' t' p', ~currSince m' t' i n p').
Admitted.
Theorem instant_insuff_bad (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t : Time) (i : nat) (p : reachableNet n) :
delivered ([-[baseMode m, basePosition l], l0, r-]) adaptNotif i n p -> ~failSafe m ->
~sufficient m r -> currSince m t i n p -> adaptNotif < t ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n
\/ notifBadPathNet i n \/ exists t, tfs m t i n p.
intros H NFS H0 H1 H2. lets CSS : H1.
dependent induction H. false. apply (Rlt_irrefl adaptNotif).
eapply Rle_lt_trans. rewrite <- x. apply Rle_refl. apply adaptNotif_positive.
dependent destruction H1.
lets IIA : instant_insuff_abort H H0 H1 H4.
assert (reachableNet n') as p'. eapply reachNetDisc; eassumption.
assert (switchStateNet i n') as SSN2. inversion H3. inversion H5. inversion H7.
netState_auto_pre. eapply switLisSt. eassumption.
assert (switchStateNet i n) as SSN1. inversion H2. inversion H5. inversion H7.
netState_auto_pre. eapply switCurSt. eassumption.
lets PSN2 : paused_switch_net i p'. rewrite <- PSN2 in SSN2.
lets PSN1 : paused_switch_net i p. rewrite <- PSN1 in SSN1.
rename H2 into SWIN. elim IIA; [intro IL | intro IR]; clear IIA.
assert (nextModeNet m i n) as NM. eapply nextSince_next. eassumption.
lets IIA : insuff_incomingNotif_abort NM w H0 IL. elim_intro IIA IIL IIR.
left. assumption.
false. eapply state_disj_paused_notifAbort. apply SSN2. assumption.
false. eapply state_disj_paused_notifAbort. apply SSN1. assumption.
lets IH : IHdelivered NFS H0 H1 H3. reflexivity.
lets IHC : IH H1. clear IH. rename IHC into IH. elimOr3 IH IH.
assert (currModeNet m i n) as CMN. eapply currSince_curr. eassumption.
lets IIB : insuff_incomingNotif_bad CMN w H0 IH0.
elim_intro IIB INN NBN. left. assumption. right. left. assumption.
right. eapply notifBad_pres_tfs; assumption.
invertClearAs2 IH t0 TFS.
lets TPNC : tfs_pres_not_currSince w TFS. elim_intro TPNC TF NCS.
right. right. exists t0. assumption. false. eapply NCS. eassumption.
assert (t0 < adaptNotif) as TLAN. rewrite <- x. simpl. Rplus_lt_tac.
delPos. lets DIN : delivered_incomingNetNotif H TLAN. left.
lets IND : incomingNetNotif_del p w DIN. destruct IND. my_applys_eq i0.
apply timeEqR. simpl. rewrite <- x. simpl. ring.
Qed.
Theorem deliv_next_suff (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t t' : Time) (i : nat) (p : reachableNet n) :
nextSince m t i n p ->
delivered ([-[baseMode m, basePosition l], l0, r-]) t' i n p ->
adaptNotif < t' -> t' < t -> sufficient m r.
introv H H0. gen t.
induction H0; intros u G1 G2 G3; [false | dependent destruction G1..].
false. eapply Rlt_not_le. apply G2. simpl. timeNonneg.
false. eapply Rlt_not_le. apply G3. simpl. timeNonneg.
eapply IHdelivered; try assumption. apply G1. apply G3.
lets Q : Rlt_or_le adaptNotif t.
elim_intro Q Q1 Q2.
eapply IHdelivered; try assumption. apply G1. simpl in G3. Rplus_lt_tac.
apply Rle_lt_or_eq_dec in Q2. elim_intro Q2 F1 F2.
lets K : delivered_incomingNetNotif H0 F1.
lets K1 : incomingNetNotif_del p w K. invertClearAs2 K1 K2 K3. simpl in K2. false.
eapply Rle_not_lt. apply K2. simpl in G2. Rplus_lt_tac.
lets K : suffDec m r. elim_intro K K1 K2. assumption.
replace t with adaptNotif in H0; [ |apply timeEqR; symmetry; assumption].
assert (adaptNotif < t0) as H. simpl in G3. rewrite F2 in G3. Rplus_lt_tac.
lets G : instant_insuff_abort H0 K2 G1 H.
elim_intro G H1 H2.
lets H4 : incomingNetNotif_del p w H1. invertClearAs2 H4 H5 H6. false.
eapply Rle_not_lt. apply H5. simpl. delPos.
lets nau : notifAbortPathNet_urgent p H2 w. contradiction nau.
Qed.
Theorem insuff_react (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t t' : Time) (i : nat) (p : reachableNet n) :
currSince m t i n p ->
delivered ([-[baseMode m, basePosition l], l0, r-]) t' i n p ->
forall q : adaptNotif < t', t' < t -> ~sufficient m r -> ~failSafe m ->
exists x, minusTime t' adaptNotif (Rlt_le adaptNotif t' q) <= (time x) /\
tfs m x i n p.
intro. generalize dependent l. generalize dependent l0. generalize dependent r.
generalize dependent t'. induction H; intros;
match goal with [ H : ~failSafe m |- _ ] => rename H into Q end.
addHyp (switchCurr_listen_trans_tau n n' a i w H0 H1).
generalize dependent w. rewrite H5. intros. dependent destruction H2.
addHyp (deliv_next_suff n m l l0 r t t0 i p H H2 q H3).
contradiction H4.
dependent destruction H1. contradict q. eapply Rle_not_lt.
simpl. timeNonneg.
addHyp (IHcurrSince t0 r l0 l H1 q H2 H3 Q). clear IHcurrSince.
invertClearAs2 H4 x TFA. decompAnd2 TFA TFL TF. rename TF into H4.
assert (tfsStateNet i n'). apply currSince_curr in H.
apply tfs_rel_state in H4. apply (tfs_currMode_disc_pres n n' a i m w H Q H4).
exists x. split. assumption. constructor; assumption.
dependent destruction H0. rename t0 into t'.
assert (t' < t). eapply Rplus_lt_reg_r. unfold addDelayTime in H1.
simpl in H1. apply H1.
addHyp (Rlt_or_le adaptNotif t'). invertClear H4.
lets IH : IHcurrSince H0 H5 H3 H2 Q. decompExAnd IH x TL TF. clear IHcurrSince.
replace ((minusTime (nonneg (time (delToTime (t' +dt+ d))))
(nonneg (time adaptNotif)) (Rlt_le (nonneg (time adaptNotif))
(nonneg (time (delToTime (t' +dt+ d)))) q))) with
(delToTime (minusTime t' adaptNotif (Rlt_le adaptNotif t' H5) +dt+ d)).
exists (x +dt+ d). split. apply Rplus_le_compat_r. assumption.
constructor. assumption. apply timeEqR. simpl. ring.
remember ([baseMode m, basePosition l]) as v. apply Rle_lt_or_eq_dec in H5. invertClear H5.
addHyp (delivered_incomingNetNotif n v r l0 t' i p H0 H4).
remember (minusTime (nonneg (time adaptNotif)) (nonneg (time t'))
(Rlt_le (nonneg (time t')) (nonneg (time adaptNotif)) H4)) as t''.
addHyp (incomingNetNotif_del n n' d ((baseDistance r)::v) t'' i p w H5). invertClear H6.
rename x into Q1. generalize dependent Q1. rewrite Heqt''. intros.
simpl in Q1. simpl in q.
assert (adaptNotif - t' < d). apply Rplus_lt_swap_rl. assumption.
contradict H6. apply Rle_not_lt. assumption.
apply timeEqR in H4. rewrite H4 in H0, H3. rewrite Heqv in H0.
addHyp (instant_insuff_bad n m l l0 r t i p H0 Q H2 H H3).
decompose [or] H5; clear H5.
remember ([baseDistance r, baseMode m, basePosition l]) as v2.
addHyp (incomingNetNotif_del n n' d v2 zeroTime i p w H6). invertClear H5.
rename x into Q2. clear H7. contradict Q2. apply Rlt_not_le. simpl. delPos.
contradiction (notifBadPathNet_urgent i n n' d H7 w).
invertClearAs2 H7 x TF. lets TFD : tfsDel w TF. exists (x +dt+ d).
split. simpl. rewrite H4. apply Rminus_le_swap_lr. cut (0 <= x). intro LT0.
my_applys_eq LT0. ring. timeNonneg. apply TFD. Qed.
(rn : reachableNet n) (w : n -NA- a -NA> n') :
badOvlpStateNet i n -> listeningStateNet i n' ->
currModeNet m i n ->
exists t, tfs m t i n' (reachNetDisc n n' a rn w).
Admitted.
Theorem notifBad_pres_tfs (m : Mode) (n n' : Network)
(a : ActDiscNet) (i : nat) (rn : reachableNet n)
(w : n -NA- a -NA> n') :
notifBadPathNet i n -> currModeNet m i n' -> ~failSafe m ->
notifBadPathNet i n' \/ (exists t, tfs m t i n' (reachNetDisc n n' a rn w)).
introz U.
lets CPB : currModeNet_notifBad_pres_bkwd U0 U U1.
elim_intro CPB CMN TFD.
lets NBC : notifBadPathNet_cases U CMN. or_flat. ex_flat.
lets RNN : rangeBad_next_net w OR CMN. left. or_flat.
eapply rangeBad_notifBad_net; eassumption.
ex_flat.
assert (badOvlpStateNet i n') as BOS. eapply currEq_eq_badOvlp_net.
reflexivity. eassumption. apply badOvlp_notifBad_net; assumption.
lets BNN : badOvlp_next_net w OR0. or_flat.
left. apply badOvlp_notifBad_net; assumption.
right. eapply badOvlp_listening_tfs; eassumption.
right. apply TFD. Qed.
Lemma tfs_pres_not_currSince m t i n n' p a
(w : n -NA- a -NA> n') : tfs m t i n p ->
tfs m t i n' (reachNetDisc n n' a p w) \/
(forall m' t' p', ~currSince m' t' i n p').
Admitted.
Theorem instant_insuff_bad (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t : Time) (i : nat) (p : reachableNet n) :
delivered ([-[baseMode m, basePosition l], l0, r-]) adaptNotif i n p -> ~failSafe m ->
~sufficient m r -> currSince m t i n p -> adaptNotif < t ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n
\/ notifBadPathNet i n \/ exists t, tfs m t i n p.
intros H NFS H0 H1 H2. lets CSS : H1.
dependent induction H. false. apply (Rlt_irrefl adaptNotif).
eapply Rle_lt_trans. rewrite <- x. apply Rle_refl. apply adaptNotif_positive.
dependent destruction H1.
lets IIA : instant_insuff_abort H H0 H1 H4.
assert (reachableNet n') as p'. eapply reachNetDisc; eassumption.
assert (switchStateNet i n') as SSN2. inversion H3. inversion H5. inversion H7.
netState_auto_pre. eapply switLisSt. eassumption.
assert (switchStateNet i n) as SSN1. inversion H2. inversion H5. inversion H7.
netState_auto_pre. eapply switCurSt. eassumption.
lets PSN2 : paused_switch_net i p'. rewrite <- PSN2 in SSN2.
lets PSN1 : paused_switch_net i p. rewrite <- PSN1 in SSN1.
rename H2 into SWIN. elim IIA; [intro IL | intro IR]; clear IIA.
assert (nextModeNet m i n) as NM. eapply nextSince_next. eassumption.
lets IIA : insuff_incomingNotif_abort NM w H0 IL. elim_intro IIA IIL IIR.
left. assumption.
false. eapply state_disj_paused_notifAbort. apply SSN2. assumption.
false. eapply state_disj_paused_notifAbort. apply SSN1. assumption.
lets IH : IHdelivered NFS H0 H1 H3. reflexivity.
lets IHC : IH H1. clear IH. rename IHC into IH. elimOr3 IH IH.
assert (currModeNet m i n) as CMN. eapply currSince_curr. eassumption.
lets IIB : insuff_incomingNotif_bad CMN w H0 IH0.
elim_intro IIB INN NBN. left. assumption. right. left. assumption.
right. eapply notifBad_pres_tfs; assumption.
invertClearAs2 IH t0 TFS.
lets TPNC : tfs_pres_not_currSince w TFS. elim_intro TPNC TF NCS.
right. right. exists t0. assumption. false. eapply NCS. eassumption.
assert (t0 < adaptNotif) as TLAN. rewrite <- x. simpl. Rplus_lt_tac.
delPos. lets DIN : delivered_incomingNetNotif H TLAN. left.
lets IND : incomingNetNotif_del p w DIN. destruct IND. my_applys_eq i0.
apply timeEqR. simpl. rewrite <- x. simpl. ring.
Qed.
Theorem deliv_next_suff (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t t' : Time) (i : nat) (p : reachableNet n) :
nextSince m t i n p ->
delivered ([-[baseMode m, basePosition l], l0, r-]) t' i n p ->
adaptNotif < t' -> t' < t -> sufficient m r.
introv H H0. gen t.
induction H0; intros u G1 G2 G3; [false | dependent destruction G1..].
false. eapply Rlt_not_le. apply G2. simpl. timeNonneg.
false. eapply Rlt_not_le. apply G3. simpl. timeNonneg.
eapply IHdelivered; try assumption. apply G1. apply G3.
lets Q : Rlt_or_le adaptNotif t.
elim_intro Q Q1 Q2.
eapply IHdelivered; try assumption. apply G1. simpl in G3. Rplus_lt_tac.
apply Rle_lt_or_eq_dec in Q2. elim_intro Q2 F1 F2.
lets K : delivered_incomingNetNotif H0 F1.
lets K1 : incomingNetNotif_del p w K. invertClearAs2 K1 K2 K3. simpl in K2. false.
eapply Rle_not_lt. apply K2. simpl in G2. Rplus_lt_tac.
lets K : suffDec m r. elim_intro K K1 K2. assumption.
replace t with adaptNotif in H0; [ |apply timeEqR; symmetry; assumption].
assert (adaptNotif < t0) as H. simpl in G3. rewrite F2 in G3. Rplus_lt_tac.
lets G : instant_insuff_abort H0 K2 G1 H.
elim_intro G H1 H2.
lets H4 : incomingNetNotif_del p w H1. invertClearAs2 H4 H5 H6. false.
eapply Rle_not_lt. apply H5. simpl. delPos.
lets nau : notifAbortPathNet_urgent p H2 w. contradiction nau.
Qed.
Theorem insuff_react (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t t' : Time) (i : nat) (p : reachableNet n) :
currSince m t i n p ->
delivered ([-[baseMode m, basePosition l], l0, r-]) t' i n p ->
forall q : adaptNotif < t', t' < t -> ~sufficient m r -> ~failSafe m ->
exists x, minusTime t' adaptNotif (Rlt_le adaptNotif t' q) <= (time x) /\
tfs m x i n p.
intro. generalize dependent l. generalize dependent l0. generalize dependent r.
generalize dependent t'. induction H; intros;
match goal with [ H : ~failSafe m |- _ ] => rename H into Q end.
addHyp (switchCurr_listen_trans_tau n n' a i w H0 H1).
generalize dependent w. rewrite H5. intros. dependent destruction H2.
addHyp (deliv_next_suff n m l l0 r t t0 i p H H2 q H3).
contradiction H4.
dependent destruction H1. contradict q. eapply Rle_not_lt.
simpl. timeNonneg.
addHyp (IHcurrSince t0 r l0 l H1 q H2 H3 Q). clear IHcurrSince.
invertClearAs2 H4 x TFA. decompAnd2 TFA TFL TF. rename TF into H4.
assert (tfsStateNet i n'). apply currSince_curr in H.
apply tfs_rel_state in H4. apply (tfs_currMode_disc_pres n n' a i m w H Q H4).
exists x. split. assumption. constructor; assumption.
dependent destruction H0. rename t0 into t'.
assert (t' < t). eapply Rplus_lt_reg_r. unfold addDelayTime in H1.
simpl in H1. apply H1.
addHyp (Rlt_or_le adaptNotif t'). invertClear H4.
lets IH : IHcurrSince H0 H5 H3 H2 Q. decompExAnd IH x TL TF. clear IHcurrSince.
replace ((minusTime (nonneg (time (delToTime (t' +dt+ d))))
(nonneg (time adaptNotif)) (Rlt_le (nonneg (time adaptNotif))
(nonneg (time (delToTime (t' +dt+ d)))) q))) with
(delToTime (minusTime t' adaptNotif (Rlt_le adaptNotif t' H5) +dt+ d)).
exists (x +dt+ d). split. apply Rplus_le_compat_r. assumption.
constructor. assumption. apply timeEqR. simpl. ring.
remember ([baseMode m, basePosition l]) as v. apply Rle_lt_or_eq_dec in H5. invertClear H5.
addHyp (delivered_incomingNetNotif n v r l0 t' i p H0 H4).
remember (minusTime (nonneg (time adaptNotif)) (nonneg (time t'))
(Rlt_le (nonneg (time t')) (nonneg (time adaptNotif)) H4)) as t''.
addHyp (incomingNetNotif_del n n' d ((baseDistance r)::v) t'' i p w H5). invertClear H6.
rename x into Q1. generalize dependent Q1. rewrite Heqt''. intros.
simpl in Q1. simpl in q.
assert (adaptNotif - t' < d). apply Rplus_lt_swap_rl. assumption.
contradict H6. apply Rle_not_lt. assumption.
apply timeEqR in H4. rewrite H4 in H0, H3. rewrite Heqv in H0.
addHyp (instant_insuff_bad n m l l0 r t i p H0 Q H2 H H3).
decompose [or] H5; clear H5.
remember ([baseDistance r, baseMode m, basePosition l]) as v2.
addHyp (incomingNetNotif_del n n' d v2 zeroTime i p w H6). invertClear H5.
rename x into Q2. clear H7. contradict Q2. apply Rlt_not_le. simpl. delPos.
contradiction (notifBadPathNet_urgent i n n' d H7 w).
invertClearAs2 H7 x TF. lets TFD : tfsDel w TF. exists (x +dt+ d).
split. simpl. rewrite H4. apply Rminus_le_swap_lr. cut (0 <= x). intro LT0.
my_applys_eq LT0. ring. timeNonneg. apply TFD. Qed.
This page has been generated by coqdoc