1 (* ========================================================================= *)
2 (* Proof that Tarski's axioms for geometry hold in Euclidean space. *)
3 (* ========================================================================= *)
5 needs "Multivariate/convex.ml";;
7 (* ------------------------------------------------------------------------- *)
8 (* Axiom 1 (reflexivity for equidistance). *)
9 (* ------------------------------------------------------------------------- *)
11 let TARSKI_AXIOM_1_EUCLIDEAN = prove
12 (`!a b:real^2. dist(a,b) = dist(b,a)`,
15 (* ------------------------------------------------------------------------- *)
16 (* Axiom 2 (transitivity for equidistance). *)
17 (* ------------------------------------------------------------------------- *)
19 let TARSKI_AXIOM_2_EUCLIDEAN = prove
21 dist(a,b) = dist(p,q) /\ dist(a,b) = dist(r,s)
22 ==> dist(p,q) = dist(r,s)`,
25 (* ------------------------------------------------------------------------- *)
26 (* Axiom 3 (identity for equidistance). *)
27 (* ------------------------------------------------------------------------- *)
29 let TARSKI_AXIOM_3_EUCLIDEAN = prove
30 (`!a b c. dist(a,b) = dist(c,c) ==> a = b`,
33 (* ------------------------------------------------------------------------- *)
34 (* Axiom 4 (segment construction). *)
35 (* ------------------------------------------------------------------------- *)
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
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]]]);;
51 (* ------------------------------------------------------------------------- *)
52 (* Axiom 5 (five-segments axiom). *)
53 (* ------------------------------------------------------------------------- *)
55 let TARSKI_AXIOM_5_EUCLIDEAN = prove
56 (`!a b c x:real^2 a' b' c' x':real^2.
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')`,
65 ~(b = a) /\ between b (a,x) /\ between b (a,y) /\ dist(b,x) = dist(b,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`];
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]);;
90 (* ------------------------------------------------------------------------- *)
91 (* Axiom 6 (identity for between-ness). *)
92 (* ------------------------------------------------------------------------- *)
94 let TARSKI_AXIOM_6_EUCLIDEAN = prove
95 (`!a b. between b (a,a) ==> a = b`,
96 SIMP_TAC[BETWEEN_REFL_EQ]);;
98 (* ------------------------------------------------------------------------- *)
99 (* Axiom 7 (Pasch's axiom). *)
100 (* ------------------------------------------------------------------------- *)
102 let TARSKI_AXIOM_7_EUCLIDEAN = prove
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
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;
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
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]]);;
146 (* ------------------------------------------------------------------------- *)
147 (* Axiom 8 (lower 2-dimensional axiom). *)
148 (* ------------------------------------------------------------------------- *)
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
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);;
159 (* ------------------------------------------------------------------------- *)
160 (* Axiom 9 (upper 2-dimensional axiom). *)
161 (* ------------------------------------------------------------------------- *)
163 let TARSKI_AXIOM_9_EUCLIDEAN = prove
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);;
177 (* ------------------------------------------------------------------------- *)
178 (* Axiom 10 (Euclidean axiom). *)
179 (* ------------------------------------------------------------------------- *)
181 let TARSKI_AXIOM_10_EUCLIDEAN = prove
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);;
199 (* ------------------------------------------------------------------------- *)
200 (* Axiom 11 (Continuity). *)
201 (* ------------------------------------------------------------------------- *)
203 let TARSKI_AXIOM_11_EUCLIDEAN = prove
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}`
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
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]]);;