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


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


module Sgtrnaf = 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;;



let UXCKFPE2=
prove_by_refinement(
` !s vv. is_scs_v39 s /\ vv IN BBs_v39 s
/\  taustar_v39 s vv < &0
 ==> ~(BBprime2_v39 s = {})`,

  (* {{{ proof *)
[
REPEAT GEN_TAC
THEN  STRIP_TAC
THEN MRESA_TAC UXCKFPE[`s:scs_v39`;`vv:num->real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?vv1. vv1 IN A`;BBprime2_v39;IN;BBindex_min_v39;]
THEN STRIP_TAC
THEN SUBGOAL_THEN`?n. (?vv1. BBprime_v39 s vv1 /\
     BBindex_v39 s vv1=n)` ASSUME_TAC;

EXISTS_TAC`BBindex_v39 s vv1`
THEN EXISTS_TAC`vv1:num->real^3`
THEN ASM_REWRITE_TAC[];

POP_ASSUM MP_TAC
THEN REWRITE_TAC[MINIMAL]
THEN STRIP_TAC
THEN EXISTS_TAC`vv1':num->real^3`
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th] THEN ASSUME_TAC (SYM th))
THEN ASM_REWRITE_TAC[Misc_defs_and_lemmas.min_num;ARITH_RULE`(A=B:num)<=> (B=A)`]
THEN STRIP_TAC
THEN MATCH_MP_TAC SELECT_UNIQUE
THEN ASM_REWRITE_TAC[BETA_THM;IMAGE;IN_ELIM_THM;]
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN EQ_TAC;

STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`(?x. BBprime_v39 s x /\ BBindex_v39 s vv1' = BBindex_v39 s x)`ASSUME_TAC;

EXISTS_TAC`vv1':num->real^3`
THEN ASM_REWRITE_TAC[];

STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`BBindex_v39 s vv1'`)
THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <= BBindex_v39 s vv1' ==>
BBindex_v39 s x < BBindex_v39 s vv1' \/ BBindex_v39 s x = BBindex_v39 s vv1'`)
THEN RESA_TAC
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN 
MRESA1_TAC th` BBindex_v39 s x`)
THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC;

EXISTS_TAC`x:num->real^3`
THEN ASM_REWRITE_TAC[];

POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[];

STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;



EXISTS_TAC`vv1':num->real^3`
THEN ASM_REWRITE_TAC[];


REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <BBindex_v39 s vv1'   \/ BBindex_v39 s vv1' <= BBindex_v39 s x`)
THEN RESA_TAC;



REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN 
MRESA1_TAC th` BBindex_v39 s x`)
THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC;

EXISTS_TAC`x:num->real^3`
THEN ASM_REWRITE_TAC[];


POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[];
]);;
  (* }}} *)




let SGTRNAF =
prove(
`!s vv. is_scs_v39 s/\ unadorned_v39 s /\ vv IN BBs_v39 s /\
  taustar_v39 s vv < &0
 ==> ~(MMs_v39 s = {})`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC unadorned_MMs
THEN RESA_TAC
THEN MATCH_MP_TAC UXCKFPE2
THEN EXISTS_TAC`vv:num->real^3`
THEN ASM_REWRITE_TAC[]);;



 end;;


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