1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* Section: Appendix *)
4 (* Chapter: Local Fan *)
5 (* Author: John Harrison *)
7 (* ========================================================================== *)
9 module Pqcsxwg = struct
12 (* ------------------------------------------------------------------------- *)
13 (* Suite of continuity properties for sqrt. *)
14 (* ------------------------------------------------------------------------- *)
16 let CONTINUOUS_WITHIN_SQRT_COMPOSE = prove
18 (\x. lift(f x)) continuous (at a within s) /\
19 (&0 < f a \/ !x. x IN s ==> &0 <= f x)
20 ==> (\x. lift(sqrt(f x))) continuous (at a within s)`,
23 `(\x:real^N. lift(sqrt(f x))) = (lift o sqrt o drop) o (lift o f)`
24 SUBST1_TAC THENL [REWRITE_TAC[o_DEF; LIFT_DROP]; ALL_TAC] THEN
26 (MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN
27 CONJ_TAC THENL [ASM_REWRITE_TAC[o_DEF]; ALL_TAC])
29 [MATCH_MP_TAC CONTINUOUS_AT_WITHIN THEN
30 MATCH_MP_TAC CONTINUOUS_AT_SQRT THEN ASM_REWRITE_TAC[o_DEF; LIFT_DROP];
31 MATCH_MP_TAC CONTINUOUS_WITHIN_LIFT_SQRT THEN
32 ASM_REWRITE_TAC[FORALL_IN_IMAGE; o_DEF; LIFT_DROP]]);;
34 let CONTINUOUS_AT_SQRT_COMPOSE = prove
36 (\x. lift(f x)) continuous (at a) /\ (&0 < f a \/ !x. &0 <= f x)
37 ==> (\x. lift(sqrt(f x))) continuous (at a)`,
39 MP_TAC(ISPECL [`f:real^N->real`; `(:real^N)`; `a:real^N`]
40 CONTINUOUS_WITHIN_SQRT_COMPOSE) THEN
41 REWRITE_TAC[WITHIN_UNIV; IN_UNIV]);;
43 let REAL_CONTINUOUS_WITHIN_SQRT_COMPOSE = prove
45 f real_continuous (at a within s) /\
46 (&0 < f a \/ !x. x IN s ==> &0 <= f x)
47 ==> (\x. sqrt(f x)) real_continuous (at a within s)`,
48 REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1; o_DEF] THEN
49 REWRITE_TAC[CONTINUOUS_WITHIN_SQRT_COMPOSE]);;
51 let REAL_CONTINUOUS_AT_SQRT_COMPOSE = prove
53 f real_continuous (at a) /\
54 (&0 < f a \/ !x. &0 <= f x)
55 ==> (\x. sqrt(f x)) real_continuous (at a)`,
56 REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1; o_DEF] THEN
57 REWRITE_TAC[CONTINUOUS_AT_SQRT_COMPOSE]);;
59 let CONTINUOUS_WITHINREAL_SQRT_COMPOSE = prove
60 (`!f s a. (\x. lift(f x)) continuous (atreal a within s) /\
61 (&0 < f a \/ !x. x IN s ==> &0 <= f x)
62 ==> (\x. lift(sqrt(f x))) continuous (atreal a within s)`,
63 REWRITE_TAC[(* Xbjrphc. *)CONTINUOUS_CONTINUOUS_WITHINREAL] THEN
64 REWRITE_TAC[o_DEF] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
65 MATCH_MP_TAC CONTINUOUS_WITHIN_SQRT_COMPOSE THEN
66 ASM_REWRITE_TAC[FORALL_IN_IMAGE; LIFT_DROP]);;
68 let CONTINUOUS_ATREAL_SQRT_COMPOSE = prove
69 (`!f a. (\x. lift(f x)) continuous (atreal a) /\ (&0 < f a \/ !x. &0 <= f x)
70 ==> (\x. lift(sqrt(f x))) continuous (atreal a)`,
72 MP_TAC(ISPECL [`f:real->real`; `(:real)`; `a:real`]
73 CONTINUOUS_WITHINREAL_SQRT_COMPOSE) THEN
74 REWRITE_TAC[WITHINREAL_UNIV; IN_UNIV]);;
76 let REAL_CONTINUOUS_WITHINREAL_SQRT_COMPOSE = prove
77 (`!f s a. f real_continuous (atreal a within s) /\
78 (&0 < f a \/ !x. x IN s ==> &0 <= f x)
79 ==> (\x. sqrt(f x)) real_continuous (atreal a within s)`,
80 REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1; o_DEF] THEN
81 REWRITE_TAC[CONTINUOUS_WITHINREAL_SQRT_COMPOSE]);;
83 let REAL_CONTINUOUS_ATREAL_SQRT_COMPOSE = prove
84 (`!f a. f real_continuous (atreal a) /\
85 (&0 < f a \/ !x. &0 <= f x)
86 ==> (\x. sqrt(f x)) real_continuous (atreal a)`,
87 REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1; o_DEF] THEN
88 REWRITE_TAC[CONTINUOUS_ATREAL_SQRT_COMPOSE]);;
90 (* ------------------------------------------------------------------------- *)
91 (* Flyspeck definition of mk_simplex (corrected). *)
92 (* ------------------------------------------------------------------------- *)
94 let mk_simplex1 = new_definition `mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 =
95 (let uinv = &1 / ups_x x1 x2 x6 in
96 let d = delta_x x1 x2 x3 x4 x5 x6 in
97 let d5 = delta_x5 x1 x2 x3 x4 x5 x6 in
98 let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in
99 let vcross = (v1 - v0) cross (v2 - v0) in
100 v0 + uinv % ((&2 * sqrt d) % vcross + d5 % (v1 - v0) + d4 % (v2 - v0)))`;;
102 let MK_SIMPLEX_TRANSLATION = prove
103 (`!a v0 v1 v2 x1 x2 x3 x4 x5 x6.
104 mk_simplex1 (a + v0) (a + v1) (a + v2) x1 x2 x3 x4 x5 x6 =
105 a + mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6`,
106 REPEAT GEN_TAC THEN REWRITE_TAC[mk_simplex1] THEN
107 CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
108 REWRITE_TAC[VECTOR_ARITH `(a + x) - (a + y):real^N = x - y`] THEN
109 REWRITE_TAC[GSYM VECTOR_ADD_ASSOC]);;
111 add_translation_invariants [MK_SIMPLEX_TRANSLATION];;
113 (* ------------------------------------------------------------------------- *)
114 (* The first part of PQCSXWG. *)
115 (* ------------------------------------------------------------------------- *)
117 let PQCSXWG1_concl = `!v0 v1 v2 v3 x1 x2 x3 x4 x5 x6.
118 &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
119 ~collinear {v0,v1,v2} /\
120 x1 = dist(v1,v0) pow 2 /\
121 x2 = dist(v2,v0) pow 2 /\
122 x6 = dist(v1,v2) pow 2 /\
123 &0 < delta_x x1 x2 x3 x4 x5 x6 /\
124 v3 = mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
125 (x3 = dist(v3,v0) pow 2 /\
126 x5 = dist(v3,v1) pow 2 /\
127 x4 = dist(v3,v2) pow 2 /\
128 (v1 - v0) dot ((v2 - v0) cross (v3 - v0)) > &0)`;;
132 GEOM_ORIGIN_TAC `v0:real^3` THEN REPEAT GEN_TAC THEN
133 REWRITE_TAC[mk_simplex1; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
134 REPEAT LET_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
135 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC SUBST1_TAC) THEN
136 REWRITE_TAC[GSYM CONJ_ASSOC] THEN
137 DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
138 REWRITE_TAC[dist; VECTOR_SUB_RZERO] THEN
139 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
140 REWRITE_TAC[CROSS_RADD; CROSS_RMUL;
141 VECTOR_ARITH `(a + x % b + c) - b:real^N = a + (x - &1) % b + c`;
142 VECTOR_ARITH `(a + b + x % c) - c:real^N = a + b + (x - &1) % c`] THEN
144 `!a b c. norm(a % vcross + b % v1 + c % v2:real^3) pow 2 =
145 norm(a % vcross) pow 2 + norm(b % v1 + c % v2) pow 2`
146 (fun th -> REWRITE_TAC[th])
148 [REPEAT GEN_TAC THEN MATCH_MP_TAC NORM_ADD_PYTHAGOREAN THEN
149 EXPAND_TAC "vcross" THEN REWRITE_TAC[orthogonal] THEN VEC3_TAC;
151 REWRITE_TAC[CROSS_REFL; VECTOR_MUL_RZERO; VECTOR_ADD_RID; real_gt] THEN
152 REWRITE_TAC[DOT_RADD; DOT_RMUL; DOT_CROSS_SELF] THEN
153 REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_RID] THEN
154 REWRITE_TAC[VEC3_RULE `v1 dot (v2 cross v) = (v1 cross v2) dot v`] THEN
155 SUBGOAL_THEN `~(vcross:real^3 = vec 0)` ASSUME_TAC THENL
156 [EXPAND_TAC "vcross" THEN REWRITE_TAC[CROSS_EQ_0] THEN ASM_REWRITE_TAC[];
157 ASM_SIMP_TAC[GSYM NORM_POW_2; NORM_POS_LT; REAL_POW_LT; REAL_LT_MUL_EQ;
158 REAL_ARITH `&0 < x * &2 * y <=> &0 < x * y`; SQRT_POS_LT]] THEN
159 SUBGOAL_THEN `&0 < ups_x x1 x2 x6` ASSUME_TAC THENL
160 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I
161 [Collect_geom2.NOT_COL_EQ_UPS_X_POS]) THEN
162 MAP_EVERY EXPAND_TAC ["x1"; "x2"; "x6"] THEN REWRITE_TAC[DIST_SYM];
163 EXPAND_TAC "uinv" THEN
164 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH]] THEN
165 REWRITE_TAC[NORM_MUL; REAL_POW_MUL; REAL_POW2_ABS] THEN
166 ASM_SIMP_TAC[SQRT_POW_2; REAL_LT_IMP_LE] THEN
167 REWRITE_TAC[REAL_ARITH `x * &2 pow 2 * y = &4 * x * y`] THEN
168 REWRITE_TAC[NORM_POW_2; VECTOR_ARITH
169 `(a + b) dot (a + b:real^3) = a dot a + b dot b + &2 * a dot b`] THEN
170 REWRITE_TAC[DOT_LMUL] THEN REWRITE_TAC[DOT_RMUL] THEN
171 ONCE_REWRITE_TAC[REAL_ARITH
172 `x3:real = a + b /\ x5 = a + c /\ x4 = a + d <=>
173 x3 = a + b /\ x3 - x5 = b - c /\ x3 - x4 = b - d`] THEN
174 REWRITE_TAC[REAL_ARITH
175 `(b * b * x + c * c * y + &2 * b * c * z) -
176 ((b - &1) * (b - &1) * x + c * c * y + &2 * (b - &1) * c * z) =
177 (&2 * b - &1) * x + &2 * c * z /\
178 (b * b * x + c * c * y + &2 * b * c * z) -
179 (b * b * x + (c - &1) * (c - &1) * y + &2 * b * (c - &1) * z) =
180 (&2 * c - &1) * y + &2 * b * z`] THEN
181 RULE_ASSUM_TAC(REWRITE_RULE[DIST_0]) THEN
182 ASM_REWRITE_TAC[GSYM NORM_POW_2; REAL_ARITH
183 `x = (&2 * b - &1) * y + &2 * c * z <=>
184 b * y + c * z = (y + x) / &2`] THEN
185 EXPAND_TAC "vcross" THEN REWRITE_TAC[NORM_POW_2; DOT_CROSS] THEN
186 ASM_REWRITE_TAC[GSYM NORM_POW_2] THEN
187 SUBST1_TAC(VECTOR_ARITH `(v2:real^3) dot v1 = v1 dot v2`) THEN
188 REWRITE_TAC[GSYM REAL_POW_2] THEN
189 SUBGOAL_THEN `(v1:real^3) dot v2 = ((x1 + x2) - x6) / &2` SUBST1_TAC THENL
190 [MAP_EVERY EXPAND_TAC ["x1"; "x2"; "x6"] THEN
191 REWRITE_TAC[dist; NORM_POW_2; DOT_RSUB; DOT_LSUB] THEN
192 REWRITE_TAC[DOT_SYM] THEN REAL_ARITH_TAC;
194 REWRITE_TAC[REAL_ARITH
195 `(&4 * u pow 2 * d) * x + (u * e) * (u * e) * y + (u * f) * (u * f) * z +
196 &2 * (u * e) * (u * f) * j =
197 u pow 2 * (&4 * d * x + e pow 2 * y + f pow 2 * z + &2 * e * f * j)`] THEN
198 REWRITE_TAC[REAL_ARITH
199 `(u * d) * x + (u * e) * y:real = z <=> u * (d * x + e * y) = z`] THEN
200 EXPAND_TAC "uinv" THEN MATCH_MP_TAC(REAL_FIELD
202 u pow 2 * x = y /\ u * a = b /\ u * c = d
203 ==> x = (&1 / u) pow 2 * y /\
204 (&1 / u) * b = a /\ (&1 / u) * d = c`) THEN
205 ASM_REWRITE_TAC[] THEN MAP_EVERY EXPAND_TAC ["uinv"; "d"; "d5"; "d4"] THEN
206 REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP REAL_LT_IMP_NZ)) THEN
207 REWRITE_TAC[Nonlin_def.delta_x5; Nonlin_def.delta_x4] THEN
208 REWRITE_TAC[Sphere.ups_x; Sphere.delta_x] THEN CONV_TAC REAL_RING);;
210 (* ------------------------------------------------------------------------- *)
211 (* The continuity part. *)
212 (* ------------------------------------------------------------------------- *)
214 let CONTINUOUS_MK_SIMPLEX_WITHINREAL = prove
215 (`!v0 v1 v2 x1 x2 x3 x4 x5 x6 s a.
216 ~(ups_x (x1 a) (x2 a) (x6 a) = &0) /\
217 &0 < delta_x (x1 a) (x2 a) (x3 a) (x4 a) (x5 a) (x6 a) /\
218 v0 continuous (atreal a within s) /\
219 v1 continuous (atreal a within s) /\
220 v2 continuous (atreal a within s) /\
221 x1 real_continuous (atreal a within s) /\
222 x2 real_continuous (atreal a within s) /\
223 x3 real_continuous (atreal a within s) /\
224 x4 real_continuous (atreal a within s) /\
225 x5 real_continuous (atreal a within s) /\
226 x6 real_continuous (atreal a within s)
227 ==> (\t. mk_simplex1 (v0 t) (v1 t) (v2 t)
228 (x1 t) (x2 t) (x3 t) (x4 t) (x5 t) (x6 t))
229 continuous (atreal a within s)`,
231 REPEAT((MATCH_MP_TAC REAL_CONTINUOUS_MUL ORELSE
232 MATCH_MP_TAC REAL_CONTINUOUS_ADD ORELSE
233 MATCH_MP_TAC REAL_CONTINUOUS_SUB) THEN CONJ_TAC) THEN
234 ASM_SIMP_TAC[REAL_CONTINUOUS_NEG; REAL_CONTINUOUS_CONST] in
235 REPEAT STRIP_TAC THEN REWRITE_TAC[mk_simplex1] THEN
236 CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
237 MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_REWRITE_TAC[] THEN
238 MATCH_MP_TAC CONTINUOUS_MUL THEN CONJ_TAC THENL
239 [REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1; real_div; REAL_MUL_LID] THEN
240 MATCH_MP_TAC REAL_CONTINUOUS_INV_WITHINREAL THEN
241 ASM_REWRITE_TAC[] THEN REWRITE_TAC[Sphere.ups_x] THEN POLY_CONT_TAC;
243 MATCH_MP_TAC CONTINUOUS_ADD THEN CONJ_TAC THENL
244 [MATCH_MP_TAC CONTINUOUS_MUL THEN
245 ASM_SIMP_TAC[CONTINUOUS_CROSS; CONTINUOUS_SUB] THEN
246 REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1] THEN
247 MATCH_MP_TAC REAL_CONTINUOUS_LMUL THEN
248 MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SQRT_COMPOSE THEN
249 ASM_REWRITE_TAC[] THEN REWRITE_TAC[Sphere.delta_x] THEN POLY_CONT_TAC;
250 MATCH_MP_TAC CONTINUOUS_ADD THEN
251 REWRITE_TAC[Nonlin_def.delta_x5; Nonlin_def.delta_x4] THEN
252 CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_MUL THEN
253 ASM_SIMP_TAC[CONTINUOUS_SUB; GSYM REAL_CONTINUOUS_CONTINUOUS1] THEN
256 let PQCSXWG2_WITHINREAL = prove
257 (`!v0 v1 v2 x1 x2 x3 x4 x5 x6 s a.
258 ~collinear {v0 a,v1 a,v2 a} /\
259 x1 a = dist(v1 a,v0 a) pow 2 /\
260 x2 a = dist(v2 a,v0 a) pow 2 /\
261 x6 a = dist(v1 a,v2 a) pow 2 /\
262 &0 < delta_x (x1 a) (x2 a) (x3 a) (x4 a) (x5 a) (x6 a) /\
263 v0 continuous (atreal a within s) /\
264 v1 continuous (atreal a within s) /\
265 v2 continuous (atreal a within s) /\
266 x1 real_continuous (atreal a within s) /\
267 x2 real_continuous (atreal a within s) /\
268 x3 real_continuous (atreal a within s) /\
269 x4 real_continuous (atreal a within s) /\
270 x5 real_continuous (atreal a within s) /\
271 x6 real_continuous (atreal a within s)
272 ==> (\t. mk_simplex1 (v0 t) (v1 t) (v2 t)
273 (x1 t) (x2 t) (x3 t) (x4 t) (x5 t) (x6 t))
274 continuous (atreal a within s)`,
275 REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
276 MATCH_MP_TAC CONTINUOUS_MK_SIMPLEX_WITHINREAL THEN
277 ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I
278 [Collect_geom2.NOT_COL_EQ_UPS_X_POS]) THEN
279 REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN REWRITE_TAC[DIST_SYM] THEN
282 let PQCSXWG2_ATREAL = prove
283 (`!v0 v1 v2 x1 x2 x3 x4 x5 x6 a.
284 ~collinear {v0 a,v1 a,v2 a} /\
285 x1 a = dist(v1 a,v0 a) pow 2 /\
286 x2 a = dist(v2 a,v0 a) pow 2 /\
287 x6 a = dist(v1 a,v2 a) pow 2 /\
288 &0 < delta_x (x1 a) (x2 a) (x3 a) (x4 a) (x5 a) (x6 a) /\
289 v0 continuous (atreal a) /\
290 v1 continuous (atreal a) /\
291 v2 continuous (atreal a) /\
292 x1 real_continuous (atreal a) /\
293 x2 real_continuous (atreal a) /\
294 x3 real_continuous (atreal a) /\
295 x4 real_continuous (atreal a) /\
296 x5 real_continuous (atreal a) /\
297 x6 real_continuous (atreal a)
298 ==> (\t. mk_simplex1 (v0 t) (v1 t) (v2 t)
299 (x1 t) (x2 t) (x3 t) (x4 t) (x5 t) (x6 t))
300 continuous (atreal a)`,
301 ONCE_REWRITE_TAC[GSYM WITHINREAL_UNIV] THEN
302 REWRITE_TAC[PQCSXWG2_WITHINREAL]);;
304 let PQCSXWG2_concl = `!(v0:real^3) v1 v2 v3 x1 x2 x3 x4 x5 x6.
305 &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
306 ~collinear {v0,v1,v2} /\
307 x1 = dist(v1,v0) pow 2 /\
308 x2 = dist(v2,v0) pow 2 /\
309 x6 = dist(v1,v2) pow 2 /\
310 &0 < delta_x x1 x2 x3 x4 x5 x6 /\
311 v3 = mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
312 (\q. mk_simplex1 v0 v1 v2 x1 x2 x3 x4 q x6) continuous atreal x5`;;
316 REPEAT STRIP_TAC THEN MATCH_MP_TAC PQCSXWG2_ATREAL THEN
317 ASM_REWRITE_TAC[REAL_CONTINUOUS_CONST; CONTINUOUS_CONST;
318 REAL_CONTINUOUS_AT_ID]);;