proposition: Theorem ails_alarm_when_conflict : forall (intr : Trajectory) (evad : EvaderTrajectory) (T : TimeT), h intr = V -> h (tr evad) = V -> (AlertRange < d intr evad)%R -> conflict intr evad T = true -> ails_alert (measure2state intr 0) (measure2state (tr evad) 0).
proof: Proof. Proof with trivial. intros; cut (Die intr evad T T <= ConflictRange)%R... intro... case (Rle_dec (l intr evad T) (MaxDistance T)); intro... case (Rle_dec (MinDistance T) (l intr evad T)); intro... cut (Omega (beta intr evad T + thetat intr 0) = false)... intro; apply (ails_alarm_tau_gt0 intr evad T)... case (Rle_dec (tau (measure2state intr 0) (measure2state (tr evad) 0) 0) 0); intro... rewrite Rplus_comm in H4; generalize (ails_no_conflict_tau_le0 intr evad T H H0 r0 r H1 H4 r1); intro; rewrite H5 in H2; elim diff_false_true... auto with real... cut (Omega (beta intr evad T + thetat intr 0) = false \/ Omega (beta intr evad T + thetat intr 0) = true)... intro; elim H4; intro... cut (ConflictRange + vi intr < l intr evad T)%R... cut (rho_vi intr * T <= PI - rho_vi intr)%R... intros; generalize (no_conflict_Omega intr evad T H7 H6 H5); intro; rewrite H8 in H2; elim diff_false_true... apply Rplus_le_reg_l with (rho_vi intr)... replace (rho_vi intr + (PI - rho_vi intr))%R with PI... cut (rho_vi intr <= rho_vi intr * T)%R... intro; apply Rle_trans with (rho_vi intr * T + rho_vi intr * T)%R... apply Rplus_le_compat_r... cut (rho_vi intr * T <= PI / 2)%R... intro; rewrite (double_var PI); apply Rle_trans with (rho_vi intr * T + PI / 2)%R... apply Rplus_le_compat_l... apply Rplus_le_compat_r... left; replace (rho_vi intr) with rho_V... apply rho_t_PI2... unfold rho_V, rho_vi in |- *; unfold vi in |- *; rewrite H... pattern (rho_vi intr) at 1 in |- *; rewrite <- (Rmult_1_r (rho_vi intr)); apply rho_t_le; left; apply Rlt_le_trans with MinT... unfold MinT in |- *; unfold MaxT, tstep in |- *; apply Rmult_lt_reg_l with 2%R... prove_sup... rewrite Rmult_1_r; rewrite Rmult_minus_distr_l... rewrite <- Rinv_r_sym; [ prove_sup | discrR ]... apply (cond_1 T)... ring... apply Rlt_le_trans with (MinDistance T)... apply Rlt_le_trans with MinDistance_lb... replace (vi intr) with V... rewrite Rplus_comm... apply MinDistance_lb_majoration... apply MinDistance_lb_0... unfold Omega in |- *; case (Rle_dec (PI / 2) (beta intr evad T + thetat intr 0)); intro... case (Rle_dec (beta intr evad T + thetat intr 0) (3 * (PI / 2))); intros... right... left... left... cut (l intr evad T < MinDistance T)%R... cut (0 <= rho_vi intr * T)%R... cut (rho_vi intr * T < 2)%R... intros; unfold MinDistance in H4; unfold m in H4... cut (r_V = r_vi intr)... cut (rho_V = rho_vi intr)... intros; unfold MinDistance in H6; unfold m in H6... rewrite H8 in H6; rewrite H7 in H6... generalize (no_conflict_lt_min intr evad T H5 H4 H6); intro... rewrite H9 in H2... elim diff_false_true... unfold rho_V, rho_vi in |- *; unfold vi in |- *; rewrite H... unfold r_V, r_vi in |- *; unfold vi in |- *; rewrite H... replace (rho_vi intr) with rho_V... apply rho_t_2... unfold rho_V, rho_vi in |- *; unfold vi in |- *; rewrite H... left; apply Rmult_lt_0_compat... unfold rho_vi in |- *; apply rrho.rho_pos... apply Rlt_le_trans with MinT... apply MinT_is_pos... apply (cond_1 T)... auto with real... cut (MaxDistance T < l intr evad T)%R... intro; unfold MaxDistance in H4; cut (V = vi intr)... intro; rewrite H5 in H4... generalize (no_conflict_gt_max intr evad T H4); intro... rewrite H6 in H2... elim diff_false_true... symmetry in |- *; unfold vi in |- *; rewrite H... auto with real... apply (conflict_T_e_0 intr evad T)... Qed.
imports: Bool Reals trajectory_const trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory alarm alpha_no_conflict