Library NARMsgPosition

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.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.NARMisc.

Open Scope R_scope.

Theorem sent_outgoing (n : Network) (v : list BaseType) (t : Time) (i : nat)
  (p : reachableNet n) :
  sent v t i n p -> forall q : t < msgLatency,
  outgoing v (minusTime msgLatency t (Rlt_le t msgLatency q)) i n.
  intros. induction H.
  invertClear H2.
  addHyp (outList_received_in l2 l2' v H5).
  econstructor. rewrite <- H6 in H0.
  apply H0. replace (minusTime msgLatency zeroTime (Rlt_le zeroTime msgLatency q))
  with msgLatency. apply H2. apply timeEqR. simpl. ring.
  addHyp (IHsent q). clear IHsent.
  remember (minusTime msgLatency t (Rlt_le t msgLatency q)) as t'.
  assert (0 < t'). rewrite Heqt'. simpl. apply RltMinusBothSides. assumption.
  addHyp (outgoing_disc_pres n n' a v t' i w H0 H1). assumption.
  simpl in q. assert (t < msgLatency). eapply Rplus_lt_weaken_lr. apply q. apply Rlt_le.
  delPos. addHyp (IHsent H0). clear IHsent.
  remember (minusTime msgLatency t (Rlt_le t msgLatency H0)) as t'.
  addHyp (outgoing_del n n' d v t' i w H1). invertClear H2.
  replace (minusTime (nonneg (time msgLatency)) (nonneg (time (delToTime (t +dt+ d))))
  (Rlt_le (nonneg (time (delToTime (t +dt+ d)))) (nonneg (time msgLatency)) q)) with
  (minusTime t' d x). apply H3. clear H1 H3. generalize dependent x. rewrite Heqt'.
  intros. apply timeEqR. simpl. ring. Qed.

Theorem fst_sent (n : Network) (m : Mode) (t : Time) (i : nat)
  (p : reachableNet n) : nextSince m t i n p ->
  exists l0, sent [baseMode m, basePosition l0] t i n p.
  intros. induction H.
  state_pred_net_destr H0. state_pred_net_destr H1.
  link_netentdisc_tac b.
  state_pred_elim H2 H5. state_pred_elim H9 H10. state_pred_elim H9 H10.
  state_pred_elim H16 H12.
  Admitted.
Theorem sent_out_del (n : Network) (v : list BaseType) (i : nat)
  (p : reachableNet n) : sent v msgLatency i n p ->
  outgoing v zeroTime i n \/
  exists r l, delivered ([-v, l, r-]) zeroTime i n p.
  introz U. remember msgLatency as mL. induction U.
  false. eapply Rlt_not_le. apply msgLatency_positive. rewrite <- HeqmL.
  apply Rle_refl.
  apply IHU in HeqmL. clear IHU. elim_intro HeqmL OZ EDZ.
  lets OZX : OZ. inversion OZX.
  lets OTD : outgoing_timeout_disc OZ. or_flat.
  left. eassumption.
  ex_flat. right. exists x. exists l. eassumption.
  right. ex_flat. exists x x0. constructor. assumption.
  assert (t < msgLatency). rewrite <- HeqmL. simpl. Rplus_lt_tac.
  delPos.
  lets SO : sent_outgoing U H. left.
  assert (outgoing v d i n) as OD. my_applys_eq SO.
  apply timeEqR. simpl. rewrite <- HeqmL. simpl.
  destruct d. destruct delay. simpl. ring.
  lets OGD : outgoing_del w OD. invertClear OGD.
  my_applys_eq H0. apply timeEqR. simpl. destruct d; destruct delay.
  simpl. ring. Qed.

Theorem sent_delivered (n : Network) (v : list BaseType) (t : Time) (i : nat)
  (p : reachableNet n) : sent v t i n p -> forall q : msgLatency < t,
  exists r l,
  delivered ([-v, l, r-]) (minusTime t msgLatency (Rlt_le msgLatency t q)) i n p.
  intros. induction H. contradict q. apply Rle_not_lt. simpl. timeNonneg.
  addHyp (IHsent q). clear IHsent. decompose [ex] H0. clear H0. rename x0 into l.
  rename x into r.
  exists r. exists l. constructor. assumption.
  addHyp (Rlt_or_le msgLatency t). invertClear H0.
  addHyp (IHsent H1). clear IHsent. decompose [ex] H0. exists x. exists x0.
  replace (minusTime (nonneg (time (delToTime (t +dt+ d))))
  (nonneg (time msgLatency)) (Rlt_le (nonneg (time msgLatency))
  (nonneg (time (delToTime (t +dt+ d)))) q)) with
  (delToTime ((minusTime t msgLatency (Rlt_le msgLatency t H1)) +dt+ d)).
  apply deliveredDel. assumption. apply timeEqR. simpl. ring.
  apply Rle_lt_or_eq_dec in H1. invertClear H1.
  addHyp (sent_outgoing n v t i p H H0).
  remember ((minusTime msgLatency t (Rlt_le t msgLatency H0))) as t'.
  addHyp (outgoing_del n n' d v t' i w H1).
  invertClear H2. assert (t +dt+ d <= msgLatency). simpl. clear H3. rename x into Q.
  rewrite Heqt' in Q. simpl in Q.
  rewrite Rplus_comm. apply Rminus_le_swap_rr. assumption.
  contradict q. apply Rle_not_lt. assumption.
  apply timeEqR in H0. rewrite H0 in H. addHyp (sent_out_del n v i p H).
  invertClear H1.
  addHyp (outgoing_del_contra n n' d v i w H2). inversion H1.
  decompose [ex] H2. rename x0 into l. rename x into r. exists r.
  exists l.
  replace (minusTime (nonneg (time (delToTime (t +dt+ d))))
  (nonneg (time msgLatency)) (Rlt_le (nonneg (time msgLatency))
  (nonneg (time (delToTime (t +dt+ d)))) q)) with
  (delToTime (zeroTime +dt+ d)).
  apply deliveredDel. assumption. apply timeEqR. simpl. rewrite H0. ring.
  Qed.

Theorem sent_pos_bound (n : Network) (m : Mode) (t : Time) (i : nat)
  (l l0 : Position) (p : reachableNet n) :
  sent [baseMode m, basePosition l0] t i n p -> inPosNet l i n ->
  dist2d l l0 <= speedMax*t.
  intros. generalize dependent l. induction H; intros.
  rename H3 into QQ. rename H2 into H3. rename H1 into H2. rename H0 into H1.
  rename QQ into H0. swapRename l l1.
  addHyp (reachable_net_prot n i q l1 h k p H). apply reachableProt_triple in H4.
  simpl in H4. invertClear H4. symmetry in H8.
  rewrite H8 in H2.
  assert (inPosNet l i n) as Q. erewrite inPos_pres_disc. apply H0. apply w.
  link_partripdiscex_tac2 p1' p2' p3'. link_partripout_tac Y.
  Focus 3. lets LO : listener_outProc_out_not H7 Y. false.
  lets BO : bc_outProc_out Y H5.
  remember ([|q, l1, h, k|]) as e. assert (reachableEnt e). eapply reachable_net_ent.
  apply p. apply H. assert (bcReadyStateEnt m l0 e). rewrite Heqe. constructor.
  rewrite H8. constructor. apply BO. lets BP : bcReady_pos H4 H9.
  eapply inPos_ent_net in BP. assert (l0 = l). eapply inPos_unique. apply BP.
  apply Q. rewrite H10. rewrite dist2D_refl. simpl. rewrite Rmult_0_r. apply Rle_refl.
  assumption.
  lets OO : ovlp_outProc_out Y H6. decompEx2 OO u r OO'.
  remember ([|q, l1, h, k|]) as e. assert (reachableEnt e). eapply reachable_net_ent.
  apply p. apply H. assert (ovReadyStateEnt m u l0 e).
  rewrite Heqe. constructor. rewrite H8. constructor. apply OO'.
  lets OP : ovReady_pos H4 H9. eapply inPos_ent_net in OP.
  assert (l0 = l). eapply inPos_unique. apply OP. apply Q. rewrite H10.
  rewrite dist2D_refl. simpl. rewrite Rmult_0_r. apply Rle_refl. assumption.
  assert (inPosNet l i n) as Q. erewrite inPos_pres_disc. apply H0. apply w.
  apply IHsent. assumption.
  addHyp (inPos_del_bound_bkwd n n' d l i H0 w). invertClear H1. rename x into l1.
  invertClear H2. apply IHsent in H1. clear IHsent. rewrite distSymmetric in H3.
  addHyp (dist_tri_ineq l l1 l0). eapply Rle_trans. apply H2. simpl. rewrite Rmult_plus_distr_l.
  rewrite Rplus_comm. simpl in H1, H3. apply Rplus_le_compat; assumption. Qed.

Theorem fst_delivered (n : Network) (m : Mode) (t : Time) (i : nat)
  (l : Position) (p : reachableNet n) :
  nextSince m t i n p -> inPosNet l i n -> forall q : msgLatency < t,
  exists l0 l1 r,
  delivered ([-[baseMode m, basePosition l0], l1, r-])
  (minusTime t msgLatency (Rlt_le msgLatency t q)) i n p /\
  dist2d l l0 <= speedMax*t.
  introz U. lets FS : fst_sent U. invertClearAs2 FS l0 SEN.
  lets SPB : sent_pos_bound SEN U0.
  lets SD : sent_delivered SEN U1. ex_flat.
  exists l0 x0 x.
  split; assumption. Qed.