# Library AILS.alarm

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.

unfold AlertRange in |- *; prove_sup.
Qed.

Lemma conflict_beta_theta :
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)
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...
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
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 :
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
Proof with trivial.
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...
Qed.

Lemma alarm_NOT_Omega_tau :
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
(0 < tau (measure2state intr 0) (measure2state (tr evad) 0) 0)%R
(RR (measure2state intr 0) (measure2state (tr evad) 0)
Proof with trivial.
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...
Qed.

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
Proof with trivial.
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 :
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
(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
(tau (measure2state intr 0) (measure2state (tr evad) 0) 0));
intro...
Qed.

Theorem ails_alarm_tau_gt0 :
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
(0 < tau (measure2state intr 0) (measure2state (tr evad) 0) 0)%R
conflict intr evad T = true
Proof with trivial.
case (Req_EM_var (trkrate (bank (measure2state intr 0))) 0);
intro...
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)) -
(yt (measure2state intr 0) +
Rsqr z / (g × tand (bank (measure2state intr 0))) ×
(cosd (heading (measure2state intr 0)) -
(heading (measure2state intr 0)) (bank (measure2state intr 0)) =
measure2state intr 0)...
intro; rewrite H4...
cut
intro; rewrite H5...
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;
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;
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;
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;
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;