# Library AILS.ails_trajectory

Require Import Reals.
Require Import trajectory_const.
Require Import trajectory_def.
Require Import constants.
Require Import ycngftys.
Require Import ycngstys.
Require Import tau.
Require Import ails.
Require Import trajectory.
Require Import measure2state.

Lemma d_distance :
distance (measure2state (tr evad) 0) (measure2state intr 0) = d intr evad.
Proof with trivial.
unfold distance, d in |- *; unfold Die in |- *; simpl in |- *;
unfold xi, yi in |- ×...
Qed.

Lemma R_T :
Rsqr (RR (measure2state intr 0) (measure2state (tr evad) 0) T) =
(Rsqr (l intr evad T × cos (beta intr evad T + thetat intr 0) - V × T) +
Rsqr (l intr evad T × sin (beta intr evad T + thetat intr 0)))%R.
Proof with trivial.
unfold Rminus in |- ×...
repeat rewrite Rplus_assoc...
set (z := 250%R)...
rewrite
(Rplus_comm (Rsqr (l intr evad T × cos (beta intr evad T + thetat intr 0))))
...
repeat rewrite Rplus_assoc...
replace
(Rsqr (l intr evad T × sin (beta intr evad T + thetat intr 0)) +
Rsqr (l intr evad T × cos (beta intr evad T + thetat intr 0)))%R with
rewrite <- (Rplus_comm (Rsqr (l intr evad T)))...
repeat rewrite <- Rplus_assoc...
replace
(2 × (l intr evad T × cos (beta intr evad T + thetat intr 0)) × (V × T))%R
with
(2 × (l intr evad T × (V × T) × cos (beta intr evad T + thetat intr 0)))%R...
cut
dist_euc (x (tr evad) T) (y (tr evad) T) (x intr 0%R) (y intr 0%R))...
intro...
rewrite H...
cut
((V × T)%R =
dist_euc (x (tr evad) 0%R + T × z - T × z × cos (thetat intr 0))
(y (tr evad) 0%R - T × z × sin (thetat intr 0))
intro...
rewrite H0...
cut
(RR (measure2state intr 0) (measure2state (tr evad) 0) T =
dist_euc (x (tr evad) 0%R + T × z - T × z × cos (thetat intr 0))
(y (tr evad) 0%R - T × z × sin (thetat intr 0))
(x intr 0%R) (y intr 0%R))...
intro; rewrite H1...
replace
(Rsqr
(dist_euc (x (tr evad) 0 + T × z - T × z × cos (thetat intr 0))
(y (tr evad) 0 - T × z × sin (thetat intr 0))
Rsqr (dist_euc (x (tr evad) T) (y (tr evad) T) (x intr 0) (y intr 0)) +
-
(2 ×
(dist_euc (x (tr evad) T) (y (tr evad) T) (x intr 0) (y intr 0) ×
dist_euc (x (tr evad) 0 + T × z - T × z × cos (thetat intr 0))
(y (tr evad) 0 - T × z × sin (thetat intr 0))
cos (beta intr evad T + thetat intr 0))))%R with
(Rsqr
(dist_euc (x (tr evad) 0 + T × z - T × z × cos (thetat intr 0))
(y (tr evad) 0 - T × z × sin (thetat intr 0))
Rsqr (dist_euc (x (tr evad) T) (y (tr evad) T) (x intr 0) (y intr 0)) -
2 ×
(dist_euc (x (tr evad) T) (y (tr evad) T) (x intr 0) (y intr 0) ×
dist_euc (x (tr evad) 0 + T × z - T × z × cos (thetat intr 0))
(y (tr evad) 0 - T × z × sin (thetat intr 0))
(x (tr evad) T) (y (tr evad) T) × cos (beta intr evad T + thetat intr 0)))%R...
apply law_cosines...
unfold dist_euc in |- ×...
replace
(sqrt
(Rsqr (x (tr evad) T - x intr 0%R) + Rsqr (y (tr evad) T - y intr 0%R)))
intro; rewrite H2...
generalize (tr_cond2 evad (val T)); intro...
rewrite H3...
replace
(x (tr evad) 0 + T × z - T × z × cos (thetat intr 0) -
(x (tr evad) 0 + h (tr evad) × T))%R with (- T × z × cos (thetat intr 0))%R...
replace (y (tr evad) 0 - T × z × sin (thetat intr 0) - y (tr evad) 0)%R with
(- T × z × sin (thetat intr 0))%R...
replace
(Rsqr (- T × z × cos (thetat intr 0)) + Rsqr (- T × z × sin (thetat intr 0)))%R
with (Rsqr (T × z))...
rewrite sqrt_Rsqr...
rewrite <- H2...
rewrite <- H3...
generalize xe_0; intro...
unfold xe, xi in H4...
generalize ye_0; intro...
unfold ye, yi in H5...
replace (x intr 0 - (l intr evad T × cos (beta intr evad T) + x intr 0))%R
with (- (l intr evad T × cos (beta intr evad T)))%R...
unfold Rminus in |- ×...
replace
(y intr 0 + - (y intr 0 + - (l intr evad T × sin (beta intr evad T))))%R
rewrite cos_plus...
unfold Rminus in |- ×...
rewrite Rmult_plus_distr_l...
replace
(- (l intr evad T × cos (beta intr evad T)) ×
(- T × z × cos (thetat intr 0)) +
l intr evad T × sin (beta intr evad T) × (- T × z × sin (thetat intr 0)))%R
with
(l intr evad T × cos (beta intr evad T) × T × z × cos (thetat intr 0) +
l intr evad T × - sin (beta intr evad T) × T × z × sin (thetat intr 0))%R...
replace (- (sin (beta intr evad T) × sin (thetat intr 0)))%R with
(- sin (beta intr evad T) × sin (thetat intr 0))%R...
repeat rewrite <- Rmult_assoc...
repeat rewrite Rmult_assoc...
pattern (cos (beta intr evad T)) at 1 in |- *;
rewrite (Rmult_comm (cos (beta intr evad T)))...
repeat rewrite <- Rmult_assoc...
replace
(l intr evad T × T × z × cos (beta intr evad T) × cos (thetat intr 0))%R
with
(l intr evad T × T × z × cos (thetat intr 0) × cos (beta intr evad T))%R...
apply Rplus_eq_compat_l...
repeat rewrite Rmult_assoc...
apply Rmult_eq_compat_l...
repeat rewrite <- Rmult_assoc...
repeat rewrite <- (Rmult_comm (sin (thetat intr 0)))...
repeat rewrite Rmult_assoc...
apply Rmult_eq_compat_l...
rewrite (Rmult_comm (- sin (beta intr evad T)))...
repeat rewrite Rmult_assoc...
repeat rewrite Rmult_assoc...
repeat apply Rmult_eq_compat_l...
ring...
rewrite Ropp_mult_distr_l_reverse...
rewrite <- Ropp_mult_distr_l_reverse...
replace
(- l intr evad T × cos (beta intr evad T) × (- T × z × cos (thetat intr 0)))%R
with
(l intr evad T × cos (beta intr evad T) × T × z × cos (thetat intr 0))%R...
apply Rplus_eq_compat_l...
repeat rewrite Rmult_assoc...
apply Rmult_eq_compat_l...
repeat rewrite <- Rmult_assoc...
repeat rewrite <- (Rmult_comm (sin (thetat intr 0)))...
apply Rmult_eq_compat_l...
repeat rewrite <- (Rmult_comm z)...
apply Rmult_eq_compat_l...
ring...
repeat rewrite <- Rmult_assoc...
repeat rewrite <- (Rmult_comm (cos (thetat intr 0)))...
apply Rmult_eq_compat_l...
repeat rewrite <- (Rmult_comm z)...
apply Rmult_eq_compat_l...
ring...
ring...
ring...
left; apply Rmult_lt_0_compat...
apply Rlt_le_trans with MinT...
apply MinT_is_pos...
apply (cond_1 T)...
unfold z in |- *; prove_sup...
replace (- T × z × cos (thetat intr 0))%R with
(- T × (z × cos (thetat intr 0)))%R...
replace (- T × z × sin (thetat intr 0))%R with
(- T × (z × sin (thetat intr 0)))%R...
repeat rewrite Rsqr_mult...
repeat rewrite <- Rsqr_neg...
rewrite cos2...
unfold Rminus in |- *; rewrite Rmult_plus_distr_l...
rewrite Rmult_1_r...
ring...
repeat rewrite Rmult_assoc...
repeat rewrite Rmult_assoc...
unfold Rminus in |- ×...
rewrite (Rplus_comm (y (tr evad) 0%R))...
repeat rewrite Rplus_assoc...
rewrite Rplus_opp_r; rewrite Rplus_0_r...
repeat rewrite <- Ropp_mult_distr_l_reverse...
replace (v V) with z...
unfold Rminus in |- ×...
ring...
unfold Rminus in |- *; unfold RR, dist_euc in |- ×...
replace
(sqrt
(Rsqr (dx (measure2state intr 0) (measure2state (tr evad) 0) T) +
Rsqr (dy (measure2state intr 0) (measure2state (tr evad) 0) T))) with
(sqrt
(Rsqr
(x intr 0%R + T × z × cosd (toDeg (theta intr 0%R)) -
(x (tr evad) 0%R + T × z)) +
Rsqr
(y intr 0%R + T × z × sind (toDeg (theta intr 0%R)) - y (tr evad) 0%R)))...
unfold cosd, sind, thetat in |- ×...
rewrite
(Rsqr_neg
(x intr 0%R + T × z × cos (theta intr 0%R) - (x (tr evad) 0%R + T × z)))
...
rewrite
(Rsqr_neg (y intr 0%R + T × z × sin (theta intr 0%R) - y (tr evad) 0%R))
...
replace
(- (x intr 0 + T × z × cos (theta intr 0) - (x (tr evad) 0 + T × z)))%R with
(x (tr evad) 0 + T × z - T × z × cos (theta intr 0) - x intr 0)%R...
replace (- (y intr 0 + T × z × sin (theta intr 0) - y (tr evad) 0))%R with
(y (tr evad) 0 - T × z × sin (theta intr 0) - y intr 0)%R...
unfold Rminus in |- ×...
repeat rewrite Ropp_plus_distr...
rewrite Ropp_involutive...
rewrite <- (Rplus_comm (y (tr evad) 0%R))...
repeat rewrite Rplus_assoc...
apply Rplus_eq_compat_l...
rewrite (Rplus_comm (- y intr 0%R))...
unfold Rminus in |- ×...
repeat rewrite Ropp_plus_distr...
repeat rewrite Ropp_involutive...
rewrite <- (Rplus_comm (x (tr evad) 0%R + T × z))...
repeat rewrite Rplus_assoc...
repeat apply Rplus_eq_compat_l...
rewrite (Rplus_comm (- x intr 0%R))...
cut (v V = z)...
intro...
rewrite H0...
unfold dist_euc in |- ×...
generalize (tr_cond1 evad (val T)); intro...
generalize (tr_cond2 evad (val T)); intro...
rewrite H1...
rewrite H2...
rewrite H0...
replace
(x (tr evad) 0 + T × z - T × z × cos (thetat intr 0) -
(x (tr evad) 0 + z × T))%R with (- (T × z × cos (thetat intr 0)))%R...
replace (y (tr evad) 0 - T × z × sin (thetat intr 0) - y (tr evad) 0)%R with
(- (T × z × sin (thetat intr 0)))%R...
repeat rewrite <- Rsqr_neg...
repeat rewrite Rsqr_mult...
rewrite cos2...
replace
(Rsqr T × Rsqr z × (1 - Rsqr (sin (thetat intr 0))) +
Rsqr T × Rsqr z × Rsqr (sin (thetat intr 0)))%R with
(Rsqr T × Rsqr z)%R...
rewrite <- Rsqr_mult...
rewrite sqrt_Rsqr...
apply Rmult_comm...
left; apply Rmult_lt_0_compat...
apply Rlt_le_trans with MinT...
apply MinT_is_pos...
apply (cond_1 T)...
unfold z in |- *; prove_sup...
unfold Rminus in |- ×...
rewrite Rmult_plus_distr_l...
rewrite Rmult_1_r...
ring...
unfold Rminus in |- ×...
rewrite (Rplus_comm (y (tr evad) 0%R))...
rewrite Rplus_assoc...
rewrite Rplus_opp_r...
symmetry in |- *; apply Rplus_0_r...
unfold Rminus in |- ×...
rewrite Ropp_plus_distr...
rewrite (Rplus_comm (- x (tr evad) 0%R))...
repeat rewrite Rplus_assoc...
rewrite (Rplus_comm (x (tr evad) 0%R))...
repeat rewrite Rplus_assoc...
rewrite Rplus_opp_l; rewrite Rplus_0_r...
ring...
unfold l, dist_euc in |- ×...
unfold Die in |- ×...
unfold xi, yi in |- ×...
rewrite (Rsqr_neg (x intr 0%R - x (tr evad) T))...
rewrite (Rsqr_neg (y intr 0%R - y (tr evad) T))...
unfold Rminus in |- ×...
repeat rewrite Ropp_plus_distr...
repeat rewrite Ropp_involutive...
rewrite <- (Rplus_comm (x (tr evad) T))...
rewrite <- (Rplus_comm (y (tr evad) T))...
repeat rewrite Rmult_assoc...
repeat apply Rmult_eq_compat_l...
rewrite <- (Rmult_comm (V × T))...
repeat rewrite Rmult_assoc...
repeat rewrite Rsqr_mult...
rewrite sin2...
unfold Rminus in |- ×...
rewrite Rmult_plus_distr_l...
rewrite Rmult_1_r...
ring...
Qed.