diff options
Diffstat (limited to 'theories/Reals/Rgeom.v')
| -rw-r--r-- | theories/Reals/Rgeom.v | 234 |
1 files changed, 124 insertions, 110 deletions
diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index 9ce20839..8ac9c07f 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rgeom.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Rgeom.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -14,174 +14,188 @@ Require Import SeqSeries. Require Import Rtrigo. Require Import R_sqrt. Open Local Scope R_scope. +(** * Distance *) + Definition dist_euc (x0 y0 x1 y1:R) : R := sqrt (Rsqr (x0 - x1) + Rsqr (y0 - y1)). Lemma distance_refl : forall x0 y0:R, dist_euc x0 y0 x0 y0 = 0. -intros x0 y0; unfold dist_euc in |- *; apply Rsqr_inj; - [ apply sqrt_positivity; apply Rplus_le_le_0_compat; - [ apply Rle_0_sqr | apply Rle_0_sqr ] - | right; reflexivity - | rewrite Rsqr_0; rewrite Rsqr_sqrt; - [ unfold Rsqr in |- *; ring - | apply Rplus_le_le_0_compat; [ apply Rle_0_sqr | apply Rle_0_sqr ] ] ]. +Proof. + intros x0 y0; unfold dist_euc in |- *; apply Rsqr_inj; + [ apply sqrt_positivity; apply Rplus_le_le_0_compat; + [ apply Rle_0_sqr | apply Rle_0_sqr ] + | right; reflexivity + | rewrite Rsqr_0; rewrite Rsqr_sqrt; + [ unfold Rsqr in |- *; ring + | apply Rplus_le_le_0_compat; [ apply Rle_0_sqr | apply Rle_0_sqr ] ] ]. Qed. Lemma distance_symm : - forall x0 y0 x1 y1:R, dist_euc x0 y0 x1 y1 = dist_euc x1 y1 x0 y0. -intros x0 y0 x1 y1; unfold dist_euc in |- *; apply Rsqr_inj; - [ apply sqrt_positivity; apply Rplus_le_le_0_compat - | apply sqrt_positivity; apply Rplus_le_le_0_compat - | repeat rewrite Rsqr_sqrt; - [ unfold Rsqr in |- *; ring - | apply Rplus_le_le_0_compat - | apply Rplus_le_le_0_compat ] ]; apply Rle_0_sqr. + forall x0 y0 x1 y1:R, dist_euc x0 y0 x1 y1 = dist_euc x1 y1 x0 y0. +Proof. + intros x0 y0 x1 y1; unfold dist_euc in |- *; apply Rsqr_inj; + [ apply sqrt_positivity; apply Rplus_le_le_0_compat + | apply sqrt_positivity; apply Rplus_le_le_0_compat + | repeat rewrite Rsqr_sqrt; + [ unfold Rsqr in |- *; ring + | apply Rplus_le_le_0_compat + | apply Rplus_le_le_0_compat ] ]; apply Rle_0_sqr. Qed. Lemma law_cosines : - forall x0 y0 x1 y1 x2 y2 ac:R, - let a := dist_euc x1 y1 x0 y0 in - let b := dist_euc x2 y2 x0 y0 in - let c := dist_euc x2 y2 x1 y1 in - a * c * cos ac = (x0 - x1) * (x2 - x1) + (y0 - y1) * (y2 - y1) -> - Rsqr b = Rsqr c + Rsqr a - 2 * (a * c * cos ac). -unfold dist_euc in |- *; intros; repeat rewrite Rsqr_sqrt; - [ rewrite H; unfold Rsqr in |- *; ring - | apply Rplus_le_le_0_compat - | apply Rplus_le_le_0_compat - | apply Rplus_le_le_0_compat ]; apply Rle_0_sqr. + forall x0 y0 x1 y1 x2 y2 ac:R, + let a := dist_euc x1 y1 x0 y0 in + let b := dist_euc x2 y2 x0 y0 in + let c := dist_euc x2 y2 x1 y1 in + a * c * cos ac = (x0 - x1) * (x2 - x1) + (y0 - y1) * (y2 - y1) -> + Rsqr b = Rsqr c + Rsqr a - 2 * (a * c * cos ac). +Proof. + unfold dist_euc in |- *; intros; repeat rewrite Rsqr_sqrt; + [ rewrite H; unfold Rsqr in |- *; ring + | apply Rplus_le_le_0_compat + | apply Rplus_le_le_0_compat + | apply Rplus_le_le_0_compat ]; apply Rle_0_sqr. Qed. Lemma triangle : - forall x0 y0 x1 y1 x2 y2:R, - dist_euc x0 y0 x1 y1 <= dist_euc x0 y0 x2 y2 + dist_euc x2 y2 x1 y1. -intros; unfold dist_euc in |- *; apply Rsqr_incr_0; - [ rewrite Rsqr_plus; repeat rewrite Rsqr_sqrt; - [ replace (Rsqr (x0 - x1)) with - (Rsqr (x0 - x2) + Rsqr (x2 - x1) + 2 * (x0 - x2) * (x2 - x1)); - [ replace (Rsqr (y0 - y1)) with + forall x0 y0 x1 y1 x2 y2:R, + dist_euc x0 y0 x1 y1 <= dist_euc x0 y0 x2 y2 + dist_euc x2 y2 x1 y1. +Proof. + intros; unfold dist_euc in |- *; apply Rsqr_incr_0; + [ rewrite Rsqr_plus; repeat rewrite Rsqr_sqrt; + [ replace (Rsqr (x0 - x1)) with + (Rsqr (x0 - x2) + Rsqr (x2 - x1) + 2 * (x0 - x2) * (x2 - x1)); + [ replace (Rsqr (y0 - y1)) with (Rsqr (y0 - y2) + Rsqr (y2 - y1) + 2 * (y0 - y2) * (y2 - y1)); [ apply Rplus_le_reg_l with - (- Rsqr (x0 - x2) - Rsqr (x2 - x1) - Rsqr (y0 - y2) - + (- Rsqr (x0 - x2) - Rsqr (x2 - x1) - Rsqr (y0 - y2) - Rsqr (y2 - y1)); - replace - (- Rsqr (x0 - x2) - Rsqr (x2 - x1) - Rsqr (y0 - y2) - - Rsqr (y2 - y1) + - (Rsqr (x0 - x2) + Rsqr (x2 - x1) + 2 * (x0 - x2) * (x2 - x1) + + replace + (- Rsqr (x0 - x2) - Rsqr (x2 - x1) - Rsqr (y0 - y2) - + Rsqr (y2 - y1) + + (Rsqr (x0 - x2) + Rsqr (x2 - x1) + 2 * (x0 - x2) * (x2 - x1) + (Rsqr (y0 - y2) + Rsqr (y2 - y1) + 2 * (y0 - y2) * (y2 - y1)))) - with (2 * ((x0 - x2) * (x2 - x1) + (y0 - y2) * (y2 - y1))); - [ replace + with (2 * ((x0 - x2) * (x2 - x1) + (y0 - y2) * (y2 - y1))); + [ replace (- Rsqr (x0 - x2) - Rsqr (x2 - x1) - Rsqr (y0 - y2) - - Rsqr (y2 - y1) + - (Rsqr (x0 - x2) + Rsqr (y0 - y2) + - (Rsqr (x2 - x1) + Rsqr (y2 - y1)) + - 2 * sqrt (Rsqr (x0 - x2) + Rsqr (y0 - y2)) * - sqrt (Rsqr (x2 - x1) + Rsqr (y2 - y1)))) with + Rsqr (y2 - y1) + + (Rsqr (x0 - x2) + Rsqr (y0 - y2) + + (Rsqr (x2 - x1) + Rsqr (y2 - y1)) + + 2 * sqrt (Rsqr (x0 - x2) + Rsqr (y0 - y2)) * + sqrt (Rsqr (x2 - x1) + Rsqr (y2 - y1)))) with (2 * - (sqrt (Rsqr (x0 - x2) + Rsqr (y0 - y2)) * - sqrt (Rsqr (x2 - x1) + Rsqr (y2 - y1)))); + (sqrt (Rsqr (x0 - x2) + Rsqr (y0 - y2)) * + sqrt (Rsqr (x2 - x1) + Rsqr (y2 - y1)))); [ apply Rmult_le_compat_l; - [ left; cut (0%nat <> 2%nat); - [ intros; generalize (lt_INR_0 2 (neq_O_lt 2 H)); - intro H0; assumption + [ left; cut (0%nat <> 2%nat); + [ intros; generalize (lt_INR_0 2 (neq_O_lt 2 H)); + intro H0; assumption | discriminate ] - | apply sqrt_cauchy ] + | apply sqrt_cauchy ] + | ring ] | ring ] - | ring ] + | ring_Rsqr ] | ring_Rsqr ] - | ring_Rsqr ] - | apply Rplus_le_le_0_compat; apply Rle_0_sqr - | apply Rplus_le_le_0_compat; apply Rle_0_sqr - | apply Rplus_le_le_0_compat; apply Rle_0_sqr ] - | apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr - | apply Rplus_le_le_0_compat; apply sqrt_positivity; - apply Rplus_le_le_0_compat; apply Rle_0_sqr ]. + | apply Rplus_le_le_0_compat; apply Rle_0_sqr + | apply Rplus_le_le_0_compat; apply Rle_0_sqr + | apply Rplus_le_le_0_compat; apply Rle_0_sqr ] + | apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr + | apply Rplus_le_le_0_compat; apply sqrt_positivity; + apply Rplus_le_le_0_compat; apply Rle_0_sqr ]. Qed. (******************************************************************) -(** Translation *) +(** * Translation *) (******************************************************************) Definition xt (x tx:R) : R := x + tx. Definition yt (y ty:R) : R := y + ty. Lemma translation_0 : forall x y:R, xt x 0 = x /\ yt y 0 = y. -intros x y; split; [ unfold xt in |- * | unfold yt in |- * ]; ring. +Proof. + intros x y; split; [ unfold xt in |- * | unfold yt in |- * ]; ring. Qed. Lemma isometric_translation : - forall x1 x2 y1 y2 tx ty:R, - Rsqr (x1 - x2) + Rsqr (y1 - y2) = - Rsqr (xt x1 tx - xt x2 tx) + Rsqr (yt y1 ty - yt y2 ty). -intros; unfold Rsqr, xt, yt in |- *; ring. + forall x1 x2 y1 y2 tx ty:R, + Rsqr (x1 - x2) + Rsqr (y1 - y2) = + Rsqr (xt x1 tx - xt x2 tx) + Rsqr (yt y1 ty - yt y2 ty). +Proof. + intros; unfold Rsqr, xt, yt in |- *; ring. Qed. (******************************************************************) -(** Rotation *) +(** * Rotation *) (******************************************************************) Definition xr (x y theta:R) : R := x * cos theta + y * sin theta. Definition yr (x y theta:R) : R := - x * sin theta + y * cos theta. Lemma rotation_0 : forall x y:R, xr x y 0 = x /\ yr x y 0 = y. -intros x y; unfold xr, yr in |- *; split; rewrite cos_0; rewrite sin_0; ring. +Proof. + intros x y; unfold xr, yr in |- *; split; rewrite cos_0; rewrite sin_0; ring. Qed. Lemma rotation_PI2 : - forall x y:R, xr x y (PI / 2) = y /\ yr x y (PI / 2) = - x. -intros x y; unfold xr, yr in |- *; split; rewrite cos_PI2; rewrite sin_PI2; - ring. + forall x y:R, xr x y (PI / 2) = y /\ yr x y (PI / 2) = - x. +Proof. + intros x y; unfold xr, yr in |- *; split; rewrite cos_PI2; rewrite sin_PI2; + ring. Qed. Lemma isometric_rotation_0 : - forall x1 y1 x2 y2 theta:R, - Rsqr (x1 - x2) + Rsqr (y1 - y2) = - Rsqr (xr x1 y1 theta - xr x2 y2 theta) + - Rsqr (yr x1 y1 theta - yr x2 y2 theta). -intros; unfold xr, yr in |- *; - replace - (x1 * cos theta + y1 * sin theta - (x2 * cos theta + y2 * sin theta)) with - (cos theta * (x1 - x2) + sin theta * (y1 - y2)); - [ replace - (- x1 * sin theta + y1 * cos theta - (- x2 * sin theta + y2 * cos theta)) - with (cos theta * (y1 - y2) + sin theta * (x2 - x1)); - [ repeat rewrite Rsqr_plus; repeat rewrite Rsqr_mult; repeat rewrite cos2; - ring; replace (x2 - x1) with (- (x1 - x2)); - [ rewrite <- Rsqr_neg; ring | ring ] - | ring ] - | ring ]. + forall x1 y1 x2 y2 theta:R, + Rsqr (x1 - x2) + Rsqr (y1 - y2) = + Rsqr (xr x1 y1 theta - xr x2 y2 theta) + + Rsqr (yr x1 y1 theta - yr x2 y2 theta). +Proof. + intros; unfold xr, yr in |- *; + replace + (x1 * cos theta + y1 * sin theta - (x2 * cos theta + y2 * sin theta)) with + (cos theta * (x1 - x2) + sin theta * (y1 - y2)); + [ replace + (- x1 * sin theta + y1 * cos theta - (- x2 * sin theta + y2 * cos theta)) + with (cos theta * (y1 - y2) + sin theta * (x2 - x1)); + [ repeat rewrite Rsqr_plus; repeat rewrite Rsqr_mult; repeat rewrite cos2; + ring_simplify; replace (x2 - x1) with (- (x1 - x2)); + [ rewrite <- Rsqr_neg; ring | ring ] + | ring ] + | ring ]. Qed. Lemma isometric_rotation : - forall x1 y1 x2 y2 theta:R, - dist_euc x1 y1 x2 y2 = - dist_euc (xr x1 y1 theta) (yr x1 y1 theta) (xr x2 y2 theta) - (yr x2 y2 theta). -unfold dist_euc in |- *; intros; apply Rsqr_inj; - [ apply sqrt_positivity; apply Rplus_le_le_0_compat - | apply sqrt_positivity; apply Rplus_le_le_0_compat - | repeat rewrite Rsqr_sqrt; - [ apply isometric_rotation_0 - | apply Rplus_le_le_0_compat - | apply Rplus_le_le_0_compat ] ]; apply Rle_0_sqr. + forall x1 y1 x2 y2 theta:R, + dist_euc x1 y1 x2 y2 = + dist_euc (xr x1 y1 theta) (yr x1 y1 theta) (xr x2 y2 theta) + (yr x2 y2 theta). +Proof. + unfold dist_euc in |- *; intros; apply Rsqr_inj; + [ apply sqrt_positivity; apply Rplus_le_le_0_compat + | apply sqrt_positivity; apply Rplus_le_le_0_compat + | repeat rewrite Rsqr_sqrt; + [ apply isometric_rotation_0 + | apply Rplus_le_le_0_compat + | apply Rplus_le_le_0_compat ] ]; apply Rle_0_sqr. Qed. (******************************************************************) -(** Similarity *) +(** * Similarity *) (******************************************************************) Lemma isometric_rot_trans : - forall x1 y1 x2 y2 tx ty theta:R, - Rsqr (x1 - x2) + Rsqr (y1 - y2) = - Rsqr (xr (xt x1 tx) (yt y1 ty) theta - xr (xt x2 tx) (yt y2 ty) theta) + - Rsqr (yr (xt x1 tx) (yt y1 ty) theta - yr (xt x2 tx) (yt y2 ty) theta). -intros; rewrite <- isometric_rotation_0; apply isometric_translation. + forall x1 y1 x2 y2 tx ty theta:R, + Rsqr (x1 - x2) + Rsqr (y1 - y2) = + Rsqr (xr (xt x1 tx) (yt y1 ty) theta - xr (xt x2 tx) (yt y2 ty) theta) + + Rsqr (yr (xt x1 tx) (yt y1 ty) theta - yr (xt x2 tx) (yt y2 ty) theta). +Proof. + intros; rewrite <- isometric_rotation_0; apply isometric_translation. Qed. Lemma isometric_trans_rot : - forall x1 y1 x2 y2 tx ty theta:R, - Rsqr (x1 - x2) + Rsqr (y1 - y2) = - Rsqr (xt (xr x1 y1 theta) tx - xt (xr x2 y2 theta) tx) + - Rsqr (yt (yr x1 y1 theta) ty - yt (yr x2 y2 theta) ty). -intros; rewrite <- isometric_translation; apply isometric_rotation_0. -Qed.
\ No newline at end of file + forall x1 y1 x2 y2 tx ty theta:R, + Rsqr (x1 - x2) + Rsqr (y1 - y2) = + Rsqr (xt (xr x1 y1 theta) tx - xt (xr x2 y2 theta) tx) + + Rsqr (yt (yr x1 y1 theta) ty - yt (yr x2 y2 theta) ty). +Proof. + intros; rewrite <- isometric_translation; apply isometric_rotation_0. +Qed. |