100/pascal.ml

   1 (* ========================================================================= *)
   2 (* Pascal's hexagon theorem for projective and affine planes.                *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/cross.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* A lemma we want to justify some of the axioms.                            *)
   9 (* ------------------------------------------------------------------------- *)
  10
  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);;
  20
  21 (* ------------------------------------------------------------------------- *)
  22 (* Type of directions.                                                       *)
  23 (* ------------------------------------------------------------------------- *)
  24
  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)`);;
  27
  28 parse_as_infix("||",(11,"right"));;
  29 parse_as_infix("_|_",(11,"right"));;
  30
  31 let perpdir = new_definition
  32  `x _|_ y <=> orthogonal (dest_dir x) (dest_dir y)`;;
  33
  34 let pardir = new_definition
  35  `x || y <=> (dest_dir x) cross (dest_dir y) = vec 0`;;
  36
  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]);;
  41
  42 let [PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS] = (CONJUNCTS o prove)
  43  (`(!x. x || x) /\
  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);;
  47
  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]);;
  52
  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);;
  60
  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]);;
  65
  66 let DIRECTION_AXIOM_3 = prove
  67  (`?p p' p''.
  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
  73   VEC3_TAC);;
  74
  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
  78   SUBGOAL_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]]);;
  86
  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);;
  93
  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]);;
  98
  99 let line_tybij = define_quotient_type "line" ("mk_line","dest_line") `(||)`;;
 100
 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);;
 104
 105 let perpl,perpl_th =
 106   lift_function (snd line_tybij) (PARDIR_REFL,PARDIR_TRANS)
 107                 "perpl" PERPDIR_WELLDEF;;
 108
 109 let line_lift_thm = lift_theorem line_tybij
 110  (PARDIR_REFL,PARDIR_SYM,PARDIR_TRANS) [perpl_th];;
 111
 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;;
 116
 117 let point_tybij = new_type_definition "point" ("mk_point","dest_point")
 118  (prove(`?x:line. T`,REWRITE_TAC[]));;
 119
 120 parse_as_infix("on",(11,"right"));;
 121
 122 let on = new_definition `p on l <=> perpl (dest_point p) l`;;
 123
 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]);;
 129
 130 let POINT_TAC th = REWRITE_TAC[on; POINT_CLAUSES] THEN ACCEPT_TAC th;;
 131
 132 let AXIOM_1 = prove
 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);;
 136
 137 let AXIOM_2 = prove
 138  (`!l l'. ?p. p on l /\ p on l'`,
 139   POINT_TAC LINE_AXIOM_2);;
 140
 141 let AXIOM_3 = prove
 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);;
 145
 146 let AXIOM_4 = prove
 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);;
 150
 151 (* ------------------------------------------------------------------------- *)
 152 (* Mappings from vectors in R^3 to projective lines and points.              *)
 153 (* ------------------------------------------------------------------------- *)
 154
 155 let projl = new_definition
 156  `projl x = mk_line((||) (mk_dir x))`;;
 157
 158 let projp = new_definition
 159  `projp x = mk_point(projl x)`;;
 160
 161 (* ------------------------------------------------------------------------- *)
 162 (* Mappings in the other direction, to (some) homogeneous coordinates.       *)
 163 (* ------------------------------------------------------------------------- *)
 164
 165 let PROJL_TOTAL = prove
 166  (`!l. ?x. ~(x = vec 0) /\ l = projl x`,
 167   GEN_TAC THEN
 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]]);;
 172
 173 let homol = new_specification ["homol"]
 174   (REWRITE_RULE[SKOLEM_THM] PROJL_TOTAL);;
 175
 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]);;
 179
 180 let homop_def = new_definition
 181  `homop p = homol(dest_point p)`;;
 182
 183 let homop = prove
 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);;
 188
 189 (* ------------------------------------------------------------------------- *)
 190 (* Key equivalences of concepts in projective space and homogeneous coords.  *)
 191 (* ------------------------------------------------------------------------- *)
 192
 193 let parallel = new_definition
 194  `parallel x y <=> x cross y = vec 0`;;
 195
 196 let ON_HOMOL = prove
 197  (`!p l. p on l <=> orthogonal (homop p) (homol l)`,
 198   REPEAT GEN_TAC THEN
 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]);;
 203
 204 let EQ_HOMOL = prove
 205  (`!l l'. l = l' <=> parallel (homol l) (homol l')`,
 206   REPEAT GEN_TAC THEN
 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]);;
 212
 213 let EQ_HOMOP = prove
 214  (`!p p'. p = p' <=> parallel (homop p) (homop p')`,
 215   REWRITE_TAC[homop_def; GSYM EQ_HOMOL] THEN
 216   MESON_TAC[point_tybij]);;
 217
 218 (* ------------------------------------------------------------------------- *)
 219 (* A "welldefinedness" result for homogeneous coordinate map.                *)
 220 (* ------------------------------------------------------------------------- *)
 221
 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]);;
 233
 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]);;
 238
 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]);;
 247
 248 (* ------------------------------------------------------------------------- *)
 249 (* Brackets, collinearity and their connection.                              *)
 250 (* ------------------------------------------------------------------------- *)
 251
 252 let bracket = define
 253  `bracket[a;b;c] = det(vector[homop a;homop b;homop c])`;;
 254
 255 let COLLINEAR = new_definition
 256  `COLLINEAR s <=> ?l. !p. p IN s ==> p on l`;;
 257
 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]);;
 262
 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]);;
 269
 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]);;
 273
 274 let COLLINEAR_BRACKET = prove
 275  (`!p1 p2 p3. COLLINEAR {p1,p2,p3} <=> bracket[p1;p2;p3] = &0`,
 276   let lemma = prove
 277    (`!a b c x y.
 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
 288     CONV_TAC REAL_RING;
 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]]);;
 301
 302 (* ------------------------------------------------------------------------- *)
 303 (* Conics and bracket condition for 6 points to be on a conic.               *)
 304 (* ------------------------------------------------------------------------- *)
 305
 306 let homogeneous_conic = new_definition
 307  `homogeneous_conic con <=>
 308     ?a b c d e f.
 309        ~(a = &0 /\ b = &0 /\ c = &0 /\ d = &0 /\ e = &0 /\ f = &0) /\
 310        con = {x:real^3 | a * x$1 pow 2 + b * x$2 pow 2 + c * x$3 pow 2 +
 311                          d * x$1 * x$2 + e * x$1 * x$3 + f * x$2 * x$3 = &0}`;;
 312
 313 let projective_conic = new_definition
 314  `projective_conic con <=>
 315         ?c. homogeneous_conic c /\ con = {p | (homop p) IN c}`;;
 316
 317 let HOMOGENEOUS_CONIC_BRACKET = prove
 318  (`!con x1 x2 x3 x4 x5 x6.
 319         homogeneous_conic con /\
 320         x1 IN con /\ x2 IN con /\ x3 IN con /\
 321         x4 IN con /\ x5 IN con /\ x6 IN con
 322         ==> det(vector[x6;x1;x4]) * det(vector[x6;x2;x3]) *
 323             det(vector[x5;x1;x3]) * det(vector[x5;x2;x4]) =
 324             det(vector[x6;x1;x3]) * det(vector[x6;x2;x4]) *
 325             det(vector[x5;x1;x4]) * det(vector[x5;x2;x3])`,
 326   REPEAT GEN_TAC THEN REWRITE_TAC[homogeneous_conic; EXTENSION] THEN
 327   ONCE_REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 328   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 329   ASM_REWRITE_TAC[IN_ELIM_THM; DET_3; VECTOR_3] THEN
 330   CONV_TAC REAL_RING);;
 331
 332 let PROJECTIVE_CONIC_BRACKET = prove
 333  (`!con p1 p2 p3 p4 p5 p6.
 334         projective_conic con /\
 335         p1 IN con /\ p2 IN con /\ p3 IN con /\
 336         p4 IN con /\ p5 IN con /\ p6 IN con
 337         ==> bracket[p6;p1;p4] * bracket[p6;p2;p3] *
 338             bracket[p5;p1;p3] * bracket[p5;p2;p4] =
 339             bracket[p6;p1;p3] * bracket[p6;p2;p4] *
 340             bracket[p5;p1;p4] * bracket[p5;p2;p3]`,
 341   REPEAT GEN_TAC THEN REWRITE_TAC[bracket; projective_conic] THEN
 342   DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
 343   ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 344   MATCH_MP_TAC HOMOGENEOUS_CONIC_BRACKET THEN ASM_MESON_TAC[]);;
 345
 346 (* ------------------------------------------------------------------------- *)
 347 (* Pascal's theorem with all the nondegeneracy principles we use directly.   *)
 348 (* ------------------------------------------------------------------------- *)
 349
 350 let PASCAL_DIRECT = prove
 351  (`!con x1 x2 x3 x4 x5 x6 x6 x8 x9.
 352         ~COLLINEAR {x2,x5,x7} /\
 353         ~COLLINEAR {x1,x2,x5} /\
 354         ~COLLINEAR {x1,x3,x6} /\
 355         ~COLLINEAR {x2,x4,x6} /\
 356         ~COLLINEAR {x3,x4,x5} /\
 357         ~COLLINEAR {x1,x5,x7} /\
 358         ~COLLINEAR {x2,x5,x9} /\
 359         ~COLLINEAR {x1,x2,x6} /\
 360         ~COLLINEAR {x3,x6,x8} /\
 361         ~COLLINEAR {x2,x4,x5} /\
 362         ~COLLINEAR {x2,x4,x7} /\
 363         ~COLLINEAR {x2,x6,x8} /\
 364         ~COLLINEAR {x3,x4,x6} /\
 365         ~COLLINEAR {x3,x5,x8} /\
 366         ~COLLINEAR {x1,x3,x5}
 367         ==> projective_conic con /\
 368             x1 IN con /\ x2 IN con /\ x3 IN con /\
 369             x4 IN con /\ x5 IN con /\ x6 IN con /\
 370             COLLINEAR {x1,x9,x5} /\
 371             COLLINEAR {x1,x8,x6} /\
 372             COLLINEAR {x2,x9,x4} /\
 373             COLLINEAR {x2,x7,x6} /\
 374             COLLINEAR {x3,x8,x4} /\
 375             COLLINEAR {x3,x7,x5}
 376             ==> COLLINEAR {x7,x8,x9}`,
 377   REPEAT GEN_TAC THEN DISCH_TAC THEN
 378   REWRITE_TAC[TAUT `a /\ b /\ c /\ d /\ e /\ f /\ g /\ h ==> p <=>
 379                     a /\ b /\ c /\ d /\ e /\ f /\ g ==> h ==> p`] THEN
 380   DISCH_THEN(MP_TAC o MATCH_MP PROJECTIVE_CONIC_BRACKET) THEN
 381   REWRITE_TAC[COLLINEAR_BRACKET; IMP_IMP; GSYM CONJ_ASSOC] THEN
 382   MATCH_MP_TAC(TAUT `!q. (p ==> q) /\ (q ==> r) ==> p ==> r`) THEN
 383   EXISTS_TAC
 384    `bracket[x1;x2;x5] * bracket[x1;x3;x6] *
 385     bracket[x2;x4;x6] * bracket[x3;x4;x5] =
 386     bracket[x1;x2;x6] * bracket[x1;x3;x5] *
 387     bracket[x2;x4;x5] * bracket[x3;x4;x6] /\
 388     bracket[x1;x5;x7] * bracket[x2;x5;x9] =
 389     --bracket[x1;x2;x5] * bracket[x5;x9;x7] /\
 390     bracket[x1;x2;x6] * bracket[x3;x6;x8] =
 391     bracket[x1;x3;x6] * bracket[x2;x6;x8] /\
 392     bracket[x2;x4;x5] * bracket[x2;x9;x7] =
 393     --bracket[x2;x4;x7] * bracket[x2;x5;x9] /\
 394     bracket[x2;x4;x7] * bracket[x2;x6;x8] =
 395     --bracket[x2;x4;x6] * bracket[x2;x8;x7] /\
 396     bracket[x3;x4;x6] * bracket[x3;x5;x8] =
 397     bracket[x3;x4;x5] * bracket[x3;x6;x8] /\
 398     bracket[x1;x3;x5] * bracket[x5;x8;x7] =
 399     --bracket[x1;x5;x7] * bracket[x3;x5;x8]` THEN
 400   CONJ_TAC THENL
 401    [REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THEN
 402     REWRITE_TAC[bracket; DET_3; VECTOR_3] THEN CONV_TAC REAL_RING;
 403     ALL_TAC] THEN
 404   REWRITE_TAC[IMP_CONJ] THEN
 405   REPEAT(ONCE_REWRITE_TAC[IMP_IMP] THEN
 406          DISCH_THEN(MP_TAC o MATCH_MP (REAL_RING
 407           `a = b /\ x:real = y ==> a * x = b * y`))) THEN
 408   REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_LNEG; REAL_MUL_RNEG] THEN
 409   REWRITE_TAC[REAL_NEG_NEG] THEN
 410   RULE_ASSUM_TAC(REWRITE_RULE[COLLINEAR_BRACKET]) THEN
 411   REWRITE_TAC[REAL_MUL_AC] THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL] THEN
 412   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
 413   ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL] THEN
 414   FIRST_X_ASSUM(MP_TAC o CONJUNCT1) THEN
 415   REWRITE_TAC[bracket; DET_3; VECTOR_3] THEN CONV_TAC REAL_RING);;
 416
 417 (* ------------------------------------------------------------------------- *)
 418 (* With longer but more intuitive non-degeneracy conditions, basically that  *)
 419 (* the 6 points divide into two groups of 3 and no 3 are collinear unless    *)
 420 (* they are all in the same group.                                           *)
 421 (* ------------------------------------------------------------------------- *)
 422
 423 let PASCAL = prove
 424  (`!con x1 x2 x3 x4 x5 x6 x6 x8 x9.
 425         ~COLLINEAR {x1,x2,x4} /\
 426         ~COLLINEAR {x1,x2,x5} /\
 427         ~COLLINEAR {x1,x2,x6} /\
 428         ~COLLINEAR {x1,x3,x4} /\
 429         ~COLLINEAR {x1,x3,x5} /\
 430         ~COLLINEAR {x1,x3,x6} /\
 431         ~COLLINEAR {x2,x3,x4} /\
 432         ~COLLINEAR {x2,x3,x5} /\
 433         ~COLLINEAR {x2,x3,x6} /\
 434         ~COLLINEAR {x4,x5,x1} /\
 435         ~COLLINEAR {x4,x5,x2} /\
 436         ~COLLINEAR {x4,x5,x3} /\
 437         ~COLLINEAR {x4,x6,x1} /\
 438         ~COLLINEAR {x4,x6,x2} /\
 439         ~COLLINEAR {x4,x6,x3} /\
 440         ~COLLINEAR {x5,x6,x1} /\
 441         ~COLLINEAR {x5,x6,x2} /\
 442         ~COLLINEAR {x5,x6,x3}
 443         ==> projective_conic con /\
 444             x1 IN con /\ x2 IN con /\ x3 IN con /\
 445             x4 IN con /\ x5 IN con /\ x6 IN con /\
 446             COLLINEAR {x1,x9,x5} /\
 447             COLLINEAR {x1,x8,x6} /\
 448             COLLINEAR {x2,x9,x4} /\
 449             COLLINEAR {x2,x7,x6} /\
 450             COLLINEAR {x3,x8,x4} /\
 451             COLLINEAR {x3,x7,x5}
 452             ==> COLLINEAR {x7,x8,x9}`,
 453   REPEAT GEN_TAC THEN DISCH_TAC THEN
 454   DISCH_THEN(fun th ->
 455     MATCH_MP_TAC(TAUT `(~p ==> p) ==> p`) THEN DISCH_TAC THEN
 456     MP_TAC th THEN MATCH_MP_TAC PASCAL_DIRECT THEN
 457     ASSUME_TAC(funpow 7 CONJUNCT2 th)) THEN
 458   REPEAT CONJ_TAC THEN
 459   REPEAT(POP_ASSUM MP_TAC) THEN
 460   REWRITE_TAC[COLLINEAR_BRACKET; bracket; DET_3; VECTOR_3] THEN
 461   CONV_TAC REAL_RING);;
 462
 463 (* ------------------------------------------------------------------------- *)
 464 (* Homogenization and hence mapping from affine to projective plane.         *)
 465 (* ------------------------------------------------------------------------- *)
 466
 467 let homogenize = new_definition
 468  `(homogenize:real^2->real^3) x = vector[x$1; x$2; &1]`;;
 469
 470 let projectivize = new_definition
 471  `projectivize = projp o homogenize`;;
 472
 473 let HOMOGENIZE_NONZERO = prove
 474  (`!x. ~(homogenize x = vec 0)`,
 475   REWRITE_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3;
 476               homogenize] THEN
 477   REAL_ARITH_TAC);;
 478
 479 (* ------------------------------------------------------------------------- *)
 480 (* Conic in affine plane.                                                    *)
 481 (* ------------------------------------------------------------------------- *)
 482
 483 let affine_conic = new_definition
 484  `affine_conic con <=>
 485     ?a b c d e f.
 486        ~(a = &0 /\ b = &0 /\ c = &0 /\ d = &0 /\ e = &0 /\ f = &0) /\
 487        con = {x:real^2 | a * x$1 pow 2 + b * x$2 pow 2 + c * x$1 * x$2 +
 488                          d * x$1 + e * x$2 + f = &0}`;;
 489
 490 (* ------------------------------------------------------------------------- *)
 491 (* Relationships between affine and projective notions.                      *)
 492 (* ------------------------------------------------------------------------- *)
 493
 494 let COLLINEAR_PROJECTIVIZE = prove
 495  (`!a b c. collinear{a,b,c} <=>
 496            COLLINEAR{projectivize a,projectivize b,projectivize c}`,
 497   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COLLINEAR_3] THEN
 498   REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL] THEN
 499   REWRITE_TAC[COLLINEAR_BRACKET; projectivize; o_THM; bracket] THEN
 500   MATCH_MP_TAC EQ_TRANS THEN
 501   EXISTS_TAC `det(vector[homogenize a; homogenize b; homogenize c]) = &0` THEN
 502   CONJ_TAC THENL
 503    [REWRITE_TAC[homogenize; DOT_2; VECTOR_SUB_COMPONENT; DET_3; VECTOR_3] THEN
 504     CONV_TAC REAL_RING;
 505     MAP_EVERY (MP_TAC o C SPEC PARALLEL_PROJP_HOMOP)
 506      [`homogenize a`; `homogenize b`; `homogenize c`] THEN
 507     MAP_EVERY (MP_TAC o C SPEC HOMOGENIZE_NONZERO)
 508      [`a:real^2`; `b:real^2`; `c:real^2`] THEN
 509     MAP_EVERY (MP_TAC o CONJUNCT1 o C SPEC homop)
 510      [`projp(homogenize a)`; `projp(homogenize b)`; `projp(homogenize c)`] THEN
 511     REWRITE_TAC[parallel; cross; CART_EQ; DIMINDEX_3; FORALL_3; VECTOR_3;
 512                 DET_3; VEC_COMPONENT] THEN
 513     CONV_TAC REAL_RING]);;
 514
 515 let AFFINE_PROJECTIVE_CONIC = prove
 516  (`!con. affine_conic con <=> ?con'. projective_conic con' /\
 517                                      con = {x | projectivize x IN con'}`,
 518   REWRITE_TAC[affine_conic; projective_conic; homogeneous_conic] THEN
 519   GEN_TAC THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 520   ONCE_REWRITE_TAC[MESON[]
 521    `(?con' con a b c d e f. P con' con a b c d e f) <=>
 522     (?a b d e f c con' con. P con' con a b c d e f)`] THEN
 523   MAP_EVERY (fun s ->
 524    AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 525    X_GEN_TAC(mk_var(s,`:real`)) THEN REWRITE_TAC[])
 526    ["a"; "b"; "c"; "d"; "e"; "f"] THEN
 527   REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM2; GSYM CONJ_ASSOC] THEN
 528   REWRITE_TAC[IN_ELIM_THM; projectivize; o_THM] THEN
 529   BINOP_TAC THENL [CONV_TAC TAUT; AP_TERM_TAC] THEN
 530   REWRITE_TAC[EXTENSION] THEN X_GEN_TAC `x:real^2` THEN
 531   MP_TAC(SPEC `x:real^2` HOMOGENIZE_NONZERO) THEN
 532   DISCH_THEN(MP_TAC o MATCH_MP PARALLEL_PROJP_HOMOP_EXPLICIT) THEN
 533   DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
 534   ASM_REWRITE_TAC[IN_ELIM_THM; VECTOR_MUL_COMPONENT] THEN
 535   REWRITE_TAC[homogenize; VECTOR_3] THEN
 536   UNDISCH_TAC `~(k = &0)` THEN CONV_TAC REAL_RING);;
 537
 538 (* ------------------------------------------------------------------------- *)
 539 (* Hence Pascal's theorem for the affine plane.                              *)
 540 (* ------------------------------------------------------------------------- *)
 541
 542 let PASCAL_AFFINE = prove
 543  (`!con x1 x2 x3 x4 x5 x6 x7 x8 x9:real^2.
 544         ~collinear {x1,x2,x4} /\
 545         ~collinear {x1,x2,x5} /\
 546         ~collinear {x1,x2,x6} /\
 547         ~collinear {x1,x3,x4} /\
 548         ~collinear {x1,x3,x5} /\
 549         ~collinear {x1,x3,x6} /\
 550         ~collinear {x2,x3,x4} /\
 551         ~collinear {x2,x3,x5} /\
 552         ~collinear {x2,x3,x6} /\
 553         ~collinear {x4,x5,x1} /\
 554         ~collinear {x4,x5,x2} /\
 555         ~collinear {x4,x5,x3} /\
 556         ~collinear {x4,x6,x1} /\
 557         ~collinear {x4,x6,x2} /\
 558         ~collinear {x4,x6,x3} /\
 559         ~collinear {x5,x6,x1} /\
 560         ~collinear {x5,x6,x2} /\
 561         ~collinear {x5,x6,x3}
 562         ==> affine_conic con /\
 563             x1 IN con /\ x2 IN con /\ x3 IN con /\
 564             x4 IN con /\ x5 IN con /\ x6 IN con /\
 565             collinear {x1,x9,x5} /\
 566             collinear {x1,x8,x6} /\
 567             collinear {x2,x9,x4} /\
 568             collinear {x2,x7,x6} /\
 569             collinear {x3,x8,x4} /\
 570             collinear {x3,x7,x5}
 571             ==> collinear {x7,x8,x9}`,
 572   REWRITE_TAC[COLLINEAR_PROJECTIVIZE; AFFINE_PROJECTIVE_CONIC] THEN
 573   REPEAT(GEN_TAC ORELSE DISCH_TAC) THEN
 574   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP PASCAL) THEN
 575   ASM_REWRITE_TAC[] THEN
 576   FIRST_X_ASSUM(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 577   MATCH_MP_TAC MONO_EXISTS THEN ASM SET_TAC[]);;
 578
 579 (* ------------------------------------------------------------------------- *)
 580 (* Special case of a circle where nondegeneracy is simpler.                  *)
 581 (* ------------------------------------------------------------------------- *)
 582
 583 let COLLINEAR_NOT_COCIRCULAR = prove
 584  (`!r c x y z:real^2.
 585         dist(c,x) = r /\ dist(c,y) = r /\ dist(c,z) = r /\
 586         ~(x = y) /\ ~(x = z) /\ ~(y = z)
 587         ==> ~collinear {x,y,z}`,
 588   ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
 589   REWRITE_TAC[GSYM DOT_EQ_0] THEN
 590   ONCE_REWRITE_TAC[COLLINEAR_3] THEN
 591   REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL; DOT_2] THEN
 592   REWRITE_TAC[dist; NORM_EQ_SQUARE; CART_EQ; DIMINDEX_2; FORALL_2;
 593               DOT_2; VECTOR_SUB_COMPONENT] THEN
 594   CONV_TAC REAL_RING);;
 595
 596 let PASCAL_AFFINE_CIRCLE = prove
 597  (`!c r x1 x2 x3 x4 x5 x6 x7 x8 x9:real^2.
 598         PAIRWISE (\x y. ~(x = y)) [x1;x2;x3;x4;x5;x6] /\
 599         dist(c,x1) = r /\ dist(c,x2) = r /\ dist(c,x3) = r /\
 600         dist(c,x4) = r /\ dist(c,x5) = r /\ dist(c,x6) = r /\
 601         collinear {x1,x9,x5} /\
 602         collinear {x1,x8,x6} /\
 603         collinear {x2,x9,x4} /\
 604         collinear {x2,x7,x6} /\
 605         collinear {x3,x8,x4} /\
 606         collinear {x3,x7,x5}
 607         ==> collinear {x7,x8,x9}`,
 608   GEN_TAC THEN GEN_TAC THEN
 609   MP_TAC(SPEC `{x:real^2 | dist(c,x) = r}` PASCAL_AFFINE) THEN
 610   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 611   REWRITE_TAC[PAIRWISE; ALL; IN_ELIM_THM] THEN
 612   GEN_REWRITE_TAC LAND_CONV [IMP_IMP] THEN
 613   DISCH_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 614   ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 615    [REPEAT CONJ_TAC THEN MATCH_MP_TAC COLLINEAR_NOT_COCIRCULAR THEN
 616     MAP_EVERY EXISTS_TAC [`r:real`; `c:real^2`] THEN ASM_REWRITE_TAC[];
 617     REWRITE_TAC[affine_conic; dist; NORM_EQ_SQUARE] THEN
 618     ASM_CASES_TAC `&0 <= r` THEN ASM_REWRITE_TAC[] THENL
 619      [MAP_EVERY EXISTS_TAC
 620        [`&1`; `&1`; `&0`; `-- &2 * (c:real^2)$1`; `-- &2 * (c:real^2)$2`;
 621         `(c:real^2)$1 pow 2 + (c:real^2)$2 pow 2 - r pow 2`] THEN
 622       REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 623       REWRITE_TAC[DOT_2; VECTOR_SUB_COMPONENT] THEN REAL_ARITH_TAC;
 624       REPLICATE_TAC 5 (EXISTS_TAC `&0`) THEN EXISTS_TAC `&1` THEN
 625       REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN REAL_ARITH_TAC]]);;