1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
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.
|
