Require Import Bool.
Require Import Reals.
Require Import trajectory_const.
Require Import trajectory_def.
Require Import constants.
Require Import ycngftys.
Require Import ycngstys.
Require Import ails_def.
Require Import math_prop.
Require Import tau.
Require Import ails.
Require Import trajectory.
Require Import measure2state.
Require Import ails_trajectory.

Lemma AlertRange_pos : (0 < AlertRange)%R.
unfold AlertRange in |- *; prove_sup.
Qed.

Lemma conflict_beta_theta :
 ∀ (intr : Trajectory) (evad : EvaderTrajectory) (T : TimeT),
 h intr = V →
 (MinDistance T ≤ l intr evad T)%R →
 (l intr evad T ≤ MaxDistance T)%R →
 Omega (beta intr evad T + thetat intr 0) = false →
 conflict intr evad T = true →
 (beta intr evad T + thetat intr 0 ≤ MinBeta)%R ∨
 (2 × PI - MinBeta < beta intr evad T + thetat intr 0)%R.
Proof with trivial.
intros intr evad T hyp_intr; intros; set (beta_p := beta intr evad T) in H1;
 set (thetat_p := thetat intr) in H1; set (l_p := l intr evad T) in H, H0;
 set (conflict_p := conflict intr evad) in H2;
assert (hyp1 : r_V = r_vi intr)...
unfold r_V, r_vi in |- *; unfold vi in |- *; rewrite hyp_intr...
assert (hyp2 : rho_V = rho_vi intr)...
unfold rho_V, rho_vi in |- *; unfold vi in |- *; rewrite hyp_intr...
case (Rtotal_order (beta_p + thetat_p 0%R) MinBeta); intro...
left; left...
elim H3; intro...
left; right...
case (Rlt_le_dec (2 × PI - MinBeta) (beta_p + thetat_p 0%R)); intro...
right...
assert (H5 := conflict_T_e_0 intr evad T H2)...
cut (0 ≤ e intr evad T T)%R...
cut (0 ≤ ConflictRange)%R...
intros; assert (H8 := Rsqr_incr_1 (e intr evad T T) ConflictRange H5 H7 H6);
 unfold e in H8; rewrite isometric_evader in H8; rewrite Rsqr_sqrt in H8...
change (MinBeta < beta_p + thetat_p 0)%R in H4;
 cut
  ((beta_p + thetat_p 0 < PI / 2)%R ∨ (3 × (PI / 2) < beta_p + thetat_p 0)%R)...
intro; elim H9; intro...
cut
 (l_p × sin (beta_p + thetat_p 0) + r_V × (cos (rho_V × T) - 1) ≤
  yp intr evad T T)%R...
cut
 (r_V × sin (rho_V × T) - l_p × cos (beta_p + thetat_p 0) ≤ xp intr evad T T)%R...
intros;
 generalize
  (Math_prop_no_conflict_1 (beta_p + thetat_p 0%R) l_p
     (xp intr evad T T) (yp intr evad T T) T H H0
     (Rlt_le MinBeta (beta_p + thetat_p 0%R) H4)
     (Rlt_le (beta_p + thetat_p 0%R) (PI / 2) H10) H12 H11);
 intro;
 generalize
  (Rlt_le_trans (Rsqr ConflictRange)
     (Rsqr (xp intr evad T T) + Rsqr (yp intr evad T T))
     (Rsqr ConflictRange) H13 H8); intro;
 elim (Rlt_irrefl (Rsqr ConflictRange) H14)...
rewrite hyp1; rewrite hyp2...
apply (xpt_PI intr evad T)...
left; apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 T) ]...
rewrite <- hyp2; left; apply Rlt_trans with (PI / 2)%R...
apply rho_t_PI2...
apply PI2_Rlt_PI...
rewrite hyp1; rewrite hyp2; cut (0 ≤ T)%R...
cut (rho_vi intr × T ≤ PI / 2)%R...
intros; generalize (ypt_PI2 intr evad T T H12 H11); intro...
elim H13; intros...
rewrite <- hyp2; left; apply rho_t_PI2...
left; apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 T) ]...
cut
 (yp intr evad T T ≤
  l_p × sin (beta_p + thetat_p 0) - r_V × (cos (rho_V × T) - 1))%R...
cut
 (r_V × sin (rho_V × T) - l_p × cos (beta_p + thetat_p 0) ≤ xp intr evad T T)%R...
intros;
 generalize
  (Math_prop_no_conflict_2 (beta_p + thetat_p 0%R) l_p
     (xp intr evad T T) (yp intr evad T T) T H H0
     (Rlt_le (3 × (PI / 2)) (beta_p + thetat_p 0%R) H10) r H12 H11);
 intro...
elim
 (Rlt_irrefl (Rsqr ConflictRange)
    (Rlt_le_trans (Rsqr ConflictRange)
       (Rsqr (xp intr evad T T) + Rsqr (yp intr evad T T))
       (Rsqr ConflictRange) H13 H8))...
rewrite hyp1; rewrite hyp2; apply (xpt_PI intr evad T)...
left; apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 T) ]...
rewrite <- hyp2; left; apply Rlt_trans with (PI / 2)%R...
apply rho_t_PI2...
apply PI2_Rlt_PI...
rewrite hyp1; rewrite hyp2; cut (0 ≤ T)%R...
cut (rho_vi intr × T ≤ PI / 2)%R...
intros; generalize (ypt_PI2 intr evad T T H12 H11); intro; elim H13; intros...
rewrite <- hyp2; left; apply rho_t_PI2...
left; apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 T) ]...
cut (Omega (beta_p + thetat_p 0%R) = false)...
unfold Omega in |- *; case (Rle_dec (PI / 2) (beta_p + thetat_p 0%R)); intro...
case (Rle_dec (beta_p + thetat_p 0%R) (3 × (PI / 2))); intros...
elim diff_true_false...
right; auto with real...
intro; left; auto with real...
apply Rplus_le_le_0_compat; apply Rle_0_sqr...
unfold ConflictRange in |- *; left; prove_sup...
unfold e in |- *; apply sqrt_positivity; apply Rsqr_evader_distance_pos...
Qed.

Lemma alarm_NOT_Omega_T :
 ∀ (intr : Trajectory) (evad : EvaderTrajectory) (T : TimeT),
 h intr = V →
 h (tr evad) = V →
 (MinDistance T ≤ l intr evad T)%R →
 (l intr evad T ≤ MaxDistance T)%R →
 Omega (beta intr evad T + thetat intr 0) = false →
 conflict intr evad T = true →
 (RR (measure2state intr 0) (measure2state (tr evad) 0) T ≤ AlertRange)%R.
Proof with trivial.
intros intr evad T hyp_intr hyp_evad; intros; apply Rsqr_incr_0_var...
rewrite R_T...
generalize (conflict_beta_theta intr evad T hyp_intr H H0 H1 H2); intro;
 elim H3; intro...
cut (0 ≤ beta intr evad T + thetat intr 0)%R...
intro;
 apply
  (Math_prop_alarm_1 (beta intr evad T + thetat intr 0)
     (l intr evad T) T H H0 H5 H4)...
generalize (beta_def intr evad T); intro; decompose [and] H5; intros...
cut (beta intr evad T + thetat intr 0 ≤ 2 × PI)%R...
intro;
 apply
  (Math_prop_alarm_2 (beta intr evad T + thetat intr 0)
     (l intr evad T) T H H0
     (Rlt_le (2 × PI - MinBeta) (beta intr evad T + thetat intr 0) H4))...
generalize (beta_def intr evad T); intro; decompose [and] H5; intros; left...
left; apply AlertRange_pos...
Qed.

Lemma alarm_NOT_Omega_tau :
 ∀ (intr : Trajectory) (evad : EvaderTrajectory) (T : TimeT),
 h intr = V →
 h (tr evad) = V →
 (MinDistance T ≤ l intr evad T)%R →
 (l intr evad T ≤ MaxDistance T)%R →
 Omega (beta intr evad T + thetat intr 0) = false →
 conflict intr evad T = true →
 (0 < tau (measure2state intr 0) (measure2state (tr evad) 0) 0)%R →
 (RR (measure2state intr 0) (measure2state (tr evad) 0)
    (tau (measure2state intr 0) (measure2state (tr evad) 0) 0) ≤ AlertRange)%R.
Proof with trivial.
intros intr evad T hyp_intr hyp_evad; intros;
 apply
  Rle_trans with (RR (measure2state intr 0) (measure2state (tr evad) 0) T)...
generalize
 (derivative_eq_zero_min (measure2state intr 0) (measure2state (tr evad) 0) 0
    T); repeat rewrite Rplus_0_l; intro...
apply (alarm_NOT_Omega_T intr evad T hyp_intr hyp_evad H H0 H1 H2)...
Qed.

Lemma alarm_NOT_Omega_AlertTime :
 ∀ (intr : Trajectory) (evad : EvaderTrajectory) (T : TimeT),
 h intr = V →
 h (tr evad) = V →
 (MinDistance T ≤ l intr evad T)%R →
 (l intr evad T ≤ MaxDistance T)%R →
 Omega (beta intr evad T + thetat intr 0) = false →
 conflict intr evad T = true →
 (AlertTime < tau (measure2state intr 0) (measure2state (tr evad) 0) 0)%R →
 (RR (measure2state intr 0) (measure2state (tr evad) 0) AlertTime ≤
  AlertRange)%R.
Proof with trivial.
intros intr evad T hyp_intr hyp_evad; intros;
 apply
  Rle_trans with (RR (measure2state intr 0) (measure2state (tr evad) 0) T)...
rewrite <- (Rplus_0_l AlertTime); rewrite <- (Rplus_0_l T);
 apply asymptotic_decrease_tau...
left...
unfold AlertTime in |- *; apply Rle_trans with MaxT...
apply (cond_2 T)...
unfold MaxT in |- *; left; prove_sup...
apply (alarm_NOT_Omega_T _ _ _ hyp_intr hyp_evad H H0 H1 H2)...
Qed.

Lemma chktrack_NOT_Omega_trkrate_eq_0 :
 ∀ (intr : Trajectory) (evad : EvaderTrajectory) (T : TimeT),
 h intr = V →
 h (tr evad) = V →
 (MinDistance T ≤ l intr evad T)%R →
 (l intr evad T ≤ MaxDistance T)%R →
 Omega (beta intr evad T + thetat intr 0) = false →
 conflict intr evad T = true →
 (0 < tau (measure2state intr 0) (measure2state (tr evad) 0) 0)%R →
 chktrack (measure2state intr 0) (measure2state (tr evad) 0) 0.
Proof with trivial.
intros intr evad T hyp_intr hyp_evad; intros; unfold chktrack in |- *;
 case (Rle_dec (tau (measure2state intr 0) (measure2state (tr evad) 0) 0) 0);
 intro...
elim
 (Rlt_irrefl 0
    (Rlt_le_trans 0
       (tau (measure2state intr 0) (measure2state (tr evad) 0) 0) 0 H3 r))...
rewrite Rplus_0_l;
 case
  (Rlt_dec AlertTime
     (tau (measure2state intr 0) (measure2state (tr evad) 0) 0));
 intro...
apply (alarm_NOT_Omega_AlertTime intr evad T)...
apply (alarm_NOT_Omega_tau intr evad T)...
Qed.


Theorem ails_alarm_tau_gt0 :
 ∀ (intr : Trajectory) (evad : EvaderTrajectory) (T : TimeT),
 h intr = V →
 h (tr evad) = V →
 (MinDistance T ≤ l intr evad T)%R →
 (l intr evad T ≤ MaxDistance T)%R →
 Omega (beta intr evad T + thetat intr 0) = false →
 (0 < tau (measure2state intr 0) (measure2state (tr evad) 0) 0)%R →
 conflict intr evad T = true →
 ails_alert (measure2state intr 0) (measure2state (tr evad) 0).
Proof with trivial.
intros intr evad T hyp_intr hyp_evad; intros; unfold ails_alert in |- *;
 case (Req_EM_var (trkrate (bank (measure2state intr 0))) 0);
 intro...
apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)...
case (Rle_dec 3 (trkrate (bank (measure2state intr 0)))); intro...
unfold arc_loop in |- *; rewrite mod_eq_0...
case (Rlt_le_dec 0 (trkrate (bank (measure2state intr 0)))); intro...
unfold INR in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r;
 repeat rewrite Rplus_0_r; unfold intruderSpeed in |- *;
 replace (v V) with 250%R...
cut
 (let z := 250%R in
  mkState
    (xt (measure2state intr 0) +
     Rsqr z / (g × tand (bank (measure2state intr 0))) ×
     (sind (heading (measure2state intr 0)) -
      sind (heading (measure2state intr 0))))
    (yt (measure2state intr 0) +
     Rsqr z / (g × tand (bank (measure2state intr 0))) ×
     (cosd (heading (measure2state intr 0)) -
      cosd (heading (measure2state intr 0))))
    (heading (measure2state intr 0)) (bank (measure2state intr 0)) =
  measure2state intr 0)...
intro; rewrite H4...
cut
 (mkState (xt (measure2state (tr evad) 0)) (yt (measure2state (tr evad) 0))
    (heading (measure2state (tr evad) 0)) (bank (measure2state (tr evad) 0)) =
  measure2state (tr evad) 0)...
intro; rewrite H5...
apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)...
unfold Rminus in |- *; repeat rewrite Rplus_opp_r; repeat rewrite Rmult_0_r;
 repeat rewrite Rplus_0_r...
unfold INR in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r;
 repeat rewrite Rplus_0_r; unfold Rminus in |- *; repeat rewrite Rplus_opp_r;
 unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)...
case (Rle_dec (3 / 2) (trkrate (bank (measure2state intr 0)))); intro...
unfold arc_loop in |- *; rewrite mod_eq_0;
 case (Rlt_le_dec 0 (trkrate (bank (measure2state intr 0))));
 intro...
repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 unfold Rminus in |- *; repeat rewrite Rplus_opp_r;
 unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)...
repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 unfold Rminus in |- *; repeat rewrite Rplus_opp_r;
 unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)...
case (Rle_dec (3 / 4) (trkrate (bank (measure2state intr 0)))); intro...
unfold arc_loop in |- *; rewrite mod_eq_0;
 case (Rlt_le_dec 0 (trkrate (bank (measure2state intr 0))));
 intro...
repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 unfold Rminus in |- *; repeat rewrite Rplus_opp_r;
 unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)...
repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 unfold Rminus in |- *; repeat rewrite Rplus_opp_r;
 unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)...
unfold arc_loop in |- *; rewrite mod_eq_0;
 case (Rlt_le_dec 0 (trkrate (bank (measure2state intr 0))));
 intro...
repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 unfold Rminus in |- *; repeat rewrite Rplus_opp_r;
 unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)...
repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 unfold Rminus in |- *; repeat rewrite Rplus_opp_r;
 unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r;
 apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)...
Qed.