colo12-c703.uibk.ac.at Git - Multivariate Analysis/.git/blob - Multivariate/tarski.ml

   1 (* ========================================================================= *)
   2 (* Proof that Tarski's axioms for geometry hold in Euclidean space.          *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/convex.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Axiom 1 (reflexivity for equidistance).                                   *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let TARSKI_AXIOM_1_EUCLIDEAN = prove
  12  (`!a b:real^2. dist(a,b) = dist(b,a)`,
  13   NORM_ARITH_TAC);;
  14
  15 (* ------------------------------------------------------------------------- *)
  16 (* Axiom 2 (transitivity for equidistance).                                  *)
  17 (* ------------------------------------------------------------------------- *)
  18
  19 let TARSKI_AXIOM_2_EUCLIDEAN = prove
  20  (`!a b p q r s.
  21         dist(a,b) = dist(p,q) /\ dist(a,b) = dist(r,s)
  22         ==> dist(p,q) = dist(r,s)`,
  23   REAL_ARITH_TAC);;
  24
  25 (* ------------------------------------------------------------------------- *)
  26 (* Axiom 3 (identity for equidistance).                                      *)
  27 (* ------------------------------------------------------------------------- *)
  28
  29 let TARSKI_AXIOM_3_EUCLIDEAN = prove
  30  (`!a b c. dist(a,b) = dist(c,c) ==> a = b`,
  31   NORM_ARITH_TAC);;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* Axiom 4 (segment construction).                                           *)
  35 (* ------------------------------------------------------------------------- *)
  36
  37 let TARSKI_AXIOM_4_EUCLIDEAN = prove
  38  (`!a q b c:real^2. ?x:real^2. between a (q,x) /\ dist(a,x) = dist(b,c)`,
  39   GEOM_ORIGIN_TAC `a:real^2` THEN REPEAT GEN_TAC THEN
  40   REWRITE_TAC[DIST_0] THEN ASM_CASES_TAC `q:real^2 = vec 0` THENL
  41    [ASM_SIMP_TAC[BETWEEN_REFL; VECTOR_CHOOSE_SIZE; DIST_POS_LE];
  42     EXISTS_TAC `--(dist(b:real^2,c) / norm(q) % q):real^2` THEN
  43     REWRITE_TAC[between; DIST_0] THEN
  44     REWRITE_TAC[dist; NORM_MUL; NORM_NEG; REAL_ABS_DIV; REAL_ABS_NORM;
  45                 VECTOR_ARITH `q - --(a % q) = (&1 + a) % q`] THEN
  46     CONJ_TAC THENL
  47      [MATCH_MP_TAC(REAL_RING `a = &1 + b ==> a * q = q + b * q`) THEN
  48       SIMP_TAC[REAL_ABS_REFL; REAL_POS; REAL_LE_ADD; REAL_LE_DIV; NORM_POS_LE];
  49       ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0]]]);;
  50
  51 (* ------------------------------------------------------------------------- *)
  52 (* Axiom 5 (five-segments axiom).                                            *)
  53 (* ------------------------------------------------------------------------- *)
  54
  55 let TARSKI_AXIOM_5_EUCLIDEAN = prove
  56  (`!a b c x:real^2 a' b' c' x':real^2.
  57         ~(a = b) /\
  58         dist(a,b) = dist(a',b') /\
  59         dist(a,c) = dist(a',c') /\
  60         dist(b,c) = dist(b',c') /\
  61         between b (a,x) /\ between b' (a',x') /\ dist(b,x) = dist(b',x')
  62         ==> dist(c,x) = dist(c',x')`,
  63   let lemma = prove
  64    (`!a b x y:real^N.
  65       ~(b = a) /\ between b (a,x) /\ between b (a,y) /\ dist(b,x) = dist(b,y)
  66       ==> x = y`,
  67     REPEAT STRIP_TAC THEN REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE
  68      [IMP_CONJ] BETWEEN_EXISTS_EXTENSION))) THEN ASM_SIMP_TAC[] THEN
  69     REPEAT STRIP_TAC THEN UNDISCH_TAC `dist(b:real^N,x) = dist(b,y)` THEN
  70     ASM_REWRITE_TAC[NORM_ARITH `dist(b:real^N,b + x) = norm x`; NORM_MUL] THEN
  71     ASM_SIMP_TAC[REAL_EQ_MUL_RCANCEL; NORM_EQ_0; real_abs; VECTOR_SUB_EQ]) in
  72   REPEAT STRIP_TAC THEN MP_TAC(ISPECL
  73    [`a:real^2`; `b:real^2`; `c:real^2`; `a':real^2`; `b':real^2`; `c':real^2`]
  74    RIGID_TRANSFORMATION_BETWEEN_3) THEN
  75   ANTS_TAC THENL [ASM_MESON_TAC[DIST_EQ_0; DIST_SYM]; ALL_TAC] THEN
  76   DISCH_THEN(X_CHOOSE_THEN `k:real^2`
  77    (X_CHOOSE_THEN `f:real^2->real^2` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC))) THEN
  78   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN SUBST_ALL_TAC) THEN
  79   SUBGOAL_THEN `x' = k + (f:real^2->real^2) x` SUBST1_TAC THENL
  80    [MATCH_MP_TAC lemma THEN MAP_EVERY EXISTS_TAC
  81       [`k + (f:real^2->real^2) a`; `k + (f:real^2->real^2) b`];
  82     ALL_TAC] THEN
  83   ASM_REWRITE_TAC[NORM_ARITH `dist(a + x:real^N,a + y) = dist(x,y)`;
  84     BETWEEN_TRANSLATION; VECTOR_ARITH `a + x:real^N = a + y <=> x = y`] THEN
  85   ASM_MESON_TAC[BETWEEN_TRANSLATION; orthogonal_transformation;
  86                 NORM_ARITH `dist(a + x:real^N,a + y) = dist(x,y)`;
  87                 ORTHOGONAL_TRANSFORMATION_ISOMETRY; BETWEEN_LINEAR_IMAGE_EQ;
  88                 DIST_EQ_0; ORTHOGONAL_TRANSFORMATION_INJECTIVE]);;
  89
  90 (* ------------------------------------------------------------------------- *)
  91 (* Axiom 6 (identity for between-ness).                                      *)
  92 (* ------------------------------------------------------------------------- *)
  93
  94 let TARSKI_AXIOM_6_EUCLIDEAN = prove
  95  (`!a b. between b (a,a) ==> a = b`,
  96   SIMP_TAC[BETWEEN_REFL_EQ]);;
  97
  98 (* ------------------------------------------------------------------------- *)
  99 (* Axiom 7 (Pasch's axiom).                                                  *)
 100 (* ------------------------------------------------------------------------- *)
 101
 102 let TARSKI_AXIOM_7_EUCLIDEAN = prove
 103  (`!a b c p q:real^2.
 104         between p (a,c) /\ between q (b,c)
 105         ==> ?x. between x (p,b) /\ between x (q,a)`,
 106   REPEAT GEN_TAC THEN ASM_CASES_TAC `q:real^2 = c` THENL
 107    [ASM_MESON_TAC[BETWEEN_REFL; BETWEEN_SYM]; POP_ASSUM MP_TAC] THEN
 108   ASM_CASES_TAC `p:real^2 = a /\ b:real^2 = q` THENL
 109    [ASM_MESON_TAC[BETWEEN_REFL; BETWEEN_SYM]; POP_ASSUM MP_TAC] THEN
 110   GEOM_ORIGIN_TAC `a:real^2` THEN GEOM_NORMALIZE_TAC `q:real^2` THEN
 111   CONJ_TAC THENL
 112    [ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[BETWEEN_REFL_EQ] THEN
 113     REWRITE_TAC[UNWIND_THM2; between; DIST_0] THEN NORM_ARITH_TAC;
 114     ALL_TAC] THEN
 115   GEOM_BASIS_MULTIPLE_TAC 1 `q:real^2` THEN SIMP_TAC
 116    [NORM_MUL; NORM_BASIS; real_abs; DIMINDEX_2; ARITH; REAL_MUL_RID] THEN
 117   GEN_TAC THEN REPEAT(DISCH_THEN(K ALL_TAC)) THEN SIMP_TAC[VECTOR_MUL_LID] THEN
 118   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[BETWEEN_SYM] THEN DISCH_TAC THEN
 119   DISCH_TAC THEN DISCH_THEN(CONJUNCTS_THEN2
 120    (X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC o
 121      REWRITE_RULE[BETWEEN_IN_SEGMENT; IN_SEGMENT])
 122    (MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] BETWEEN_EXISTS_EXTENSION))) THEN
 123   ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `e:real` THEN
 124   STRIP_TAC THEN ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT; IN_SEGMENT] THEN
 125   REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
 126   SUBGOAL_THEN `&0 < &1 - d + e` ASSUME_TAC THENL
 127    [ASM_CASES_TAC `d = &1 /\ e = &0` THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
 128     REPEAT(FIRST_X_ASSUM(MP_TAC o check (is_eq o concl))) THEN
 129     ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_MUL_RZERO] THEN
 130     ASM_REWRITE_TAC[VECTOR_ADD_RID; IMP_IMP];
 131     EXISTS_TAC `(&1 - d + e - d * e) / (&1 - d + e) % basis 1:real^2` THEN
 132     CONJ_TAC THENL
 133      [EXISTS_TAC `e / (&1 - d + e)` THEN
 134       ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ] THEN
 135       REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
 136       SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; BASIS_COMPONENT; VEC_COMPONENT;
 137        ARITH; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
 138        VECTOR_SUB_COMPONENT] THEN
 139       UNDISCH_TAC `&0 < &1 - d + e` THEN CONV_TAC REAL_FIELD;
 140       EXISTS_TAC `(&1 - d + e - d * e) / (&1 - d + e)` THEN
 141       ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ] THEN
 142       SUBGOAL_THEN `&0 <= (&1 - d) * (&1 + e) /\ &0 <= d * e` MP_TAC THENL
 143        [CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL; ALL_TAC] THEN
 144       ASM_REAL_ARITH_TAC]]);;
 145
 146 (* ------------------------------------------------------------------------- *)
 147 (* Axiom 8 (lower 2-dimensional axiom).                                      *)
 148 (* ------------------------------------------------------------------------- *)
 149
 150 let TARSKI_AXIOM_8_EUCLIDEAN = prove
 151  (`?a b c:real^2. ~between b (a,c) /\ ~between c (b,a) /\ ~between a (c,b)`,
 152   REWRITE_TAC[GSYM DE_MORGAN_THM] THEN ONCE_REWRITE_TAC[BETWEEN_SYM] THEN
 153   REWRITE_TAC[GSYM COLLINEAR_BETWEEN_CASES; COLLINEAR_3_2D] THEN
 154   MAP_EVERY EXISTS_TAC
 155    [`vec 0:real^2`; `basis 1:real^2`; `basis 2:real^2`] THEN
 156   SIMP_TAC[BASIS_COMPONENT; VEC_COMPONENT; DIMINDEX_2; ARITH] THEN
 157   CONV_TAC REAL_RAT_REDUCE_CONV);;
 158
 159 (* ------------------------------------------------------------------------- *)
 160 (* Axiom 9 (upper 2-dimensional axiom).                                      *)
 161 (* ------------------------------------------------------------------------- *)
 162
 163 let TARSKI_AXIOM_9_EUCLIDEAN = prove
 164  (`!p q a b c:real^2.
 165         ~(p = q) /\
 166         dist(a,p) = dist(a,q) /\ dist(b,p) = dist(b,q) /\ dist(c,p) = dist(c,q)
 167         ==> between b (a,c) \/ between c (b,a) \/ between a (c,b)`,
 168   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[BETWEEN_SYM] THEN
 169   REWRITE_TAC[GSYM COLLINEAR_BETWEEN_CASES] THEN
 170   REWRITE_TAC[dist; NORM_EQ; NORM_ARITH
 171     `~(p = q) <=> ~(norm(p - q) = &0)`] THEN
 172   ONCE_REWRITE_TAC[REAL_RING `~(x = &0) <=> ~(x pow 2 = &0)`] THEN
 173   REWRITE_TAC[NORM_POW_2; COLLINEAR_3_2D] THEN
 174   REWRITE_TAC[DOT_2; VECTOR_SUB_COMPONENT] THEN
 175   CONV_TAC REAL_FIELD);;
 176
 177 (* ------------------------------------------------------------------------- *)
 178 (* Axiom 10 (Euclidean axiom).                                               *)
 179 (* ------------------------------------------------------------------------- *)
 180
 181 let TARSKI_AXIOM_10_EUCLIDEAN = prove
 182  (`!a b c d t:real^N.
 183         between d (a,t) /\ between d (b,c) /\ ~(a = d)
 184         ==> ?x y. between b (a,x) /\ between c (a,y) /\ between t (x,y)`,
 185   REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `a:real^N` THEN REPEAT STRIP_TAC THEN
 186   MP_TAC(ISPECL [`vec 0:real^N`; `d:real^N`; `t:real^N`]
 187         BETWEEN_EXISTS_EXTENSION) THEN
 188   ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM; VECTOR_ARITH
 189    `d + u % (d - vec 0):real^N = (&1 + u) % d`] THEN
 190   X_GEN_TAC `u:real` THEN STRIP_TAC THEN
 191   MAP_EVERY EXISTS_TAC [`(&1 + u) % b:real^N`; `(&1 + u) % c:real^N`] THEN
 192   ASM_REWRITE_TAC[between; dist; GSYM VECTOR_SUB_LDISTRIB] THEN
 193   ASM_REWRITE_TAC[VECTOR_SUB_LZERO; NORM_NEG;
 194                   VECTOR_ARITH `b - (&1 + u) % b:real^N = --(u % b)`] THEN
 195   ASM_SIMP_TAC[NORM_MUL; REAL_LE_ADD; REAL_POS; real_abs] THEN
 196   REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; REAL_EQ_MUL_LCANCEL] THEN
 197   ASM_REWRITE_TAC[GSYM dist; GSYM between] THEN REAL_ARITH_TAC);;
 198
 199 (* ------------------------------------------------------------------------- *)
 200 (* Axiom 11 (Continuity).                                                    *)
 201 (* ------------------------------------------------------------------------- *)
 202
 203 let TARSKI_AXIOM_11_EUCLIDEAN = prove
 204  (`!X Y:real^2->bool.
 205         (?a. !x y. x IN X /\ y IN Y ==> between x (a,y))
 206         ==> (?b. !x y. x IN X /\ y IN Y ==> between b (x,y))`,
 207   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN GEOM_ORIGIN_TAC `a:real^2` THEN
 208   REPEAT GEN_TAC THEN ASM_CASES_TAC `!x:real^2. x IN X ==> x = vec 0` THENL
 209    [ASM_MESON_TAC[BETWEEN_REFL]; POP_ASSUM MP_TAC] THEN
 210   ASM_CASES_TAC `Y:real^2->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
 211   SUBGOAL_THEN `?c:real^2. c IN Y` (CHOOSE_THEN MP_TAC) THENL
 212    [ASM SET_TAC[]; REPEAT(POP_ASSUM MP_TAC)] THEN
 213   GEOM_BASIS_MULTIPLE_TAC 1 `c:real^2` THEN
 214   X_GEN_TAC `c:real` THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
 215   DISCH_TAC THEN DISCH_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP] THEN
 216   DISCH_THEN(X_CHOOSE_THEN `z:real^2` STRIP_ASSUME_TAC) THEN
 217   DISCH_THEN(LABEL_TAC "*") THEN
 218   SUBGOAL_THEN `X SUBSET IMAGE (\c. c % basis 1:real^2) {c | &0 <= c} /\
 219                 Y SUBSET IMAGE (\c. c % basis 1:real^2) {c | &0 <= c}`
 220   MP_TAC THENL
 221    [REWRITE_TAC[SUBSET; IN_IMAGE; IN_ELIM_THM] THEN
 222     MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL
 223      [X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL
 224        [`x:real^2`; `c % basis 1:real^2`]) THEN
 225       ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT; IN_SEGMENT] THEN
 226       REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; IN_ELIM_THM] THEN
 227       ASM_MESON_TAC[VECTOR_MUL_ASSOC; REAL_LE_MUL];
 228       DISCH_THEN(MP_TAC o SPEC `z:real^2`) THEN ASM_REWRITE_TAC[] THEN
 229       DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
 230       UNDISCH_TAC `~(z:real^2 = vec 0)` THEN
 231       ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; DE_MORGAN_THM] THEN
 232       STRIP_TAC THEN X_GEN_TAC `y:real^2` THEN DISCH_TAC THEN
 233       REMOVE_THEN "*" (MP_TAC o SPECL [`z:real^2`; `y:real^2`]) THEN
 234       ASM_REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
 235       REWRITE_TAC[BETWEEN_IN_SEGMENT; IN_SEGMENT] THEN
 236       REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; IN_ELIM_THM] THEN
 237       DISCH_THEN(X_CHOOSE_THEN `u:real` MP_TAC) THEN
 238       ASM_CASES_TAC `u = &0` THEN
 239       ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_EQ_0] THEN
 240       STRIP_TAC THEN EXISTS_TAC `inv(u) * d:real` THEN
 241       ASM_REWRITE_TAC[GSYM VECTOR_MUL_ASSOC] THEN
 242       ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; VECTOR_MUL_ASSOC] THEN
 243       ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID]];
 244     REWRITE_TAC[SUBSET_IMAGE] THEN REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
 245     DISCH_THEN(CONJUNCTS_THEN2
 246      (X_CHOOSE_THEN `s:real->bool` STRIP_ASSUME_TAC)
 247      (X_CHOOSE_THEN `t:real->bool` STRIP_ASSUME_TAC)) THEN
 248     REMOVE_THEN "*" MP_TAC THEN
 249     ASM_REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
 250     DISCH_THEN(fun th ->
 251       EXISTS_TAC `sup s % basis 1 :real^2` THEN MP_TAC th) THEN
 252     REWRITE_TAC[between; dist; NORM_ARITH `norm(vec 0 - x) = norm x`] THEN
 253     REWRITE_TAC[GSYM VECTOR_SUB_RDISTRIB; NORM_MUL] THEN
 254     SIMP_TAC[NORM_BASIS; DIMINDEX_GE_1; LE_REFL; REAL_MUL_RID] THEN
 255     ASM_SIMP_TAC[REAL_ARITH
 256      `&0 <= x /\ &0 <= y ==> (abs y = abs x + abs(x - y) <=> x <= y)`] THEN
 257     DISCH_TAC THEN X_GEN_TAC `x:real` THEN DISCH_TAC THEN
 258     X_GEN_TAC `y:real` THEN DISCH_TAC THEN MATCH_MP_TAC(REAL_ARITH
 259      `x <= s /\ s <= y ==> abs(x - y) = abs(x - s) + abs(s - y)`) THEN
 260     MP_TAC(SPEC `s:real->bool` SUP) THEN
 261     ASM_MESON_TAC[IMAGE_EQ_EMPTY; MEMBER_NOT_EMPTY]]);;