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


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


module Cqaoqlr = 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;;
open Aursipd;;
open Cuxvzoz;;
open Rrcwnsj;;
open Tfitskc;;



let K_SUC_2_MOD_SUB=prove(`1<k ==> (k - SUC ((i + 2) MOD k) + 1) MOD k= (k- SUC((i+1) MOD k)) MOD k`,
SIMP_TAC[GSYM ADD1;]
THEN STRIP_TAC
THEN ASM_SIMP_TAC [SUC_MOD_EQ_MOD_SUC;ARITH_RULE`1<k ==> SUC (k - SUC ((i + 2) MOD k)) = k- (i+2) MOD k`;ARITH_RULE`i+2=SUC(SUC i)`]);;

let K_SUC_2_MOD_SUB_ID=prove(`1<k ==> (k - SUC ((i + 2) MOD k) + 2) MOD k= (k- SUC((i) MOD k)) MOD k`,
SIMP_TAC[GSYM ADD1;]
THEN STRIP_TAC
THEN ASM_SIMP_TAC [SUC_MOD_EQ_MOD_SUC;ARITH_RULE`1<k ==> SUC (k - SUC ((i + 2) MOD k)) = k- (i+2) MOD k`;ARITH_RULE`i+2=SUC(SUC i)`
]
THEN MRESA_TAC SUC_MOD_EQ_MOD_SUC[`SUC i`;`k`]
THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i) MOD k`;`k`]
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i MOD k)`;`k`]
THEN ASM_SIMP_TAC[ARITH_RULE`1<k==>SUC (k - SUC (SUC i MOD k))=k - SUC i MOD k`]
);;

let A_B_J_SCS_OPP=prove(`scs_a_v39 (scs_opp_v39 s) i j = scs_a_v39 s (scs_k_v39 s- SUC(i MOD scs_k_v39 s)) (scs_k_v39 s- SUC(j MOD scs_k_v39 s))
/\ scs_b_v39 (scs_opp_v39 s) i j = scs_b_v39 s (scs_k_v39 s- SUC(i MOD scs_k_v39 s)) (scs_k_v39 s- SUC(j MOD scs_k_v39 s))
/\ scs_J_v39 (scs_opp_v39 s) i j = scs_J_v39 s (scs_k_v39 s- SUC(i MOD scs_k_v39 s)) (scs_k_v39 s- SUC(j MOD scs_k_v39 s))`,
REWRITE_TAC[scs_opp_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;peropp2]);;

let SUC_OPP_ID=prove(`1<k ==> SUC (k - SUC i MOD k) MOD k= (k- i MOD k) MOD k`,
STRIP_TAC
THEN MRESA_TAC SUC_MOD_EQ_MOD_SUC[`(i)`;`k`]
THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (i) MOD k`;`k`]
THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC ( i) MOD k)`;`k`]
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (i MOD k)`;`k`]
THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC (i MOD k))`;`k`]
THEN ASM_SIMP_TAC[ARITH_RULE`1<k==>SUC (k - SUC (i MOD k))=k - i MOD k`]);;




let K_SUC_2_MOD_F_SUB_ID=prove(`1<k ==> (k - SUC ((i + 2) MOD k) + 3) MOD k= (k- SUC((i+k-1) MOD k)) MOD k`,
SIMP_TAC[GSYM ADD1;]
THEN STRIP_TAC
THEN ASM_SIMP_TAC [SUC_MOD_EQ_MOD_SUC;ARITH_RULE`1<k ==> SUC (k - SUC ((i + 2) MOD k)) = k- (i+2) MOD k`;ARITH_RULE`i+2=SUC(SUC i)/\ i+3=SUC(i+2)`
]
THEN MRESA_TAC SUC_MOD_EQ_MOD_SUC[`(SUC i)`;`k`]
THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i) MOD k`;`k`]
THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC (SUC i) MOD k)`;`k`]
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i MOD k)`;`k`]
THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC (SUC i MOD k))`;`k`]
THEN ASM_SIMP_TAC[ARITH_RULE`1<k==>SUC (k - SUC (SUC i MOD k))=k - SUC i MOD k/\ SUC (i + k - 1)= 1*k+i`;SUC_OPP_ID;MOD_MULT_ADD]);;

let ELEMENT1_SYM_0=prove(`{--a}= IMAGE (\x:real^N. --x) {a}`,
REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION;IN_SING;SET_RULE`a IN{b,c} <=> a=b\/ a=c`]
THEN GEN_TAC
THEN EQ_TAC
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
THEN SET_TAC[]);;

let SCS_GENERIC_SYM_0=prove(`BBs_v39 s v/\ is_scs_v39 s/\ scs_generic v 
==> scs_generic (\i. --v (scs_k_v39 s - SUC (i MOD scs_k_v39 s)))`,
REWRITE_TAC[scs_generic;BBs_v39;is_scs_v39;LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_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 MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_E_EQ_NEG;]
THEN ASM_TAC
THEN REWRITE_TAC[generic]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC IN_SYM_0[`u`;`IMAGE (\i. --(v:num->real^3) i) (:num)`][IMAGE_V_SYM_0;REFL_SYM_0]
THEN MRESAL_TAC IMAGE_E_SYM_0[`{v',w}`;`v:num->real^3`][GSYM ELEMENT2_SYM_0]
THEN THAYTHES_TAC (33-24)[`-- v':real^3`;`-- w:real^3`;`-- u:real^3`][ ELEMENT2_SYM_0;AFF_GE_VEC0_SYM_0;AFF_LT_VEC0_SYM_0;ELEMENT1_SYM_0;GSYM INTER_SYM_0]
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC SET_EQ_SYM_0[`IMAGE (\x:real^3. --x) (aff_ge {vec 0:real^3} {v', w} INTER aff_lt {vec 0} {u})`;`{}:real^3->bool`][REFL_SYM_0;IMAGE_CLAUSES]);;

let UNADORNED_OPP=prove(`is_scs_v39 s /\ unadorned_v39 s
==> unadorned_v39 (scs_opp_v39 s)`,
REWRITE_TAC[LET_DEF;LET_END_DEF;unadorned_v39;scs_opp_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;peropp;EXTENSION;IN]
THEN RESA_TAC
THEN SET_TAC[]);;

let BASIC_OPP=prove(`is_scs_v39 s /\ scs_basic_v39 s
==> scs_basic_v39 (scs_opp_v39 s)`,
SIMP_TAC[scs_basic;UNADORNED_OPP;A_B_J_SCS_OPP]);;


let DIAG_OPP=prove_by_refinement(`3<k /\ scs_diag k i j ==> scs_diag k (k - SUC (i MOD k)) (k - SUC (j MOD k))`,
[REWRITE_TAC[scs_diag]
THEN REPEAT RESA_TAC;

DICH_TAC 3
THEN REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC OPP_SUC_MOD[`i`;`k`]
THEN MRESA_TAC OPP_SUC_MOD[`j`;`k`];

DICH_TAC 1
THEN REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1<k/\ SUC (k - SUC (i MOD k))= k- i MOD k/\ SUC (k - SUC (SUC (k - SUC i MOD k) MOD k))
=(k - (SUC (k - SUC i MOD k) MOD k))`)
THEN RESA_TAC
THEN MRESA_TAC OPP_SUC_MOD[`j`;`k`]
THEN POP_ASSUM MP_TAC
THEN DICH_TAC 4
THEN RESA_TAC
THEN SYM_ASSUM_TAC
THEN MRESA_TAC SUC_OPP_ID[`i`;`k`]
THEN SYM_ASSUM_TAC
THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`k - SUC (SUC (k - SUC i MOD k) MOD k)`;`j`;`k`][MOD_REFL;]
THEN STRIP_TAC
THEN DICH_TAC 1
THEN ASM_SIMP_TAC[MOD_REFL;GSYM SUC_MOD_EQ_MOD_SUC;OPP_SUC_MOD];

DICH_TAC 2
THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1<k/\ SUC (k - SUC (j MOD k))= k- j MOD k/\ SUC (k - SUC (SUC (k - SUC j MOD k) MOD k))
=(k - (SUC (k - SUC j MOD k) MOD k))`)
THEN RESA_TAC
THEN MRESA_TAC OPP_SUC_MOD[`i`;`k`]
THEN POP_ASSUM MP_TAC
THEN DICH_TAC 4
THEN RESA_TAC
THEN SYM_ASSUM_TAC
THEN MRESA_TAC SUC_OPP_ID[`j`;`k`]
THEN SYM_ASSUM_TAC
THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`k - SUC (SUC (k - SUC j MOD k) MOD k)`;`i`;`k`][MOD_REFL;]
THEN STRIP_TAC
THEN DICH_TAC 1
THEN ASM_SIMP_TAC[MOD_REFL;GSYM SUC_MOD_EQ_MOD_SUC;OPP_SUC_MOD]]);;


let CQAOQLR_concl = 
`main_nonlinear_terminal_v11
==> (!s (v:num->real^3) i.
  3< scs_k_v39 s/\ 
  is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
  (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)/\ &4 * h0 < scs_b_v39 s i j)) /\
 &2< scs_b_v39 s i (i+1) /\ &2< scs_b_v39 s (i+1) (i+2)/\
scs_a_v39 s (i+2) (i+3)< scs_b_v39 s (i+2) (i+3) /\
scs_a_v39 s (i+ scs_k_v39 s -1) i< scs_b_v39 s (i+scs_k_v39 s -1) i 
==>
  scs_a_v39 s (i) (i+1) = &2 /\ scs_b_v39 s (i) (i+1) <= &2 * h0 /\
  scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) <= &2 * h0  ==>
  (dist(v i,v (i+1)) = &2 <=> dist(v(i+1),v(i+2)) = &2))`;;

let CQAOQLR = prove_by_refinement( CQAOQLR_concl,
[
REPEAT STRIP_TAC
THEN EQ_TAC;

STRIP_TAC
THEN MP_TAC TFITSKC
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`s:scs_v39`
THEN ASM_REWRITE_TAC[];

ASM_TAC
THEN REWRITE_TAC[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 MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ ~(k<=3)/\ 1<k`)
THEN RESA_TAC
THEN MRESA_TAC MM_SCS_OPP[`s`;`v`;`k`]
THEN MRESA_TAC(GEN_ALL OPP_IS_SCS)[`(scs_opp_v39 s)`;`s:scs_v39`]
THEN MP_TAC TFITSKC
THEN RESA_TAC
THEN THAYTHES_TAC 0[`(scs_opp_v39 s)`;`(\i. -- peropp (v:num->real^3) k i)`;`k- SUC((i+2) MOD k)`][IN]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[peropp;OPP_SUC_MOD;K_SUC_2_MOD_SUB;K_SUC_2_MOD_SUB_ID;DIST_SYM_0;K_SCS_OPP;A_B_J_SCS_OPP;K_SUC_2_MOD_F_SUB_ID]
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MP_TAC SCS_GENERIC_SYM_0
THEN RESA_TAC
THEN MP_TAC BASIC_OPP
THEN RESA_TAC
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(i+1) MOD k`;`v:num->real^3`;`i+1`][MOD_REFL;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(i+2) MOD k`;`v:num->real^3`;`i+2`][MOD_REFL;]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`(i+1) MOD k`;`i MOD k `;`s:scs_v39`;`i+1`;`i`][MOD_REFL]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(i+1) MOD k`;`i MOD k `;`s:scs_v39`;`i+1`;`i`][MOD_REFL]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`(i) MOD k`;`(i+k-1) MOD k `;`s:scs_v39`;`i`;`i+k-1`][MOD_REFL]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(i) MOD k`;`(i+k-1) MOD k `;`s:scs_v39`;`i`;`i+k-1`][MOD_REFL]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(i+2) MOD k`;`(i+1) MOD k `;`s:scs_v39`;`i+2`;`i+1`][MOD_REFL]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MATCH_DICH_TAC 0
THEN STRIP_TAC;

ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_TAC;

STRIP_TAC;

ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_TAC;

STRIP_TAC;

ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_TAC;

STRIP_TAC;

ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
THEN REPEAT RESA_TAC;

REPEAT GEN_TAC
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MATCH_DICH_TAC(36-6)
THEN MATCH_MP_TAC DIAG_OPP
THEN ASM_REWRITE_TAC[]]);;


 end;;


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