(* ========================================================================== *) (* 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)`, ASM_REWRITE_TAC[MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;scs_half_slice_v39;is_scs_v39;scs_diag;scs_v39_explicit;unadorned_v39] );; 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) *)