-
Notifications
You must be signed in to change notification settings - Fork 0
/
Ch04_congruence_between_properties.v
307 lines (258 loc) · 5.96 KB
/
Ch04_congruence_between_properties.v
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
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
(* Julien Narboux *)
(* Formalization of *)
(* Tarski's axiomatic *)
Require Export Ch03_between_properties.
Lemma l4_2 : forall A B C D A' B' C' D',
IFSC A B C D A' B' C' D' -> Cong B D B' D'.
Proof with Tarski.
intros.
unfold IFSC in H.
intuition.
cases_equality A C.
treat_equalities...
assert (exists E, Bet A C E /\ C <> E)...
DecompExAnd H6 E.
assert (exists E', Bet A' C' E' /\ Cong C' E' C E)...
DecompExAnd H6 E'.
assert (Cong E D E' D').
eapply five_segments_with_def.
assert (OFSC A C E D A' C' E' D').
unfold OFSC.
intuition.
apply H6.
assumption.
assert (OFSC E C B D E' C' B' D').
unfold OFSC.
intuition;esTarski.
esTarski.
Qed.
Lemma l4_3 : forall A B C A' B' C',
Bet A B C -> Bet A' B' C' ->
Cong A C A' C' -> Cong B C B' C' -> Cong A B A' B'.
Proof with Tarski.
intros.
assert (IFSC A B C A A' B' C' A').
unfold IFSC;intuition.
apply cong_commutativity.
eapply l4_2.
apply H3.
Qed.
Hint Resolve l4_2 l4_3 : Tarski.
(** A generalization of the Cong predicate for three points. *)
Definition Cong_3 := fun A1 A2 A3 B1 B2 B3 =>
Cong A1 A2 B1 B2 /\ Cong A1 A3 B1 B3 /\ Cong A2 A3 B2 B3.
Lemma l4_5 : forall A B C A' C',
Bet A B C -> Cong A C A' C' ->
exists B', Bet A' B' C' /\ Cong_3 A B C A' B' C'.
Proof with Tarski.
intros.
assert (exists D', Bet C' A' D' /\ A' <> D')...
DecompExAnd H1 D'.
assert (exists B', Bet D' A' B' /\ Cong A' B' A B)...
DecompExAnd H1 B'.
assert (exists C'', Bet D' B' C'' /\ Cong B' C'' B C)...
DecompExAnd H1 C''.
assert (Bet A' B' C'');Between.
assert (Bet D' A' C'');Between.
assert (Cong A C A' C'').
eapply l2_11.
apply H.
apply H1.
sTarski.
sTarski.
assert (C''=C').
assert (D' <> A').
auto.
eapply construction_unicity.
apply H10.
eauto.
apply cong_symmetry.
apply H9.
sTarski.
sTarski.
exists B'.
unfold Cong_3.
intuition.
subst C'...
subst C''.
sTarski.
Qed.
Hint Resolve l4_5 : Tarski.
Lemma l4_6 : forall A B C A' B' C',
Bet A B C -> Cong_3 A B C A' B' C' -> Bet A' B' C'.
Proof with Tarski.
intros.
assert (exists B'', Bet A' B'' C' /\ Cong_3 A B C A' B'' C').
eapply l4_5...
unfold Cong_3 in H0;intuition...
DecompExAnd H1 B''.
assert (Cong_3 A' B'' C' A' B' C').
unfold Cong_3 in *;intuition;esTarski.
assert (IFSC A' B'' C' B'' A' B'' C' B');unfold IFSC;intuition.
unfold Cong_3 in *;intuition...
unfold Cong_3 in *;intuition...
assert (Cong B'' B'' B'' B').
eapply l4_2;eauto.
treat_equalities...
Qed.
Hint Unfold Col.
(** Permutation lemmas for Col *)
Lemma col_permutation_1 : forall A B C,
Col A B C -> Col B C A.
Proof.
unfold Col.
intuition.
Qed.
Lemma col_permutation_2 : forall A B C,
Col A B C -> Col C A B.
Proof.
unfold Col.
intuition.
Qed.
Lemma col_permutation_3 : forall A B C,
Col A B C -> Col C B A.
Proof.
unfold Col.
intuition.
Qed.
Lemma col_permutation_4 : forall A B C,
Col A B C -> Col B A C.
Proof.
unfold Col.
intuition.
Qed.
Lemma col_permutation_5 : forall A B C,
Col A B C -> Col A C B.
Proof.
unfold Col.
intuition.
Qed.
Hint Resolve col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : sTarski.
Hint Resolve col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : Col.
Ltac Col := eauto with Col.
(** Trivial lemmas for Col. *)
Lemma col_trivial_1 : forall A B, Col A A B.
Proof.
unfold Col.
intuition.
Qed.
Lemma col_trivial_2 : forall A B, Col A B B.
Proof.
unfold Col.
intuition.
Qed.
Lemma col_trivial_3 : forall A B, Col A B A.
Proof.
unfold Col.
intuition.
Qed.
Hint Resolve col_trivial_1 col_trivial_2 col_trivial_3 : Tarski.
Lemma l4_13 : forall A B C A' B' C',
Col A B C -> Cong_3 A B C A' B' C' -> Col A' B' C'.
Proof.
unfold Col.
intros.
intuition.
left.
eapply l4_6;eauto.
right.
left.
eapply l4_6;eauto.
unfold Cong_3 in *;intuition.
right.
right.
eapply l4_6;eauto.
unfold Cong_3 in *;intuition.
Qed.
Lemma l4_14 : forall A B C A' B',
Col A B C -> Cong A B A' B' ->
exists C', Cong_3 A B C A' B' C'.
Proof with Tarski.
intros.
unfold Col in H;intuition.
assert (exists C', Bet A' B' C' /\ Cong B' C' B C)...
DecompExAnd H C'.
assert (Cong A C A' C').
eapply l2_11;esTarski.
exists C'...
unfold Cong_3;intuition...
Focus 2.
assert (exists C', Bet B' A' C' /\ Cong A' C' A C)...
DecompExAnd H1 C'.
exists C'...
unfold Cong_3;intuition...
eapply ( l2_11 B A C B' A' C');esTarski.
assert (exists B'0 : Point, Bet B' B'0 A' /\ Cong_3 B C A B' B'0 A').
eapply l4_5;esTarski.
DecompExAnd H1 C'.
exists C'...
unfold Cong_3 in *;intuition...
Qed.
(** Five segments configuration. *)
Definition FSC := fun A B C D A' B' C' D' =>
Col A B C /\ Cong_3 A B C A' B' C' /\ Cong A D A' D' /\ Cong B D B' D'.
Lemma l4_16 : forall A B C D A' B' C' D',
FSC A B C D A' B' C' D' -> A<>B -> Cong C D C' D'.
Proof with Tarski.
unfold FSC.
intros.
intuition.
unfold Col in H1.
intuition.
assert (Bet A' B' C').
eapply l4_6; try apply H3;unfold Cong_3 in *;intuition...
unfold Cong_3 in H;intuition.
assert (A<>B);auto.
eapply five_segments;try apply H5;auto.
assert (Bet B' C' A').
apply (l4_6 B C A B' C' A')...
unfold Cong_3 in *;intuition.
unfold Cong_3 in H;intuition.
assert (IFSC A C B D A' C' B' D').
unfold IFSC;intuition.
eapply l4_2.
apply H6.
assert (Bet C' A' B').
apply (l4_6 C A B C' A' B')...
unfold Cong_3 in *;intuition.
unfold Cong_3 in H;intuition.
eapply five_segments.
2:apply H.
3:assumption.
3:apply between_symmetry;apply H1.
3:apply between_symmetry;apply H3.
sTarski.
sTarski.
auto.
Qed.
Lemma l4_17 : forall A B C P Q,
A<>B -> Col A B C ->
Cong A P A Q -> Cong B P B Q -> Cong C P C Q.
Proof.
intros.
assert (FSC A B C P A B C Q);unfold FSC;unfold Cong_3;intuition.
eapply l4_16.
apply H3.
assumption.
Qed.
Lemma l4_18 : forall A B C C',
A<>B -> Col A B C ->
Cong A C A C' -> Cong B C B C' -> C=C'.
Proof.
intros.
assert (Cong C C C C').
eapply l4_17;eauto.
treat_equalities.
auto.
Qed.
Lemma l4_19 : forall A B C C',
Bet A C B -> Cong A C A C' -> Cong B C B C' -> C=C'.
Proof with Tarski.
intros.
cases_equality A B.
treat_equalities...
assert (Col A B C);unfold Col;intuition...
eapply l4_18;eauto.
Qed.