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


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


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

let SUR_MOD_FUN=
prove(`~(k=0)==> ?i. (i+p) MOD k = p' MOD k`,

STRIP_TAC
THEN MP_TAC(ARITH_RULE`p MOD k<= p' MOD k\/ p' MOD k< p MOD k`)
THEN RESA_TAC
THENL[
EXISTS_TAC`p' MOD k- p MOD k`
THEN MRESA_TAC DIVISION[`p'`;`k`]
THEN MP_TAC(ARITH_RULE`p' MOD k< k /\ p MOD k<= p' MOD k ==> p' MOD k - p MOD k < k /\ p' MOD k - p MOD k + p MOD k= p' MOD k`)
THEN RESA_TAC
THEN MRESAS_TAC MOD_LT[`p' MOD k- p MOD k`;`k`][DIVISION]
THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);

EXISTS_TAC`p' MOD k +k - p MOD k`
THEN MRESA_TAC DIVISION[`p`;`k`]
THEN MP_TAC(ARITH_RULE`p MOD k< k /\ p' MOD k< p MOD k ==> p' MOD k +k - p MOD k < k /\ (p' MOD k + k - p MOD k) + p MOD k=1*k+ p' MOD k`)
THEN RESA_TAC
THEN MRESAS_TAC MOD_LT[`p' MOD k+k- p MOD k`;`k`][DIVISION]
THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k+k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL;MOD_MULT_ADD]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);;
let TRANS_DIAG=
prove(`~(k=0)/\ (i+p) MOD k = p' MOD k /\ p' + q = p + q'
==> (i+q) MOD k= q' MOD k `,

STRIP_TAC
THEN MATCH_MP_TAC Hdplygy.MOD_EQ_MOD
THEN EXISTS_TAC`p:num`
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[ARITH_RULE`p + i + q= (i +p)+ q:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i+p:num`;`q`;`k`]
THEN POP_ASSUM(fun th-> ASM_SIMP_TAC[SYM th;MOD_ADD_MOD]));;

(*************)


(*******************)


let scs_components = 
prove_by_refinement(
  `!s. dest_scs_v39 s = (scs_k_v39 s,scs_d_v39 s,scs_a_v39
s,scs_am_v39 s ,scs_bm_v39 s,scs_b_v39 s,scs_J_v39 s,
                         scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Wrgcvdr_cizmrrh.PAIR_EQ2;scs_k_v39;scs_d_v39;scs_a_v39;];
  REWRITE_TAC[scs_am_v39;scs_bm_v39;scs_b_v39;];
  REWRITE_TAC[scs_J_v39;scs_hi_v39;scs_lo_v39;];
  REWRITE_TAC[scs_str_v39];

BY(REWRITE_TAC[Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.part4;
Misc_defs_and_lemmas.part5;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop0;Misc_defs_and_lemmas.drop3;Misc_defs_and_lemmas.drop1;Misc_defs_and_lemmas.part0;Misc_defs_and_lemmas.part8;Misc_defs_and_lemmas.drop2])
  ]);;
  (* }}} *)

let scs_inj = 
prove_by_refinement(
  `!s s'. scs_basic_v39 s /\  scs_basic_v39 s' /\
    scs_d_v39 s = scs_d_v39 s' /\
    scs_k_v39 s = scs_k_v39 s' /\
    (scs_a_v39 s = scs_a_v39 s') /\
    (scs_b_v39 s = scs_b_v39 s')
  ==> (s = s')`,


  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REPEAT (FIRST_X_ASSUM_ST `scs_basic_v39` MP_TAC);
  REWRITE_TAC[scs_basic;unadorned_v39];
  ONCE_REWRITE_TAC[EQ_SYM_EQ];
  REWRITE_TAC[SET_RULE `{} = a <=> a = {}`];
  REPEAT WEAKER_STRIP_TAC;
  ONCE_REWRITE_TAC[GSYM scs_v39];
  AP_TERM_TAC;
  ASM_REWRITE_TAC[scs_components];
  TYPIFY `scs_J_v39 s = scs_J_v39 s'` (C SUBGOAL_THEN SUBST1_TAC);
    BY(ASM_REWRITE_TAC[FUN_EQ_THM]);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)



let DIAG_PSORT1=
prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\ 
p' + q = p + q' /\ ~(k=0) /\ (psort k (i',j) = psort k (p,q))
==>  (psort k (i+i',i+j) = psort k (p',q'))`,


[
REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC TRANS_DIAG
THEN RESA_TAC
THEN MP_TAC(SET_RULE`i' MOD k <= j MOD k \/ ~(i' MOD k <= j MOD k)`)
THEN RESA_TAC;

MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][]
THEN MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
THEN RESA_TAC;

MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`];


MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;




let DIAG_PSORT2=
prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\ 
p' + q = p + q' /\ ~(k=0) /\ (psort k (i+i',i+j) = psort k (p',q'))
==> 
(psort k (i',j) = psort k (p,q))`,

[
REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC TRANS_DIAG
THEN RESA_TAC
THEN MP_TAC(SET_RULE`(i+i') MOD k <= (i+j) MOD k \/ ~((i+i') MOD k <= (i+j) MOD k)`)
THEN RESA_TAC;

MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];

MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
THEN RESA_TAC;


MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
THEN RESA_TAC;

MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];

MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;



let DIAG_PSORT=
prove(
 ` ~(k=0) /\ (i+p) MOD k = p' MOD k /\ 
p' + q = p + q' /\ ~(k=0) 
==>
((psort k (i+i',i+j) = psort k (p',q'))
<=> 
(psort k (i',j) = psort k (p,q)))`,

STRIP_TAC
THEN EQ_TAC
THEN STRIP_TAC
THENL[
MATCH_MP_TAC DIAG_PSORT2
THEN RESA_TAC;
MATCH_MP_TAC DIAG_PSORT1
THEN RESA_TAC]);;
let TRANS_DIAG=
prove(`
~(k=0)
==> (scs_diag k i' j<=> scs_diag k (i+i') (i+j)) `,

SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + i') = i + (i' + 1)/\ SUC i= i+1`;Ocbicby.MOD_EQ_MOD_SHIFT]);;

let A_EQ_PSORT=
prove(` is_scs_v39 s  /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
==> scs_a_v39 s i j= scs_a_v39 s p q`,

REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
THEN RESA_TAC
THEN 
REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN MRESA_TAC CHANGE_A_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC);;

let B_EQ_PSORT=
prove(` is_scs_v39 s  /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
==> scs_b_v39 s i j= scs_b_v39 s p q`,

REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
THEN RESA_TAC
THEN 
REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN MRESA_TAC CHANGE_B_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC);;
let PROPERTY_OF_K_SCS=
prove(`is_scs_v39 s==> ~(scs_k_v39 s= 0)/\ 0< scs_k_v39 s/\ 1< scs_k_v39 s/\ 2< scs_k_v39 s`,

STRIP_TAC
THEN MP_TAC Axjrpnc.is_scs_k_le_3
THEN RESA_TAC 
THEN DICH_TAC 0
THEN ARITH_TAC);;

let PSORT_PERIODIC=
prove(`~(k=0) ==> psort (k) (i + k,j) = psort (k) (i,j)
/\ psort (k) (i,j+k) = psort (k) (i,j)`,

REPEAT RESA_TAC
THEN REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
THEN ONCE_REWRITE_TAC[ARITH_RULE`i+k=1*k+i`]
THEN ASM_SIMP_TAC[MOD_MULT_ADD]);;

let DIAG_NOT_PSORT = 
prove_by_refinement( 
`~(k=0) /\ scs_diag k i j ==> !i'. ~(psort k (i,j) = psort k (i',SUC i'))`,

[
REWRITE_TAC[scs_diag;psort;LET_DEF;LET_END_DEF]
THEN STRIP_TAC
THEN GEN_TAC
THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k\/ ~(i MOD k <= j MOD k)`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE`i' MOD k <= SUC i' MOD k\/ ~(i' MOD k <= SUC i' MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
THEN POP_ASSUM MP_TAC
THEN SYM_ASSUM_TAC
THEN ASM_REWRITE_TAC[];

REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`i'`;`k`]
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN ASM_REWRITE_TAC[];

MP_TAC(ARITH_RULE`i' MOD k <= SUC i' MOD k\/ ~(i' MOD k <= SUC i' MOD k)`)
THEN RESA_TAC;


REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`i'`;`k`]
THEN POP_ASSUM MP_TAC
THEN SYM_ASSUM_TAC
THEN ASM_REWRITE_TAC[];

REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN ASM_REWRITE_TAC[]]);;

let YRTAFYH_concl = 
  `!s i j.
    is_scs_v39 s /\
    scs_basic_v39 s /\
    3 < scs_k_v39 s /\
    scs_diag (scs_k_v39 s) i j /\
    scs_a_v39 s i j <= cstab ==>
    is_scs_v39 (scs_stab_diag_v39 s i j) /\ scs_basic_v39 (scs_stab_diag_v39 s i j)
    `;;


let YRTAFYH=  prove_by_refinement(YRTAFYH_concl,
[

REPEAT RESA_TAC
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC;

DICH_TAC 8
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MP_TAC th THEN ASSUME_TAC(th))
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;scs_stab_diag_v39;is_scs_v39;scs_v39_explicit;mk_unadorned_v39;scs_basic;periodic;periodic2]
THEN REPEAT RESA_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`;

SET_TAC[];

SET_TAC[];

SET_TAC[];

SET_TAC[];

ASM_SIMP_TAC[PSORT_PERIODIC];

ASM_SIMP_TAC[PSORT_PERIODIC];

ASM_SIMP_TAC[PSORT_PERIODIC];

ASM_SIMP_TAC[PSORT_PERIODIC];

ASM_SIMP_TAC[Terminal.psort_sym];

REAL_ARITH_TAC;

MP_TAC(SET_RULE`psort k (i,j) = psort k (i',j') \/ ~(psort k (i,j) = psort k (i',j'))`)
THEN RESA_TAC;

MRESAL_TAC A_EQ_PSORT[`i'`;`j'`;`s`;`i`;`j`][];

THAYTHE_TAC (30-21)[`i'`;`j'`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;

MP_TAC(SET_RULE`psort k (i,j) = psort k (i',j') \/ ~(psort k (i,j) = psort k (i',j'))`)
THEN RESA_TAC
THEN REAL_ARITH_TAC;

MP_TAC(SET_RULE`psort 3 (i,j) = psort 3 (i',SUC i') \/ ~(psort 3 (i,j) = psort 3 (i', SUC i'))`)
THEN RESA_TAC;

REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

MATCH_DICH_TAC (31-24)
THEN ASM_REWRITE_TAC[];

MP_TAC(SET_RULE`psort k (i,j) = psort k (i',SUC i') \/ ~(psort k (i,j) = psort k (i', SUC i'))`)
THEN RESA_TAC;

REAL_ARITH_TAC;

MP_TAC DIAG_NOT_PSORT
THEN RESA_TAC;

REWRITE_TAC[scs_basic;scs_stab_diag_v39;LET_DEF;LET_END_DEF;unadorned_v39;mk_unadorned_v39;scs_v39_explicit]]);;


let STAB_IS_SCS=
prove(`!s i j.
    is_scs_v39 s /\
    scs_basic_v39 s /\
    3 < scs_k_v39 s /\
    scs_diag (scs_k_v39 s) i j /\
    scs_a_v39 s i j <= cstab ==>
    is_scs_v39 (scs_stab_diag_v39 s i j) `,

SIMP_TAC[YRTAFYH]);;

 end;;


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