(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Contains proofs of CDTETAT and SZIPOAS                                     *)
(* ========================================================================== *)


flyspeck_needs "tame/TameGeneral.hl";;
flyspeck_needs "tame/ssreflect/tame_lemmas-compiled.hl";;



module Cdtetat_tame = struct


open Hypermap_and_fan;;
open Fan_defs;;
open Tame_defs;;
open Tame_general;;
open Tame_lemmas;;



(* This approximation of pi is sufficient for the next lemma *)
let PI_APPROX_4 = 
prove(`#3.1415 <= pi /\ pi <= #3.1416`,
MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC);;
(* This lemma is a part of the proof of CDTETAT *)
let CDTETAT_lemma1 = 
prove(`!p t:num. &p * (#0.852) + &t * (#1.15) <= &2 * pi /\ &2 * pi < &p * #1.9 + &t * pi ==> (p, t) IN { (0,3), (0,4), (0,5), (1,2), (1,3), (1,4), (2,1), (2,2), (2,3), (3,1), (3,2), (3,3), (4,0), (4,1),(4,2), (5,0), (5,1), (6,0), (6,1), (7,0) }`,
REPEAT STRIP_TAC THEN SUBGOAL_THEN `p <= 7` ASSUME_TAC THENL [ REMOVE_ASSUM THEN 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 DISCH_TAC THEN SUBGOAL_THEN `p < 8` (fun th -> MP_TAC th THEN ARITH_TAC) THEN REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN MP_TAC PI_APPROX_4 THEN REAL_ARITH_TAC; ALL_TAC ] THEN SUBGOAL_THEN `&t <= (&2 * #3.1416 - &p * #0.852) / #1.15` MP_TAC THENL [ REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN MP_TAC PI_APPROX_4 THEN REAL_ARITH_TAC; ALL_TAC ] THEN SUBGOAL_THEN `&2 - (&p * #1.9) / pi < &t` MP_TAC THENL [ MP_TAC (REAL_FIELD `&0 < pi ==> &2 - (&p * #1.9) / pi = (&2 * pi - &p * #1.9) / pi`) THEN SUBGOAL_TAC "A" `&0 < pi` [ MP_TAC PI_APPROX_4 THEN REAL_ARITH_TAC ] THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN ASM_SIMP_TAC[REAL_LT_LDIV_EQ] THEN REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ALL_TAC ] THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM THEN REMOVE_ASSUM THEN DISCH_TAC THEN DISCH_TAC THEN SUBGOAL_THEN `&2 - (&p * #1.9) / #3.1415 < &t` MP_TAC THENL [ MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&2 - (&p * #1.9) / pi` THEN ASM_REWRITE_TAC[REAL_ARITH `a - b <= a - c <=> c <= b`] THEN REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ARITH `&0 <= &p * #1.9`] THEN MATCH_MP_TAC REAL_LE_INV2 THEN MP_TAC PI_APPROX_4 THEN REAL_ARITH_TAC; ALL_TAC ] THEN REMOVE_ASSUM THEN DISCH_THEN (LABEL_TAC "A") THEN DISCH_THEN (LABEL_TAC "B") THEN DISJ_CASES_TAC (ARITH_RULE `7 < p \/ p < 8`) THENL [ ASM_MESON_TAC[NOT_LE]; ALL_TAC ] THEN POP_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[gen_NUM_CASES 8] th)) THEN POP_ASSUM MP_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th -> SUBST_ALL_TAC th) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REPEAT STRIP_TAC THENL [ SUBGOAL_THEN `2 < t /\ t < 6` ASSUME_TAC THENL [ REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ALL_TAC ] THEN ASM SET_TAC[ARITH_RULE `2 < t /\ t < 6 ==> t = 3 \/ t = 4 \/ t = 5`]; SUBGOAL_THEN `1 < t /\ t < 5` ASSUME_TAC THENL [ REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ALL_TAC ] THEN ASM SET_TAC[ARITH_RULE `1 < t /\ t < 5 ==> t = 2 \/ t = 3 \/ t = 4`]; SUBGOAL_THEN `0 < t /\ t < 4` ASSUME_TAC THENL [ REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ALL_TAC ] THEN ASM SET_TAC[ARITH_RULE `0 < t /\ t < 4 ==> t = 1 \/ t = 2 \/ t = 3`]; SUBGOAL_THEN `0 < t /\ t < 4` ASSUME_TAC THENL [ REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ALL_TAC ] THEN ASM SET_TAC[ARITH_RULE `0 < t /\ t < 4 ==> t = 1 \/ t = 2 \/ t = 3`]; SUBGOAL_THEN `t < 3` ASSUME_TAC THENL [ REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ALL_TAC ] THEN ASM SET_TAC[ARITH_RULE `t < 3 ==> t = 0 \/ t = 1 \/ t = 2`]; SUBGOAL_THEN `t < 2` ASSUME_TAC THENL [ REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ALL_TAC ] THEN ASM SET_TAC[ARITH_RULE `t < 2 ==> t = 0 \/ t = 1`]; SUBGOAL_THEN `t < 2` ASSUME_TAC THENL [ REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ALL_TAC ] THEN ASM SET_TAC[ARITH_RULE `t < 2 ==> t = 0 \/ t = 1`]; SUBGOAL_THEN `t < 1` ASSUME_TAC THENL [ REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ALL_TAC ] THEN ASM SET_TAC[ARITH_RULE `t < 1 ==> t = 0`] ]);;
(* CDTETAT (with assumptions) *)
let CDTETAT = 
prove(`kcblrqc_ineq_def ==> !V x. contravening V /\ x IN dart_of_fan (V,ESTD V) ==> (let (p,q,r) = type_of_node (hypermap_of_fan (V, ESTD V)) x in ((p,q+r) IN { (0,3), (0,4), (0,5), (1,2), (1,3), (1,4), (2,1), (2,2), (2,3), (3,1), (3,2), (3,3), (4,0), (4,1),(4,2), (5,0), (5,1), (6,0), (6,1), (7,0) }))`,
REPEAT STRIP_TAC THEN MP_TAC (ISPEC `V:real^3->bool` CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`hypermap_of_fan (V:real^3->bool,ESTD V)`; `x:real^3#real^3`] NODE_TYPE_lemma) THEN ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN; Jgtdebu.JGTDEBU4] THEN DISCH_THEN (fun th -> ALL_TAC) THEN CONV_TAC let_CONV THEN ABBREV_TAC `H = hypermap_of_fan (V,ESTD V)` THEN ABBREV_TAC `A = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 3}` THEN ABBREV_TAC `B = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 4}` THEN ABBREV_TAC `C = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 5}` THEN MATCH_MP_TAC CDTETAT_lemma1 THEN MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] SUM_AZIM_DART_FULLY_SURROUNDED) THEN MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] FULLY_SURROUNDED_NODE_DECOMPOSITION) THEN ASM_SIMP_TAC[CONTRAVENING_IMP_FULLY_SURROUNDED] THEN CONV_TAC (DEPTH_CONV let_CONV) THEN ASM_REWRITE_TAC[] THEN ABBREV_TAC `D = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 4}` THEN DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC) THEN STRIP_TAC THEN 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 [ REWRITE_TAC[REAL_OF_NUM_EQ] THEN MATCH_MP_TAC CARD_UNION_EQ THEN ASM_SIMP_TAC[GSYM DISJOINT]; ALL_TAC ] THEN FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (is_eq o concl)) THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN SUBGOAL_THEN `!y:real^3#real^3. y IN node H x ==> y IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL [ REWRITE_TAC[GSYM SUBSET] THEN MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] NODE_SUBSET_DART_OF_FAN) THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN 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 [ EXPAND_TAC "A" THEN GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN MP_TAC TRIANGULAR_FACE_AZIM_DART_BOUNDS THEN UNDISCH_TAC `kcblrqc_ineq_def` THEN SIMP_TAC[kcblrqc_ineq_def] THEN DISCH_THEN (fun th -> ALL_TAC) THEN DISCH_THEN (MP_TAC o SPECL [`V:real^3->bool`; `y:real^3#real^3`]) THEN ASM_SIMP_TAC[REAL_ARITH `a < #1.893 ==> a < #1.9`]; ALL_TAC ] THEN SUBGOAL_THEN `!y. y IN D ==> azim_dart (V,ESTD V) y < pi /\ #1.15 < azim_dart (V,ESTD V) y` ASSUME_TAC THENL [ EXPAND_TAC "D" THEN GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN MP_TAC (SPEC `V:real^3->bool` non_triangular_face_azim_dart_bound) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (MP_TAC o SPEC `y:real^3#real^3`) THEN ASM_SIMP_TAC[ARITH_RULE `3 < a <=> a >= 4`] THEN MP_TAC (SPECL [`V:real^3->bool`] CONTRAVENING_IMP_FULLY_SURROUNDED) THEN ASM_REWRITE_TAC[fully_surrounded] THEN DISCH_THEN (MP_TAC o SPEC `y:real^3#real^3`) THEN ASM_SIMP_TAC[]; ALL_TAC ] THEN DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_ADD2 THEN ONCE_REWRITE_TAC[GSYM REAL_LE_NEG] THEN GEN_REWRITE_TAC (PAT_CONV `(\f. --sum A f <= x /\ --sum D f <= y)`) [GSYM ETA_AX] THEN REWRITE_TAC[GSYM SUM_NEG] THEN REWRITE_TAC[REAL_NEG_RMUL] THEN CONJ_TAC THEN MATCH_MP_TAC SUM_BOUND THEN ASM_SIMP_TAC[REAL_LE_NEG; REAL_LT_IMP_LE]; SUBGOAL_THEN `x:real^3#real^3 IN A \/ x IN D` MP_TAC THENL [ REWRITE_TAC[GSYM IN_UNION] THEN FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN REWRITE_TAC[Hypermap.node_refl]; ALL_TAC ] THEN STRIP_TAC THENL [ MATCH_MP_TAC REAL_LTE_ADD2 THEN CONJ_TAC THENL [ MATCH_MP_TAC SUM_BOUND_LT THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN EXISTS_TAC `x:real^3#real^3` THEN ASM_SIMP_TAC[]; MATCH_MP_TAC SUM_BOUND THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] ]; ALL_TAC ] THEN MATCH_MP_TAC REAL_LET_ADD2 THEN CONJ_TAC THENL [ MATCH_MP_TAC SUM_BOUND THEN ASM_SIMP_TAC[REAL_LT_IMP_LE]; MATCH_MP_TAC SUM_BOUND_LT THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN EXISTS_TAC `x:real^3#real^3` THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[] ] ]);;
(* SZIPOAS *)
let SZIPOAS = 
prove(`kcblrqc_ineq_def ==> !V. contravening V ==> tame_11b (hypermap_of_fan (V, ESTD V))`,
REPEAT STRIP_TAC THEN REWRITE_TAC[tame_11b] THEN MP_TAC (ISPEC `V:real^3->bool` CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN GEN_TAC THEN ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN DISCH_TAC THEN 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 ASM_SIMP_TAC[CONTRAVENING_IMP_FULLY_SURROUNDED; Jgtdebu.JGTDEBU4] THEN FIRST_X_ASSUM (MP_TAC o SPECL [`V:real^3->bool`; `x:real^3#real^3`] o MATCH_MP CDTETAT) THEN ASM_REWRITE_TAC[type_of_node] THEN CONV_TAC (DEPTH_CONV let_CONV) THEN ABBREV_TAC `H = hypermap_of_fan (V,ESTD(V))` THEN ABBREV_TAC `p = CARD (set_of_triangles_meeting_node H (x:real^3#real^3))` THEN ABBREV_TAC `q = CARD (set_of_quadrilaterals_meeting_node H (x:real^3#real^3))` THEN ABBREV_TAC `r = CARD (set_of_exceptional_meeting_node H (x:real^3#real^3))` THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; PAIR_EQ] THEN ARITH_TAC);;
end;;