(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Packing                                                           *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2012-11-23                                                           *)
(* ========================================================================== *)

(*
Dec 21, 2012.

Use nonlinear inequalities to prove OXLZLEZ

The purpose of this file is to justify the hypothesis cc_bool_prep_v9.
by means of an induction argument.

However, this was abandoned midstream, because there is difficultly
in applying the reduction step to the hypothesis 'txq' in OXL_def.hl.

*)

module Oxl_lemma = struct

 open Oxl_def;;
 open Hales_tactic;;

end;;

(*
let cc_real_model_simple2 = prove_by_refinement(
`!cc n cc' x. 
  ~(n=0) /\
  cc_card_v9 cc = n /\   
    cc_card_v9 cc' = (n+1) /\ 
    cc_bool_model_v9 cc /\
    cc_real_model_v9 cc' /\
    cc_bool_model_v9 cc' /\
  periodic (cc_azim_v9 cc) (n) /\
  periodic (cc_gg_v9 cc) (n) /\
  periodic (cc_gg3a_v9 cc) (n) /\
  periodic (cc_gg3b_v9 cc) (n) /\
    (cc_qy_v9 cc' x) /\
    (cc_qy_v9 cc' (x+1)) /\
    cc_azim_v9 cc 0 = cc_azim_v9 cc' x + cc_azim_v9 cc' (x+1) /\
    cc_gg_v9 cc 0 = cc_gg_v9 cc' x + cc_gg_v9 cc' (x+1) /\
    cc_gg3a_v9 cc 0 = cc_gg3a_v9 cc' x + cc_gg3a_v9 cc' (x+1) /\
    cc_gg3b_v9 cc 0 = cc_gg3b_v9 cc' x + cc_gg3b_v9 cc' (x+1) /\
   (!i. i IN 1..n - 1 ==> cc_azim_v9 cc i = cc_azim_v9 cc' (x + 1 +i)) /\ 
   (!i. i IN 1..n - 1 ==> cc_gg_v9 cc i = cc_gg_v9 cc' (x + 1 +i)) /\ 
   (!i. i IN 1..n - 1 ==> cc_gg3a_v9 cc i = cc_gg3a_v9 cc' (x + 1 +i)) /\ 
   (!i. i IN 1..n - 1 ==> cc_gg3b_v9 cc i = cc_gg3b_v9 cc' (x + 1 +i)) /\ 
   cc_subcrit_v9 cc 0 = cc_subcrit_v9 cc' x /\
   cc_crit_v9 cc 0 = cc_crit_v9 cc' x /\
   cc_supercrit_v9 cc 0 = cc_supercrit_v9 cc' x /\
   cc_small_v9 cc 0 = cc_small_v9 cc' x /\
   cc_small_eta_v9 cc 0 = cc_small_eta_v9 cc' x /\
   cc_4cell_v9 cc 0 = cc_4cell_v9 cc' x /\
   (!i. i IN 1..n - 1 ==> cc_subcrit_v9 cc i = cc_subcrit_v9 cc' (x + 1 +i)) /\ 
   (!i. i IN 1..n - 1 ==> cc_crit_v9 cc i = cc_crit_v9 cc' (x + 1 +i)) /\ 
   (!i. i IN 1..n - 1 ==> cc_supercrit_v9 cc i = cc_supercrit_v9 cc' (x + 1 +i)) /\ 
   (!i. i IN 1..n - 1 ==> cc_small_v9 cc i = cc_small_v9 cc' (x + 1 +i)) /\ 
   (!i. i IN 1..n - 1 ==> cc_small_eta_v9 cc i = cc_small_eta_v9 cc' (x + 1 +i)) /\ 
   (!i. i IN 1..n - 1 ==> cc_4cell_v9 cc i = cc_4cell_v9 cc' (x + 1 +i)) 
   ==>  cc_real_model_v9 cc`,
  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  MATCH_MP_TAC cc_real_model_simple;
  EXISTS_TAC `n:num`;
  ASM_REWRITE_TAC[];
  SUBGOAL_THEN `periodic (cc_subcrit_v9 cc) n /\ periodic (cc_crit_v9 cc) n /\ periodic (cc_supercrit_v9 cc) n /\ periodic (cc_small_v9 cc) n /\ periodic (cc_small_eta_v9 cc) n /\ periodic (cc_4cell_v9 cc) n` MP_TAC;
    REPEAT (FIRST_X_ASSUM_ST `cc_bool_model_v9` MP_TAC);
    EXPAND_TAC "n";
    BY(MESON_TAC[cc_bool_model_v9]);
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  SUBGOAL_THEN `periodic (cc_hassmall_v9 cc) n /\  periodic (cc_qu_v9 cc) n /\  periodic (cc_qx_v9 cc) n /\ periodic (cc_qy_v9 cc) n ` MP_TAC;
    EXPAND_TAC "n";
    MATCH_MP_TAC periodic_fn;
    BY(ASM_REWRITE_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  ASM_REWRITE_TAC[];
  SUBGOAL_THEN `cc_qy_v9 cc 0` ASSUME_TAC;
    ASM_REWRITE_TAC[cc_qy_v9];
    BY(ASM_REWRITE_TAC[GSYM cc_qy_v9]);
  SUBGOAL_THEN `(n = 4 /\   (?i. cc_4cell_v9 cc i /\       cc_crit_v9 cc i /\       cc_qu_v9 cc (i + 1) /\       cc_qu_v9 cc (i + 2) /\       cc_qu_v9 cc (i + 3))) <=> F` (unlist REWRITE_TAC);
    BY(ASM_MESON_TAC[CASE_3Q1H]);
  SUBGOAL_THEN `sum (0..n - 1) (cc_azim_v9 cc) = &2 * pi` (unlist REWRITE_TAC);
    INTRO_TAC (cc_cut_sum) [`cc_azim_v9 cc'`;`x:num`];
    DISCH_THEN GMATCH_SIMP_TAC;
    ASM_SIMP_TAC[];
    REPEAT (FIRST_X_ASSUM_ST `cc_real_model_v9` MP_TAC);
    FIRST_X_ASSUM_ST `cc_card_v9` MP_TAC;
    COPY_TAC;
    DISCH_THEN (SUBST1_TAC o GSYM);
    REWRITE_TAC[cc_real_model_v9];
    REPEAT WEAK_STRIP_TAC;
    ASM_REWRITE_TAC[];
    SUBGOAL_THEN `n = cc_card_v9 cc' - 1` SUBST1_TAC;
      FIRST_X_ASSUM_ST `~(n=0)` MP_TAC;
      REPEAT (FIRST_X_ASSUM_ST `cc_card_v9` MP_TAC);
      BY(ARITH_TAC);
    BY(ASM_REWRITE_TAC[]);
  COMMENT "done with exceptional conjuncts";
  SUBGOAL_THEN `!i. i IN 0..n-1 <=> (i=0 \/ i IN 1..n-1)` (unlist REWRITE_TAC);
    REWRITE_TAC[IN_NUMSEG];
    BY(ARITH_TAC);
  CONJ_TAC THEN REPEAT WEAK_STRIP_TAC THEN ASM_SIMP_TAC[cc_real_model_v9];
      ENOUGH_TO_SHOW_TAC `#0.606 <= cc_azim_v9 cc' x /\ #0.606 <= cc_azim_v9 cc' (x+1)`;
        BY(REAL_ARITH_TAC);
      REPEAT (FIRST_X_ASSUM_ST `cc_real_model_v9` MP_TAC);
      BY(REWRITE_TAC[cc_real_model_v9] THEN DISCH_THEN (unlist REWRITE_TAC));
    REPEAT (FIRST_X_ASSUM_ST `cc_real_model_v9` MP_TAC);
    BY(REWRITE_TAC[cc_real_model_v9] THEN DISCH_THEN (unlist REWRITE_TAC));
  SUBGOAL_THEN `~cc_4cell_v9 cc 0 /\ ~cc_qu_v9 cc 0 /\ ~cc_qx_v9 cc 0 /\ ~cc_4cell_v9 cc' x /\ ~cc_qu_v9 cc' x /\ ~cc_qx_v9 cc' x` MP_TAC;
    FIRST_X_ASSUM MP_TAC;
    ASM_REWRITE_TAC[cc_qy_v9;cc_qu_v9;cc_qx_v9];
    BY(MESON_TAC[]);
  REPEAT WEAK_STRIP_TAC;
  SUBGOAL_THEN `(!i. i = 0 \/ i IN 1..n - 1 ==> cc_4cell_v9 cc i ==> cc_azim_v9 cc i <  #2.8) /\  (!i. i = 0 \/ i IN 1..n - 1 ==> cc_qu_v9 cc i ==> --cc_eps <= cc_gg_v9 cc i) /\ (!i. i = 0 \/ i IN 1..n - 1      ==> cc_qu_v9 cc i /\ ~cc_small_eta_v9 cc i      ==> cc_eps <= cc_gg_v9 cc i) /\ (!i. i = 0 \/ i IN 1..n - 1      ==> cc_4cell_v9 cc i      ==> a_spine5 + b_spine5 * cc_azim_v9 cc i <= cc_gg_v9 cc i) /\ (!i. i = 0 \/ i IN 1..n - 1      ==> cc_qu_v9 cc i      ==> -- #0.0659 +  #0.042 * cc_azim_v9 cc i <= cc_gg_v9 cc i) /\ (!i. i = 0 \/ i IN 1..n - 1      ==> cc_qu_v9 cc i      ==> -- #0.0142852 +  #0.00609451 * cc_azim_v9 cc i <= cc_gg_v9 cc i) /\ (!i. i = 0 \/ i IN 1..n - 1      ==> cc_qu_v9 cc i      ==>  #0.161517 -  #0.119482 * cc_azim_v9 cc i <= cc_gg_v9 cc i) /\ (!i. i = 0 \/ i IN 1..n - 1 ==> cc_qx_v9 cc i ==>  #0.0 <= cc_gg_v9 cc i) /\ (!i. i = 0 \/ i IN 1..n - 1      ==> cc_qx_v9 cc i /\  #2.3 < cc_azim_v9 cc i      ==> cc_eps <= cc_gg_v9 cc i)` (unlist REWRITE_TAC);
    FIRST_X_ASSUM_ST `cc_real_model_v9` MP_TAC;
    REWRITE_TAC[cc_real_model_v9];
    REPEAT WEAK_STRIP_TAC;
    REWRITE_TAC[MESON[] `((!i. p i ) /\ (!i. q i)) <=> (!i. p i /\ q i)`];
    GEN_TAC;
    ASM_CASES_TAC `i = 0`;
      BY(ASM_REWRITE_TAC[]);
    (ASM_SIMP_TAC[]);
comment "unfinished, to here";
 (*
repeat conj then st/r then asimp[cc_real_model_v9]
rep 5 (fxa mp) then mt[]
fxast `cc_real_model_v9` mp
rt[cc_real_model_v9]
dthen (unlist amt)
rep 5 (fxa mp) then mt[]
fxast `cc_real_model_v9` mp
rt[cc_real_model_v9]
 *)
  ]);;
  (* }}} *)
*)

(*
g XSBYGIQ_concl;;

let XSBYGIQ = prove_by_refinement(
  XSBYGIQ_concl,
  (* {{{ proof *)
  [
  GOAL_TERM (fun w -> (ABBREV_TAC ( env w `bad_set  = \cc. {i | i IN 0..(cc_card_v9 cc - 1) /\ cc_qy_v9 cc i /\ cc_qy_v9 cc (i+1) }`)));
  GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!cc. FINITE (bad_set cc)`) ASSUME_TAC));
    GEN_TAC;
    EXPAND_TAC "bad_set";
    MATCH_MP_TAC FINITE_SUBSET;
    GOAL_TERM (fun w -> (EXISTS_TAC ( env w `0.. cc_card_v9 cc - 1`)));
    REWRITE_TAC[FINITE_NUMSEG;SUBSET];
    REWRITE_TAC[IN_ELIM_THM];
    BY(MESON_TAC[]);
  COMMENT "set up induction";
  REPEAT WEAK_STRIP_TAC;
  PROOF_BY_CONTR_TAC;
  GOAL_TERM (fun w -> (ENOUGH_TO_SHOW_TAC ( env w `(!k. (!cc. (bad_set cc) HAS_SIZE k ==> ~( cc_bool_model_v9 cc /\        cc_real_model_v9 cc /\       sum (0..cc_card_v9 cc - 1) (cc_gg_v9 cc) < &0)))`)));
    DISCH_THEN (C INTRO_TAC [`CARD(bad_set cc)`;`cc`]);
    ASM_REWRITE_TAC[];
    BY(ASM_MESON_TAC[HAS_SIZE]);
  INDUCT_TAC;
    GEN_TAC;
    REWRITE_TAC[HAS_SIZE_0];
    EXPAND_TAC "bad_set";
    ONCE_REWRITE_TAC[EXTENSION];
    REWRITE_TAC[IN_ELIM_THM;NOT_IN_EMPTY];
    REPEAT WEAK_STRIP_TAC;
    FIRST_X_ASSUM_ST `?` MP_TAC;
    REWRITE_TAC[];
    GOAL_TERM (fun w -> (EXISTS_TAC ( env w `cc'`)));
    ASM_REWRITE_TAC[];
    REWRITE_TAC[cc_bool_prep_v9];
    GEN_TAC;
    SUBGOAL_THEN `~(cc_card_v9 cc' = 0)` ASSUME_TAC;
      BY(ASM_MESON_TAC[cc_bool_model_v9]);
    ABBREV_TAC `x = i MOD cc_card_v9 cc'`;
    FIRST_X_ASSUM_ST `cc_qy_v9` (C INTRO_TAC [`x`]);
    REPEAT WEAK_STRIP_TAC;
    FIRST_X_ASSUM_ST `~` MP_TAC;
    REWRITE_TAC[];
    EXPAND_TAC "x";
    GMATCH_SIMP_TAC MOD_IN_NUMSEG;
    ASM_REWRITE_TAC[];
    INTRO_TAC periodic_fn [`cc'`];
    ASM_REWRITE_TAC[];
    REPEAT WEAK_STRIP_TAC;
    CONJ_TAC;
      EXPAND_TAC "x";
      GMATCH_SIMP_TAC (GSYM periodic_mod);
      BY(ASM_REWRITE_TAC[]);
    EXPAND_TAC "x";
    SUBGOAL_THEN `cc_qy_v9 cc' ((i DIV cc_card_v9 cc') * cc_card_v9 cc' + (i MOD cc_card_v9 cc'  + 1))` MP_TAC;
      INTRO_TAC (GSYM DIVISION) [`i`;`cc_card_v9 cc'`];
      ASM_REWRITE_TAC[];
      REPEAT WEAK_STRIP_TAC;
      SUBGOAL_THEN `i DIV cc_card_v9 cc' * cc_card_v9 cc' + x + 1 = i + 1` SUBST1_TAC;
        BY(FIRST_X_ASSUM_ST `DIV` MP_TAC THEN ARITH_TAC);
      BY(ASM_REWRITE_TAC[]);
    SUBST1_TAC (arith `i DIV cc_card_v9 cc' * cc_card_v9 cc' + i MOD cc_card_v9 cc' + 1 =  (i MOD cc_card_v9 cc' + 1) + i DIV cc_card_v9 cc' * cc_card_v9 cc'`);
    GMATCH_SIMP_TAC periodic_nk;
    BY(ASM_SIMP_TAC[arith `~(n=0) ==> (0 < n)`]);
  COMMENT "base case of induction completed, now induct step";
  REPEAT WEAK_STRIP_TAC;
  COMMENT "pick element in bad set";
  GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `?x. x IN bad_set cc'`) MP_TAC));
    REWRITE_TAC[MEMBER_NOT_EMPTY];
    REWRITE_TAC[GSYM HAS_SIZE_0];
    FIRST_X_ASSUM_ST `SUC` MP_TAC;
    REWRITE_TAC[HAS_SIZE];
    DISCH_THEN (unlist REWRITE_TAC);
    BY(ARITH_TAC);
  REPEAT WEAK_STRIP_TAC;
  COMMENT "construct reduced cc";
  ABBREV_TAC `n = cc_card_v9 cc' - 1`;
  ABBREV_TAC `cutr = \ (f:num->real) j. if (0 = j MOD n) then f x + f (x+1) else f (x + 1 + (j MOD n))`;
  ABBREV_TAC `cutb = \ (g:num->bool) j. if (0 = j MOD n) then g x else g (x + 1 + (j MOD n))`;
  INTRO_TAC CC_EXISTS [`cutr (cc_azim_v9 cc')`;`cutr (cc_gg_v9 cc')`;`cutr (cc_gg3a_v9 cc')`;`cutr (cc_gg3b_v9 cc')`;`cutb (cc_subcrit_v9 cc')`;`cutb (cc_crit_v9 cc')`;`cutb (cc_supercrit_v9 cc')`;`cutb (cc_small_v9 cc')`;`cutb (cc_small_eta_v9 cc')`;`cutb (cc_4cell_v9 cc')`;`n`];
  REPEAT WEAK_STRIP_TAC;
  GOAL_TERM (fun w -> (FIRST_X_ASSUM (MP_TAC o (ISPEC ( env w `cc''`)))));
  REWRITE_TAC[TAUT (`((x ==> ~y) ==> F) <=> x /\ y`)];
  COMMENT "size of n";
  SUBGOAL_THEN `~(cc_card_v9 cc'' = 0)` ASSUME_TAC;
    INTRO_TAC CC_CARD2 [`cc'`];
    ASM_REWRITE_TAC[];
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
  COMMENT "periodicity";
  GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!f. periodic (cutr f) n`) ASSUME_TAC));
    REWRITE_TAC[periodic];
    EXPAND_TAC "cutr";
    REPEAT WEAK_STRIP_TAC;
    SUBGOAL_THEN ` (i + n) MOD n = i MOD n` SUBST1_TAC;
      BY(MESON_TAC[MOD_MULT_ADD;arith `(i + n) = (1 * n + i)`]);
    BY(MESON_TAC[]);
  GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!g. periodic (cutb g) n`) ASSUME_TAC));
    REWRITE_TAC[periodic];
    EXPAND_TAC "cutb";
    REPEAT WEAK_STRIP_TAC;
    SUBGOAL_THEN ` (i + n) MOD n = i MOD n` SUBST1_TAC;
      BY(MESON_TAC[MOD_MULT_ADD;arith `(i + n) = (1 * n + i)`]);
    BY(MESON_TAC[]);
  (COMMENT "bad_set");
  SUBGOAL_THEN `BIJ (\j. j+ (x + 1)) (1..(n-1)) ((x+2)..(x+n))` ASSUME_TAC;
    REWRITE_TAC[BIJ;INJ];
    SUBCONJ_TAC;
      REWRITE_TAC[IN_NUMSEG];
      BY(ARITH_TAC);
    REPEAT WEAK_STRIP_TAC;
    REWRITE_TAC[SURJ];
    ASM_REWRITE_TAC[];
    REWRITE_TAC[IN_NUMSEG];
    REPEAT WEAK_STRIP_TAC;
    GOAL_TERM (fun w -> (EXISTS_TAC ( env w `x' - (x + 1)`)));
    REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
    BY(ARITH_TAC);
  SUBGOAL_THEN `1 <= n` ASSUME_TAC;
    INTRO_TAC (CC_CARD2) [`cc'`];
    ASM_REWRITE_TAC[];
    REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `x - 1` MP_TAC);
    BY(ARITH_TAC);
  SUBGOAL_THEN `!i. i IN 1..(n-1) ==> i MOD n = i` ASSUME_TAC;
    REWRITE_TAC[IN_NUMSEG];
    GEN_TAC;
    INTRO_TAC MOD_LT [`i`;`n`];
    BY(ARITH_TAC);
  GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!f. cutr f 0 = (f:num->real) x + f (x + 1)`) ASSUME_TAC));
    EXPAND_TAC "cutr";
    GMATCH_SIMP_TAC MOD_0;
    REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
    BY(ARITH_TAC);
  GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!g. cutb g 0 = (g:num->bool) x `) ASSUME_TAC));
    EXPAND_TAC "cutb";
    GMATCH_SIMP_TAC MOD_0;
    REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC);
    BY(ARITH_TAC);
  GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!i f. i IN 1..(n-1) ==> cutr f i = f (x + 1 + i)`) ASSUME_TAC));
    REPEAT WEAK_STRIP_TAC;
    EXPAND_TAC "cutr";
    GOAL_TERM (fun w -> (FIRST_X_ASSUM (MP_TAC o ISPEC ( env w `i`))));
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    COND_CASES_TAC;
      REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
      REWRITE_TAC[IN_NUMSEG];
      BY(ARITH_TAC);
    BY(REWRITE_TAC[]);
  GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!i g. i IN 1..(n-1) ==> cutb g  i = g (x + 1 + i)`) ASSUME_TAC));
    REPEAT WEAK_STRIP_TAC;
    EXPAND_TAC "cutb";
    GOAL_TERM (fun w -> (FIRST_X_ASSUM_ST `MOD` (MP_TAC o ISPEC ( env w `i`))));
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    COND_CASES_TAC;
      REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
      REWRITE_TAC[IN_NUMSEG];
      BY(ARITH_TAC);
    BY(REWRITE_TAC[]);
  (COMMENT " NOT FINISHED TO HERE, 4 CONJUNCTS TO GO. ")
(* NOT FINISHED *)
  ]);;
  (* }}} *)
*)