(* ========================================================================== *)
(* 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;;