1 (* ========================================================================= *)
2 (* #87: Desargues's theorem. *)
3 (* ========================================================================= *)
5 needs "Multivariate/cross.ml";;
7 (* ------------------------------------------------------------------------- *)
8 (* A lemma we want to justify some of the axioms. *)
9 (* ------------------------------------------------------------------------- *)
11 let NORMAL_EXISTS = prove
12 (`!u v:real^3. ?w. ~(w = vec 0) /\ orthogonal u w /\ orthogonal v w`,
13 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[ORTHOGONAL_SYM] THEN
14 MP_TAC(ISPEC `{u:real^3,v}` ORTHOGONAL_TO_SUBSPACE_EXISTS) THEN
15 REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY; DIMINDEX_3] THEN
16 DISCH_THEN MATCH_MP_TAC THEN MATCH_MP_TAC LET_TRANS THEN
17 EXISTS_TAC `CARD {u:real^3,v}` THEN CONJ_TAC THEN
18 SIMP_TAC[DIM_LE_CARD; FINITE_INSERT; FINITE_EMPTY] THEN
19 SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN ARITH_TAC);;
21 (* ------------------------------------------------------------------------- *)
22 (* Type of directions. *)
23 (* ------------------------------------------------------------------------- *)
25 let direction_tybij = new_type_definition "direction" ("mk_dir","dest_dir")
26 (MESON[BASIS_NONZERO; LE_REFL; DIMINDEX_GE_1] `?x:real^3. ~(x = vec 0)`);;
28 parse_as_infix("||",(11,"right"));;
29 parse_as_infix("_|_",(11,"right"));;
31 let perpdir = new_definition
32 `x _|_ y <=> orthogonal (dest_dir x) (dest_dir y)`;;
34 let pardir = new_definition
35 `x || y <=> (dest_dir x) cross (dest_dir y) = vec 0`;;
37 let DIRECTION_CLAUSES = prove
38 (`((!x. P(dest_dir x)) <=> (!x. ~(x = vec 0) ==> P x)) /\
39 ((?x. P(dest_dir x)) <=> (?x. ~(x = vec 0) /\ P x))`,
40 MESON_TAC[direction_tybij]);;
42 let [PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS] = (CONJUNCTS o prove)
44 (!x y. x || y <=> y || x) /\
45 (!x y z. x || y /\ y || z ==> x || z)`,
46 REWRITE_TAC[pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);;
48 let PARDIR_EQUIV = prove
49 (`!x y. ((||) x = (||) y) <=> x || y`,
50 REWRITE_TAC[FUN_EQ_THM] THEN
51 MESON_TAC[PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS]);;
53 let DIRECTION_AXIOM_1 = prove
54 (`!p p'. ~(p || p') ==> ?l. p _|_ l /\ p' _|_ l /\
55 !l'. p _|_ l' /\ p' _|_ l' ==> l' || l`,
56 REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN REPEAT STRIP_TAC THEN
57 MP_TAC(SPECL [`p:real^3`; `p':real^3`] NORMAL_EXISTS) THEN
58 MATCH_MP_TAC MONO_EXISTS THEN
59 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);;
61 let DIRECTION_AXIOM_2 = prove
62 (`!l l'. ?p. p _|_ l /\ p _|_ l'`,
63 REWRITE_TAC[perpdir; DIRECTION_CLAUSES] THEN
64 MESON_TAC[NORMAL_EXISTS; ORTHOGONAL_SYM]);;
66 let DIRECTION_AXIOM_3 = prove
68 ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\
69 ~(?l. p _|_ l /\ p' _|_ l /\ p'' _|_ l)`,
70 REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN MAP_EVERY
71 (fun t -> EXISTS_TAC t THEN SIMP_TAC[BASIS_NONZERO; DIMINDEX_3; ARITH])
72 [`basis 1 :real^3`; `basis 2 : real^3`; `basis 3 :real^3`] THEN
75 let DIRECTION_AXIOM_4_WEAK = prove
76 (`!l. ?p p'. ~(p || p') /\ p _|_ l /\ p' _|_ l`,
77 REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN REPEAT STRIP_TAC THEN
79 `orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 2) l /\
80 ~((l cross basis 1) cross (l cross basis 2) = vec 0) \/
81 orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 3) l /\
82 ~((l cross basis 1) cross (l cross basis 3) = vec 0) \/
83 orthogonal (l cross basis 2) l /\ orthogonal (l cross basis 3) l /\
84 ~((l cross basis 2) cross (l cross basis 3) = vec 0)`
85 MP_TAC THENL [POP_ASSUM MP_TAC THEN VEC3_TAC; MESON_TAC[CROSS_0]]);;
87 let ORTHOGONAL_COMBINE = prove
88 (`!x a b. a _|_ x /\ b _|_ x /\ ~(a || b)
89 ==> ?c. c _|_ x /\ ~(a || c) /\ ~(b || c)`,
90 REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN
91 REPEAT STRIP_TAC THEN EXISTS_TAC `a + b:real^3` THEN
92 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);;
94 let DIRECTION_AXIOM_4 = prove
95 (`!l. ?p p' p''. ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\
96 p _|_ l /\ p' _|_ l /\ p'' _|_ l`,
97 MESON_TAC[DIRECTION_AXIOM_4_WEAK; ORTHOGONAL_COMBINE]);;
99 let line_tybij = define_quotient_type "line" ("mk_line","dest_line") `(||)`;;
101 let PERPDIR_WELLDEF = prove
102 (`!x y x' y'. x || x' /\ y || y' ==> (x _|_ y <=> x' _|_ y')`,
103 REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);;
106 lift_function (snd line_tybij) (PARDIR_REFL,PARDIR_TRANS)
107 "perpl" PERPDIR_WELLDEF;;
109 let line_lift_thm = lift_theorem line_tybij
110 (PARDIR_REFL,PARDIR_SYM,PARDIR_TRANS) [perpl_th];;
112 let LINE_AXIOM_1 = line_lift_thm DIRECTION_AXIOM_1;;
113 let LINE_AXIOM_2 = line_lift_thm DIRECTION_AXIOM_2;;
114 let LINE_AXIOM_3 = line_lift_thm DIRECTION_AXIOM_3;;
115 let LINE_AXIOM_4 = line_lift_thm DIRECTION_AXIOM_4;;
117 let point_tybij = new_type_definition "point" ("mk_point","dest_point")
118 (prove(`?x:line. T`,REWRITE_TAC[]));;
120 parse_as_infix("on",(11,"right"));;
122 let on = new_definition `p on l <=> perpl (dest_point p) l`;;
124 let POINT_CLAUSES = prove
125 (`((p = p') <=> (dest_point p = dest_point p')) /\
126 ((!p. P (dest_point p)) <=> (!l. P l)) /\
127 ((?p. P (dest_point p)) <=> (?l. P l))`,
128 MESON_TAC[point_tybij]);;
130 let POINT_TAC th = REWRITE_TAC[on; POINT_CLAUSES] THEN ACCEPT_TAC th;;
133 (`!p p'. ~(p = p') ==> ?l. p on l /\ p' on l /\
134 !l'. p on l' /\ p' on l' ==> (l' = l)`,
135 POINT_TAC LINE_AXIOM_1);;
138 (`!l l'. ?p. p on l /\ p on l'`,
139 POINT_TAC LINE_AXIOM_2);;
142 (`?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
143 ~(?l. p on l /\ p' on l /\ p'' on l)`,
144 POINT_TAC LINE_AXIOM_3);;
147 (`!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
148 p on l /\ p' on l /\ p'' on l`,
149 POINT_TAC LINE_AXIOM_4);;
151 (* ------------------------------------------------------------------------- *)
152 (* Mappings from vectors in R^3 to projective lines and points. *)
153 (* ------------------------------------------------------------------------- *)
155 let projl = new_definition
156 `projl x = mk_line((||) (mk_dir x))`;;
158 let projp = new_definition
159 `projp x = mk_point(projl x)`;;
161 (* ------------------------------------------------------------------------- *)
162 (* Mappings in the other direction, to (some) homogeneous coordinates. *)
163 (* ------------------------------------------------------------------------- *)
165 let PROJL_TOTAL = prove
166 (`!l. ?x. ~(x = vec 0) /\ l = projl x`,
168 SUBGOAL_THEN `?d. l = mk_line((||) d)` (CHOOSE_THEN SUBST1_TAC) THENL
169 [MESON_TAC[fst line_tybij; snd line_tybij];
170 REWRITE_TAC[projl] THEN EXISTS_TAC `dest_dir d` THEN
171 MESON_TAC[direction_tybij]]);;
173 let homol = new_specification ["homol"]
174 (REWRITE_RULE[SKOLEM_THM] PROJL_TOTAL);;
176 let PROJP_TOTAL = prove
177 (`!p. ?x. ~(x = vec 0) /\ p = projp x`,
178 REWRITE_TAC[projp] THEN MESON_TAC[PROJL_TOTAL; point_tybij]);;
180 let homop_def = new_definition
181 `homop p = homol(dest_point p)`;;
184 (`!p. ~(homop p = vec 0) /\ p = projp(homop p)`,
185 GEN_TAC THEN REWRITE_TAC[homop_def; projp; MESON[point_tybij]
186 `p = mk_point l <=> dest_point p = l`] THEN
187 MATCH_ACCEPT_TAC homol);;
189 (* ------------------------------------------------------------------------- *)
190 (* Key equivalences of concepts in projective space and homogeneous coords. *)
191 (* ------------------------------------------------------------------------- *)
193 let parallel = new_definition
194 `parallel x y <=> x cross y = vec 0`;;
197 (`!p l. p on l <=> orthogonal (homop p) (homol l)`,
199 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [homop; homol] THEN
200 REWRITE_TAC[on; projp; projl; REWRITE_RULE[] point_tybij] THEN
201 REWRITE_TAC[GSYM perpl_th; perpdir] THEN BINOP_TAC THEN
202 MESON_TAC[homol; homop; direction_tybij]);;
205 (`!l l'. l = l' <=> parallel (homol l) (homol l')`,
207 GEN_REWRITE_TAC (LAND_CONV o BINOP_CONV) [homol] THEN
208 REWRITE_TAC[projl; MESON[fst line_tybij; snd line_tybij]
209 `mk_line((||) l) = mk_line((||) l') <=> (||) l = (||) l'`] THEN
210 REWRITE_TAC[PARDIR_EQUIV] THEN REWRITE_TAC[pardir; parallel] THEN
211 MESON_TAC[homol; direction_tybij]);;
214 (`!p p'. p = p' <=> parallel (homop p) (homop p')`,
215 REWRITE_TAC[homop_def; GSYM EQ_HOMOL] THEN
216 MESON_TAC[point_tybij]);;
218 (* ------------------------------------------------------------------------- *)
219 (* A "welldefinedness" result for homogeneous coordinate map. *)
220 (* ------------------------------------------------------------------------- *)
222 let PARALLEL_PROJL_HOMOL = prove
223 (`!x. parallel x (homol(projl x))`,
224 GEN_TAC THEN REWRITE_TAC[parallel] THEN ASM_CASES_TAC `x:real^3 = vec 0` THEN
225 ASM_REWRITE_TAC[CROSS_0] THEN MP_TAC(ISPEC `projl x` homol) THEN
226 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
227 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [projl] THEN
228 DISCH_THEN(MP_TAC o AP_TERM `dest_line`) THEN
229 REWRITE_TAC[MESON[fst line_tybij; snd line_tybij]
230 `dest_line(mk_line((||) l)) = (||) l`] THEN
231 REWRITE_TAC[PARDIR_EQUIV] THEN REWRITE_TAC[pardir] THEN
232 ASM_MESON_TAC[direction_tybij]);;
234 let PARALLEL_PROJP_HOMOP = prove
235 (`!x. parallel x (homop(projp x))`,
236 REWRITE_TAC[homop_def; projp; REWRITE_RULE[] point_tybij] THEN
237 REWRITE_TAC[PARALLEL_PROJL_HOMOL]);;
239 let PARALLEL_PROJP_HOMOP_EXPLICIT = prove
240 (`!x. ~(x = vec 0) ==> ?a. ~(a = &0) /\ homop(projp x) = a % x`,
241 MP_TAC PARALLEL_PROJP_HOMOP THEN MATCH_MP_TAC MONO_FORALL THEN
242 REWRITE_TAC[parallel; CROSS_EQ_0; COLLINEAR_LEMMA] THEN
243 GEN_TAC THEN ASM_CASES_TAC `x:real^3 = vec 0` THEN
244 ASM_REWRITE_TAC[homop] THEN MATCH_MP_TAC MONO_EXISTS THEN
245 X_GEN_TAC `c:real` THEN ASM_CASES_TAC `c = &0` THEN
246 ASM_REWRITE_TAC[homop; VECTOR_MUL_LZERO]);;
248 (* ------------------------------------------------------------------------- *)
249 (* Brackets, collinearity and their connection. *)
250 (* ------------------------------------------------------------------------- *)
253 `bracket[a;b;c] = det(vector[homop a;homop b;homop c])`;;
255 let COLLINEAR = new_definition
256 `COLLINEAR s <=> ?l. !p. p IN s ==> p on l`;;
258 let COLLINEAR_SINGLETON = prove
259 (`!a. COLLINEAR {a}`,
260 REWRITE_TAC[COLLINEAR; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
261 MESON_TAC[AXIOM_1; AXIOM_3]);;
263 let COLLINEAR_PAIR = prove
264 (`!a b. COLLINEAR{a,b}`,
265 REPEAT GEN_TAC THEN ASM_CASES_TAC `a:point = b` THEN
266 ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SINGLETON] THEN
267 REWRITE_TAC[COLLINEAR; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
268 ASM_MESON_TAC[AXIOM_1]);;
270 let COLLINEAR_TRIPLE = prove
271 (`!a b c. COLLINEAR{a,b,c} <=> ?l. a on l /\ b on l /\ c on l`,
272 REWRITE_TAC[COLLINEAR; FORALL_IN_INSERT; NOT_IN_EMPTY]);;
274 let COLLINEAR_BRACKET = prove
275 (`!p1 p2 p3. COLLINEAR {p1,p2,p3} <=> bracket[p1;p2;p3] = &0`,
278 x cross y = vec 0 /\ ~(x = vec 0) /\
279 orthogonal a x /\ orthogonal b x /\ orthogonal c x
280 ==> orthogonal a y /\ orthogonal b y /\ orthogonal c y`,
281 REWRITE_TAC[orthogonal] THEN VEC3_TAC) in
282 REPEAT GEN_TAC THEN EQ_TAC THENL
283 [REWRITE_TAC[COLLINEAR_TRIPLE; bracket; ON_HOMOL; LEFT_IMP_EXISTS_THM] THEN
284 MP_TAC homol THEN MATCH_MP_TAC MONO_FORALL THEN
285 GEN_TAC THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN
286 REWRITE_TAC[DET_3; orthogonal; DOT_3; VECTOR_3; CART_EQ;
287 DIMINDEX_3; FORALL_3; VEC_COMPONENT] THEN
289 ASM_CASES_TAC `p1:point = p2` THENL
290 [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_PAIR]; ALL_TAC] THEN
291 POP_ASSUM MP_TAC THEN
292 REWRITE_TAC[parallel; COLLINEAR_TRIPLE; bracket; EQ_HOMOP; ON_HOMOL] THEN
293 REPEAT STRIP_TAC THEN
294 EXISTS_TAC `mk_line((||) (mk_dir(homop p1 cross homop p2)))` THEN
295 MATCH_MP_TAC lemma THEN EXISTS_TAC `homop p1 cross homop p2` THEN
296 ASM_REWRITE_TAC[ORTHOGONAL_CROSS] THEN
297 REWRITE_TAC[orthogonal] THEN ONCE_REWRITE_TAC[DOT_SYM] THEN
298 ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ONCE_REWRITE_TAC[DOT_SYM] THEN
299 ASM_REWRITE_TAC[DOT_CROSS_DET] THEN
300 REWRITE_TAC[GSYM projl; GSYM parallel; PARALLEL_PROJL_HOMOL]]);;
302 (* ------------------------------------------------------------------------- *)
303 (* Rather crude shuffling of bracket triple into canonical order. *)
304 (* ------------------------------------------------------------------------- *)
306 let BRACKET_SWAP,BRACKET_SHUFFLE = (CONJ_PAIR o prove)
307 (`bracket[x;y;z] = --bracket[x;z;y] /\
308 bracket[x;y;z] = bracket[y;z;x] /\
309 bracket[x;y;z] = bracket[z;x;y]`,
310 REWRITE_TAC[bracket; DET_3; VECTOR_3] THEN CONV_TAC REAL_RING);;
312 let BRACKET_SWAP_CONV =
313 let conv = GEN_REWRITE_CONV I [BRACKET_SWAP] in
314 fun tm -> let th = conv tm in
315 let tm' = rand(rand(concl th)) in
316 if term_order tm tm' then th else failwith "BRACKET_SWAP_CONV";;
318 (* ------------------------------------------------------------------------- *)
319 (* Direct proof following Richter-Gebert's "Meditations on Ceva's Theorem", *)
320 (* except for a change of variable names. The degenerate conditions here are *)
321 (* just those that naturally get used in the proof. *)
322 (* ------------------------------------------------------------------------- *)
324 let DESARGUES_DIRECT = prove
325 (`~COLLINEAR {A',B,S} /\
326 ~COLLINEAR {A,P,C} /\
327 ~COLLINEAR {A,P,R} /\
328 ~COLLINEAR {A,C,B} /\
329 ~COLLINEAR {A,B,R} /\
330 ~COLLINEAR {C',P,A'} /\
331 ~COLLINEAR {C',P,B} /\
332 ~COLLINEAR {C',P,B'} /\
333 ~COLLINEAR {C',A',S} /\
334 ~COLLINEAR {C',A',B'} /\
335 ~COLLINEAR {P,C,A'} /\
336 ~COLLINEAR {P,C,B} /\
337 ~COLLINEAR {P,A',R} /\
338 ~COLLINEAR {P,B,Q} /\
339 ~COLLINEAR {P,Q,B'} /\
340 ~COLLINEAR {C,B,S} /\
342 ==> COLLINEAR {P,A',A} /\
343 COLLINEAR {P,B,B'} /\
344 COLLINEAR {P,C',C} /\
346 COLLINEAR {B',C',Q} /\
348 COLLINEAR {A',C',R} /\
351 ==> COLLINEAR {Q,S,R}`,
352 REPEAT GEN_TAC THEN REWRITE_TAC[COLLINEAR_BRACKET] THEN DISCH_TAC THEN
354 `(bracket[P;A';A] = &0
355 ==> bracket[P;A';R] * bracket[P;A;C] =
356 bracket[P;A';C] * bracket[P;A;R]) /\
357 (bracket[P;B;B'] = &0
358 ==> bracket[P;B;Q] * bracket[P;B';C'] =
359 bracket[P;B;C'] * bracket[P;B';Q]) /\
360 (bracket[P;C';C] = &0
361 ==> bracket[P;C';B] * bracket[P;C;A'] =
362 bracket[P;C';A'] * bracket[P;C;B]) /\
364 ==> bracket[B;C;P] * bracket[B;Q;S] =
365 bracket[B;C;S] * bracket[B;Q;P]) /\
366 (bracket[B';C';Q] = &0
367 ==> bracket[B';C';A'] * bracket[B';Q;P] =
368 bracket[B';C';P] * bracket[B';Q;A']) /\
370 ==> bracket[A;R;P] * bracket[A;C;B] =
371 bracket[A;R;B] * bracket[A;C;P]) /\
372 (bracket[A';C';R] = &0
373 ==> bracket[A';C';P] * bracket[A';R;S] =
374 bracket[A';C';S] * bracket[A';R;P]) /\
376 ==> bracket[B;S;C] * bracket[B;A;R] =
377 bracket[B;S;R] * bracket[B;A;C]) /\
378 (bracket[A';S;B'] = &0
379 ==> bracket[A';S;C'] * bracket[A';B';Q] =
380 bracket[A';S;Q] * bracket[A';B';C'])`
382 [REWRITE_TAC[bracket; DET_3; VECTOR_3] THEN CONV_TAC REAL_RING;
384 REPEAT(MATCH_MP_TAC(TAUT
385 `(c ==> d ==> b ==> e) ==> ((a ==> b) /\ c ==> a /\ d ==> e)`)) THEN
386 DISCH_THEN(fun th -> DISCH_THEN(MP_TAC o MATCH_MP th)) THEN
387 REPEAT(ONCE_REWRITE_TAC[IMP_IMP] THEN
388 DISCH_THEN(MP_TAC o MATCH_MP (REAL_RING
389 `a = b /\ x:real = y ==> a * x = b * y`))) THEN
390 POP_ASSUM MP_TAC THEN REWRITE_TAC[BRACKET_SHUFFLE] THEN
391 CONV_TAC(ONCE_DEPTH_CONV BRACKET_SWAP_CONV) THEN
392 REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_LNEG; REAL_MUL_RNEG] THEN
393 REWRITE_TAC[REAL_NEG_NEG; REAL_NEG_EQ_0] THEN DISCH_TAC THEN
394 MATCH_MP_TAC(TAUT `!b. (a ==> b) /\ (b ==> c) ==> a ==> c`) THEN
395 EXISTS_TAC `bracket[B;Q;S] * bracket[A';R;S] =
396 bracket[B;R;S] * bracket[A';Q;S]` THEN
397 CONJ_TAC THENL [POP_ASSUM MP_TAC THEN CONV_TAC REAL_RING; ALL_TAC] THEN
398 FIRST_X_ASSUM(MP_TAC o CONJUNCT1) THEN
399 REWRITE_TAC[bracket; DET_3; VECTOR_3] THEN CONV_TAC REAL_RING);;