proposition: Lemma conflict_beta_theta : forall (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: Proof. 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.
imports: Bool Reals trajectory_const trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory