Library NetAuxBasics
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 Reals.
Require Import List.
Require Import ComhCoq.Extras.LibTactics.
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.NetworkLanguage.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.ProtAuxResults.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.GenTacs.
Inductive initialNet : Network -> Prop :=
| initNtNil : initialNet []
| initNtCons e n : initialEnt e -> initialNet n ->
initialNet (e :: n).
Inductive reachableNet : Network -> Type :=
| reachNetInit (n : Network) : initialNet n -> reachableNet n
| reachNetDisc (n n' : Network) (a : ActDiscNet) : reachableNet n ->
n -NA- a -NA> n' -> reachableNet n'
| reachNetDel (n n' : Network) (d : Delay) : reachableNet n ->
n -ND- d -ND> n' -> reachableNet n'.
Lemma link_net_prot_reach n p l h k i :
reachableNet n -> [|p, l, h, k|] @ i .: n -> reachableProt p.
Admitted.
Ltac link_netprotreach_tac U :=
match goal with
[H : reachableNet ?n, H0 : [|_, _, _, _|] @ _ .: ?n |- _] =>
let U1 := fresh U in lets U1 : link_net_prot_reach H H0
end.
Parameter currModeNet : Mode -> nat -> Network -> Prop.
Inductive transGuard (t : Time) (i : nat) (n : Network) : Prop :=
| tgWitness (p : ProcTerm) (l : Position) (h : Interface) (m m' : Mode) :
[| p , l , h , <| m , m' , t |> |] @ i .: n -> transGuard t i n.
Parameter nextModeNet : Mode -> nat -> Network -> Prop.
Inductive inPosNet (l : Position) (i : nat) (n : Network) : Prop :=
| ipWitness (p : ProcTerm) (h : Interface) (k : ModeState) :
[| p , l , h , k |] @ i .: n -> inPosNet l i n.
Inductive distNet (i i' : nat) (n : Network) : Distance -> Prop :=
| dnWitness (l l' : Position) : inPosNet l i n -> inPosNet l' i' n ->
distNet i i' n (distFun l l').
Inductive outgoing (v : list BaseType) (t : Time) (i : nat) (n : Network) : Prop :=
| ogWitness (p : ProcTerm) (l : Position) (li : InputList) (lo : OutputList) (ln : NotifList) (k : ModeState) :
[| p , l , (mkInterface li lo ln) , k |] @ i .: n -> In (<( v , t )>) (outList lo) -> outgoing v t i n.
Inductive incomingNet (v : list BaseType) (i : nat) (n : Network) : Prop :=
| icWitness (p : ProcTerm) (l : Position) (li : InputList) (lo : OutputList) (ln : NotifList) (k : ModeState) :
[| p , l , (mkInterface li lo ln) , k |] @ i .: n -> In (<( v , zeroTime )>) (inList li) -> incomingNet v i n.
Inductive incomingNetNotif (v : list BaseType) (t : Time) (i : nat) (n : Network) : Prop :=
| icnWitness (p : ProcTerm) (l : Position) (li : InputList) (lo : OutputList) (ln : NotifList) (k : ModeState) :
[| p , l , (mkInterface li lo ln) , k |] @ i .: n -> In (<( v , t )>) (notifList ln) -> incomingNetNotif v t i n.
Inductive mState_in_net (k : ModeState) (i : nat) (n : Network) : Prop :=
minet (p : ProcTerm) (l : Position) (h : Interface) :
[|p, l, h, k|] @ i .: n -> mState_in_net k i n.
Inductive liftEntNet (X : Entity -> Prop) (i : nat) (n : Network) : Prop :=
| lenWitness (e : Entity) : X e -> e @ i .: n -> liftEntNet X i n.
Definition bcWaitStateNet m x := liftEntNet (bcWaitStateEnt m x).
Definition sleepingStateNet := liftEntNet sleepingStateEnt.
Definition bcReadyStateNet m l := liftEntNet (bcReadyStateEnt m l).
Definition dormantStateNet := liftEntNet dormantStateEnt.
Definition tfsStartStateNet := liftEntNet tfsStartStateEnt.
Definition initStateNet m := liftEntNet (initStateEnt m).
Definition ovWaitStateNet m t x y := liftEntNet (ovWaitStateEnt m t x y).
Definition ovReadyStateNet m t l := liftEntNet (ovReadyStateEnt m t l).
Definition switchCurrStateNet := liftEntNet switchCurrStateEnt.
Definition switchListenStateNet := liftEntNet switchListenStateEnt.
Definition switchBcStateNet m := liftEntNet (switchBcStateEnt m).
Definition tfsCurrStateNet := liftEntNet tfsCurrStateEnt.
Definition tfsBcStateNet := liftEntNet tfsBcStateEnt.
Definition tfsListenStateNet := liftEntNet tfsListenStateEnt.
Definition pausedStateNet := liftEntNet pausedStateEnt.
Definition tfsNextStateNet m := liftEntNet (tfsNextStateEnt m).
Definition listeningStateNet := liftEntNet listeningStateEnt.
Definition currCompStateNet m'' r := liftEntNet (currCompStateEnt m'' r).
Definition badOvlpStateNet := liftEntNet badOvlpStateEnt.
Definition rangeBadStateNet m := liftEntNet (rangeBadStateEnt m).
Definition currEqStateNet m m'' := liftEntNet (currEqStateEnt m m'').
Definition broadcastStateNet := liftEntNet broadcastStateEnt.
Definition overlapStateNet := liftEntNet overlapStateEnt.
Definition tfsStateNet := liftEntNet tfsStateEnt.
Definition nextSinceStateNet := liftEntNet (nextSinceStateEnt).
Definition switchStateNet := liftEntNet switchStateEnt.
Definition listenerStateNet := liftEntNet listenerStateEnt.
Definition ovAbortStateNet := liftEntNet ovAbortStateEnt.
Conjecture tfsStateNet_dec : forall (i : nat) (n : Network), decidable (tfsStateNet i n).
Conjecture tfsCurrNet_dec : forall (i : nat) (n : Network),
decidable (tfsCurrStateNet i n).
Lemma tfsCurrStateNet_bktrk_net : forall (n n' : Network) (i : nat) (a : ActDiscNet),
tfsCurrStateNet i n' -> n -NA- a -NA> n' ->
tfsCurrStateNet i n \/
(exists m mF, exists p,
tfsNextStateNet m i n /\ failSafe mF /\
mState_in_net (<| m, mF, modeTransTime m mF p |>) i n'). Admitted.
Conjecture tfsCurrState_del_pres_net : forall (n n' : Network) (d : Delay) (i : nat),
n -ND- d -ND> n' ->
(tfsCurrStateNet i n <-> tfsCurrStateNet i n').
Lemma mState_switch_states : forall (n n' : Network) (i : nat)
(a : ActDiscNet) (k k' : ModeState), reachableNet n -> k <> k' ->
n -NA- a -NA> n' -> mState_in_net k i n -> mState_in_net k' i n' ->
(tfsCurrStateNet i n /\ tfsBcStateNet i n') \/
(switchCurrStateNet i n /\ switchListenStateNet i n'). Admitted.
Conjecture tfsState_del_pres_net : forall (n n' : Network) (i : nat) (d : Delay),
n -ND- d -ND> n' -> (tfsStateNet i n <-> tfsStateNet i n').
Lemma switch_states_mState : forall (n n' : Network) (i : nat) (a : ActDiscNet)
(m : Mode), n -NA- a -NA> n' -> switchCurrStateNet i n ->
switchListenStateNet i n' -> nextModeNet m i n -> currModeNet m i n'. Admitted.
A network transition which sees a software component of some entity
transform to a different software term is necessarily a tau transition.
Lemma procNeq_tau_net p p' l l' h h' k k' n n' a i :
[|p, l, h, k|] @ i .: n -> [|p', l', h', k'|] @ i .: n' ->
n -NA- a -NA> n' -> p <> p' -> a = anTau. Admitted.
[|p, l, h, k|] @ i .: n -> [|p', l', h', k'|] @ i .: n' ->
n -NA- a -NA> n' -> p <> p' -> a = anTau. Admitted.
The action linking a change from switchCurr to switchListen is always a tau.
Lemma switchCurr_listen_trans_tau (n n' : Network) (a : ActDiscNet) (i : nat) :
n -NA- a -NA> n' -> switchCurrStateNet i n -> switchListenStateNet i n' ->
a = anTau. introz U.
state_pred_net_destr U0. state_pred_net_destr U1.
assert (p <> p0). unfold not; intro. subst.
Focus 2.
eapply procNeq_tau_net. apply H0.
eassumption. eassumption. eassumption.
Admitted.
Lemma tfsStart_tfs_net i n :
tfsStartStateNet i n -> tfsStateNet i n. Admitted.
Lemma tfsNext_tfs_net m i n :
tfsNextStateNet m i n -> tfsStateNet i n. Admitted.
Lemma tfsCurr_tfs_net i n :
tfsCurrStateNet i n -> tfsStateNet i n. Admitted.
Lemma tfsBc_tfs_net i n :
tfsBcStateNet i n -> tfsStateNet i n. Admitted.
Lemma tfsListen_tfs_net i n :
tfsListenStateNet i n -> tfsStateNet i n. Admitted.
n -NA- a -NA> n' -> switchCurrStateNet i n -> switchListenStateNet i n' ->
a = anTau. introz U.
state_pred_net_destr U0. state_pred_net_destr U1.
assert (p <> p0). unfold not; intro. subst.
Focus 2.
eapply procNeq_tau_net. apply H0.
eassumption. eassumption. eassumption.
Admitted.
Lemma tfsStart_tfs_net i n :
tfsStartStateNet i n -> tfsStateNet i n. Admitted.
Lemma tfsNext_tfs_net m i n :
tfsNextStateNet m i n -> tfsStateNet i n. Admitted.
Lemma tfsCurr_tfs_net i n :
tfsCurrStateNet i n -> tfsStateNet i n. Admitted.
Lemma tfsBc_tfs_net i n :
tfsBcStateNet i n -> tfsStateNet i n. Admitted.
Lemma tfsListen_tfs_net i n :
tfsListenStateNet i n -> tfsStateNet i n. Admitted.
The following three tactics are mostly simply auxiliaries to the main
result of fwd_track_net_tac.
Ltac first_eexists_5 t := first [t | (do 1 eexists);t | (do 2 eexists);t |
(do 3 eexists);t | (do 4 eexists);t | (do 5 eexists);t].
Ltac econstr_easssump := econstructor; eassumption.
Ltac first_ex_econ_eass := first_eexists_5 econstr_easssump.
(do 3 eexists);t | (do 4 eexists);t | (do 5 eexists);t].
Ltac econstr_easssump := econstructor; eassumption.
Ltac first_ex_econ_eass := first_eexists_5 econstr_easssump.
RE is the entity level result upon which this tactic works. Essentially,
this tactic lifts RE from the entity to the network level. Note that the tactic
assumes a disjunctive goal of two branches and may not work otherwise.
Ltac fwd_track_net_tac RE :=
let U := fresh in let U0 := fresh in
intros U U0; destruct U0;
let e' := fresh "e'" in let b := fresh "b" in
let LNE := fresh "LNE" in
link_netentdiscfwd_tac e' b LNE;
[subst; left | match goal with [LNE1 : _ -EA- b ->> e', e : Entity,
H0 : _ ?e |- _] =>
lets LOW : RE LNE1 H0;
or_flat; ex_flat; [left | right] end];
first_ex_econ_eass.
Lemma tfsStart_next_net n n' a i :
n -NA- a -NA> n' -> tfsStartStateNet i n ->
tfsStartStateNet i n' \/ exists m, tfsNextStateNet m i n'.
fwd_track_net_tac tfsStart_next_ent. Qed.
Lemma tfsNext_next_net m n n' a i :
n -NA- a -NA> n' -> tfsNextStateNet m i n ->
tfsNextStateNet m i n' \/ tfsCurrStateNet i n'.
fwd_track_net_tac tfsNext_next_ent. Qed.
Lemma tfsCurr_next_net n n' a i :
n -NA- a -NA> n' -> tfsCurrStateNet i n ->
tfsCurrStateNet i n' \/ tfsBcStateNet i n'.
fwd_track_net_tac tfsCurr_next_ent. Qed.
Lemma tfsBc_next_net n n' a i :
n -NA- a -NA> n' -> tfsBcStateNet i n ->
tfsBcStateNet i n' \/ tfsListenStateNet i n'.
fwd_track_net_tac tfsBc_next_ent. Qed.
Lemma tfsListen_next_net n n' a i :
n -NA- a -NA> n' -> tfsListenStateNet i n ->
tfsListenStateNet i n' \/ dormantStateNet i n'.
fwd_track_net_tac tfsListen_next_ent. Qed.
Lemma rangeBad_next_net m m'' i n n' a :
n -NA- a -NA> n' -> rangeBadStateNet m'' i n -> currModeNet m i n ->
rangeBadStateNet m'' i n' \/ currEqStateNet m m'' i n'.
Admitted.
Lemma badOvlp_next_net i n n' a :
n -NA- a -NA> n' -> badOvlpStateNet i n ->
badOvlpStateNet i n' \/ listeningStateNet i n'.
Admitted.
Ltac netState_auto_pre := match goal with [U : [|_, _, _, _|] = _,
U1 : _ $||$ _ $||$ _ = _ |- _] =>
eapply lenWitness;[ | eassumption];
rewrite <- U; eapply lifpe; rewrite <- U1 end; constructor.
let U := fresh in let U0 := fresh in
intros U U0; destruct U0;
let e' := fresh "e'" in let b := fresh "b" in
let LNE := fresh "LNE" in
link_netentdiscfwd_tac e' b LNE;
[subst; left | match goal with [LNE1 : _ -EA- b ->> e', e : Entity,
H0 : _ ?e |- _] =>
lets LOW : RE LNE1 H0;
or_flat; ex_flat; [left | right] end];
first_ex_econ_eass.
Lemma tfsStart_next_net n n' a i :
n -NA- a -NA> n' -> tfsStartStateNet i n ->
tfsStartStateNet i n' \/ exists m, tfsNextStateNet m i n'.
fwd_track_net_tac tfsStart_next_ent. Qed.
Lemma tfsNext_next_net m n n' a i :
n -NA- a -NA> n' -> tfsNextStateNet m i n ->
tfsNextStateNet m i n' \/ tfsCurrStateNet i n'.
fwd_track_net_tac tfsNext_next_ent. Qed.
Lemma tfsCurr_next_net n n' a i :
n -NA- a -NA> n' -> tfsCurrStateNet i n ->
tfsCurrStateNet i n' \/ tfsBcStateNet i n'.
fwd_track_net_tac tfsCurr_next_ent. Qed.
Lemma tfsBc_next_net n n' a i :
n -NA- a -NA> n' -> tfsBcStateNet i n ->
tfsBcStateNet i n' \/ tfsListenStateNet i n'.
fwd_track_net_tac tfsBc_next_ent. Qed.
Lemma tfsListen_next_net n n' a i :
n -NA- a -NA> n' -> tfsListenStateNet i n ->
tfsListenStateNet i n' \/ dormantStateNet i n'.
fwd_track_net_tac tfsListen_next_ent. Qed.
Lemma rangeBad_next_net m m'' i n n' a :
n -NA- a -NA> n' -> rangeBadStateNet m'' i n -> currModeNet m i n ->
rangeBadStateNet m'' i n' \/ currEqStateNet m m'' i n'.
Admitted.
Lemma badOvlp_next_net i n n' a :
n -NA- a -NA> n' -> badOvlpStateNet i n ->
badOvlpStateNet i n' \/ listeningStateNet i n'.
Admitted.
Ltac netState_auto_pre := match goal with [U : [|_, _, _, _|] = _,
U1 : _ $||$ _ $||$ _ = _ |- _] =>
eapply lenWitness;[ | eassumption];
rewrite <- U; eapply lifpe; rewrite <- U1 end; constructor.
Assume a network state predicate as the goal, and enough information in the
hypothesis to prove it: an entInNet, an equality between that entity and its
various components, and an equality between a process triple and the process of
that entity. Then this tactic should solve the goal.
Ltac netState_auto_tac :=
netState_auto_pre; eassumption.
Lemma tfsState_elim_net i n :
tfsStateNet i n -> tfsStartStateNet i n \/
(exists m, tfsNextStateNet m i n) \/
tfsCurrStateNet i n \/ tfsBcStateNet i n \/
tfsListenStateNet i n. intro. inversion H. inversion H0.
inversion H2. inversion H4.
left. netState_auto_tac.
right. left. eexists. netState_auto_tac.
right. right. left. netState_auto_tac.
right. right. right. left. netState_auto_tac.
right. right. right. right. netState_auto_tac.
Qed.
Lemma tfsListen_failSafe_net m i n :
tfsListenStateNet i n -> currModeNet m i n -> failSafe m.
Admitted.
Lemma tfs_currMode_disc_pres (n n' : Network) (a : ActDiscNet) (i : nat) (m : Mode) :
n -NA- a -NA> n' -> currModeNet m i n -> ~ failSafe m ->
tfsStateNet i n -> tfsStateNet i n'. introz U.
apply tfsState_elim_net in U2. or_flat; ex_flat; [ |
rename H into OR | ..];[eapply tfsStart_next_net in OR |
eapply tfsNext_next_net in OR | eapply tfsCurr_next_net in OR |
eapply tfsBc_next_net in OR | ];
try eassumption; or_flat; ex_flat.
apply tfsStart_tfs_net; assumption.
eapply tfsNext_tfs_net; eassumption.
eapply tfsNext_tfs_net; eassumption.
apply tfsCurr_tfs_net; assumption.
apply tfsCurr_tfs_net; assumption.
apply tfsBc_tfs_net; assumption.
apply tfsBc_tfs_net; assumption.
apply tfsListen_tfs_net; assumption.
false. apply U1. eapply tfsListen_failSafe_net; eassumption.
Qed.
Lemma paused_switch_net (n : Network) (i : nat) :
reachableNet n -> (pausedStateNet i n <-> switchStateNet i n). Admitted.
Lemma bcWaitNet_del_bkwd (n n' : Network) (m : Mode) (x : Time)
(i : nat) (d : Delay) : n -ND- d -ND> n' ->
bcWaitStateNet m x i n' -> bcWaitStateNet m (x +dt+ d) i n.
Admitted.
netState_auto_pre; eassumption.
Lemma tfsState_elim_net i n :
tfsStateNet i n -> tfsStartStateNet i n \/
(exists m, tfsNextStateNet m i n) \/
tfsCurrStateNet i n \/ tfsBcStateNet i n \/
tfsListenStateNet i n. intro. inversion H. inversion H0.
inversion H2. inversion H4.
left. netState_auto_tac.
right. left. eexists. netState_auto_tac.
right. right. left. netState_auto_tac.
right. right. right. left. netState_auto_tac.
right. right. right. right. netState_auto_tac.
Qed.
Lemma tfsListen_failSafe_net m i n :
tfsListenStateNet i n -> currModeNet m i n -> failSafe m.
Admitted.
Lemma tfs_currMode_disc_pres (n n' : Network) (a : ActDiscNet) (i : nat) (m : Mode) :
n -NA- a -NA> n' -> currModeNet m i n -> ~ failSafe m ->
tfsStateNet i n -> tfsStateNet i n'. introz U.
apply tfsState_elim_net in U2. or_flat; ex_flat; [ |
rename H into OR | ..];[eapply tfsStart_next_net in OR |
eapply tfsNext_next_net in OR | eapply tfsCurr_next_net in OR |
eapply tfsBc_next_net in OR | ];
try eassumption; or_flat; ex_flat.
apply tfsStart_tfs_net; assumption.
eapply tfsNext_tfs_net; eassumption.
eapply tfsNext_tfs_net; eassumption.
apply tfsCurr_tfs_net; assumption.
apply tfsCurr_tfs_net; assumption.
apply tfsBc_tfs_net; assumption.
apply tfsBc_tfs_net; assumption.
apply tfsListen_tfs_net; assumption.
false. apply U1. eapply tfsListen_failSafe_net; eassumption.
Qed.
Lemma paused_switch_net (n : Network) (i : nat) :
reachableNet n -> (pausedStateNet i n <-> switchStateNet i n). Admitted.
Lemma bcWaitNet_del_bkwd (n n' : Network) (m : Mode) (x : Time)
(i : nat) (d : Delay) : n -ND- d -ND> n' ->
bcWaitStateNet m x i n' -> bcWaitStateNet m (x +dt+ d) i n.
Admitted.
An entity in an initial network is itself initial.
Lemma initialNet_ent e i n : initialNet n -> e @ i .: n ->
initialEnt e. intro. generalize dependent i.
induction H; intro i. intro. inversion H.
intro. inversion H1. assumption. eapply IHinitialNet.
eassumption. Qed.
initialEnt e. intro. generalize dependent i.
induction H; intro i. intro. inversion H.
intro. inversion H1. assumption. eapply IHinitialNet.
eassumption. Qed.
Looks for an initial network in the hypotheses and also an entity in
that network and adds the hypothesis that the entity in question is initial.
Ltac initNet_ent_tac := let U0 := fresh in
match goal with [U : initialNet ?n,
U1 : ?e @ ?i .: ?n |- _] => lets U0 : initialNet_ent U U1 end.
Ltac initNet_contra U :=
inversion U as [e U1 U2]; inversion U1;
initNet_ent_tac; match goal with [U3 : [|_, _, _, _|] = ?e,
U4 : initialEnt ?e |- _] => rewrite <- U3 in U4;
inversion U4 end; match goal with [U5 : initialProc _ |- _] =>
inversion U5 end; match goal with [U6 : procProtocol = _ |- _] =>
symmetry in U6; subst_all U6 end; match reverse goal with
[U7 : context[procProtocol] |- _] => inversion U7 end; subst;
match goal with
| [U8 : context[dormant] |- _] => inversion U8
| [U8 : context[sleeping] |- _] => inversion U8
| [U8 : context[listening] |- _] => inversion U8
end.
Lemma initial_not_bcWait_net (n : Network) (m : Mode) (x : Time) (i : nat) :
initialNet n -> bcWaitStateNet m x i n -> False.
introz U.
Admitted.
match goal with [U : initialNet ?n,
U1 : ?e @ ?i .: ?n |- _] => lets U0 : initialNet_ent U U1 end.
Ltac initNet_contra U :=
inversion U as [e U1 U2]; inversion U1;
initNet_ent_tac; match goal with [U3 : [|_, _, _, _|] = ?e,
U4 : initialEnt ?e |- _] => rewrite <- U3 in U4;
inversion U4 end; match goal with [U5 : initialProc _ |- _] =>
inversion U5 end; match goal with [U6 : procProtocol = _ |- _] =>
symmetry in U6; subst_all U6 end; match reverse goal with
[U7 : context[procProtocol] |- _] => inversion U7 end; subst;
match goal with
| [U8 : context[dormant] |- _] => inversion U8
| [U8 : context[sleeping] |- _] => inversion U8
| [U8 : context[listening] |- _] => inversion U8
end.
Lemma initial_not_bcWait_net (n : Network) (m : Mode) (x : Time) (i : nat) :
initialNet n -> bcWaitStateNet m x i n -> False.
introz U.
Admitted.
If we're nextSince & we can delay, then we're in the ovWait state.
Lemma nextSince_del_ovWait (n n' : Network) (i : nat) (d : Delay) :
n -ND- d -ND> n' -> nextSinceStateNet i n ->
exists m t x y, ovWaitStateNet m t (delToTime (x +dt+ d)) (delToTime (y +dt+ d)) i n. Admitted.
Lemma switchCurr_switchListen_net_link (n n' : Network) (i : nat)
(a : ActDiscNet) (e e' : Entity) :
switchCurrStateEnt e -> switchListenStateEnt e' ->
e @ i .: n -> e' @ i .: n' -> n -NA- a -NA> n' ->
a = anTau /\ interEnt e = interEnt e'. Admitted.
Lemma init_nextMode_net m i n :
reachableNet n -> initStateNet m i n -> nextModeNet m i n.
Admitted.
Lemma ovReady_prev_net_strong m t l n n' i a :
ovReadyStateNet m t l i n' -> n -NA- a -NA> n' ->
ovReadyStateNet m t l i n \/
(exists x0 y0, ovWaitStateNet m t x0 y0 i n).
Admitted.
Lemma ovWait_prev_net_strong m t x y n n' i a :
ovWaitStateNet m t x y i n' -> n -NA- a -NA> n' ->
ovWaitStateNet m t x y i n \/
(exists t0 l0, ovReadyStateNet m t0 l0 i n) \/
initStateNet m i n. Admitted.
Lemma nextMode_pres_fwd_net m i n n' a :
reachableNet n -> nextModeNet m i n ->
~(switchCurrStateNet i n \/ ovAbortStateNet i n \/
tfsCurrStateNet i n) ->
n -NA- a -NA> n' -> nextModeNet m i n'. Admitted.
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 ovReady_del_pres_bkwd_net n n' d m t l i :
n -ND- d -ND> n' -> ovReadyStateNet m t l i n' ->
ovReadyStateNet m t l i n. Admitted.
Lemma nextModeNet_del_pres n n' d m i :
n -ND- d -ND> n' -> nextModeNet m i n -> nextModeNet m i n'.
Admitted.
Lemma ovWait_ovReady_nextMode_net m t x y l i n :
reachableNet n -> ovWaitStateNet m t x y i n \/ ovReadyStateNet m t l i n ->
nextModeNet m i n.
introz U. genDep5 m t x y l. induction U; intros l y x t m; introz V.
Admitted.
Lemma ovWaitState_nextMode_net (n : Network) (m : Mode) (t x y : Time) (i : nat):
reachableNet n -> ovWaitStateNet m t x y i n -> nextModeNet m i n.
introz U. eapply ovWait_ovReady_nextMode_net with (l := mkPosition 0 0).
assumption. left. eassumption. Qed.
Theorem del_listening_net (n n' : Network) (d : Delay) (e : Entity) (i : nat) :
reachableNet n -> n -ND- d -ND> n' -> e @ i .: n -> listeningStateNet i n.
Admitted.
Theorem inPos_pres_disc (n n' : Network) (a : ActDiscNet) (l : Position) (i : nat) :
n -NA- a -NA> n' ->
(inPosNet l i n <-> inPosNet l i n').
introz U. split; introz U. destruct U0.
link_netentdiscfwd_tac e' b U. subst. econstructor; eassumption.
inversion U2; subst; econstructor; eassumption.
destruct U0.
link_netentdiscbkwd_tac e b U. subst. econstructor; eassumption.
inversion U2; subst; econstructor; eassumption.
Qed.
Theorem currMode_pres_bkwd (n n' : Network) (a : ActDiscNet) (m' : Mode) (i : nat) :
n -NA- a -NA> n' -> currModeNet m' i n' ->
exists m, currModeNet m i n. Admitted.
Theorem currMode_pres_fwd (n n' : Network) (a : ActDiscNet) (m : Mode) (i : nat) :
n -NA- a -NA> n' -> currModeNet m i n ->
exists m', currModeNet m' i n'. Admitted.
Theorem outgoing_del (n n' : Network) (d : Delay) (v : list BaseType) (t : Time) (i : nat) :
n -ND- d -ND> n' -> outgoing v t i n ->
{p : d <= t | outgoing v (minusTime t d p) i n'}. Admitted.
Corollary outgoing_del_contra (n n' : Network) (d : Delay)
(v : list BaseType) (i : nat) : n -ND- d -ND> n' -> outgoing v zeroTime i n -> False. intros.
addHyp (outgoing_del n n' d v zeroTime i H H0). invertClear H1.
eapply Rle_not_lt. apply x. simpl. delPos. Qed.
Theorem outgoing_disc_pres (n n' : Network) (a : ActDiscNet) (v : list BaseType) (t : Time) (i : nat) :
n -NA- a -NA> n' -> outgoing v t i n -> 0 < t ->
outgoing v t i n'. introz U.
inversion U0.
link_netentdiscfwd_tac e' b LE.
subst. econstructor; eassumption.
destr_ent_inter e' p' l' k' li' lo' ln'.
lets LEO : link_ent_outList LE1. or_flat.
subst. econstructor; eassumption.
ex_flat. or_flat.
econstructor. eassumption. eapply outList_in_input_pres;
eassumption.
econstructor. eassumption. eapply outList_in_output_pres;
eassumption. Qed.
Theorem incomingNetNotif_del (n n' : Network) (d : Delay) (v : list BaseType)
(t : Time) (i : nat) :
reachableNet n -> n -ND- d -ND> n' -> incomingNetNotif v t i n ->
{p : d <= t | incomingNetNotif v (minusTime t d p) i n'}.
intro RN. introz U. destruct U0.
link_netentdelfwd_tac e' Y. destr_ent_inter e' p' l' k' li' lo' ln'.
link_entinterdel_tac Y.
inversion_clear Y1.
Rleltcases d t IQ.
exists IQ. econstructor. apply Y.
eapply notifList_del_le. apply H3. assumption.
false. assert (noSync p {| li := li; lo := lo; ln := ln |} k d) as NSY. inversion Y0.
assumption. assert (p -PD- d -PD> p') as PDD. inversion Y0. assumption.
lets NS : NSY (chanAN ;? v). decompAnd2 NS NSN NSD.
remember ([|p, l, {| li := li; lo := lo; ln := ln |}, k|]) as e0.
timezerolteq t Q.
clear NSN. mkdel t Q d'. assert (d' < d) as DD. rewrite Heqd'. assumption.
Rlttoplus DD x DP. mkdel x DP0 d''. assert (d = d' +d+ d'') as ED.
rewrite Rplus_comm in DP. apply delayEqR. simpl. my_applys_eq DP.
f_equal. rewrite Heqd''. reflexivity.
lets TNX : timeSplit_net U ED. decompExAnd TNX n1 ND1 ND2.
link_netentdelfwd_tac e1 ED.
rewrite Heqe0 in ED1. destr_ent_inter e1 p1 l1 k1 li1 lo1 ln1.
link_entinterdel_tac U. inversion U0. assert (d' <= t) as DT. rewrite Heqd'.
simpl. apply Rle_refl.
lets ND : notifList_del_le DT H13 H0. assert (minusTime t d' DT = zeroTime) as TDZ.
apply timeEqR. simpl. rewrite Heqd'. simpl. ring. rewrite TDZ in ND. clear TDZ.
assert (p -PD- d' -PD> p1 /\ k -ms- d' -ms> k1 /\
{| li := li; lo := lo; ln := ln |} -i- d' -i> {| li := li1; lo := lo1; ln := ln1 |}).
inversion ED1; (repeat split); assumption. andflat HY.
lets NSF : NSD DD HY HY2 HY1.
unfold noSyncNow in NSF. assert (discActEnabled p1 (chanAN;? v)) as DAE.
apply listening_AN_prot. assert (listeningStateNet i n1) as LSN. eapply del_listening_net.
eapply reachNetDel. apply RN. apply ND1. apply ND2. apply ED0. inversion LSN as [e IV1 IV2].
inversion IV1 as [p4 l4 h4 k4 IV3 IV4]. my_applys_eq IV3. rewrite <- IV4 in IV2.
entnetuniq2 EU n1. inversion EU. reflexivity. apply NSF in DAE. decompAnd2 DAE DI DM.
apply DI. apply notif_timeout_enabled. assumption.
clear NSD. unfold noSyncNow in NSN. assert (discActEnabled p (chanAN;? v)) as DAE.
apply listening_AN_prot. assert (listeningStateNet i n) as LSN. eapply del_listening_net.
apply RN. apply U. apply H. inversion LSN. inversion H4. my_applys_eq H6.
cut (e = e0). intros. rewrite H8 in H7. rewrite Heqe0 in H7. inversion H7.
reflexivity. entnetuniq U e e0. assumption. apply NSN in DAE. decompAnd2 DAE DI DM.
apply DI. assert (t = zeroTime) as TZ. apply timeEqR. rewrite <- Q.
reflexivity. rewrite TZ in H0. apply notif_timeout_enabled. assumption. Qed.
Theorem incomingNetNotif_disc_pres (n n' : Network) (a : ActDiscNet) (v : list BaseType) (t : Time) (i : nat) :
n -NA- a -NA> n' -> incomingNetNotif v t i n -> 0 < t ->
incomingNetNotif v t i n'. Admitted.
Lemma inPos_del_bound_bkwd (n n' : Network) (d : Delay) (l' : Position) (i : nat) :
inPosNet l' i n' -> n -ND- d -ND> n' -> exists l,
inPosNet l i n /\ dist2d l l' <= speedMax * d. Admitted.
Conjecture currMode_intro : forall (m : Mode) (e : Entity) (i : nat) (n : Network),
m = currModeEnt e -> e @ i .: n -> currModeNet m i n.
Conjecture inPos_ex : forall (i : nat) (n : Network) (e : Entity),
e @ i .: n -> exists l, inPosNet l i n.
Conjecture distNet_intro : forall (e1 e2 : Entity) (i j : nat) (n : Network) (x : Distance),
e1 @ i .: n -> e2 @ j .: n -> x = mkDistance (dist2d e1 e2) -> distNet i j n x.
Conjecture inPos_pos : forall (e : Entity) (i : nat) (l : Position) (n : Network),
e @ i .: n -> inPosNet l i n -> posEnt e = l.
Conjecture reachable_net_ent : forall (n : Network) (e : Entity) (i : nat),
reachableNet n -> e @ i .: n -> reachableEnt e.
Conjecture disc_pres_distNet_bkwd : forall (n n' : Network) (a : ActDiscNet)
(i j : nat) (x : Distance),
n -NA- a -NA> n' -> distNet i j n' x -> distNet i j n x.
Conjecture del_link_distNet_bkwd : forall (n n' : Network) (d : Delay)
(i j : nat) (x' : Distance),
n -ND- d -ND> n' -> distNet i j n' x' ->
exists x, distNet i j n x /\ x <= x' + 2*speedMax*d.
Conjecture distNet_elim : forall (i j : nat) (n : Network) (x : Distance),
distNet i j n x -> exists e1 e2,
e1 @ i .: n /\ e2 @ j .: n /\ x = {| distance := dist2d e1 e2 |}.
Lemma del_net_ent (e : Entity) (i : nat) (n n' : Network) (d : Delay) :
e @ i .: n -> n -ND- d -ND> n' -> exists e', e -ED- d ->> e'.
intros. genDep2 i n'. induction n; intros n' H0 i H.
inversion H. inversion H0. inversion H.
eexists. eassumption. eapply IHn. eassumption.
eassumption. Qed.
Lemma inRange_acc_input (n n' : Network) (v : list BaseType) (l : Position)
(r : Distance) (i : nat) (e : Entity) :
n -NA- ([-v, l, r-]) /?: -NA> n' -> e @ i .: n -> dist2d l (posEnt e) <= r ->
exists e', e -EA- ([-v, l, r-]) #? ->> e' /\ e' @ i .: n'. Admitted.
Lemma inRange_out_input (n n' : Network) (v : list BaseType) (l : Position)
(r x: Distance) (i j : nat) (e : Entity) :
n -NA- ([-v, l, r-]) /! i -NA> n' -> e @ j .: n -> i <> j -> distNet i j n' x ->
x <= r -> exists e', e -EA- ([-v, l, r-]) #? ->> e' /\ e' @ j .: n'.
genDep3 n' i j. induction n; intros. inversion H0.
inversion H. Admitted.
Conjecture transGuard_disc_pres : forall (n n' : Network)
(a : ActDiscNet) (t : Time) (i : nat),
n -NA- a -NA> n' -> transGuard t i n -> transGuard t i n'.
Conjecture transGuard_elim : forall (t : Time) (i : nat) (n : Network),
transGuard t i n -> exists m m',
mState_in_net (<| m, m', t |>) i n.
Conjecture transGuard_intro : forall (t : Time) (i : nat) (n : Network)
(m m' : Mode), mState_in_net (<| m, m', t |>) i n ->
transGuard t i n.
Conjecture mState_disc_pres : forall (n n' : Network) (i : nat)
(a : ActDiscNet) (k : ModeState), n -NA- a -NA> n' -> mState_in_net k i n ->
exists k', mState_in_net k' i n'.
Conjecture transGuard_del : forall (n n' : Network)
(d : Delay) (t : Time) (i : nat),
n -ND- d -ND> n' -> transGuard t i n ->
exists p, transGuard (minusTime t d p) i n'.
Conjecture currModeNet_del_pres : forall (n n' : Network) (d : Delay)
(m : Mode) (i : nat), n -ND- d -ND> n' ->
(currModeNet m i n <-> currModeNet m i n').
Conjecture currModeNet_dec : forall (m : Mode) (i : nat) (n : Network),
currModeNet m i n \/ ~currModeNet m i n.
Lemma initial_failSafe (n : Network) (e : Entity) (i : nat) :
initialNet n -> e @ i .: n -> failSafe e.
introz U. generalize dependent i. induction n; intros i U0.
inversion U0. inversion U. subst. inversion U0. subst.
inversion H1. assumption. eapply IHn; eassumption. Qed.
Lemma curr_switch_ent_tau (n n' : Network) (a : ActDiscNet)
(e e' : Entity) (i : nat) (m m' : Mode) :
n -NA- a -NA> n' -> e @ i .: n -> e' @ i .: n' ->
currModeEnt e = m -> currModeEnt e' = m' -> m <> m' ->
e -EA- aeTau ->> e'. Admitted.
Lemma reachable_net_prot : forall (n : Network) (i : nat)
(p : ProcTerm) (l : Position) (h : Interface) (k : ModeState),
reachableNet n -> [|p, l, h, k|] @ i .: n ->
reachableProt p. Admitted.
Lemma currMode_del_pres_bkwd (n n' : Network) (d : Delay) (m : Mode) (i : nat) :
n -ND- d -ND> n' -> currModeNet m i n' -> currModeNet m i n. Admitted.
Conjecture inPos_ent_net : forall (l : Position) (e : Entity) (i : nat) (n : Network),
inPosEnt l e -> e @ i .: n -> inPosNet l i n.
Conjecture inPos_unique : forall (l l' : Position) (i : nat) (n : Network),
inPosNet l i n -> inPosNet l' i n -> l = l'.
Lemma outNet_incomingNetNotif (n n' : Network) (v : list BaseType) (r : Distance)
(l : Position) (i : nat) : n -NA- ([-v, l, r-]) /! i -NA> n' ->
incomingNetNotif ((baseDistance r)::v) adaptNotif i n'. Admitted.
n -ND- d -ND> n' -> nextSinceStateNet i n ->
exists m t x y, ovWaitStateNet m t (delToTime (x +dt+ d)) (delToTime (y +dt+ d)) i n. Admitted.
Lemma switchCurr_switchListen_net_link (n n' : Network) (i : nat)
(a : ActDiscNet) (e e' : Entity) :
switchCurrStateEnt e -> switchListenStateEnt e' ->
e @ i .: n -> e' @ i .: n' -> n -NA- a -NA> n' ->
a = anTau /\ interEnt e = interEnt e'. Admitted.
Lemma init_nextMode_net m i n :
reachableNet n -> initStateNet m i n -> nextModeNet m i n.
Admitted.
Lemma ovReady_prev_net_strong m t l n n' i a :
ovReadyStateNet m t l i n' -> n -NA- a -NA> n' ->
ovReadyStateNet m t l i n \/
(exists x0 y0, ovWaitStateNet m t x0 y0 i n).
Admitted.
Lemma ovWait_prev_net_strong m t x y n n' i a :
ovWaitStateNet m t x y i n' -> n -NA- a -NA> n' ->
ovWaitStateNet m t x y i n \/
(exists t0 l0, ovReadyStateNet m t0 l0 i n) \/
initStateNet m i n. Admitted.
Lemma nextMode_pres_fwd_net m i n n' a :
reachableNet n -> nextModeNet m i n ->
~(switchCurrStateNet i n \/ ovAbortStateNet i n \/
tfsCurrStateNet i n) ->
n -NA- a -NA> n' -> nextModeNet m i n'. Admitted.
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 ovReady_del_pres_bkwd_net n n' d m t l i :
n -ND- d -ND> n' -> ovReadyStateNet m t l i n' ->
ovReadyStateNet m t l i n. Admitted.
Lemma nextModeNet_del_pres n n' d m i :
n -ND- d -ND> n' -> nextModeNet m i n -> nextModeNet m i n'.
Admitted.
Lemma ovWait_ovReady_nextMode_net m t x y l i n :
reachableNet n -> ovWaitStateNet m t x y i n \/ ovReadyStateNet m t l i n ->
nextModeNet m i n.
introz U. genDep5 m t x y l. induction U; intros l y x t m; introz V.
Admitted.
Lemma ovWaitState_nextMode_net (n : Network) (m : Mode) (t x y : Time) (i : nat):
reachableNet n -> ovWaitStateNet m t x y i n -> nextModeNet m i n.
introz U. eapply ovWait_ovReady_nextMode_net with (l := mkPosition 0 0).
assumption. left. eassumption. Qed.
Theorem del_listening_net (n n' : Network) (d : Delay) (e : Entity) (i : nat) :
reachableNet n -> n -ND- d -ND> n' -> e @ i .: n -> listeningStateNet i n.
Admitted.
Theorem inPos_pres_disc (n n' : Network) (a : ActDiscNet) (l : Position) (i : nat) :
n -NA- a -NA> n' ->
(inPosNet l i n <-> inPosNet l i n').
introz U. split; introz U. destruct U0.
link_netentdiscfwd_tac e' b U. subst. econstructor; eassumption.
inversion U2; subst; econstructor; eassumption.
destruct U0.
link_netentdiscbkwd_tac e b U. subst. econstructor; eassumption.
inversion U2; subst; econstructor; eassumption.
Qed.
Theorem currMode_pres_bkwd (n n' : Network) (a : ActDiscNet) (m' : Mode) (i : nat) :
n -NA- a -NA> n' -> currModeNet m' i n' ->
exists m, currModeNet m i n. Admitted.
Theorem currMode_pres_fwd (n n' : Network) (a : ActDiscNet) (m : Mode) (i : nat) :
n -NA- a -NA> n' -> currModeNet m i n ->
exists m', currModeNet m' i n'. Admitted.
Theorem outgoing_del (n n' : Network) (d : Delay) (v : list BaseType) (t : Time) (i : nat) :
n -ND- d -ND> n' -> outgoing v t i n ->
{p : d <= t | outgoing v (minusTime t d p) i n'}. Admitted.
Corollary outgoing_del_contra (n n' : Network) (d : Delay)
(v : list BaseType) (i : nat) : n -ND- d -ND> n' -> outgoing v zeroTime i n -> False. intros.
addHyp (outgoing_del n n' d v zeroTime i H H0). invertClear H1.
eapply Rle_not_lt. apply x. simpl. delPos. Qed.
Theorem outgoing_disc_pres (n n' : Network) (a : ActDiscNet) (v : list BaseType) (t : Time) (i : nat) :
n -NA- a -NA> n' -> outgoing v t i n -> 0 < t ->
outgoing v t i n'. introz U.
inversion U0.
link_netentdiscfwd_tac e' b LE.
subst. econstructor; eassumption.
destr_ent_inter e' p' l' k' li' lo' ln'.
lets LEO : link_ent_outList LE1. or_flat.
subst. econstructor; eassumption.
ex_flat. or_flat.
econstructor. eassumption. eapply outList_in_input_pres;
eassumption.
econstructor. eassumption. eapply outList_in_output_pres;
eassumption. Qed.
Theorem incomingNetNotif_del (n n' : Network) (d : Delay) (v : list BaseType)
(t : Time) (i : nat) :
reachableNet n -> n -ND- d -ND> n' -> incomingNetNotif v t i n ->
{p : d <= t | incomingNetNotif v (minusTime t d p) i n'}.
intro RN. introz U. destruct U0.
link_netentdelfwd_tac e' Y. destr_ent_inter e' p' l' k' li' lo' ln'.
link_entinterdel_tac Y.
inversion_clear Y1.
Rleltcases d t IQ.
exists IQ. econstructor. apply Y.
eapply notifList_del_le. apply H3. assumption.
false. assert (noSync p {| li := li; lo := lo; ln := ln |} k d) as NSY. inversion Y0.
assumption. assert (p -PD- d -PD> p') as PDD. inversion Y0. assumption.
lets NS : NSY (chanAN ;? v). decompAnd2 NS NSN NSD.
remember ([|p, l, {| li := li; lo := lo; ln := ln |}, k|]) as e0.
timezerolteq t Q.
clear NSN. mkdel t Q d'. assert (d' < d) as DD. rewrite Heqd'. assumption.
Rlttoplus DD x DP. mkdel x DP0 d''. assert (d = d' +d+ d'') as ED.
rewrite Rplus_comm in DP. apply delayEqR. simpl. my_applys_eq DP.
f_equal. rewrite Heqd''. reflexivity.
lets TNX : timeSplit_net U ED. decompExAnd TNX n1 ND1 ND2.
link_netentdelfwd_tac e1 ED.
rewrite Heqe0 in ED1. destr_ent_inter e1 p1 l1 k1 li1 lo1 ln1.
link_entinterdel_tac U. inversion U0. assert (d' <= t) as DT. rewrite Heqd'.
simpl. apply Rle_refl.
lets ND : notifList_del_le DT H13 H0. assert (minusTime t d' DT = zeroTime) as TDZ.
apply timeEqR. simpl. rewrite Heqd'. simpl. ring. rewrite TDZ in ND. clear TDZ.
assert (p -PD- d' -PD> p1 /\ k -ms- d' -ms> k1 /\
{| li := li; lo := lo; ln := ln |} -i- d' -i> {| li := li1; lo := lo1; ln := ln1 |}).
inversion ED1; (repeat split); assumption. andflat HY.
lets NSF : NSD DD HY HY2 HY1.
unfold noSyncNow in NSF. assert (discActEnabled p1 (chanAN;? v)) as DAE.
apply listening_AN_prot. assert (listeningStateNet i n1) as LSN. eapply del_listening_net.
eapply reachNetDel. apply RN. apply ND1. apply ND2. apply ED0. inversion LSN as [e IV1 IV2].
inversion IV1 as [p4 l4 h4 k4 IV3 IV4]. my_applys_eq IV3. rewrite <- IV4 in IV2.
entnetuniq2 EU n1. inversion EU. reflexivity. apply NSF in DAE. decompAnd2 DAE DI DM.
apply DI. apply notif_timeout_enabled. assumption.
clear NSD. unfold noSyncNow in NSN. assert (discActEnabled p (chanAN;? v)) as DAE.
apply listening_AN_prot. assert (listeningStateNet i n) as LSN. eapply del_listening_net.
apply RN. apply U. apply H. inversion LSN. inversion H4. my_applys_eq H6.
cut (e = e0). intros. rewrite H8 in H7. rewrite Heqe0 in H7. inversion H7.
reflexivity. entnetuniq U e e0. assumption. apply NSN in DAE. decompAnd2 DAE DI DM.
apply DI. assert (t = zeroTime) as TZ. apply timeEqR. rewrite <- Q.
reflexivity. rewrite TZ in H0. apply notif_timeout_enabled. assumption. Qed.
Theorem incomingNetNotif_disc_pres (n n' : Network) (a : ActDiscNet) (v : list BaseType) (t : Time) (i : nat) :
n -NA- a -NA> n' -> incomingNetNotif v t i n -> 0 < t ->
incomingNetNotif v t i n'. Admitted.
Lemma inPos_del_bound_bkwd (n n' : Network) (d : Delay) (l' : Position) (i : nat) :
inPosNet l' i n' -> n -ND- d -ND> n' -> exists l,
inPosNet l i n /\ dist2d l l' <= speedMax * d. Admitted.
Conjecture currMode_intro : forall (m : Mode) (e : Entity) (i : nat) (n : Network),
m = currModeEnt e -> e @ i .: n -> currModeNet m i n.
Conjecture inPos_ex : forall (i : nat) (n : Network) (e : Entity),
e @ i .: n -> exists l, inPosNet l i n.
Conjecture distNet_intro : forall (e1 e2 : Entity) (i j : nat) (n : Network) (x : Distance),
e1 @ i .: n -> e2 @ j .: n -> x = mkDistance (dist2d e1 e2) -> distNet i j n x.
Conjecture inPos_pos : forall (e : Entity) (i : nat) (l : Position) (n : Network),
e @ i .: n -> inPosNet l i n -> posEnt e = l.
Conjecture reachable_net_ent : forall (n : Network) (e : Entity) (i : nat),
reachableNet n -> e @ i .: n -> reachableEnt e.
Conjecture disc_pres_distNet_bkwd : forall (n n' : Network) (a : ActDiscNet)
(i j : nat) (x : Distance),
n -NA- a -NA> n' -> distNet i j n' x -> distNet i j n x.
Conjecture del_link_distNet_bkwd : forall (n n' : Network) (d : Delay)
(i j : nat) (x' : Distance),
n -ND- d -ND> n' -> distNet i j n' x' ->
exists x, distNet i j n x /\ x <= x' + 2*speedMax*d.
Conjecture distNet_elim : forall (i j : nat) (n : Network) (x : Distance),
distNet i j n x -> exists e1 e2,
e1 @ i .: n /\ e2 @ j .: n /\ x = {| distance := dist2d e1 e2 |}.
Lemma del_net_ent (e : Entity) (i : nat) (n n' : Network) (d : Delay) :
e @ i .: n -> n -ND- d -ND> n' -> exists e', e -ED- d ->> e'.
intros. genDep2 i n'. induction n; intros n' H0 i H.
inversion H. inversion H0. inversion H.
eexists. eassumption. eapply IHn. eassumption.
eassumption. Qed.
Lemma inRange_acc_input (n n' : Network) (v : list BaseType) (l : Position)
(r : Distance) (i : nat) (e : Entity) :
n -NA- ([-v, l, r-]) /?: -NA> n' -> e @ i .: n -> dist2d l (posEnt e) <= r ->
exists e', e -EA- ([-v, l, r-]) #? ->> e' /\ e' @ i .: n'. Admitted.
Lemma inRange_out_input (n n' : Network) (v : list BaseType) (l : Position)
(r x: Distance) (i j : nat) (e : Entity) :
n -NA- ([-v, l, r-]) /! i -NA> n' -> e @ j .: n -> i <> j -> distNet i j n' x ->
x <= r -> exists e', e -EA- ([-v, l, r-]) #? ->> e' /\ e' @ j .: n'.
genDep3 n' i j. induction n; intros. inversion H0.
inversion H. Admitted.
Conjecture transGuard_disc_pres : forall (n n' : Network)
(a : ActDiscNet) (t : Time) (i : nat),
n -NA- a -NA> n' -> transGuard t i n -> transGuard t i n'.
Conjecture transGuard_elim : forall (t : Time) (i : nat) (n : Network),
transGuard t i n -> exists m m',
mState_in_net (<| m, m', t |>) i n.
Conjecture transGuard_intro : forall (t : Time) (i : nat) (n : Network)
(m m' : Mode), mState_in_net (<| m, m', t |>) i n ->
transGuard t i n.
Conjecture mState_disc_pres : forall (n n' : Network) (i : nat)
(a : ActDiscNet) (k : ModeState), n -NA- a -NA> n' -> mState_in_net k i n ->
exists k', mState_in_net k' i n'.
Conjecture transGuard_del : forall (n n' : Network)
(d : Delay) (t : Time) (i : nat),
n -ND- d -ND> n' -> transGuard t i n ->
exists p, transGuard (minusTime t d p) i n'.
Conjecture currModeNet_del_pres : forall (n n' : Network) (d : Delay)
(m : Mode) (i : nat), n -ND- d -ND> n' ->
(currModeNet m i n <-> currModeNet m i n').
Conjecture currModeNet_dec : forall (m : Mode) (i : nat) (n : Network),
currModeNet m i n \/ ~currModeNet m i n.
Lemma initial_failSafe (n : Network) (e : Entity) (i : nat) :
initialNet n -> e @ i .: n -> failSafe e.
introz U. generalize dependent i. induction n; intros i U0.
inversion U0. inversion U. subst. inversion U0. subst.
inversion H1. assumption. eapply IHn; eassumption. Qed.
Lemma curr_switch_ent_tau (n n' : Network) (a : ActDiscNet)
(e e' : Entity) (i : nat) (m m' : Mode) :
n -NA- a -NA> n' -> e @ i .: n -> e' @ i .: n' ->
currModeEnt e = m -> currModeEnt e' = m' -> m <> m' ->
e -EA- aeTau ->> e'. Admitted.
Lemma reachable_net_prot : forall (n : Network) (i : nat)
(p : ProcTerm) (l : Position) (h : Interface) (k : ModeState),
reachableNet n -> [|p, l, h, k|] @ i .: n ->
reachableProt p. Admitted.
Lemma currMode_del_pres_bkwd (n n' : Network) (d : Delay) (m : Mode) (i : nat) :
n -ND- d -ND> n' -> currModeNet m i n' -> currModeNet m i n. Admitted.
Conjecture inPos_ent_net : forall (l : Position) (e : Entity) (i : nat) (n : Network),
inPosEnt l e -> e @ i .: n -> inPosNet l i n.
Conjecture inPos_unique : forall (l l' : Position) (i : nat) (n : Network),
inPosNet l i n -> inPosNet l' i n -> l = l'.
Lemma outNet_incomingNetNotif (n n' : Network) (v : list BaseType) (r : Distance)
(l : Position) (i : nat) : n -NA- ([-v, l, r-]) /! i -NA> n' ->
incomingNetNotif ((baseDistance r)::v) adaptNotif i n'. Admitted.
Linking theorem.
Lemma incoming_net_ent (v : list BaseType) (i : nat) (n : Network) :
incomingNet v i n -> exists e, incomingEnt v e /\ e @ i .: n. intro U.
invertClear U. exists ([|p, l, {| li := li; lo := lo; ln := ln |}, k|]).
split. repeat constructor. assumption. assumption. Qed.
incomingNet v i n -> exists e, incomingEnt v e /\ e @ i .: n. intro U.
invertClear U. exists ([|p, l, {| li := li; lo := lo; ln := ln |}, k|]).
split. repeat constructor. assumption. assumption. Qed.
Linking theorem.
Lemma incoming_ent_net (v : list BaseType) (e : Entity) (i : nat) (n : Network) :
incomingEnt v e -> e @ i .: n -> incomingNet v i n.
introz U. inversion U. subst. destruct h. econstructor. eassumption.
inversion U. subst. inversion H1. assumption. Qed.
Ltac inposdp :=
match goal with
[ w : ?n -NA- _ -NA> ?n', H : inPosNet ?l ?i ?n' |- inPosNet ?l ?i ?n] =>
eapply inPos_pres_disc; [apply w | assumption]
end.
Lemma net_del_elim q q0 q1 l h k i n n' d :
[|q $||$ q0 $||$ q1, l, h, k|] @ i .: n ->
n -ND- d -ND> n' ->
exists q' q0' q1' l' h' k',
[|q' $||$ q0' $||$ q1', l', h', k'|] @ i .: n' /\
q -PD- d -PD> q' /\ q0 -PD- d -PD> q0' /\ q1 -PD- d -PD> q1' /\
h -i- d -i> h' /\ k -ms- d -ms> k' /\
dist2d l l' <= speedMax * d. Admitted.
Conjecture currMode_ent_ex : forall (m : Mode) (i : nat) (n : Network),
currModeNet m i n <-> exists e, e @ i .: n /\ currModeEnt e = m.
Conjecture nextMode_ent_ex : forall (m : Mode) (i : nat) (n : Network),
nextModeNet m i n <-> exists e, e @ i .: n /\ nextModeEnt m e.
Ltac currMode_ent_ex_tac e U :=
let Q := fresh in let U1 := fresh U in let U2 := fresh U in
match goal with
[H : currModeNet ?m ?i ?n |- _ ] => lets Q : H; rewrite currMode_ent_ex in Q;
decompExAnd Q e U1 U2
end.
Ltac nextMode_ent_ex_tac e U :=
let Q := fresh in let U1 := fresh U in let U2 := fresh U in
match goal with
[H : nextModeNet ?m ?i ?n |- _ ] => lets Q : H; rewrite nextMode_ent_ex in Q;
decompExAnd Q e U1 U2
end.
Lemma mState_in_net_unique k k' i n :
mState_in_net k i n -> mState_in_net k' i n -> k = k'.
intros. inversion H. inversion H0. entnetuniq2 EN n.
inversion EN. reflexivity. Qed.
incomingEnt v e -> e @ i .: n -> incomingNet v i n.
introz U. inversion U. subst. destruct h. econstructor. eassumption.
inversion U. subst. inversion H1. assumption. Qed.
Ltac inposdp :=
match goal with
[ w : ?n -NA- _ -NA> ?n', H : inPosNet ?l ?i ?n' |- inPosNet ?l ?i ?n] =>
eapply inPos_pres_disc; [apply w | assumption]
end.
Lemma net_del_elim q q0 q1 l h k i n n' d :
[|q $||$ q0 $||$ q1, l, h, k|] @ i .: n ->
n -ND- d -ND> n' ->
exists q' q0' q1' l' h' k',
[|q' $||$ q0' $||$ q1', l', h', k'|] @ i .: n' /\
q -PD- d -PD> q' /\ q0 -PD- d -PD> q0' /\ q1 -PD- d -PD> q1' /\
h -i- d -i> h' /\ k -ms- d -ms> k' /\
dist2d l l' <= speedMax * d. Admitted.
Conjecture currMode_ent_ex : forall (m : Mode) (i : nat) (n : Network),
currModeNet m i n <-> exists e, e @ i .: n /\ currModeEnt e = m.
Conjecture nextMode_ent_ex : forall (m : Mode) (i : nat) (n : Network),
nextModeNet m i n <-> exists e, e @ i .: n /\ nextModeEnt m e.
Ltac currMode_ent_ex_tac e U :=
let Q := fresh in let U1 := fresh U in let U2 := fresh U in
match goal with
[H : currModeNet ?m ?i ?n |- _ ] => lets Q : H; rewrite currMode_ent_ex in Q;
decompExAnd Q e U1 U2
end.
Ltac nextMode_ent_ex_tac e U :=
let Q := fresh in let U1 := fresh U in let U2 := fresh U in
match goal with
[H : nextModeNet ?m ?i ?n |- _ ] => lets Q : H; rewrite nextMode_ent_ex in Q;
decompExAnd Q e U1 U2
end.
Lemma mState_in_net_unique k k' i n :
mState_in_net k i n -> mState_in_net k' i n -> k = k'.
intros. inversion H. inversion H0. entnetuniq2 EN n.
inversion EN. reflexivity. Qed.
Given a network state predicate as the goal and the corresponding
entity state predicate in the hypotheses, this solves things using
lenWitness.
Ltac netState_ent_net_tac := eapply lenWitness;
[eassumption | eassumption].
Lemma tfsNext_currModeNet_eq m1 m2 i n : currModeNet m1 i n ->
tfsNextStateNet m2 i n -> m1 = m2. Admitted.
[eassumption | eassumption].
Lemma tfsNext_currModeNet_eq m1 m2 i n : currModeNet m1 i n ->
tfsNextStateNet m2 i n -> m1 = m2. Admitted.
The nextSinceState relation can be broken down into the following cases.
Lemma nexSinceStateNet_cases i n :
nextSinceStateNet i n ->
(exists m t x y, ovWaitStateNet m t x y i n) \/
(exists m t l, ovReadyStateNet m t l i n) \/
(exists m, switchBcStateNet m i n) \/
(switchCurrStateNet i n). intros. inversion H.
inversion H0. inversion H2. subst. inversion H4.
left. Admitted.
Lemma link_net_ent_disc :
forall (n n' : Network) (e e' : Entity) (i : nat) (a : ActDiscNet),
n -NA- a -NA> n' -> e @ i .: n -> e' @ i .: n'->
(e = e' \/ (exists a', e -EA- a' ->> e')). Admitted.
Ltac link_netentdisc_tac b :=
match goal with
| [ U1 : ?n -NA- ?a -NA> ?n', U2 : ?e @ ?i .: ?n,
U3 : ?e' @ ?i .: ?n' |- _] =>
let H1 := fresh in lets H1 : link_net_ent_disc U1 U2 U3;
let H2 := fresh in let H3 := fresh in
elim_intro H1 H2 H3; [subst_all H2 |
let H4 := fresh in invertClearAs2 H3 b H4]
end.
nextSinceStateNet i n ->
(exists m t x y, ovWaitStateNet m t x y i n) \/
(exists m t l, ovReadyStateNet m t l i n) \/
(exists m, switchBcStateNet m i n) \/
(switchCurrStateNet i n). intros. inversion H.
inversion H0. inversion H2. subst. inversion H4.
left. Admitted.
Lemma link_net_ent_disc :
forall (n n' : Network) (e e' : Entity) (i : nat) (a : ActDiscNet),
n -NA- a -NA> n' -> e @ i .: n -> e' @ i .: n'->
(e = e' \/ (exists a', e -EA- a' ->> e')). Admitted.
Ltac link_netentdisc_tac b :=
match goal with
| [ U1 : ?n -NA- ?a -NA> ?n', U2 : ?e @ ?i .: ?n,
U3 : ?e' @ ?i .: ?n' |- _] =>
let H1 := fresh in lets H1 : link_net_ent_disc U1 U2 U3;
let H2 := fresh in let H3 := fresh in
elim_intro H1 H2 H3; [subst_all H2 |
let H4 := fresh in invertClearAs2 H3 b H4]
end.
Does some pre-processing on the proof of a backracking theorem at the
network level. Works where the backtracking has two predecessor cases.
Probably needs to be slightly altered if there's a need to handle more cases.
Ltac backtrack_net_pre U :=
let U1 := fresh in let e := fresh "e" in let b := fresh "b" in
state_pred_net_destr U; link_netentdiscbkwd_tac0 e b U1;
let EQ := fresh "EQ" in let EX := fresh in
match goal with [U2 : _ \/ _ |- _ ] =>
elim_intro U2 EQ EX; [left; econstructor | ];
[eassumption | | ]; [ subst; assumption | ex_flat] end.
let U1 := fresh in let e := fresh "e" in let b := fresh "b" in
state_pred_net_destr U; link_netentdiscbkwd_tac0 e b U1;
let EQ := fresh "EQ" in let EX := fresh in
match goal with [U2 : _ \/ _ |- _ ] =>
elim_intro U2 EQ EX; [left; econstructor | ];
[eassumption | | ]; [ subst; assumption | ex_flat] end.
Tactic for eliminating two contradictory state predicates H and H1
Ltac state_pred_elim_net H H1 :=
let e := fresh "e" in let e' := fresh "e'" in
let U1 := fresh in let U2 := fresh in let U3 := fresh in
let U1' := fresh in let U2' := fresh in
inversion H as [e U1 U2]; inversion H1 as [e' U1' U2'];
assert (e' = e) as U3;[eapply entInNetUnique; eassumption | ];
subst_all U3; destruct e as [p0 l0 h0 k0]; inversion U1;
inversion U1'; subst;
match goal with [SP1 : context[p0], SP2 : context[p0] |- _] =>
inversion SP1; inversion SP2 end; subst;
match goal with [PT : _ $||$ _ $||$ _ = ?p1 $||$ ?p2 $||$ ?p3 |- _] =>
inversion PT; subst;
repeat match goal with [PT : context[_ $||$ _ $||$ _] |- _] =>
clear PT end;
match goal with
| [SP1 : context[p1], SP2 : context[p1] |- _] =>
inversion SP1; subst; inversion SP2
| [SP1 : context[p2], SP2 : context[p2] |- _] =>
inversion SP1; subst; inversion SP2
| [SP1 : context[p3], SP2 : context[p3] |- _] =>
inversion SP1; subst; inversion SP2
end
end.
Lemma tfsStart_prev_net i n n' a : tfsStartStateNet i n' ->
n -NA- a -NA> n' -> tfsStartStateNet i n \/
exists m t x y, ovWaitStateNet m t x y i n.
Admitted.
Lemma ovReady_prev_net m t l i n n' a :
ovReadyStateNet m t l i n' -> n -NA- a -NA> n' ->
ovReadyStateNet m t l i n \/
exists x y, ovWaitStateNet m t x y i n. Admitted.
Lemma ovWait_del_pres_net m t x y i n n' d : n -ND- d -ND> n' ->
(ovWaitStateNet m t x y i n <-> ovWaitStateNet m t x y i n'). Admitted.
Lemma tfsNext_prev_net m i n n' a : tfsNextStateNet m i n' ->
n -NA- a -NA> n' -> tfsNextStateNet m i n \/ tfsStartStateNet i n.
intros.
backtrack_net_pre H.
lets TPE : tfsNext_prev_ent H1 H5.
elim_intro TPE TN TS;[left | right]; netState_ent_net_tac.
Qed.
Lemma del_pres_bkwd_tfsNext m i n n' d :
n -ND- d -ND> n' -> tfsNextStateNet m i n' -> tfsNextStateNet m i n.
Admitted.
Lemma del_pres_bkwd_tfsStart i n n' d :
n -ND- d -ND> n' -> tfsStartStateNet i n' -> tfsStartStateNet i n.
Admitted.
Lemma tfsNext_urgent_net m i n n' d :
tfsNextStateNet m i n -> n -ND- d -ND> n' -> False.
Admitted.
Lemma tfsStart_urgent_net i n n' d :
tfsStartStateNet i n -> n -ND- d -ND> n' -> False.
Admitted.
Lemma ovReady_wait_track_net m t l i m' t' x y n n' a :
ovReadyStateNet m t l i n -> ovWaitStateNet m' t' x y i n' ->
n -NA- a -NA> n' -> m = m' /\
(exists p, t' = minusTime t (period m) p) /\ x = t' /\ y = period m.
Admitted.
Lemma ovWait_track_net m m' t t' x x' y y' i n n' a :
ovWaitStateNet m t x y i n -> ovWaitStateNet m' t' x' y' i n' ->
n -NA- a -NA> n' -> m = m' /\ t = t' /\ x = x' /\ y = y'. Admitted.
Lemma ovWait_prev_net m t x y i n n' a : ovWaitStateNet m t x y i n' ->
n -NA- a -NA> n' ->
ovWaitStateNet m t x y i n \/
(exists l, ovReadyStateNet m (t +t+ period m) l i n) \/
initStateNet m i n.
Admitted.
Ltac reach_net_prot_tac :=
match goal with [RN : reachableNet ?n,
EIN : [|_, _, _, _|] @ _ .: ?n |- _] =>
let RNP := fresh "RNP" in
let RPT := fresh "RPT" in
lets RNP : reachable_net_prot RN EIN;
lets RPT : reachableProt_triple RNP end.
let e := fresh "e" in let e' := fresh "e'" in
let U1 := fresh in let U2 := fresh in let U3 := fresh in
let U1' := fresh in let U2' := fresh in
inversion H as [e U1 U2]; inversion H1 as [e' U1' U2'];
assert (e' = e) as U3;[eapply entInNetUnique; eassumption | ];
subst_all U3; destruct e as [p0 l0 h0 k0]; inversion U1;
inversion U1'; subst;
match goal with [SP1 : context[p0], SP2 : context[p0] |- _] =>
inversion SP1; inversion SP2 end; subst;
match goal with [PT : _ $||$ _ $||$ _ = ?p1 $||$ ?p2 $||$ ?p3 |- _] =>
inversion PT; subst;
repeat match goal with [PT : context[_ $||$ _ $||$ _] |- _] =>
clear PT end;
match goal with
| [SP1 : context[p1], SP2 : context[p1] |- _] =>
inversion SP1; subst; inversion SP2
| [SP1 : context[p2], SP2 : context[p2] |- _] =>
inversion SP1; subst; inversion SP2
| [SP1 : context[p3], SP2 : context[p3] |- _] =>
inversion SP1; subst; inversion SP2
end
end.
Lemma tfsStart_prev_net i n n' a : tfsStartStateNet i n' ->
n -NA- a -NA> n' -> tfsStartStateNet i n \/
exists m t x y, ovWaitStateNet m t x y i n.
Admitted.
Lemma ovReady_prev_net m t l i n n' a :
ovReadyStateNet m t l i n' -> n -NA- a -NA> n' ->
ovReadyStateNet m t l i n \/
exists x y, ovWaitStateNet m t x y i n. Admitted.
Lemma ovWait_del_pres_net m t x y i n n' d : n -ND- d -ND> n' ->
(ovWaitStateNet m t x y i n <-> ovWaitStateNet m t x y i n'). Admitted.
Lemma tfsNext_prev_net m i n n' a : tfsNextStateNet m i n' ->
n -NA- a -NA> n' -> tfsNextStateNet m i n \/ tfsStartStateNet i n.
intros.
backtrack_net_pre H.
lets TPE : tfsNext_prev_ent H1 H5.
elim_intro TPE TN TS;[left | right]; netState_ent_net_tac.
Qed.
Lemma del_pres_bkwd_tfsNext m i n n' d :
n -ND- d -ND> n' -> tfsNextStateNet m i n' -> tfsNextStateNet m i n.
Admitted.
Lemma del_pres_bkwd_tfsStart i n n' d :
n -ND- d -ND> n' -> tfsStartStateNet i n' -> tfsStartStateNet i n.
Admitted.
Lemma tfsNext_urgent_net m i n n' d :
tfsNextStateNet m i n -> n -ND- d -ND> n' -> False.
Admitted.
Lemma tfsStart_urgent_net i n n' d :
tfsStartStateNet i n -> n -ND- d -ND> n' -> False.
Admitted.
Lemma ovReady_wait_track_net m t l i m' t' x y n n' a :
ovReadyStateNet m t l i n -> ovWaitStateNet m' t' x y i n' ->
n -NA- a -NA> n' -> m = m' /\
(exists p, t' = minusTime t (period m) p) /\ x = t' /\ y = period m.
Admitted.
Lemma ovWait_track_net m m' t t' x x' y y' i n n' a :
ovWaitStateNet m t x y i n -> ovWaitStateNet m' t' x' y' i n' ->
n -NA- a -NA> n' -> m = m' /\ t = t' /\ x = x' /\ y = y'. Admitted.
Lemma ovWait_prev_net m t x y i n n' a : ovWaitStateNet m t x y i n' ->
n -NA- a -NA> n' ->
ovWaitStateNet m t x y i n \/
(exists l, ovReadyStateNet m (t +t+ period m) l i n) \/
initStateNet m i n.
Admitted.
Ltac reach_net_prot_tac :=
match goal with [RN : reachableNet ?n,
EIN : [|_, _, _, _|] @ _ .: ?n |- _] =>
let RNP := fresh "RNP" in
let RPT := fresh "RPT" in
lets RNP : reachable_net_prot RN EIN;
lets RPT : reachableProt_triple RNP end.
This page has been generated by coqdoc