Examples/sylvester_gallai.ml

   1 (* ========================================================================= *)
   2 (* The Sylvester-Gallai theorem.                                             *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/convex.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* The main lemma that we reduce things to.                                  *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let SYLVESTER_GALLAI_LEMMA = prove
  12  (`!p q b c:real^2.
  13         between b (q,c) /\ ~(p IN affine hull {q,c}) /\
  14         orthogonal (p - q) (c - q) /\ ~(c = b) /\ ~(c = q)
  15         ==> ~(b IN affine hull {p,c}) /\
  16             ?x. x IN affine hull {p,c} /\ dist(b,x) < dist(p,q)`,
  17   GEOM_ORIGIN_TAC `q:real^2` THEN
  18   GEOM_BASIS_MULTIPLE_TAC 1 `c:real^2` THEN
  19   X_GEN_TAC `c:real` THEN
  20   ASM_CASES_TAC `c = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN
  21   ASM_REWRITE_TAC[REAL_LE_LT] THEN DISCH_TAC THEN
  22   MAP_EVERY X_GEN_TAC [`pp:real^2`; `bb:real^2`] THEN
  23   REWRITE_TAC[BETWEEN_IN_SEGMENT; SEGMENT_CONVEX_HULL] THEN
  24   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  25   FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[SUBSET]
  26         CONVEX_HULL_SUBSET_AFFINE_HULL)) THEN
  27   SIMP_TAC[AFFINE_HULL_EQ_SPAN; HULL_INC; IN_INSERT; SPAN_INSERT_0] THEN
  28   REWRITE_TAC[SPAN_SING; IN_ELIM_THM; IN_UNIV; VECTOR_MUL_ASSOC] THEN
  29   DISCH_THEN(X_CHOOSE_THEN `bc:real` SUBST_ALL_TAC) THEN
  30   ABBREV_TAC `b:real = bc * c` THEN
  31   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  32   REWRITE_TAC[VECTOR_SUB_RZERO; orthogonal; DOT_2] THEN
  33   SIMP_TAC[VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN
  34   REWRITE_TAC[REAL_MUL_RZERO; REAL_MUL_RID; REAL_ADD_RID] THEN
  35   ASM_SIMP_TAC[REAL_ENTIRE; REAL_LT_IMP_NZ; VECTOR_MUL_EQ_0] THEN
  36   ASM_SIMP_TAC[VECTOR_MUL_RCANCEL; BASIS_NONZERO; DIMINDEX_2; ARITH] THEN
  37   STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
  38    [GSYM SEGMENT_CONVEX_HULL]) THEN
  39   REWRITE_TAC[GSYM BETWEEN_IN_SEGMENT; between; DIST_0] THEN
  40   REWRITE_TAC[dist; GSYM VECTOR_SUB_RDISTRIB; NORM_MUL] THEN
  41   SIMP_TAC[NORM_BASIS; REAL_MUL_RID; DIMINDEX_2; ARITH] THEN
  42   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
  43    `abs c = abs b + abs(b - c)
  44     ==> &0 < c ==> &0 <= b /\ (b < c \/ b = c)`)) THEN
  45   ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
  46   SUBGOAL_THEN `?p. ~(p = &0) /\ pp:real^2 = p % basis 2`
  47    (CHOOSE_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC))
  48   THENL
  49    [EXISTS_TAC `(pp:real^2)$2` THEN
  50     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EXISTS_THM]) THEN
  51     DISCH_THEN(MP_TAC o SPEC `&0`) THEN REWRITE_TAC[REAL_MUL_LZERO] THEN
  52     REWRITE_TAC[CART_EQ; DIMINDEX_2; FORALL_2] THEN
  53     SIMP_TAC[VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN
  54     ASM_REAL_ARITH_TAC;
  55     ALL_TAC] THEN
  56   REWRITE_TAC[AFFINE_HULL_2_ALT; EXISTS_IN_GSPEC; IN_UNIV; NORM_LT] THEN
  57   CONJ_TAC THENL
  58    [REWRITE_TAC[IN_ELIM_THM; CART_EQ; DIMINDEX_2; FORALL_2] THEN
  59     REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_SUB_COMPONENT;
  60                 VECTOR_MUL_COMPONENT] THEN
  61     SIMP_TAC[BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN
  62     REWRITE_TAC[REAL_MUL_RID; REAL_MUL_RZERO; REAL_ADD_LID] THEN
  63     REWRITE_TAC[REAL_RING `&0 = p + u * (&0 - p) <=> p = &0 \/ u = &1`] THEN
  64     ONCE_REWRITE_TAC[CONJ_SYM] THEN ASM_REWRITE_TAC[UNWIND_THM2] THEN
  65     ASM_REAL_ARITH_TAC;
  66     ALL_TAC] THEN
  67   REWRITE_TAC[VECTOR_ARITH
  68    `b - (p + u % (c - p)):real^2 = (b - u % c) - (&1 - u) % p`] THEN
  69   REWRITE_TAC[VECTOR_MUL_ASSOC; GSYM VECTOR_SUB_RDISTRIB] THEN
  70   REWRITE_TAC[NORM_POS_LT; GSYM DOT_POS_LT] THEN
  71   REWRITE_TAC[VECTOR_ARITH
  72    `(a - b) dot (a - b) = a dot a + b dot b - &2 * a dot b`] THEN
  73   REWRITE_TAC[DOT_LMUL; DOT_RMUL] THEN
  74   SIMP_TAC[DOT_BASIS_BASIS; DIMINDEX_2; ARITH; REAL_MUL_RZERO] THEN
  75   REWRITE_TAC[REAL_MUL_RID; REAL_SUB_RZERO] THEN
  76   SUBGOAL_THEN `&0 < c pow 2 /\ &0 < p pow 2` STRIP_ASSUME_TAC THENL
  77    [REWRITE_TAC[REAL_ARITH `&0 < x <=> &0 <= x /\ ~(x = &0)`] THEN
  78     ASM_REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE; REAL_ENTIRE];
  79     ALL_TAC] THEN
  80   ASM_CASES_TAC `b = &0` THENL
  81    [EXISTS_TAC `p pow 2 / (p pow 2 + c pow 2):real` THEN
  82     ASM_REWRITE_TAC[REAL_ARITH
  83      `(&0 - u * c) * (&0 - u * c) + ((&1 - u) * p) * ((&1 - u) * p) < p * p <=>
  84       u * u * c pow 2 < u * (&2 - u) * p pow 2`] THEN
  85     ASM_SIMP_TAC[REAL_LT_LMUL_EQ; REAL_LT_DIV; REAL_LT_ADD] THEN
  86     SIMP_TAC[REAL_ARITH `u * c < (&2 - u) * p <=> u * (p + c) < &2 * p`] THEN
  87     ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_LT_IMP_NZ; REAL_LT_ADD] THEN
  88     ASM_REAL_ARITH_TAC;
  89     EXISTS_TAC `b:real / c` THEN
  90     ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_LT_IMP_NZ; REAL_SUB_REFL] THEN
  91     REWRITE_TAC[REAL_ARITH
  92      `&0 * &0 + (u * p) * (u * p) < p * p <=> &0 < (&1 - u * u) * p * p`] THEN
  93     MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[GSYM REAL_POW_2] THEN
  94     REWRITE_TAC[REAL_SUB_LT] THEN MATCH_MP_TAC REAL_POW_1_LT THEN
  95     SIMP_TAC[ARITH_EQ; REAL_SUB_LE; REAL_ARITH `&1 - x < &1 <=> &0 < x`] THEN
  96     ASM_SIMP_TAC[ARITH_EQ; REAL_LT_RDIV_EQ; REAL_LE_LDIV_EQ] THEN
  97     ASM_REAL_ARITH_TAC]);;
  98
  99 (* ------------------------------------------------------------------------- *)
 100 (* The following lemmas drive a case analysis to pick the right points.      *)
 101 (* ------------------------------------------------------------------------- *)
 102
 103 let cases_quick = prove
 104  (`!q a b c:real^N.
 105         collinear {q,a,b,c} /\ between b (a,c)
 106         ==> between b (q,a) \/ between b (q,c)`,
 107   REPEAT GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 108   REWRITE_TAC[COLLINEAR_AFFINE_HULL; LEFT_IMP_EXISTS_THM] THEN
 109   MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN
 110   GEOM_ORIGIN_TAC `u:real^N` THEN
 111   GEOM_BASIS_MULTIPLE_TAC 1 `v:real^N` THEN
 112   GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
 113   SIMP_TAC[AFFINE_HULL_EQ_SPAN; HULL_INC; IN_INSERT] THEN
 114   REWRITE_TAC[SPAN_INSERT_0; SPAN_SING; INSERT_SUBSET; EMPTY_SUBSET] THEN
 115   REWRITE_TAC[IN_ELIM_THM; IN_UNIV] THEN STRIP_TAC THEN
 116   ASM_REWRITE_TAC[between; dist; GSYM VECTOR_SUB_RDISTRIB] THEN
 117   SIMP_TAC[NORM_MUL; NORM_BASIS; DIMINDEX_GE_1; LE_REFL] THEN
 118   REWRITE_TAC[REAL_MUL_RID; GSYM REAL_ADD_RDISTRIB] THEN
 119   REWRITE_TAC[REAL_EQ_MUL_RCANCEL] THEN
 120   ASM_CASES_TAC `abs v = &0` THEN ASM_REWRITE_TAC[] THEN
 121   REAL_ARITH_TAC);;
 122
 123 let cases_lemma = prove
 124  (`!q a b c:real^N.
 125         collinear {q,a,b,c}
 126         ==> between a (q,b) \/ between a (q,c) \/
 127             between b (q,c) \/ between b (q,a) \/
 128             between c (q,a) \/ between c (q,b)`,
 129   REPEAT STRIP_TAC THEN
 130   SUBGOAL_THEN `collinear {a:real^N,b,c}` MP_TAC THENL
 131    [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
 132         COLLINEAR_SUBSET)) THEN SET_TAC[];
 133     REWRITE_TAC[COLLINEAR_BETWEEN_CASES] THEN
 134     REPEAT(ONCE_REWRITE_TAC[TAUT `a \/ b \/ c \/ d <=> (a \/ b) \/ c \/ d`] THEN
 135            MATCH_MP_TAC MONO_OR THEN CONJ_TAC) THEN
 136     MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] cases_quick) THEN
 137     POP_ASSUM MP_TAC THEN REWRITE_TAC[INSERT_AC]]);;
 138
 139 (* ------------------------------------------------------------------------- *)
 140 (* Kelly's proof of the Sylvester-Gallai theorem.                            *)
 141 (* ------------------------------------------------------------------------- *)
 142
 143 let SYLVESTER_GALLAI = prove
 144  (`!s:real^2->bool.
 145         FINITE s /\
 146         (!a b. a IN s /\ b IN s /\ ~(a = b)
 147                ==> ?c. c IN s /\ ~(c = a) /\ ~(c = b) /\ collinear {a,b,c})
 148         ==> collinear s`,
 149   GEN_TAC THEN ASM_CASES_TAC `s:real^2->bool = {}` THEN
 150   ASM_REWRITE_TAC[COLLINEAR_EMPTY] THEN
 151   ASM_CASES_TAC `?a:real^2. s = {a}` THENL
 152    [ASM_MESON_TAC[COLLINEAR_SING]; STRIP_TAC] THEN
 153   ABBREV_TAC
 154    `L = {affine hull {a,b} | a IN s /\ b IN s /\ ~(a:real^2 = b)}` THEN
 155   SUBGOAL_THEN `FINITE(L:(real^2->bool)->bool)` ASSUME_TAC THENL
 156    [EXPAND_TAC "L" THEN
 157     ONCE_REWRITE_TAC[SET_RULE
 158      `{f x y | x IN s /\ y IN s /\ P x y} =
 159       {f x y | x IN s /\ y IN {y | y IN s /\ P x y}}`] THEN
 160     ASM_SIMP_TAC[FINITE_PRODUCT_DEPENDENT; FINITE_RESTRICT];
 161     ALL_TAC] THEN
 162   ASM_CASES_TAC `L:(real^2->bool)->bool = {}` THENL
 163    [UNDISCH_TAC `L:(real^2->bool)->bool = {}` THEN EXPAND_TAC "L" THEN
 164     ASM SET_TAC[];
 165     ALL_TAC] THEN
 166   MP_TAC(ISPEC
 167    `{ dist(closest_point l p,p) |
 168       l IN L /\ p IN {p:real^2 | p IN s /\ &0 < dist(closest_point l p,p)}}`
 169    INF_FINITE) THEN
 170   ASM_SIMP_TAC[FINITE_PRODUCT_DEPENDENT; FINITE_RESTRICT] THEN
 171   ASM_REWRITE_TAC[SET_RULE
 172    `{f x y | x IN s /\ y IN t x} = {} <=>
 173     s = {} \/ (!x. x IN s ==> t x = {})`] THEN
 174   MATCH_MP_TAC(TAUT `(p ==> r) /\ (q ==> r) ==> (~p ==> q) ==> r`) THEN
 175   CONJ_TAC THENL
 176    [SIMP_TAC[SET_RULE `{x | x IN s /\ P x} = {} <=> !x. x IN s ==> ~P x`] THEN
 177     REWRITE_TAC[GSYM DIST_NZ] THEN
 178     FIRST_X_ASSUM(X_CHOOSE_TAC `l:real^2->bool` o
 179         GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
 180     DISCH_THEN(MP_TAC o SPEC `l:real^2->bool`) THEN ASM_REWRITE_TAC[] THEN
 181     SUBGOAL_THEN `closed(l:real^2->bool) /\ ~(l = {})` ASSUME_TAC THENL
 182      [UNDISCH_TAC `(l:real^2->bool) IN L` THEN EXPAND_TAC "L" THEN
 183       REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 184       ASM_SIMP_TAC[CLOSED_AFFINE; AFFINE_AFFINE_HULL] THEN
 185       REWRITE_TAC[AFFINE_HULL_EQ_EMPTY; NOT_INSERT_EMPTY];
 186       ASM_SIMP_TAC[CLOSEST_POINT_REFL]] THEN
 187     DISCH_TAC THEN MATCH_MP_TAC COLLINEAR_SUBSET THEN
 188     EXISTS_TAC `l:real^2->bool` THEN ASM_REWRITE_TAC[SUBSET] THEN
 189     UNDISCH_TAC `(l:real^2->bool) IN L` THEN EXPAND_TAC "L" THEN
 190     REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 191     ASM_MESON_TAC[COLLINEAR_AFFINE_HULL; SUBSET_REFL];
 192     ALL_TAC] THEN
 193   SIMP_TAC[IMP_CONJ; IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
 194   MAP_EVERY X_GEN_TAC [`l:real^2->bool`; `p:real^2`] THEN DISCH_TAC THEN
 195   SUBGOAL_THEN `affine(l:real^2->bool) /\ ~(l = {})` STRIP_ASSUME_TAC THENL
 196    [UNDISCH_TAC `(l:real^2->bool) IN L` THEN EXPAND_TAC "L" THEN
 197     REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
 198     SIMP_TAC[CLOSED_AFFINE; AFFINE_AFFINE_HULL] THEN
 199     REWRITE_TAC[AFFINE_HULL_EQ_EMPTY; NOT_INSERT_EMPTY];
 200     ALL_TAC] THEN
 201   FIRST_ASSUM(ASSUME_TAC o MATCH_MP CLOSED_AFFINE) THEN
 202   ABBREV_TAC `q = closest_point l p:real^2` THEN
 203   DISCH_TAC THEN REWRITE_TAC[DIST_NZ] THEN DISCH_TAC THEN
 204   DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN
 205   DISCH_TAC THEN
 206   SUBGOAL_THEN `(q:real^2) IN l` ASSUME_TAC THENL
 207    [ASM_MESON_TAC[CLOSEST_POINT_IN_SET]; ALL_TAC] THEN
 208   SUBGOAL_THEN
 209    `?b c:real^2. b IN s /\ c IN s /\ b IN l /\ c IN l /\
 210                  ~(b = c) /\ between b (q,c)`
 211   STRIP_ASSUME_TAC THENL
 212    [UNDISCH_TAC `(l:real^2->bool) IN L` THEN EXPAND_TAC "L" THEN
 213     REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
 214     MAP_EVERY X_GEN_TAC [`a:real^2`; `b:real^2`] THEN
 215     DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
 216     SUBGOAL_THEN
 217      `?c:real^2. c IN s /\ ~(c = a) /\ ~(c = b) /\ collinear {a, b, c}`
 218     (CHOOSE_THEN MP_TAC) THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 219     ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL] THEN STRIP_TAC THEN
 220     SUBGOAL_THEN `(a:real^2) IN l /\ (b:real^2) IN l` STRIP_ASSUME_TAC THENL
 221      [EXPAND_TAC "l" THEN SIMP_TAC[HULL_INC; IN_INSERT]; ALL_TAC] THEN
 222     MP_TAC(ISPECL [`q:real^2`; `a:real^2`; `b:real^2`; `c:real^2`]
 223         cases_lemma) THEN
 224     ANTS_TAC THENL
 225      [REWRITE_TAC[COLLINEAR_AFFINE_HULL; INSERT_SUBSET; EMPTY_SUBSET] THEN
 226       MAP_EVERY EXISTS_TAC [`a:real^2`; `b:real^2`] THEN ASM_REWRITE_TAC[];
 227       ASM_MESON_TAC[]];
 228     ALL_TAC] THEN
 229   SUBGOAL_THEN `~(c:real^2 = q)` ASSUME_TAC THENL
 230    [ASM_MESON_TAC[BETWEEN_REFL_EQ]; ALL_TAC] THEN
 231   SUBGOAL_THEN `~((p:real^2) IN l)` ASSUME_TAC THENL
 232    [ASM_MESON_TAC[CLOSEST_POINT_SELF; DIST_EQ_0; REAL_LT_REFL];
 233     ALL_TAC] THEN
 234   MP_TAC(ISPECL [`p:real^2`; `q:real^2`; `b:real^2`; `c:real^2`]
 235         SYLVESTER_GALLAI_LEMMA) THEN
 236   ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
 237    [CONJ_TAC THENL
 238      [UNDISCH_TAC `~((p:real^2) IN l)` THEN REWRITE_TAC[CONTRAPOS_THM] THEN
 239       SPEC_TAC(`p:real^2`,`p:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
 240       MATCH_MP_TAC HULL_MINIMAL THEN
 241       ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
 242       EXPAND_TAC "q" THEN ONCE_REWRITE_TAC[ORTHOGONAL_SYM] THEN
 243       MATCH_MP_TAC CLOSEST_POINT_AFFINE_ORTHOGONAL THEN
 244       ASM_REWRITE_TAC[]];
 245     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
 246      (X_CHOOSE_THEN `r:real^2` STRIP_ASSUME_TAC)) THEN
 247     FIRST_X_ASSUM(MP_TAC o SPECL
 248      [`dist(closest_point (affine hull {p,c}) b:real^2,b)`;
 249       `affine hull {p:real^2,c}`; `b:real^2`]) THEN
 250     ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
 251      [REWRITE_TAC[REAL_ARITH `&0 < x <=> &0 <= x /\ ~(x = &0)`] THEN
 252       REWRITE_TAC[DIST_POS_LE; DIST_EQ_0] THEN
 253       ASM_SIMP_TAC[CLOSEST_POINT_REFL; CLOSED_AFFINE_HULL;
 254                    AFFINE_HULL_EQ_EMPTY; NOT_INSERT_EMPTY] THEN
 255       EXPAND_TAC "L" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[];
 256       MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
 257       ONCE_REWRITE_TAC[DIST_SYM] THEN
 258       FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 259        `rb < qp ==> cb <= rb ==> ~(qp <= cb)`)) THEN
 260       MATCH_MP_TAC CLOSEST_POINT_LE THEN
 261       ASM_REWRITE_TAC[CLOSED_AFFINE_HULL]]]);;