legacy/oldpacking/ch_packing/oxl_lemma.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Packing                                                           *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2012-11-23                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  10 Dec 21, 2012.
  11
  12 Use nonlinear inequalities to prove OXLZLEZ
  13
  14 The purpose of this file is to justify the hypothesis cc_bool_prep_v9.
  15 by means of an induction argument.
  16
  17 However, this was abandoned midstream, because there is difficultly
  18 in applying the reduction step to the hypothesis 'txq' in OXL_def.hl.
  19
  20 *)
  21
  22 module Oxl_lemma = struct
  23
  24  open Oxl_def;;
  25  open Hales_tactic;;
  26
  27 end;;
  28
  29 (*
  30 let cc_real_model_simple2 = prove_by_refinement(
  31 `!cc n cc' x.
  32   ~(n=0) /\
  33   cc_card_v9 cc = n /\
  34     cc_card_v9 cc' = (n+1) /\
  35     cc_bool_model_v9 cc /\
  36     cc_real_model_v9 cc' /\
  37     cc_bool_model_v9 cc' /\
  38   periodic (cc_azim_v9 cc) (n) /\
  39   periodic (cc_gg_v9 cc) (n) /\
  40   periodic (cc_gg3a_v9 cc) (n) /\
  41   periodic (cc_gg3b_v9 cc) (n) /\
  42     (cc_qy_v9 cc' x) /\
  43     (cc_qy_v9 cc' (x+1)) /\
  44     cc_azim_v9 cc 0 = cc_azim_v9 cc' x + cc_azim_v9 cc' (x+1) /\
  45     cc_gg_v9 cc 0 = cc_gg_v9 cc' x + cc_gg_v9 cc' (x+1) /\
  46     cc_gg3a_v9 cc 0 = cc_gg3a_v9 cc' x + cc_gg3a_v9 cc' (x+1) /\
  47     cc_gg3b_v9 cc 0 = cc_gg3b_v9 cc' x + cc_gg3b_v9 cc' (x+1) /\
  48    (!i. i IN 1..n - 1 ==> cc_azim_v9 cc i = cc_azim_v9 cc' (x + 1 +i)) /\
  49    (!i. i IN 1..n - 1 ==> cc_gg_v9 cc i = cc_gg_v9 cc' (x + 1 +i)) /\
  50    (!i. i IN 1..n - 1 ==> cc_gg3a_v9 cc i = cc_gg3a_v9 cc' (x + 1 +i)) /\
  51    (!i. i IN 1..n - 1 ==> cc_gg3b_v9 cc i = cc_gg3b_v9 cc' (x + 1 +i)) /\
  52    cc_subcrit_v9 cc 0 = cc_subcrit_v9 cc' x /\
  53    cc_crit_v9 cc 0 = cc_crit_v9 cc' x /\
  54    cc_supercrit_v9 cc 0 = cc_supercrit_v9 cc' x /\
  55    cc_small_v9 cc 0 = cc_small_v9 cc' x /\
  56    cc_small_eta_v9 cc 0 = cc_small_eta_v9 cc' x /\
  57    cc_4cell_v9 cc 0 = cc_4cell_v9 cc' x /\
  58    (!i. i IN 1..n - 1 ==> cc_subcrit_v9 cc i = cc_subcrit_v9 cc' (x + 1 +i)) /\
  59    (!i. i IN 1..n - 1 ==> cc_crit_v9 cc i = cc_crit_v9 cc' (x + 1 +i)) /\
  60    (!i. i IN 1..n - 1 ==> cc_supercrit_v9 cc i = cc_supercrit_v9 cc' (x + 1 +i)) /\
  61    (!i. i IN 1..n - 1 ==> cc_small_v9 cc i = cc_small_v9 cc' (x + 1 +i)) /\
  62    (!i. i IN 1..n - 1 ==> cc_small_eta_v9 cc i = cc_small_eta_v9 cc' (x + 1 +i)) /\
  63    (!i. i IN 1..n - 1 ==> cc_4cell_v9 cc i = cc_4cell_v9 cc' (x + 1 +i))
  64    ==>  cc_real_model_v9 cc`,
  65   (* {{{ proof *)
  66   [
  67   REPEAT WEAK_STRIP_TAC;
  68   MATCH_MP_TAC cc_real_model_simple;
  69   EXISTS_TAC `n:num`;
  70   ASM_REWRITE_TAC[];
  71   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;
  72     REPEAT (FIRST_X_ASSUM_ST `cc_bool_model_v9` MP_TAC);
  73     EXPAND_TAC "n";
  74     BY(MESON_TAC[cc_bool_model_v9]);
  75   REPEAT WEAK_STRIP_TAC;
  76   ASM_REWRITE_TAC[];
  77   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;
  78     EXPAND_TAC "n";
  79     MATCH_MP_TAC periodic_fn;
  80     BY(ASM_REWRITE_TAC[]);
  81   REPEAT WEAK_STRIP_TAC;
  82   ASM_REWRITE_TAC[];
  83   SUBGOAL_THEN `cc_qy_v9 cc 0` ASSUME_TAC;
  84     ASM_REWRITE_TAC[cc_qy_v9];
  85     BY(ASM_REWRITE_TAC[GSYM cc_qy_v9]);
  86   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);
  87     BY(ASM_MESON_TAC[CASE_3Q1H]);
  88   SUBGOAL_THEN `sum (0..n - 1) (cc_azim_v9 cc) = &2 * pi` (unlist REWRITE_TAC);
  89     INTRO_TAC (cc_cut_sum) [`cc_azim_v9 cc'`;`x:num`];
  90     DISCH_THEN GMATCH_SIMP_TAC;
  91     ASM_SIMP_TAC[];
  92     REPEAT (FIRST_X_ASSUM_ST `cc_real_model_v9` MP_TAC);
  93     FIRST_X_ASSUM_ST `cc_card_v9` MP_TAC;
  94     COPY_TAC;
  95     DISCH_THEN (SUBST1_TAC o GSYM);
  96     REWRITE_TAC[cc_real_model_v9];
  97     REPEAT WEAK_STRIP_TAC;
  98     ASM_REWRITE_TAC[];
  99     SUBGOAL_THEN `n = cc_card_v9 cc' - 1` SUBST1_TAC;
 100       FIRST_X_ASSUM_ST `~(n=0)` MP_TAC;
 101       REPEAT (FIRST_X_ASSUM_ST `cc_card_v9` MP_TAC);
 102       BY(ARITH_TAC);
 103     BY(ASM_REWRITE_TAC[]);
 104   COMMENT "done with exceptional conjuncts";
 105   SUBGOAL_THEN `!i. i IN 0..n-1 <=> (i=0 \/ i IN 1..n-1)` (unlist REWRITE_TAC);
 106     REWRITE_TAC[IN_NUMSEG];
 107     BY(ARITH_TAC);
 108   CONJ_TAC THEN REPEAT WEAK_STRIP_TAC THEN ASM_SIMP_TAC[cc_real_model_v9];
 109       ENOUGH_TO_SHOW_TAC `#0.606 <= cc_azim_v9 cc' x /\ #0.606 <= cc_azim_v9 cc' (x+1)`;
 110         BY(REAL_ARITH_TAC);
 111       REPEAT (FIRST_X_ASSUM_ST `cc_real_model_v9` MP_TAC);
 112       BY(REWRITE_TAC[cc_real_model_v9] THEN DISCH_THEN (unlist REWRITE_TAC));
 113     REPEAT (FIRST_X_ASSUM_ST `cc_real_model_v9` MP_TAC);
 114     BY(REWRITE_TAC[cc_real_model_v9] THEN DISCH_THEN (unlist REWRITE_TAC));
 115   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;
 116     FIRST_X_ASSUM MP_TAC;
 117     ASM_REWRITE_TAC[cc_qy_v9;cc_qu_v9;cc_qx_v9];
 118     BY(MESON_TAC[]);
 119   REPEAT WEAK_STRIP_TAC;
 120   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);
 121     FIRST_X_ASSUM_ST `cc_real_model_v9` MP_TAC;
 122     REWRITE_TAC[cc_real_model_v9];
 123     REPEAT WEAK_STRIP_TAC;
 124     REWRITE_TAC[MESON[] `((!i. p i ) /\ (!i. q i)) <=> (!i. p i /\ q i)`];
 125     GEN_TAC;
 126     ASM_CASES_TAC `i = 0`;
 127       BY(ASM_REWRITE_TAC[]);
 128     (ASM_SIMP_TAC[]);
 129 comment "unfinished, to here";
 130  (*
 131 repeat conj then st/r then asimp[cc_real_model_v9]
 132 rep 5 (fxa mp) then mt[]
 133 fxast `cc_real_model_v9` mp
 134 rt[cc_real_model_v9]
 135 dthen (unlist amt)
 136 rep 5 (fxa mp) then mt[]
 137 fxast `cc_real_model_v9` mp
 138 rt[cc_real_model_v9]
 139  *)
 140   ]);;
 141   (* }}} *)
 142 *)
 143
 144 (*
 145 g XSBYGIQ_concl;;
 146
 147 let XSBYGIQ = prove_by_refinement(
 148   XSBYGIQ_concl,
 149   (* {{{ proof *)
 150   [
 151   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) }`)));
 152   GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!cc. FINITE (bad_set cc)`) ASSUME_TAC));
 153     GEN_TAC;
 154     EXPAND_TAC "bad_set";
 155     MATCH_MP_TAC FINITE_SUBSET;
 156     GOAL_TERM (fun w -> (EXISTS_TAC ( env w `0.. cc_card_v9 cc - 1`)));
 157     REWRITE_TAC[FINITE_NUMSEG;SUBSET];
 158     REWRITE_TAC[IN_ELIM_THM];
 159     BY(MESON_TAC[]);
 160   COMMENT "set up induction";
 161   REPEAT WEAK_STRIP_TAC;
 162   PROOF_BY_CONTR_TAC;
 163   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)))`)));
 164     DISCH_THEN (C INTRO_TAC [`CARD(bad_set cc)`;`cc`]);
 165     ASM_REWRITE_TAC[];
 166     BY(ASM_MESON_TAC[HAS_SIZE]);
 167   INDUCT_TAC;
 168     GEN_TAC;
 169     REWRITE_TAC[HAS_SIZE_0];
 170     EXPAND_TAC "bad_set";
 171     ONCE_REWRITE_TAC[EXTENSION];
 172     REWRITE_TAC[IN_ELIM_THM;NOT_IN_EMPTY];
 173     REPEAT WEAK_STRIP_TAC;
 174     FIRST_X_ASSUM_ST `?` MP_TAC;
 175     REWRITE_TAC[];
 176     GOAL_TERM (fun w -> (EXISTS_TAC ( env w `cc'`)));
 177     ASM_REWRITE_TAC[];
 178     REWRITE_TAC[cc_bool_prep_v9];
 179     GEN_TAC;
 180     SUBGOAL_THEN `~(cc_card_v9 cc' = 0)` ASSUME_TAC;
 181       BY(ASM_MESON_TAC[cc_bool_model_v9]);
 182     ABBREV_TAC `x = i MOD cc_card_v9 cc'`;
 183     FIRST_X_ASSUM_ST `cc_qy_v9` (C INTRO_TAC [`x`]);
 184     REPEAT WEAK_STRIP_TAC;
 185     FIRST_X_ASSUM_ST `~` MP_TAC;
 186     REWRITE_TAC[];
 187     EXPAND_TAC "x";
 188     GMATCH_SIMP_TAC MOD_IN_NUMSEG;
 189     ASM_REWRITE_TAC[];
 190     INTRO_TAC periodic_fn [`cc'`];
 191     ASM_REWRITE_TAC[];
 192     REPEAT WEAK_STRIP_TAC;
 193     CONJ_TAC;
 194       EXPAND_TAC "x";
 195       GMATCH_SIMP_TAC (GSYM periodic_mod);
 196       BY(ASM_REWRITE_TAC[]);
 197     EXPAND_TAC "x";
 198     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;
 199       INTRO_TAC (GSYM DIVISION) [`i`;`cc_card_v9 cc'`];
 200       ASM_REWRITE_TAC[];
 201       REPEAT WEAK_STRIP_TAC;
 202       SUBGOAL_THEN `i DIV cc_card_v9 cc' * cc_card_v9 cc' + x + 1 = i + 1` SUBST1_TAC;
 203         BY(FIRST_X_ASSUM_ST `DIV` MP_TAC THEN ARITH_TAC);
 204       BY(ASM_REWRITE_TAC[]);
 205     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'`);
 206     GMATCH_SIMP_TAC periodic_nk;
 207     BY(ASM_SIMP_TAC[arith `~(n=0) ==> (0 < n)`]);
 208   COMMENT "base case of induction completed, now induct step";
 209   REPEAT WEAK_STRIP_TAC;
 210   COMMENT "pick element in bad set";
 211   GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `?x. x IN bad_set cc'`) MP_TAC));
 212     REWRITE_TAC[MEMBER_NOT_EMPTY];
 213     REWRITE_TAC[GSYM HAS_SIZE_0];
 214     FIRST_X_ASSUM_ST `SUC` MP_TAC;
 215     REWRITE_TAC[HAS_SIZE];
 216     DISCH_THEN (unlist REWRITE_TAC);
 217     BY(ARITH_TAC);
 218   REPEAT WEAK_STRIP_TAC;
 219   COMMENT "construct reduced cc";
 220   ABBREV_TAC `n = cc_card_v9 cc' - 1`;
 221   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))`;
 222   ABBREV_TAC `cutb = \ (g:num->bool) j. if (0 = j MOD n) then g x else g (x + 1 + (j MOD n))`;
 223   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`];
 224   REPEAT WEAK_STRIP_TAC;
 225   GOAL_TERM (fun w -> (FIRST_X_ASSUM (MP_TAC o (ISPEC ( env w `cc''`)))));
 226   REWRITE_TAC[TAUT (`((x ==> ~y) ==> F) <=> x /\ y`)];
 227   COMMENT "size of n";
 228   SUBGOAL_THEN `~(cc_card_v9 cc'' = 0)` ASSUME_TAC;
 229     INTRO_TAC CC_CARD2 [`cc'`];
 230     ASM_REWRITE_TAC[];
 231     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 232   COMMENT "periodicity";
 233   GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!f. periodic (cutr f) n`) ASSUME_TAC));
 234     REWRITE_TAC[periodic];
 235     EXPAND_TAC "cutr";
 236     REPEAT WEAK_STRIP_TAC;
 237     SUBGOAL_THEN ` (i + n) MOD n = i MOD n` SUBST1_TAC;
 238       BY(MESON_TAC[MOD_MULT_ADD;arith `(i + n) = (1 * n + i)`]);
 239     BY(MESON_TAC[]);
 240   GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!g. periodic (cutb g) n`) ASSUME_TAC));
 241     REWRITE_TAC[periodic];
 242     EXPAND_TAC "cutb";
 243     REPEAT WEAK_STRIP_TAC;
 244     SUBGOAL_THEN ` (i + n) MOD n = i MOD n` SUBST1_TAC;
 245       BY(MESON_TAC[MOD_MULT_ADD;arith `(i + n) = (1 * n + i)`]);
 246     BY(MESON_TAC[]);
 247   (COMMENT "bad_set");
 248   SUBGOAL_THEN `BIJ (\j. j+ (x + 1)) (1..(n-1)) ((x+2)..(x+n))` ASSUME_TAC;
 249     REWRITE_TAC[BIJ;INJ];
 250     SUBCONJ_TAC;
 251       REWRITE_TAC[IN_NUMSEG];
 252       BY(ARITH_TAC);
 253     REPEAT WEAK_STRIP_TAC;
 254     REWRITE_TAC[SURJ];
 255     ASM_REWRITE_TAC[];
 256     REWRITE_TAC[IN_NUMSEG];
 257     REPEAT WEAK_STRIP_TAC;
 258     GOAL_TERM (fun w -> (EXISTS_TAC ( env w `x' - (x + 1)`)));
 259     REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
 260     BY(ARITH_TAC);
 261   SUBGOAL_THEN `1 <= n` ASSUME_TAC;
 262     INTRO_TAC (CC_CARD2) [`cc'`];
 263     ASM_REWRITE_TAC[];
 264     REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `x - 1` MP_TAC);
 265     BY(ARITH_TAC);
 266   SUBGOAL_THEN `!i. i IN 1..(n-1) ==> i MOD n = i` ASSUME_TAC;
 267     REWRITE_TAC[IN_NUMSEG];
 268     GEN_TAC;
 269     INTRO_TAC MOD_LT [`i`;`n`];
 270     BY(ARITH_TAC);
 271   GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!f. cutr f 0 = (f:num->real) x + f (x + 1)`) ASSUME_TAC));
 272     EXPAND_TAC "cutr";
 273     GMATCH_SIMP_TAC MOD_0;
 274     REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
 275     BY(ARITH_TAC);
 276   GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!g. cutb g 0 = (g:num->bool) x `) ASSUME_TAC));
 277     EXPAND_TAC "cutb";
 278     GMATCH_SIMP_TAC MOD_0;
 279     REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC);
 280     BY(ARITH_TAC);
 281   GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!i f. i IN 1..(n-1) ==> cutr f i = f (x + 1 + i)`) ASSUME_TAC));
 282     REPEAT WEAK_STRIP_TAC;
 283     EXPAND_TAC "cutr";
 284     GOAL_TERM (fun w -> (FIRST_X_ASSUM (MP_TAC o ISPEC ( env w `i`))));
 285     ASM_REWRITE_TAC[];
 286     DISCH_THEN SUBST1_TAC;
 287     COND_CASES_TAC;
 288       REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
 289       REWRITE_TAC[IN_NUMSEG];
 290       BY(ARITH_TAC);
 291     BY(REWRITE_TAC[]);
 292   GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `!i g. i IN 1..(n-1) ==> cutb g  i = g (x + 1 + i)`) ASSUME_TAC));
 293     REPEAT WEAK_STRIP_TAC;
 294     EXPAND_TAC "cutb";
 295     GOAL_TERM (fun w -> (FIRST_X_ASSUM_ST `MOD` (MP_TAC o ISPEC ( env w `i`))));
 296     ASM_REWRITE_TAC[];
 297     DISCH_THEN SUBST1_TAC;
 298     COND_CASES_TAC;
 299       REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
 300       REWRITE_TAC[IN_NUMSEG];
 301       BY(ARITH_TAC);
 302     BY(REWRITE_TAC[]);
 303   (COMMENT " NOT FINISHED TO HERE, 4 CONJUNCTS TO GO. ")
 304 (* NOT FINISHED *)
 305   ]);;
 306   (* }}} *)
 307 *)
 308
 309
 310
 311
 312
 313
 314
 315
 316