(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)


(*
remaining conclusions from appendix to Local Fan chapter
*)


module Lkgrqui = struct



open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas1;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;





open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;


open Uxckfpe;;
open Sgtrnaf;;

open Yxionxl;;
open Qknvmlb;;



let SLICE_IS_UNADORNED=
prove(`unadorned_v39 (scs_half_slice_v39 s p q d' mkj)`,



let LKGRQUI= 
prove_by_refinement(
`	is_scs_v39 s /\ scs_diag (scs_k_v39 s) p q /\
	  is_scs_slice_v39 s s' s'' p q 
	 ==> scs_arrow_v39 {s} {s',s''}`,

[REWRITE_TAC[scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;PAIR_EQ]
THEN REPEAT STRIP_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/a=c`]
THEN RESA_TAC;

MP_TAC SCS_HALF_SLICE_IS_A_SCS
THEN RESA_TAC;

MP_TAC SCS_SLICE_SYM
THEN RESA_TAC;

MRESA_TAC (GEN_ALL SCS_HALF_SLICE_IS_A_SCS)[`s:scs_v39`;`s':scs_v39`;`q:num`;`p:num`;`s'':scs_v39`]
THEN ASM_TAC
THEN REWRITE_TAC[scs_diag]
THEN REPEAT RESA_TAC;

DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`);

ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[SET_RULE`~(A={})<=> ?vv. A vv`;]
THEN RESA_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th
THEN ASSUME_TAC th)
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF]
THEN ABBREV_TAC`mkj=scs_J_v39 s' 0 (scs_k_v39 s' - 1)`
THEN ABBREV_TAC`d'=scs_d_v39 s'`
THEN ABBREV_TAC`d''=scs_d_v39 s''`
THEN REWRITE_TAC[scs_slice_v39;PAIR_EQ]
THEN DISCH_TAC 
THEN ABBREV_TAC`vv'  = (\i. (vv:num->real^3) (i MOD (scs_k_v39 s')+ p MOD (scs_k_v39 s)))`
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN MP_TAC QKNVMLB1
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF]
THEN STRIP_TAC
THEN SUBGOAL_THEN`scs_bm_v39 s q p < &4 /\
      (scs_k_v39 s = 4 \/ scs_bm_v39 s q p <= cstab) /\
      scs_diag (scs_k_v39 s) q p` ASSUME_TAC;

ASM_TAC
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;scs_diag;is_scs_v39]
THEN REPEAT RESA_TAC;

MRESAL_TAC (GEN_ALL QKNVMLB1)[`vv:num->real^3`;`s:scs_v39`;`q:num`;`p:num`;`d'':real`;`mkj:bool`]
[LET_DEF;LET_END_DEF]
THEN ABBREV_TAC`vv''=(\i. (vv:num->real^3)
           (i MOD scs_k_v39 (scs_half_slice_v39 s q p d'' mkj) +
            q MOD scs_k_v39 s))`
THEN MP_TAC QKNVMLB3
THEN RESA_TAC
THEN REPLICATE_TAC (14-3)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th
THEN ASSUME_TAC th)
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[MMs_v39;BBprime_v39;BBprime2_v39;LET_DEF;LET_END_DEF]
THEN REWRITE_TAC[BBprime_v39;BBprime2_v39]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`taustar_v39 (scs_half_slice_v39 s p q d' mkj) vv' +
      taustar_v39 (scs_half_slice_v39 s q p d'' mkj) vv'' <=
      taustar_v39 s vv
/\ taustar_v39 s vv< &0
==> taustar_v39 (scs_half_slice_v39 s p q d' mkj) vv' < &0 \/ taustar_v39 (scs_half_slice_v39 s q p d'' mkj) vv''< &0`)
THEN RESA_TAC;


EXISTS_TAC`s':scs_v39`
THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`;]
THEN MATCH_MP_TAC SGTRNAF
THEN EXISTS_TAC`vv':num->real^3`
THEN ASM_REWRITE_TAC[IN]
THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SLICE_IS_UNADORNED];


EXISTS_TAC`s'':scs_v39`
THEN ASM_REWRITE_TAC[SET_RULE`b IN {a,b}`;]
THEN MATCH_MP_TAC SGTRNAF
THEN EXISTS_TAC`vv'':num->real^3`
THEN ASM_REWRITE_TAC[IN]
THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SLICE_IS_UNADORNED]
THEN MP_TAC SCS_SLICE_SYM
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL SCS_HALF_SLICE_IS_A_SCS)[`s:scs_v39`;`s':scs_v39`;`q:num`;`p:num`;`s'':scs_v39`];



EXISTS_TAC`s':scs_v39`
THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`;]
THEN MATCH_MP_TAC SGTRNAF
THEN EXISTS_TAC`vv':num->real^3`
THEN ASM_REWRITE_TAC[IN]
THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SLICE_IS_UNADORNED];

EXISTS_TAC`s'':scs_v39`
THEN ASM_REWRITE_TAC[SET_RULE`b IN {a,b}`;]
THEN MATCH_MP_TAC SGTRNAF
THEN EXISTS_TAC`vv'':num->real^3`
THEN ASM_REWRITE_TAC[IN]
THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SLICE_IS_UNADORNED]
THEN MP_TAC SCS_SLICE_SYM
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL SCS_HALF_SLICE_IS_A_SCS)[`s:scs_v39`;`s':scs_v39`;`q:num`;`p:num`;`s'':scs_v39`];

EXISTS_TAC`s':scs_v39`
THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`;]
THEN MATCH_MP_TAC SGTRNAF
THEN EXISTS_TAC`vv':num->real^3`
THEN ASM_REWRITE_TAC[IN]
THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SLICE_IS_UNADORNED];

EXISTS_TAC`s'':scs_v39`
THEN ASM_REWRITE_TAC[SET_RULE`b IN {a,b}`;]
THEN MATCH_MP_TAC SGTRNAF
THEN EXISTS_TAC`vv'':num->real^3`
THEN ASM_REWRITE_TAC[IN]
THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SLICE_IS_UNADORNED]
THEN MP_TAC SCS_SLICE_SYM
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL SCS_HALF_SLICE_IS_A_SCS)[`s:scs_v39`;`s':scs_v39`;`q:num`;`p:num`;`s'':scs_v39`]
;

EXISTS_TAC`s':scs_v39`
THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`;]
THEN MATCH_MP_TAC SGTRNAF
THEN EXISTS_TAC`vv':num->real^3`
THEN ASM_REWRITE_TAC[IN]
THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SLICE_IS_UNADORNED];

EXISTS_TAC`s'':scs_v39`
THEN ASM_REWRITE_TAC[SET_RULE`b IN {a,b}`;]
THEN MATCH_MP_TAC SGTRNAF
THEN EXISTS_TAC`vv'':num->real^3`
THEN ASM_REWRITE_TAC[IN]
THEN MP_TAC SCS_HALF_SLICE_IS_A_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SLICE_IS_UNADORNED]
THEN MP_TAC SCS_SLICE_SYM
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL SCS_HALF_SLICE_IS_A_SCS)[`s:scs_v39`;`s':scs_v39`;`q:num`;`p:num`;`s'':scs_v39`]
]);;



 end;;


(*
let check_completeness_claimA_concl = 
  Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) 
*)