1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* Contains proofs of CDTETAT and SZIPOAS *)
4 (* ========================================================================== *)
7 flyspeck_needs "tame/TameGeneral.hl";;
8 flyspeck_needs "tame/ssreflect/tame_lemmas-compiled.hl";;
12 module Cdtetat_tame = struct
15 open Hypermap_and_fan;;
23 (* This approximation of pi is sufficient for the next lemma *)
24 let PI_APPROX_4 = prove(`#3.1415 <= pi /\ pi <= #3.1416`,
25 MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC);;
29 (* This lemma is a part of the proof of CDTETAT *)
30 let CDTETAT_lemma1 = prove(`!p t:num. &p * (#0.852) + &t * (#1.15) <= &2 * pi /\ &2 * pi < &p * #1.9 + &t * pi ==>
31 (p, t) IN { (0,3), (0,4), (0,5), (1,2), (1,3), (1,4),
32 (2,1), (2,2), (2,3), (3,1), (3,2), (3,3),
33 (4,0), (4,1),(4,2), (5,0), (5,1),
34 (6,0), (6,1), (7,0) }`,
36 SUBGOAL_THEN `p <= 7` ASSUME_TAC THENL
39 POP_ASSUM (MP_TAC o (fun th -> MATCH_MP (REAL_ARITH `&p * #0.852 + &t * #1.15 <= &2 * pi ==> &p <= (&2 * pi) / #0.852`) th)) THEN
41 SUBGOAL_THEN `p < 8` (fun th -> MP_TAC th THEN ARITH_TAC) THEN
42 REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
43 POP_ASSUM MP_TAC THEN MP_TAC PI_APPROX_4 THEN
48 SUBGOAL_THEN `&t <= (&2 * #3.1416 - &p * #0.852) / #1.15` MP_TAC THENL
50 REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
51 MP_TAC PI_APPROX_4 THEN
56 SUBGOAL_THEN `&2 - (&p * #1.9) / pi < &t` MP_TAC THENL
58 MP_TAC (REAL_FIELD `&0 < pi ==> &2 - (&p * #1.9) / pi = (&2 * pi - &p * #1.9) / pi`) THEN
59 SUBGOAL_TAC "A" `&0 < pi` [ MP_TAC PI_APPROX_4 THEN REAL_ARITH_TAC ] THEN
60 ASM_REWRITE_TAC[] THEN
61 DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
62 ASM_SIMP_TAC[REAL_LT_LDIV_EQ] THEN
63 REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
68 REMOVE_ASSUM THEN REMOVE_ASSUM THEN
69 DISCH_TAC THEN DISCH_TAC THEN
71 SUBGOAL_THEN `&2 - (&p * #1.9) / #3.1415 < &t` MP_TAC THENL
73 MATCH_MP_TAC REAL_LET_TRANS THEN
74 EXISTS_TAC `&2 - (&p * #1.9) / pi` THEN
75 ASM_REWRITE_TAC[REAL_ARITH `a - b <= a - c <=> c <= b`] THEN
76 REWRITE_TAC[real_div] THEN
77 MATCH_MP_TAC REAL_LE_LMUL THEN
78 REWRITE_TAC[REAL_ARITH `&0 <= &p * #1.9`] THEN
79 MATCH_MP_TAC REAL_LE_INV2 THEN
80 MP_TAC PI_APPROX_4 THEN REAL_ARITH_TAC;
84 DISCH_THEN (LABEL_TAC "A") THEN DISCH_THEN (LABEL_TAC "B") THEN
86 DISJ_CASES_TAC (ARITH_RULE `7 < p \/ p < 8`) THENL
88 ASM_MESON_TAC[NOT_LE];
91 POP_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[gen_NUM_CASES 8] th)) THEN
93 POP_ASSUM MP_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
94 POP_ASSUM (fun th -> SUBST_ALL_TAC th) THEN
95 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
96 CONV_TAC REAL_RAT_REDUCE_CONV THEN REPEAT STRIP_TAC THENL
98 SUBGOAL_THEN `2 < t /\ t < 6` ASSUME_TAC THENL
100 REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
101 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
105 ASM SET_TAC[ARITH_RULE `2 < t /\ t < 6 ==> t = 3 \/ t = 4 \/ t = 5`];
107 SUBGOAL_THEN `1 < t /\ t < 5` ASSUME_TAC THENL
109 REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
110 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
114 ASM SET_TAC[ARITH_RULE `1 < t /\ t < 5 ==> t = 2 \/ t = 3 \/ t = 4`];
116 SUBGOAL_THEN `0 < t /\ t < 4` ASSUME_TAC THENL
118 REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
119 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
123 ASM SET_TAC[ARITH_RULE `0 < t /\ t < 4 ==> t = 1 \/ t = 2 \/ t = 3`];
125 SUBGOAL_THEN `0 < t /\ t < 4` ASSUME_TAC THENL
127 REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
128 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
132 ASM SET_TAC[ARITH_RULE `0 < t /\ t < 4 ==> t = 1 \/ t = 2 \/ t = 3`];
134 SUBGOAL_THEN `t < 3` ASSUME_TAC THENL
136 REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
137 POP_ASSUM MP_TAC THEN
141 ASM SET_TAC[ARITH_RULE `t < 3 ==> t = 0 \/ t = 1 \/ t = 2`];
143 SUBGOAL_THEN `t < 2` ASSUME_TAC THENL
145 REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
146 POP_ASSUM MP_TAC THEN
150 ASM SET_TAC[ARITH_RULE `t < 2 ==> t = 0 \/ t = 1`];
152 SUBGOAL_THEN `t < 2` ASSUME_TAC THENL
154 REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
155 POP_ASSUM MP_TAC THEN
159 ASM SET_TAC[ARITH_RULE `t < 2 ==> t = 0 \/ t = 1`];
161 SUBGOAL_THEN `t < 1` ASSUME_TAC THENL
163 REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
164 POP_ASSUM MP_TAC THEN
168 ASM SET_TAC[ARITH_RULE `t < 1 ==> t = 0`]
173 (* CDTETAT (with assumptions) *)
175 let CDTETAT = prove(`kcblrqc_ineq_def ==> !V x. contravening V /\ x IN dart_of_fan (V,ESTD V) ==>
176 (let (p,q,r) = type_of_node (hypermap_of_fan (V, ESTD V)) x in
177 ((p,q+r) IN { (0,3), (0,4), (0,5), (1,2), (1,3), (1,4),
178 (2,1), (2,2), (2,3), (3,1), (3,2), (3,3),
179 (4,0), (4,1),(4,2), (5,0), (5,1),
180 (6,0), (6,1), (7,0) }))`,
181 REPEAT STRIP_TAC THEN
182 MP_TAC (ISPEC `V:real^3->bool` CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
183 MP_TAC (ISPECL [`hypermap_of_fan (V:real^3->bool,ESTD V)`; `x:real^3#real^3`] NODE_TYPE_lemma) THEN
184 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN; Jgtdebu.JGTDEBU4] THEN
185 DISCH_THEN (fun th -> ALL_TAC) THEN
186 CONV_TAC let_CONV THEN
187 ABBREV_TAC `H = hypermap_of_fan (V,ESTD V)` THEN
188 ABBREV_TAC `A = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 3}` THEN
189 ABBREV_TAC `B = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 4}` THEN
190 ABBREV_TAC `C = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 5}` THEN
191 MATCH_MP_TAC CDTETAT_lemma1 THEN
193 MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] SUM_AZIM_DART_FULLY_SURROUNDED) THEN
194 MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] FULLY_SURROUNDED_NODE_DECOMPOSITION) THEN
196 ASM_SIMP_TAC[CONTRAVENING_IMP_FULLY_SURROUNDED] THEN
197 CONV_TAC (DEPTH_CONV let_CONV) THEN
198 ASM_REWRITE_TAC[] THEN
199 ABBREV_TAC `D = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 4}` THEN
201 DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
202 DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC) THEN
205 SUBGOAL_THEN `&(CARD (B:real^3#real^3->bool) + CARD (C:real^3#real^3->bool)) = &(CARD (D:real^3#real^3->bool))` MP_TAC THENL
207 REWRITE_TAC[REAL_OF_NUM_EQ] THEN
208 MATCH_MP_TAC CARD_UNION_EQ THEN
209 ASM_SIMP_TAC[GSYM DISJOINT];
213 FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (is_eq o concl)) THEN
214 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
216 SUBGOAL_THEN `!y:real^3#real^3. y IN node H x ==> y IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL
218 REWRITE_TAC[GSYM SUBSET] THEN
219 MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] NODE_SUBSET_DART_OF_FAN) THEN
224 SUBGOAL_THEN `!y. y IN A ==> azim_dart (V,ESTD V) y < #1.9 /\ #0.852 < azim_dart (V,ESTD V) y` ASSUME_TAC THENL
226 EXPAND_TAC "A" THEN GEN_TAC THEN
227 REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
228 MP_TAC TRIANGULAR_FACE_AZIM_DART_BOUNDS THEN
229 UNDISCH_TAC `kcblrqc_ineq_def` THEN SIMP_TAC[kcblrqc_ineq_def] THEN DISCH_THEN (fun th -> ALL_TAC) THEN
230 DISCH_THEN (MP_TAC o SPECL [`V:real^3->bool`; `y:real^3#real^3`]) THEN
231 ASM_SIMP_TAC[REAL_ARITH `a < #1.893 ==> a < #1.9`];
235 SUBGOAL_THEN `!y. y IN D ==> azim_dart (V,ESTD V) y < pi /\ #1.15 < azim_dart (V,ESTD V) y` ASSUME_TAC THENL
237 EXPAND_TAC "D" THEN GEN_TAC THEN
238 REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
239 MP_TAC (SPEC `V:real^3->bool` non_triangular_face_azim_dart_bound) THEN ASM_REWRITE_TAC[] THEN
240 DISCH_THEN (MP_TAC o SPEC `y:real^3#real^3`) THEN
241 ASM_SIMP_TAC[ARITH_RULE `3 < a <=> a >= 4`] THEN
242 MP_TAC (SPECL [`V:real^3->bool`] CONTRAVENING_IMP_FULLY_SURROUNDED) THEN
243 ASM_REWRITE_TAC[fully_surrounded] THEN
244 DISCH_THEN (MP_TAC o SPEC `y:real^3#real^3`) THEN
249 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
253 MATCH_MP_TAC REAL_LE_ADD2 THEN
254 ONCE_REWRITE_TAC[GSYM REAL_LE_NEG] THEN
255 GEN_REWRITE_TAC (PAT_CONV `(\f. --sum A f <= x /\ --sum D f <= y)`) [GSYM ETA_AX] THEN
256 REWRITE_TAC[GSYM SUM_NEG] THEN
257 REWRITE_TAC[REAL_NEG_RMUL] THEN
258 CONJ_TAC THEN MATCH_MP_TAC SUM_BOUND THEN ASM_SIMP_TAC[REAL_LE_NEG; REAL_LT_IMP_LE];
260 SUBGOAL_THEN `x:real^3#real^3 IN A \/ x IN D` MP_TAC THENL
262 REWRITE_TAC[GSYM IN_UNION] THEN
263 FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
264 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
265 REWRITE_TAC[Hypermap.node_refl];
271 MATCH_MP_TAC REAL_LTE_ADD2 THEN
274 MATCH_MP_TAC SUM_BOUND_LT THEN
275 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
276 EXISTS_TAC `x:real^3#real^3` THEN
278 MATCH_MP_TAC SUM_BOUND THEN
279 ASM_SIMP_TAC[REAL_LT_IMP_LE]
284 MATCH_MP_TAC REAL_LET_ADD2 THEN
287 MATCH_MP_TAC SUM_BOUND THEN
288 ASM_SIMP_TAC[REAL_LT_IMP_LE];
289 MATCH_MP_TAC SUM_BOUND_LT THEN
290 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
291 EXISTS_TAC `x:real^3#real^3` THEN
292 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[]
302 let SZIPOAS = prove(`kcblrqc_ineq_def ==>
303 !V. contravening V ==> tame_11b (hypermap_of_fan (V, ESTD V))`,
304 REPEAT STRIP_TAC THEN REWRITE_TAC[tame_11b] THEN
305 MP_TAC (ISPEC `V:real^3->bool` CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
307 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
310 MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] FULLY_SURROUNDED_IMP_CARD_NODE_EQ_SUM_NODE_TYPE) THEN
311 ASM_SIMP_TAC[CONTRAVENING_IMP_FULLY_SURROUNDED; Jgtdebu.JGTDEBU4] THEN
312 FIRST_X_ASSUM (MP_TAC o SPECL [`V:real^3->bool`; `x:real^3#real^3`] o MATCH_MP CDTETAT) THEN
313 ASM_REWRITE_TAC[type_of_node] THEN
314 CONV_TAC (DEPTH_CONV let_CONV) THEN
315 ABBREV_TAC `H = hypermap_of_fan (V,ESTD(V))` THEN
316 ABBREV_TAC `p = CARD (set_of_triangles_meeting_node H (x:real^3#real^3))` THEN
317 ABBREV_TAC `q = CARD (set_of_quadrilaterals_meeting_node H (x:real^3#real^3))` THEN
318 ABBREV_TAC `r = CARD (set_of_exceptional_meeting_node H (x:real^3#real^3))` THEN
320 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; PAIR_EQ] THEN