| products/Sources/formale Sprachen/Coq/theories/Reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Rgeom.v Sprache: CoqOriginal von: Coq© |
|
||||||
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo1. Require Import R_sqrt. Local Open 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. Proof. intros x0 y0; unfold dist_euc; 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; 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. Proof. intros x0 y0 x1 y1; unfold dist_euc; 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; 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). Proof. unfold dist_euc; intros; repeat rewrite Rsqr_sqrt; [ rewrite H; unfold Rsqr; 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. Proof. intros; unfold dist_euc; 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 (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) + (Rsqr (y0 - y2) + Rsqr (y2 - y1) + 2 * (y0 - y2) * (y2 - y1)))) 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 (2 * (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 | discriminate ] | apply sqrt_cauchy ] | ring ] | ring ] | 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 ]. Qed. (******************************************************************) (** * 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. Proof. intros x y; split; [ unfold xt | unfold yt ]; 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). Proof. intros; unfold Rsqr, xt, yt; ring. Qed. (******************************************************************) (** * 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. Proof. intros x y; unfold xr, yr; 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. Proof. intros x y; unfold xr, yr; 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). Proof. intros; unfold xr, yr; 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). Proof. unfold dist_euc; 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 *) (******************************************************************) 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). 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). Proof. intros; rewrite <- isometric_translation; apply isometric_rotation_0. Qed. ¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
