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



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


module Fektyiy = 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;;
open Odxlstcv2;;

open Yxionxl2;;
open Eyypqdw;;
open Ocbicby;;
open Imjxphr;;

open Nuxcoea;;


let FEKTYIY_concl = `!s v.
  is_scs_v39 s /\ v IN MMs_v39 s /\ 3 < scs_k_v39 s  ==>
  ~coplanar ({vec 0} UNION IMAGE v (:num))`;;

let FEKTYIY= prove_by_refinement((FEKTYIY_concl),
[
REWRITE_TAC[Trigonometry2.coplanar1;IN]
THEN REPEAT STRIP_TAC
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
THEN ABBREV_TAC`v0= (v:num->real^3) 0`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`0`;`v`]
THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k:num`]
THEN SUBGOAL_THEN`{ITER n (rho_node1 FF) v0 | n <= k+1} = V`ASSUME_TAC;

MRESA_TAC Localization.LOFA_IMP_LT_CARD_SET_V_ALT[`V`;`E`;`FF`;`v0:real^3`]
THEN MATCH_MP_TAC(GEN_ALL(SET_RULE`A SUBSET B/\ B SUBSET C/\ A=C==> B=C`))
THEN TYPIFY `{ITER n (rho_node1 FF) v0 | n < CARD V}` EXISTS_TAC
THEN STRIP_TAC;

ASM_REWRITE_TAC[]
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;]
THEN REPEAT RESA_TAC
THEN TYPIFY `n` EXISTS_TAC
THEN DICH_TAC 1
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN EXPAND_TAC"V"
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IMAGE;SET_RULE`(a:A) IN(:A)`]
THEN REPEAT RESA_TAC
THEN TYPIFY `n` EXISTS_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)`)
THEN RESA_TAC
THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v0`;`v`;` 0`][ARITH_RULE`a+0=a`];

POP_ASSUM MP_TAC
THEN MRESAL_TAC Nuxcoea.MMS_IMP_BBPRIME[`s:scs_v39`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
THEN MP_TAC (SET_RULE`{vec 0:real^3} UNION V SUBSET x ==> vec 0 IN x /\V SUBSET x`)
THEN RESA_TAC
THEN STRIP_TAC
THEN MRESA_TAC Lunar_deform.AZIM_PI_ITER_LOCAL_FAN[`E`;`V`;`V`;`x`;`k+1`;`FF`;`v0:real^3`]
THEN MRESA_TAC JKQEWGV1[`s:scs_v39`;`v`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`~(a< b)<=> b<=a`;sol_local]
THEN MATCH_MP_TAC (REAL_ARITH`&0< a/\ b= &0==> a<= &2 *a +b`)
THEN REWRITE_TAC[PI_WORKS]
THEN MATCH_MP_TAC SUM_EQ_0
THEN GEN_TAC
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA[`V:real^3->bool`;`FF`;`E`;`x'`]
THEN MRESA_TAC Local_lemmas.DETER_RHO_NODE[`V:real^3->bool`;`E`;`FF`;`FST x'`;`SND x'`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IMP_IN_V2[`E`;`FF`;`x'`;`V`]
THEN MRESA_TAC Local_lemmas1.LF_AZIM_CYCLE_EQ_IVS_ND[`V`;`E`;`FF`;`FST x'`]
THEN DICH_TAC (27-22)
THEN EXPAND_TAC "FF"
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[IMAGE;IN_ELIM_THM]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)/\ (k+1)-1=k/\ ~(k=0)/\ 1<k/\ SUC (x'' + k - 1) =1 * k + x''`)
THEN RESA_TAC
THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v0`;`v`;` 0`][ARITH_RULE`a+0=a`]
THEN DICH_TAC (34-21)
THEN MRESA_TAC DIVISION[`x''+k-1`;`k`]
THEN RESA_TAC
THEN THAYTHEL_TAC 0 [`(x''+k-1) MOD k`][ARITH_RULE`a+1= SUC a/\ a+2= SUC (SUC a)`]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC Yxionxl2.MOD_SUC_MOD[`x''+k-1`;`k`]
THEN MRESA_TAC MOD_REFL[`x'' `;`k`]
THEN MRESA_TAC MOD_MULT_ADD[`1`;`k`;`x''`]
THEN MRESA_TAC
CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC ((x'' + k - 1) MOD k)`;`v:num->real^3`;`SUC ((x'' + k - 1) MOD k) MOD k`]
THEN MRESA_TAC
CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`x'' MOD k`;`v:num->real^3`;`x''`]
THEN MRESA_TAC Yxionxl2.MOD_SUC_MOD[`x''`;`k`]
THEN MRESA_TAC Yxionxl2.MOD_SUC_MOD[`SUC((x''+k-1) MOD k)`;`k`]
THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN MRESA_TAC MOD_REFL[`SUC x'' `;`k`]
THEN MRESA_TAC MOD_REFL[`x''+k-1 `;`k`]
THEN MRESA_TAC
CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC (SUC ((x'' + k - 1) MOD k))`;`v:num->real^3`;`SUC(SUC ((x'' + k - 1) MOD k)) MOD k`]
THEN MRESA_TAC
CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC x'' MOD k`;`v:num->real^3`;`SUC x''`]
THEN MRESA_TAC
CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(x''+k-1) MOD k`;`v:num->real^3`;`x''+k-1`]
THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v x''`;`v`;` x''`][ARITH_RULE`a+0=a`]
THEN MRESA_TAC WL_IN_V[`x''`;`v`]
THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
THEN RESA_TAC
THEN THAYTHE_TAC 0[`v x''`]
THEN REWRITE_TAC[ARITH_RULE`a+k-1=k-1+a`]
THEN SYM_ASSUM_TAC
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0< pi==> ~(pi= &0)`)
THEN ASM_REWRITE_TAC[PI_WORKS]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[Rogers.AZIM_COMPL_EXT]
THEN REAL_ARITH_TAC]);;



 end;;


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