Library NARMisc

Require Import Program.Equality.
Require Import ComhCoq.Extras.LibTactics.


Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.ProtAuxResults.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.ProtAuxResults.

Lemma state_disj_paused_notifAbort i n :
  pausedStateNet i n -> notifAbortPathNet i n -> False. Admitted.
Lemma state_disj_tfsCurr_start : forall (i : nat) (n : Network),
  tfsCurrStateNet i n -> tfsStartStateNet i n -> False. Admitted.
Lemma state_disj_tfsCurr_bc : forall (i : nat) (n : Network),
  tfsCurrStateNet i n -> tfsBcStateNet i n -> False. Admitted.
Lemma state_disj_tfsCurr_switchListen : forall (i : nat) (n : Network),
  tfsCurrStateNet i n -> switchListenStateNet i n -> False. Admitted.
Lemma init_nextMode_net m i n :
  initStateNet m i n -> nextModeNet m i n. Admitted. Lemma ovWait_ovReady_nextMode_net i n (p : reachableNet n) :
  (forall m t x y, ovWaitStateNet m t x y i n ->
   nextModeNet m i n) /\
  (forall m t l, ovReadyStateNet m t l i n -> nextModeNet m i n).
  Admitted. Lemma switchBc_nextMode_net m i n :
  switchBcStateNet m i n -> nextModeNet m i n. Admitted. Lemma switchCurr_nextSince_nextMode_net m t i n p :
  nextSince m t i n p ->
  switchCurrStateNet i n -> nextModeNet m i n. Admitted.
Lemma nextSince_switchBc_modeEq m m' t i n p :
  nextSince m t i n p -> switchBcStateNet m' i n -> m = m'.
  Admitted.
Lemma nextSince_ovWait_modeEq m m' t t' x y i n p :
  nextSince m t i n p -> ovWaitStateNet m' t' x y i n -> m = m'.
  Admitted. Lemma nextSince_ovReaddy_modeEq m m' t t' l i n p :
  nextSince m t i n p -> ovReadyStateNet m' t' l i n -> m = m'.
  Admitted.
Theorem tfs_rel_state (n : Network) (m : Mode) (t : Time) (i : nat)
  (p : reachableNet n) : tfs m t i n p -> tfsStateNet i n .
  intros.
  induction H.
  invertClear H. econstructor;[ |apply H2]. invertClear H1.
  constructor. invertClear H. repeat constructor.
  Admitted.
Lemma tfsStart_tfs_zero : forall (n : Network) (t : Time)
  (i : nat) (m : Mode) (p : reachableNet n),
  tfs m t i n p -> tfsStartStateNet i n -> t = zeroTime.
  intros. induction p. initNet_contra H0.
  dependent destruction H. reflexivity.
  Admitted.
Lemma tfsNext_tfs_zero : forall (n : Network) (t : Time)
  (i : nat) (m : Mode) (p : reachableNet n),
  tfs m t i n p -> tfsNextStateNet m i n -> t = zeroTime.
  intros. induction p. initNet_contra H0.
  Admitted.
Lemma currModeNet_switch_states n n' a m m' i :
  reachableNet n -> n -NA- a -NA> n' -> currModeNet m i n ->
  currModeNet m' i n' -> m <> m' ->
  (switchCurrStateNet i n /\ switchListenStateNet i n') \/
  (tfsCurrStateNet i n /\ tfsBcStateNet i n'). Admitted.
Lemma tfsNext_tfs_mode_eq : forall (n : Network) (t : Time)
  (i : nat) (m1 m2 : Mode) (p : reachableNet n),
  tfs m1 t i n p -> tfsNextStateNet m2 i n -> m1 = m2.
  Admitted.
Theorem nextSince_rel_state (n : Network) (m : Mode) (t : Time) (i : nat)
  (p : reachableNet n) : nextSince m t i n p -> nextSinceStateNet i n.
  intro U. induction U.
  netprottrip H1 U q l0 h k.
  dofirst4 econstructor. apply U0. apply U.
  assumption.
  netprottrip IHU U q l h k.
  lets DX : net_del_elim U0 w. decompEx6 DX q' q0' q1' l' h' k' DE.
  andflat Q. dofirst3 econstructor. eapply del_pres_nextSinceState.
  apply U1. apply Q0. apply Q. Qed.

Lemma nextSince_next : forall (m : Mode) (t : Time) (i : nat)
  (n : Network) (p : reachableNet n),
  nextSince m t i n p -> nextModeNet m i n.
  intros. lets NSR : nextSince_rel_state H.
  lets NSC : nexSinceStateNet_cases NSR.
  lets OON : ovWait_ovReady_nextMode_net i n p. andflat OON.
  elimOr4 NSC NSC; ex_flat.
  eapply OON0. replace m with x. eassumption. symmetry.
  eapply nextSince_ovWait_modeEq; eassumption.
  eapply OON1. replace m with x. eassumption. symmetry.
  eapply nextSince_ovReaddy_modeEq; eassumption.
  eapply switchBc_nextMode_net. replace m with x. eassumption. symmetry.
  eapply nextSince_switchBc_modeEq; eassumption.
  eapply switchCurr_nextSince_nextMode_net; eassumption.
  Qed.

Theorem delivered_received (n : Network) (v : list BaseType) (t : Time) (r x : Distance)
  (i j : nat) (p : reachableNet n) (l : Position) :
  delivered ([-v, l, r-]) t i n p -> i <> j ->
  distNet i j n x -> x + 2*speedMax*t <= r -> received v t j n p.
  intros. generalize dependent x.
  induction H; intros.
  simpl in H1. rewrite Rmult_0_r in H2. rewrite Rplus_0_r in H2.
  addHyp (distNet_elim i j n' x H1). decompose [ex] H. clear H. decompose [and] H4.
  clear H4. rename x0 into e1'. rename x1 into e2'.
  addHyp (link_net_ent_disc_bkwd n n' e2' j (([-v, l, r-]) /! i) w H5).
  decompExAnd H3 e2 H4 Q.
  addHyp (inRange_out_input n n' v l r x i j e2 w H4 H0 H1 H2).
  invertClear H3. invertClear H7.
  eapply receivedBase. apply H4. apply H8. apply H3.
  addHyp (disc_pres_distNet_bkwd n n' a i j x w H1).
  constructor. apply (IHdelivered H0 x);assumption.
  remember (reachNetDel n n' d p w) as p'.
  assert (delivered ([-v, l, r-]) (t +dt+ d) i n' p'). rewrite Heqp'. constructor.
  assumption.
  rename x into x'.
  assert (nonneg (distance x') +
  2 * nonneg speedMax * nonneg (time t) + 2 * nonneg speedMax * pos (delay d)
  <= nonneg (distance r)). rewrite Rmult_assoc in H2. simpl in H2.
  repeat rewrite Rmult_plus_distr_l in H2. rewrite <- Rplus_assoc in H2.
  repeat rewrite <- Rmult_assoc in H2. assumption.
  addHyp (del_link_distNet_bkwd n n' d i j x' w H1). invertClear H5.
  invertClear H6.
  apply (Rplus_le_compat_r (2*speedMax*t)) in H7.
  assert (x + 2 * speedMax * t <= r). eapply Rle_trans. apply H7.
  eapply Rle_trans;[ |apply H2]. apply Req_le. simpl. ring.
  assert (received v t j n p). apply (IHdelivered H0 x); assumption.
  rewrite Heqp'. constructor. assumption.
  Qed.

Theorem currSince_curr (n : Network) (m : Mode) (t : Time) (i : nat)
  (p : reachableNet n) : currSince m t i n p -> currModeNet m i n.
  intros.
  induction H.
  eapply switch_states_mState; try apply w; try assumption. eapply nextSince_next.
  apply H.
  assumption.
  erewrite <- currModeNet_del_pres. apply IHcurrSince. apply w.
  Qed.

Theorem tfs_transGuard (n : Network) (m : Mode) (t : Time) (i : nat)
  (p : reachableNet n) :
  tfsCurrStateNet i n -> tfs m t i n p ->
  exists t', transGuard t' i n /\ t + t' <= trans m.
  intros.
  induction H0.
  apply False_ind. eapply state_disj_tfsCurr_start. apply H. assumption.
  addHyp (tfsCurrNet_dec i n). invertClear H2.
  apply IHtfs in H3. invertClear H3. rename x into t'. invertClear H2.
  exists t'. split;[ |assumption].
  addHyp (transGuard_elim t' i n H3). decompose [ex] H2. rename x into m1.
  rename x0 into m2.
  remember (<| m1, m2, t' |>) as k. addHyp (mState_disc_pres n n' i a k w H6).
  invertClear H5. rename x into k'.
  addHyp (eqDecModeState k k'). invertClear H5.
  eapply transGuard_intro. rewrite <- H8 in H7. rewrite Heqk in H7. apply H7.
  apply False_ind. lets H5 : mState_switch_states p H8 w H6 H7.
  invertClear H5; invertClear H9. eapply state_disj_tfsCurr_bc. apply H.
  assumption. eapply state_disj_tfsCurr_switchListen. apply H. assumption.
  addHyp (tfsCurrStateNet_bktrk_net n n' i a H w). invertClear H2. contradiction H3.
  decompose [ex] H4. clear H4. rename x into m1. rename x0 into mF.
  decompose [and] H2. clear H2.
  addHyp (tfsNext_tfs_mode_eq n t i m m1 p H0 H4). rewrite <- H2 in H4.
  addHyp (tfsNext_tfs_zero n t i m p H0 H4). rewrite H5. simpl.
  exists (modeTransTime m1 mF x1). rewrite Rplus_0_l.
  generalize dependent x1. rewrite <- H2. intros. split.
  eapply transGuard_intro. apply H7. apply modeTransTime_bound.
  addHyp (tfsCurrState_del_pres_net n n' d i w). addHyp H. rewrite <- H1 in H2.
  apply IHtfs in H2. invertClear H2. rename x into t'. invertClear H3.
  addHyp (transGuard_del n n' d t' i w H2). invertClear H3.
  remember (minusTime t' d x) as t0. exists t0. split. assumption.
  rewrite Heqt0. eapply Rle_trans;[ |apply H4]. apply Req_le.
  simpl. ring. Qed.


Theorem tfs_bound (n : Network) (m : Mode) (t : Time) (i : nat)
  (p : reachableNet n) : tfs m t i n p -> t <= trans m.
  intros.
  generalize dependent t. induction p; intros.
  dependent destruction H. simpl. timeNonneg.
  dependent destruction H. simpl. timeNonneg.
  apply IHp. assumption. addHyp H. rename H0 into Q.
  remember (reachNetDel n n' d p s) as p'. rewrite Heqp' in H.
  dependent destruction H. simpl. timeNonneg.
  addHyp (tfs_rel_state n m t i p H). invertClear H0. invertClear H1.
  invertClear H0. rewrite <- H4 in H3.
  addHyp (del_net_ent e i n n' d H2 s). rewrite <- H3 in H2.
  invertClear H0. rename x into e'. rewrite <- H3 in H5.
  invertClear H1.
  Admitted.
Theorem outgoing_timeout_disc (n n' : Network) (a : ActDiscNet) (i : nat)
  (p : reachableNet n) (w : n -NA- a -NA> n') (v : list BaseType) (l : Position) :
  outgoing v zeroTime i n ->
  outgoing v zeroTime i n' \/
  exists r, delivered ([-v, l, r-]) zeroTime i n' (reachNetDisc n n' a p w).
  introz U.
  destruct a.
  destruct m as [v' l' r'].
  Admitted.
Lemma notifAbortPathNet_urgent (i : nat) (n n' : Network) (d : Delay) :
  reachableNet n -> notifAbortPathNet i n -> n -ND- d -ND> n' -> False. Admitted.
Lemma notifBadPathNet_urgent i n n' d :
  notifBadPathNet i n -> n -ND- d -ND> n' -> False. Admitted.
Lemma msgBadPathNet_urgent (n n' : Network) (d : Delay) (i : nat) :
  msgBadPathNet i n -> n -ND- d -ND> n' -> False. Admitted.
Lemma msgAbort_paused_disj_net (i : nat) (n : Network) :
  msgAbortPathNet i n -> pausedStateNet i n -> False.
  introz U. inversion U. inversion U0. entnetuniq EN e e0.
  subst. clear H0. inversion H1. subst. inversion H; subst.
  Admitted.

Lemma tfsState_not_currSince (m : Mode) (t : Time) (i : nat) (n n' : Network)
  (p : reachableNet n) (a : ActDiscNet) (w : n -NA- a -NA> n') :
  tfsStateNet i n -> ~tfsStateNet i n' -> ~currSince m t i n p. Admitted.
Lemma msgBad_disc_net (n n' : Network) (a : ActDiscNet) (i : nat) (m : Mode)
  (p : reachableNet n) (w : n -NA- a -NA> n') :
  msgBadPathNet i n -> currModeNet m i n ->
  msgBadPathNet i n' \/ tfs m zeroTime i n' (reachNetDisc n n' a p w). Admitted.

Lemma tfs_zero_disc_pres (n n' : Network) (a : ActDiscNet) (i : nat) (m : Mode)
  (p : reachableNet n) (w : n -NA- a -NA> n') :
  tfs m zeroTime i n p ->
  tfs m zeroTime i n' (reachNetDisc n n' a p w). Admitted.
Lemma ovWait_nextSince_time (n : Network) (m : Mode) (x y t t1: Time) (i : nat)
  (p : reachableNet n) :
  ovWaitStateNet m t x y i n -> nextSince m t1 i n p -> period m - y <= t1.
  intros OW NS. generalize dependent OW. induction NS; intro OW.
  lets OWT : ovReady_wait_track_net H0 H1 w. andflat EQ.
  invertClearAs2 EQ1 pr EQM. subst. clear EQ.
  Admitted.
Lemma nextSince_ovWait_modes_eq (n : Network) (m1 m2 : Mode) (t t1 x y : Time)
  (i : nat) (p : reachableNet n) :
  ovWaitStateNet m1 t x y i n -> nextSince m2 t1 i n p -> m1 = m2. Admitted.
Lemma bcWait_bktrk_net (n n' : Network) (m : Mode) (x : Time)
  (i : nat) (a : ActDiscNet) (p : reachableNet n) :
  bcWaitStateNet m x i n' -> n -NA- a -NA> n' ->
  bcWaitStateNet m x i n \/ (sleepingStateNet i n /\ x = zeroTime) \/
  (exists l, bcReadyStateNet m l i n /\ x = period m /\
  sent [baseMode m, basePosition l] zeroTime i n p). Admitted.
Lemma msgAbortPathNet_urgent i n n' d :
  reachableNet n -> msgAbortPathNet i n -> n -ND- d -ND> n' -> False.
  intros. inversion H. link_netentdelfwd_tac e' LD.
  assert (reachableEnt e) as RE. eapply reachable_net_ent; eassumption.
  eapply msgAbortPathEnt_urgent; eassumption. Qed.

Lemma notifBadPathNet_cases m i n :
  notifBadPathNet i n -> currModeNet m i n ->
  rangeBadStateNet m i n \/
  badOvlpStateNet i n.
  intros. rename H0 into CMN. inversion H.
  inversion H0.
  apply currMode_ent_ex in CMN. ex_flat. and_flat.
  subst. entnetuniq2 EN n. subst.
  left. eexists;[ | apply H1]. simpl.
  econstructor. assumption.
  subst. right. econstructor;[ | apply H1]. subst.
  constructor. assumption. Qed.

Lemma rangeBad_notifBad_net m i n :
  rangeBadStateNet m i n -> notifBadPathNet i n.
  Admitted.
Lemma badOvlp_notifBad_net i n :
  badOvlpStateNet i n -> notifBadPathNet i n.
  Admitted.
Lemma ovReady_nextSince_state m t l i n :
  ovReadyStateNet m t l i n -> nextSinceStateNet i n.
  Admitted.