proposition: Lemma cos_no_conflict : h intr = V -> h (tr evad) = V -> Alpha (beta intr evad T) = false -> (MinDistance T <= l intr evad T)%R -> (l intr evad T <= MaxDistance T)%R -> (cos (beta intr evad T + thetat intr 0) <= cos (beta intr evad T))%R -> Omega (thetat intr 0 + beta intr evad T) = false -> conflict intr evad T = false.
proof: Proof. Proof with trivial. intros hyp_intr hyp_evad; intros... unfold conflict in |- *... cut (l intr evad T * cos (beta intr evad T) < (Rsqr (ve evad * T) + Rsqr (l intr evad T) - Rsqr AlertRange) / (2 * ve evad * T))%R... cut ((thetat intr 0 + beta intr evad T < PI / 2)%R \/ (PI / 2 <= thetat intr 0 + beta intr evad T)%R /\ (3 * (PI / 2) < thetat intr 0 + beta intr evad T)%R)... intros... case (Rle_dec (Die intr evad T T) ConflictRange); intro... unfold Die in r... generalize (isometric_evader intr evad T T)... unfold Rsqr_evader_distance in |- *... unfold xe, ye in |- *... intro... rewrite H6 in r... cut (0 <= T)%R... cut (rho_vi intr * T <= PI / 2)%R... intros... generalize (ypt_PI2 intr evad T T H8 H7); intro... generalize (xpt_PI intr evad T T H8 (Rle_trans (rho_vi intr * T) (PI / 2) PI H7 (Rlt_le (PI / 2) PI PI2_Rlt_PI))); intro... elim H4; intros... rewrite Rplus_comm in H11... cut (MinBeta <= beta intr evad T + thetat intr 0)%R... intro... elim H9; intros... generalize (Math_prop_no_conflict_1 (beta intr evad T + thetat intr 0) (l intr evad T) (xp intr evad T T) (yp intr evad T T) T H0 H1 H12 (Rlt_le (beta intr evad T + thetat intr 0) (PI / 2) H11))... unfold r_V, rho_V in |- *... unfold r_vi, rho_vi in H13... unfold r_vi, rho_vi in H10... unfold vi in H10... rewrite hyp_intr in H10... unfold vi in H13... rewrite hyp_intr in H13... intro... generalize (H15 H13 H10)... intro... cut (0 <= sqrt (Rsqr (xp intr evad T T) + Rsqr (yp intr evad T T)))%R... cut (0 <= ConflictRange)%R... intros... generalize (Rsqr_incr_1 (sqrt (Rsqr (xp intr evad T T) + Rsqr (yp intr evad T T))) ConflictRange r H18 H17); intro... rewrite Rsqr_sqrt in H19... elim (Rlt_irrefl (Rsqr ConflictRange) (Rlt_le_trans (Rsqr ConflictRange) (Rsqr (xp intr evad T T) + Rsqr (yp intr evad T T)) (Rsqr ConflictRange) H16 H19))... apply Rplus_le_le_0_compat; apply Rle_0_sqr... unfold ConflictRange in |- *; left; prove_sup... apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr... apply cos_decr_0... generalize (beta_def intr evad T); intro... decompose [and] H12... left; apply Rlt_trans with (PI / 2)%R... apply PI2_Rlt_PI... left; apply MinBeta_pos... unfold MinBeta in |- *... left; apply Rlt_trans with 1%R... unfold Rdiv in |- *... apply Rmult_lt_reg_l with 1000%R... prove_sup... rewrite Rmult_1_r; rewrite (Rmult_comm 1000); rewrite Rmult_assoc... rewrite <- Rinv_l_sym; [ prove_sup | discrR ]... apply Rlt_trans with (PI / 2)%R... apply Rlt_1_PI2... apply PI2_Rlt_PI... apply Rle_trans with (cos (beta intr evad T))... apply cos_beta_NOT_Alpha... elim H11; intros... rewrite (Rplus_comm (thetat intr 0)) in H13... cut (beta intr evad T + thetat intr 0 <= 2 * PI - MinBeta)%R... intro... generalize (Math_prop_no_conflict_2 (beta intr evad T + thetat intr 0) (l intr evad T) (xp intr evad T T) (yp intr evad T T) T H0 H1 (Rlt_le (3 * (PI / 2)) (beta intr evad T + thetat intr 0) H13) H14); intro... unfold r_V, rho_V in H15... unfold r_vi, rho_vi in H10... elim H9; intros... unfold r_vi, rho_vi in H17... unfold vi in H17... rewrite hyp_intr in H17... unfold vi in H10... rewrite hyp_intr in H10... generalize (H15 H17 H10); intro... cut (0 <= sqrt (Rsqr (xp intr evad T T) + Rsqr (yp intr evad T T)))%R... cut (0 <= ConflictRange)%R... intros... generalize (Rsqr_incr_1 (sqrt (Rsqr (xp intr evad T T) + Rsqr (yp intr evad T T))) ConflictRange r H20 H19); intro... rewrite Rsqr_sqrt in H21... elim (Rlt_irrefl (Rsqr ConflictRange) (Rlt_le_trans (Rsqr ConflictRange) (Rsqr (xp intr evad T T) + Rsqr (yp intr evad T T)) (Rsqr ConflictRange) H18 H21))... apply Rplus_le_le_0_compat; apply Rle_0_sqr... unfold ConflictRange in |- *; left; prove_sup... apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr... apply cos_incr_0... left; apply Rlt_trans with (3 * (PI / 2))%R... pattern PI at 1 in |- *; rewrite <- (Rplus_0_r PI)... replace (3 * (PI / 2))%R with (PI + PI / 2)%R... apply Rplus_lt_compat_l... apply PI2_RGT_0... pattern PI at 1 in |- *; rewrite double_var; ring... generalize (beta_def intr evad T); intro... decompose [and] H14... left... left... apply Rplus_lt_reg_l with (MinBeta - PI)%R... replace (MinBeta - PI + PI)%R with MinBeta... replace (MinBeta - PI + (2 * PI - MinBeta))%R with PI... unfold MinBeta in |- *... apply Rlt_trans with 1%R... unfold Rdiv in |- *... apply Rmult_lt_reg_l with 1000%R... prove_sup... rewrite (Rmult_comm 1000); rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ repeat rewrite Rmult_1_r; prove_sup | discrR ]... apply Rlt_trans with (PI / 2)%R... apply Rlt_1_PI2... apply PI2_Rlt_PI... ring... ring... unfold Rminus in |- *... pattern (2 * PI)%R at 2 in |- *; rewrite <- (Rplus_0_r (2 * PI))... apply Rplus_le_compat_l... left; rewrite <- Ropp_0... apply Ropp_lt_gt_contravar... apply MinBeta_pos... unfold Rminus in |- *... rewrite (Rplus_comm (2 * PI))... generalize (cos_period (- MinBeta) 1)... unfold INR in |- *... rewrite Rmult_1_r... intro... rewrite H14... rewrite cos_neg... apply Rle_trans with (cos (beta intr evad T))... apply cos_beta_NOT_Alpha... left; replace (rho_vi intr) with rho_V... apply rho_t_PI2... unfold rho_vi, rho_V in |- *... unfold vi in |- *; rewrite hyp_intr... left; apply Rlt_le_trans with MinT... apply MinT_is_pos... apply (cond_1 T)... cut (Omega (thetat intr 0 + beta intr evad T) = false)... unfold Omega in |- *... case (Rle_dec (PI / 2) (thetat intr 0 + beta intr evad T)); intro... case (Rle_dec (thetat intr 0 + beta intr evad T) (3 * (PI / 2))); intros... elim diff_true_false... right... split... auto with real... intro... left; auto with real... cut (Alpha (beta intr evad T) = false)... unfold Alpha in |- *... case (Rle_dec ((Rsqr (ve evad * T) + Rsqr (l intr evad T) - Rsqr AlertRange) / (2 * ve evad * T)) (l intr evad T * cos (beta intr evad T))); intros... elim diff_true_false... auto with real... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory alarm