Update from HH
[Multivariate Analysis/.git] / 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]]);;