(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Tame Hypermap                                                     *)
(* Author: Alexey Solovyev                                                    *)
(* Date: 2010-06-17                                                           *)
(* Note: use Tame_lemmas.sum_tauVEF_upper_bound because the theorem below     *)
(*       has unproved assumptions                                             *)
(* ========================================================================== *)

(* Proof of HRXEFDM *)

flyspeck_needs "tame/TameGeneral.hl";;


module Hrxefdm_tame = struct


open Hypermap;;
open Fan_defs;;
open Tame_defs;;
open Tame_general;;
open Hypermap_and_fan;;


let tauVEF_alt1 = 
prove(`!V E f. conforming (V,E) /\ f IN face_set_of_fan (V,E) ==> tauVEF (V,E,f) = sol (vec 0) (dartset_leads_into (vec 0,V,E) f) + (&2 - &(CARD f)) * sol0 - sol0 / pi * sum f (\x. azim_dart (V,E) x * (lmfun (h_dart x) - &1))`,
REWRITE_TAC[face_set_of_fan; conforming; conforming_solid_angle] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC `f:real^3#real^3->bool`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (MP_TAC o let_RULE) THEN DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC) THEN DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC) THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN REWRITE_TAC[tauVEF] THEN REWRITE_TAC[REAL_ARITH `a * (&1 + b * (&1 - c)) = a - b * (a * (c - &1))`] THEN SUBGOAL_THEN `FINITE (f:real^3#real^3->bool)` ASSUME_TAC THENL [ POP_ASSUM MP_TAC THEN REWRITE_TAC[face_set; set_of_orbits; GSYM face] THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[FACE_FINITE]; ALL_TAC ] THEN ASM_SIMP_TAC[SUM_SUB; SUM_LMUL; SUM_CONST] THEN REAL_ARITH_TAC);;
let tauVEF_alt2 = 
prove(`!V E f. conforming (V,E) /\ f IN face_set_of_fan (V,E) ==> tauVEF (V,E,f) = sol (vec 0) (dartset_leads_into (vec 0,V,E) f) * (&1 + sol0 / pi) - sol0 / pi * sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))`,
REPEAT STRIP_TAC THEN ASM_SIMP_TAC[tauVEF_alt1] THEN REPEAT (POP_ASSUM MP_TAC) THEN REWRITE_TAC[conforming; conforming_solid_angle; face_set_of_fan] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC `f:real^3#real^3->bool`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[let_RULE th]) THEN SUBGOAL_THEN `FINITE (f:real^3#real^3->bool)` ASSUME_TAC THENL [ POP_ASSUM MP_TAC THEN REWRITE_TAC[face_set; set_of_orbits; GSYM face] THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[FACE_FINITE]; ALL_TAC ] THEN REWRITE_TAC[REAL_ARITH `a * (b - &1) = a * b - a`] THEN ASM_SIMP_TAC[SUM_SUB; SUM_CONST] THEN MP_TAC PI_POS THEN CONV_TAC REAL_FIELD);;
let CHOICE_CONST_LEMMA = 
prove(`!f s. (!x y. x IN s /\ y IN s ==> f x = f y) ==> (!x. x IN s ==> f x = f (CHOICE s))`,
MESON_TAC[CHOICE]);;
let scriptL_lemma = 
prove(`!V E. FAN (vec 0,V,E) ==> scriptL V = sum (node_set (hypermap_of_fan (V,E))) (\n. lmfun (h_dart (CHOICE n)))`,
REPEAT STRIP_TAC THEN REWRITE_TAC[scriptL] THEN MP_TAC (SPEC_ALL NODE_SET_AS_IMAGE) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `(\v:real^3. lmfun (norm v / &2)) = (\n. lmfun (h_dart (CHOICE n))) o (f:real^3->(real^3#real^3->bool))` MP_TAC THENL [ ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; h_dart]; ALL_TAC ] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN MATCH_MP_TAC (GSYM SUM_IMAGE) THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM (MP_TAC o SPECL [`x:real^3`; `y:real^3`]) THEN ASM_SIMP_TAC[]);;
let HRXEFDM_lemma1 = 
prove(`!V E. FAN (vec 0,V,E) ==> sum (face_set_of_fan (V,E)) (\f. sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))) = &2 * pi * scriptL V`,
REPEAT STRIP_TAC THEN SUBGOAL_THEN `!n. n IN node_set (hypermap_of_fan (V,E)) ==> sum n (azim_dart (V,E)) = &2 * pi` ASSUME_TAC THENL [ GEN_TAC THEN REWRITE_TAC[node_set; set_of_orbits; GSYM node] THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_SIMP_TAC[dart; HYPERMAP_OF_FAN] THEN STRIP_TAC THEN MP_TAC (SPEC_ALL SUM_AZIM_DART) THEN ASM_SIMP_TAC[]; ALL_TAC ] THEN REWRITE_TAC[face_set_of_fan; DART_SUM_lemma] THEN REWRITE_TAC[GSYM (SPEC_ALL DART_SUM_lemma)] THEN ABBREV_TAC `g = (\n. sum n (\x. azim_dart (V,E) x * lmfun (h_dart x)))` THEN MP_TAC (ISPECL [`g:(real^3#real^3->bool)->real`; `node_set (hypermap_of_fan (V,E))`] SUM_RESTRICT) THEN REWRITE_TAC[FINITE_HYPERMAP_ORBITS] THEN DISCH_TAC THEN SUBGOAL_THEN `!n. n IN node_set (hypermap_of_fan (V,E)) ==> g n = &2 * pi * lmfun (h_dart (CHOICE n))` MP_TAC THENL [ REMOVE_ASSUM THEN GEN_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN FIRST_ASSUM (fun th -> FIRST_X_ASSUM (ASSUME_TAC o (fun th2 -> MATCH_MP th2 th))) THEN MP_TAC (ISPECL [`(\x. azim_dart (V,E) x * lmfun (h_dart x))`; `n:real^3#real^3->bool`] SUM_RESTRICT) THEN SUBGOAL_THEN `FINITE (n:real^3#real^3->bool)` ASSUME_TAC THENL [ REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[node_set; set_of_orbits; GSYM node] THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[NODE_FINITE]; ALL_TAC ] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ABBREV_TAC `c = lmfun (h_dart (CHOICE (n:real^3#real^3->bool)))` THEN SUBGOAL_THEN `!x. (if x IN n then azim_dart (V,E) x * lmfun (h_dart x) else &0) = (if x IN n then azim_dart (V,E) x * c else &0)` MP_TAC THENL [ GEN_TAC THEN ASM_CASES_TAC `x:real^3#real^3 IN n` THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `h_dart (x:real^3#real^3) = h_dart (CHOICE (n:real^3#real^3->bool))` (fun th -> ASM_REWRITE_TAC[th]) THEN MP_TAC (ISPECL [`h_dart:real^3#real^3->real`; `n:real^3#real^3->bool`] CHOICE_CONST_LEMMA) THEN ANTS_TAC THENL [ REPEAT STRIP_TAC THEN REWRITE_TAC[h_dart] THEN AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN MP_TAC (SPEC_ALL FST_NODE_lemma) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN REMOVE_ASSUM THEN DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN MP_TAC (ISPECL [`(\x. azim_dart (V,E) x * c)`; `n:real^3#real^3->bool`] SUM_RESTRICT) THEN ASM_SIMP_TAC[SUM_RMUL; ETA_AX] THEN REWRITE_TAC[REAL_MUL_ASSOC]; ALL_TAC ] THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN SUBGOAL_THEN `!x. (if x IN node_set (hypermap_of_fan (V,E)) then g x else &0) = (if x IN node_set (hypermap_of_fan (V,E)) then &2 * pi * lmfun (h_dart (CHOICE x)) else &0)` MP_TAC THENL [ GEN_TAC THEN ASM_CASES_TAC `x IN node_set (hypermap_of_fan (V,E))` THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[]; ALL_TAC ] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN MP_TAC (ISPECL [`(\x:real^3#real^3->bool. &2 * pi * lmfun (h_dart (CHOICE x)))`; `node_set (hypermap_of_fan (V,E))`] SUM_RESTRICT) THEN REWRITE_TAC[FINITE_HYPERMAP_ORBITS] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN REWRITE_TAC[SUM_LMUL] THEN ASM_SIMP_TAC[scriptL_lemma]);;
let solid_angle_sum_assumption = `!V E. sum (face_set_of_fan (V,E)) (\f. sol (vec 0) (dartset_leads_into (vec 0,V,E) f) ) = &4 * pi`;; let HRXEFDM_concl = `!V. contravening V ==> ( sum (face_set_of_fan (V,ESTD V)) (\ f. tauVEF (V,ESTD V,f) ) < &4 * pi - &20 * sol0 )`;; let HRXEFDM_concl2 = mk_imp (list_mk_conj [`!V. contravening V ==> conforming (V,ESTD V)`; solid_angle_sum_assumption], HRXEFDM_concl);; (* g (HRXEFDM_concl2);; *)
let HRXEFDM = prove(HRXEFDM_concl2,
  REPEAT STRIP_TAC THEN
    REPEAT (FIRST_X_ASSUM (ASSUME_TAC o SPEC `V:real^3->bool`)) THEN
    POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
    MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
    FIRST_X_ASSUM (ASSUME_TAC o SPEC `ESTD V`) THEN

    SUBGOAL_THEN `FINITE (face_set_of_fan (V,ESTD V))` ASSUME_TAC THENL
    [
      REWRITE_TAC[face_set_of_fan; FINITE_HYPERMAP_ORBITS];
      ALL_TAC
    ] THEN

    SUBGOAL_THEN `sum (face_set_of_fan (V,ESTD V)) (\f. tauVEF (V,ESTD V,f)) = &4 * pi * (&1 + sol0 / pi) - sol0 / pi * &2 * pi * scriptL V` ASSUME_TAC THENL
    [
      MP_TAC (ISPECL [`\f. tauVEF (V,ESTD V,f)`; `face_set_of_fan (V,ESTD V)`] SUM_RESTRICT) THEN
        ASM_REWRITE_TAC[] THEN
        DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
        ABBREV_TAC `g = (\f. sol (vec 0) (dartset_leads_into (vec 0,V,ESTD V) f)  * (&1 + sol0 / pi) - sol0 / pi * sum f (\x. azim_dart (V,ESTD V) x * lmfun (h_dart x)))` THEN

        SUBGOAL_THEN `!x. (if x IN face_set_of_fan (V,ESTD V) then tauVEF (V,ESTD V,x) else &0) = (if x IN face_set_of_fan (V,ESTD V) then g x else &0)` (fun th -> REWRITE_TAC[th]) THENL
        [
          X_GEN_TAC `f:real^3#real^3->bool` THEN
            ASM_CASES_TAC `f IN face_set_of_fan (V,ESTD V)` THEN ASM_REWRITE_TAC[] THEN
            EXPAND_TAC "g" THEN
              MATCH_MP_TAC tauVEF_alt2 THEN
            ASM_REWRITE_TAC[];
          ALL_TAC
        ] THEN

        MP_TAC (ISPECL [`(\x. g x):(real^3#real^3->bool)->real`; `face_set_of_fan (V,ESTD V)`] SUM_RESTRICT) THEN
        ASM_REWRITE_TAC[] THEN
        DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
        POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN

        ASM_SIMP_TAC[SUM_SUB; SUM_RMUL; SUM_LMUL] THEN
        ASM_SIMP_TAC[HRXEFDM_lemma1] THEN
        REAL_ARITH_TAC;
      ALL_TAC
    ] THEN

    POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
    ASSUME_TAC PI_POS THEN

    ASM_SIMP_TAC[REAL_FIELD `&0 < pi ==> &4 * pi * (&1 + sol0 / pi) = &4 * pi + &4 * sol0`] THEN
    ASM_SIMP_TAC[REAL_FIELD `&0 < pi ==> sol0 / pi * &2 * pi * a = &2 * a * sol0`] THEN
    REWRITE_TAC[REAL_ARITH `(&4 * pi + &4 * a) - (&2 * b * a) = (&4 * pi - &20 * a) + &2 * a * (&12 - b)`] THEN
    REWRITE_TAC[REAL_ARITH `a + b < a <=> b < &0`] THEN
    ONCE_REWRITE_TAC[REAL_ARITH `&0 = (&2 * sol0) * &0`] THEN
    REWRITE_TAC[REAL_MUL_ASSOC] THEN
    MATCH_MP_TAC REAL_LT_LMUL THEN
    CONJ_TAC THENL
    [
      MATCH_MP_TAC REAL_LT_MUL THEN
        REWRITE_TAC[REAL_ARITH `&0 < &2`; sol0_POS];
      ALL_TAC
    ] THEN

    REWRITE_TAC[REAL_ARITH `a - b < &0 <=> b > a`] THEN
    FIRST_X_ASSUM (MP_TAC o check (fun th -> rator (concl th) = `contravening`)) THEN
    SIMP_TAC[contravening]);;
end;;