Library Main

Require Import Reals.
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.EntityLanguage.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.NARNonFS_currSince.
Require Import ComhCoq.NARMisc.
Require Import ComhCoq.NARIncomp.
Require Import ComhCoq.NARTop.

Theorem safety_aux (n : Network) (X : reachableNet n) (e1 e2 : Entity)
  (i j : nat) (H : (i <> j)%nat) (H0 : e1 @ i .: n) (H1 : e2 @ j .: n)
  (x : Distance) (Heqx : x = mkDistance (dist2d e1 e2)) (mdc : Distance) (m1 : Mode)
  (Heqm1 : m1 = e1) (m2 : Mode) (Heqm2 : m2 = e2) (Heqmdc : mdc = minDistComp m1 m2)
  (H2 : x < mdc) (H3 : ~ failSafe m1) (H4 : ~ failSafe m2) (H5 : currModeNet m1 i n)
  (H6 : currModeNet m2 j n) (t1 : Time) (H7 : currSince m1 t1 i n X) (t2 : Time)
  (H8 : currSince m2 t2 j n X) (H9 : msgLatency + Rmax adaptNotif transMax < t1)
  (H10 : msgLatency + Rmax adaptNotif transMax < t2) (H11 : t1 <= t2) : False.
  addHyp (inPos_ex i n e1 H0). invertClear H12. rename x0 into l1.
  addHyp (pre_del_suff n m1 t1 i l1 X H7 H13 H3). decompose [ex] H12. clear H12.
  rename x0 into t. rename x1 into r. rename x2 into l'. rename x3 into l''.
  decompose [and] H15. clear H15. assert (t < t2). eapply Rlt_le_trans.
  apply H17. assumption.
  inversion H14. addHyp (Rmult_le_compat_l (2*speedMax) t
  (upper (preDeliveredInterval m1)) speedMax_double_nonneg H20).
  addHyp (Rplus_lt_le_compat x mdc (2 * speedMax * t)
  (2 * speedMax * upper (preDeliveredInterval m1)) H2 H21).
  unfold sufficient in H16. addHyp (maxMinDistCompBound m1 m2).
  rewrite <- Heqmdc in H23. assert (x + 2*speedMax*t < r).
  eapply Rlt_le_trans. apply H22. eapply Rle_trans;[ |apply H16].
  simpl. eapply Rplus_le_compat. assumption. apply Rle_refl.
  apply Rlt_le in H24. addHyp (delivered_received n ([baseMode m1, basePosition l'])
  t r x i j X l'' H12 H (distNet_intro e1 e2 i j n x H0 H1 Heqx) H24).
  addHyp (inPos_ex j n e2 H1). invertClear H26. rename x0 into l2.
  addHyp (inPos_pos e1 i l1 n H0 H13). addHyp (inPos_pos e2 j l2 n H1 H27).
  rewrite H26, H28 in Heqx. addHyp (dist_tri_ineq l2 l1 l').
  assert ((distance x) = dist2d l2 l1). rewrite distSymmetric.
  rewrite Heqx. reflexivity. rewrite <- H30 in H29.
  assert (nonneg (dist2d l2 l') <= nonneg (distance x) +
  nonneg speedMax * (nonneg (time msgLatency) + nonneg (time t))).
  eapply Rle_trans. apply H29. apply Rplus_le_compat. apply Rle_refl.
  assumption.
  replace (nonneg speedMax * (nonneg (time msgLatency) + nonneg (time t))) with
  (nonneg speedMax * nonneg (time msgLatency) + nonneg speedMax * nonneg (time t))
  in H31;[ | ring]. assert (nonneg (distance x) +
  (nonneg speedMax * nonneg (time msgLatency) +
  nonneg speedMax * nonneg (time t)) < mdc +
  (nonneg speedMax * nonneg (time msgLatency) +
  nonneg speedMax * nonneg (time t))). apply Rplus_lt_le_compat.
  assumption. apply Rle_refl. assert (dist2d l2 l' < mdc +
  (nonneg speedMax * nonneg (time msgLatency) +
  nonneg speedMax * nonneg (time t))). eapply Rle_lt_trans. apply H31.
  assumption. replace (nonneg (distance mdc) +
  (nonneg speedMax * nonneg (time msgLatency) + nonneg speedMax * nonneg (time t)))
  with (nonneg speedMax * nonneg (time msgLatency) + (nonneg (distance mdc) +
  nonneg speedMax * nonneg (time t))) in H33;[ | ring].
  apply Rplus_lt_swap_rl in H33.
  apply (Rplus_lt_compat_r (speedMax*t)) in H33.
  replace (mdc + nonneg speedMax * nonneg (time t) + nonneg speedMax * nonneg (time t)) with
  (mdc + 2*nonneg speedMax * nonneg (time t)) in H33; [ | ring].
  assert (nonneg (dist2d l2 l') - nonneg speedMax * nonneg (time msgLatency) +
  nonneg speedMax * nonneg (time t) <
  nonneg (distance mdc) + 2 * nonneg speedMax * upper (preDeliveredInterval m1)).
  eapply Rlt_le_trans. apply H33. apply Rplus_le_compat. apply Rle_refl.
  assumption. rewrite Heqmdc in H34. remember (dist2d l2 l') as q0. simpl in H34.
  rewrite minDistCompSymmetric in H34.
  fold (possIncDist m2 m1) in H34. rewrite Heqq0 in H34.
  assert (zeroTime < t). simpl in H18. eapply Rle_lt_trans;[ |apply H18].
  eapply Rle_trans;[ |apply Rmax_l]. timeNonneg.
  assert ((speedMax * t) < possIncDist m2 m1). eapply Rle_lt_trans.
  apply Rmult_le_compat_l. apply cond_nonneg. apply H20.
  unfold possIncDist. simpl. apply Rplus_lt_weaken_rl. apply cond_nonneg.
  rewrite Rmult_assoc. rewrite double. apply Rlt_double.
  apply Rmult_lt_0. apply speedMax_pos. apply Rlt_le_zero_plus. apply Rlt_le_zero_plus.
  apply Rmax_lt_l. apply adaptNotif_positive. apply cond_nonneg.
  apply cond_nonneg.
  lets RPL : Rminus_plus_lt_subNonnegTot H36.
  rewrite <- multNonneg_Rmult_eq in H34. apply RPL in H34. clear H36.
  addHyp (incomp_tfs n t2 t l2 l' j m2 m1 X H8 H27 H25 H35 H15 H34).
  apply tfs_bound in H36. simpl in H18. assert (transMax < t).
  eapply Rle_lt_trans;[ |apply H18]. apply Rmax_r.
  eapply Rlt_not_le. apply H37. eapply Rle_trans. apply H36.
  apply transMaxBound. Qed.

Theorem safety (n : Network) : reachableNet n -> safe n.
  unfold safe. intros. addHyp (dec_compatible e1 e2). appDisj H2.
  unfold compatible in H2. remember (dist2d e1 e2) as x.
  apply not_Rle_lt in H2. remember (minDistComp e1 e2) as mdc.
  remember (currModeEnt e1) as m1. remember (currModeEnt e2) as m2. apply False_ind.
  assert (~failSafe m1). addHyp (fsDecMode m1). appDisj H3.
  addHyp (minDistCompFS m1 m2 H3). rewrite H4 in Heqmdc. rewrite Heqmdc in H2.
  simpl in H2.
  nonneg_lt0_contra.
  assert (~failSafe m2). addHyp (fsDecMode m2). appDisj H4.
  addHyp (minDistCompFS m2 m1 H4). rewrite minDistCompSymmetric in H5.
  rewrite H5 in Heqmdc. rewrite Heqmdc in H2. simpl in H2.
  nonneg_lt0_contra.
  addHyp (currMode_intro m1 e1 i n Heqm1 H0).
  addHyp (currMode_intro m2 e2 j n Heqm2 H1).
  addHyp (nonFS_currSince m1 i n X H5 H3). invertClear H7. rename x0 into t1.
  addHyp (nonFS_currSince m2 j n X H6 H4). invertClear H7. rename x0 into t2.
  addHyp (currSince_lower_bound n t1 m1 i X H8).
  addHyp (currSince_lower_bound n t2 m2 j X H9).
  apply lt_notEq in H. addHyp (Rle_or_le t1 t2).
  remember (mkDistance x) as x'. swapRename x x'. rewrite Heqx in Heqx'.
  assert (x < mdc). rewrite Heqx'. rewrite <- Heqx. assumption.
  invertClear H11.
  eapply safety_aux;eassumption. apply notEq_symm in H.
  rewrite distSymmetric in Heqx'. rewrite minDistCompSymmetric in Heqmdc.
  eapply safety_aux;eassumption.
Qed.