formal_lp/hypermap/main/test_ex2_complete.hl

   1 needs "../formal_lp/hypermap/main/prove_flyspeck_lp.hl";;
   2
   3 open Arith_misc;;
   4 open Linear_function;;
   5 open Prove_lp;;
   6 open Arith_nat;;
   7 open Misc_vars;;
   8 open List_hypermap_computations;;
   9 open List_conversions;;
  10 open Lp_approx_ineqs;;
  11 open Lp_ineqs;;
  12 open Lp_ineqs_proofs;;
  13 open Lp_main_estimate;;
  14 open Flyspeck_lp;;
  15
  16
  17 let split4_lemma = prove(`(a <= b /\ a <= sqrt8)
  18                            \/ (b <= a /\ b <= sqrt8)
  19                            \/ (a <= b /\ sqrt8 <= a /\ a <= &3)
  20                            \/ (b <= a /\ sqrt8 <= b /\ b <= &3)
  21                            \/ (&3 <= a /\ &3 <= b)`,
  22                          MP_TAC Flyspeck_constants.bounds THEN ARITH_TAC);;
  23
  24
  25 let split4_lemma' = INST[`ye_list (g:num#num->real^3#real^3) d1`, `a:real`;
  26                          `ye_list (g:num#num->real^3#real^3) d2`, `b:real`] split4_lemma;;
  27
  28 let d1_var = `d1:num#num` and
  29     d2_var = `d2:num#num`;;
  30
  31
  32 let rec assoc_all a list =
  33   match list with
  34     | [] -> []
  35     | (k,v) :: t -> if k = a then v :: assoc_all a t else assoc_all a t;;
  36
  37
  38 let gen_extra_ineqs =
  39   let tm_3 = `&3` and
  40       tm_sqrt8 = `sqrt8` in
  41   let r tm = prove(tm, MP_TAC Flyspeck_constants.bounds THEN ARITH_TAC) in
  42   let l_ths_list = [
  43     tm_3, r `&3 <= a ==> sqrt8 <= a`;
  44   ] in
  45   let r_ths_list = [
  46     tm_sqrt8, r `a <= sqrt8 ==> a <= &3`;
  47   ] in
  48   let a_var_real = `a:real` in
  49     fun ineq_th ->
  50       let lhs, rhs = dest_binary "real_le" (concl ineq_th) in
  51       let l_ths = map (fun th -> MP (INST[rhs, a_var_real] th) ineq_th) (assoc_all lhs l_ths_list) and
  52           r_ths = map (fun th -> MP (INST[lhs, a_var_real] th) ineq_th) (assoc_all rhs r_ths_list) in
  53         l_ths @ r_ths;;
  54
  55
  56 let dest_ye_list tm =
  57   let lhs, rhs = dest_comb tm in
  58   let c_tm = rator lhs in
  59     if (fst o dest_const) c_tm <> "ye_list" then
  60       failwith "dest_ye_list: not ye_list"
  61     else
  62       dest_pair rhs;;
  63
  64 let gen_ye_sym_ineqs ye_sym_th ineq_th =
  65   let sym_eqs tm =
  66     try
  67       let n_tm, m_tm = dest_ye_list tm in
  68         [REFL tm; INST[n_tm, n_var_num; m_tm, m_var_num] ye_sym_th]
  69     with Failure _ ->
  70       [REFL tm] in
  71   let ltm, rhs = dest_comb (concl ineq_th) in
  72   let op_tm, lhs = dest_comb ltm in
  73   let l_eqs = sym_eqs lhs and
  74       r_eqs = sym_eqs rhs in
  75     tl (allpairs (fun l_eq r_eq -> EQ_MP (MK_COMB (AP_TERM op_tm l_eq, r_eq)) ineq_th) l_eqs r_eqs);;
  76
  77
  78 let gen_all_extra_cases ye_sym_th case_tms =
  79   let case_ths = map ASSUME case_tms in
  80   let extra = List.flatten (map gen_extra_ineqs case_ths) in
  81   let sym = gen_ye_sym_ineqs ye_sym_th in
  82     extra @ List.flatten (map sym (case_ths @ extra));;
  83
  84
  85 let e_cap_var = `E:(real^3->bool)->bool`;;
  86 let lp_cond_imp_good_list = prove(`lp_cond (L, g, h:num->real^3) (V,E) ==> good_list L`, SIMP_TAC[lp_cond]);;
  87 let ye_sym0 = (add_lp_hyp false o prove)(`(!d. g d = h (FST d), h (SND d))
  88                                          ==> ye_list (g:num#num->real^3#real^3) (n,m) = ye_list g (m,n)`,
  89                                          DISCH_TAC THEN ASM_REWRITE_TAC Lp_ineqs_def.list_defs2 THEN
  90                                            REWRITE_TAC[Lp_ineqs_def.ye_fan; DIST_SYM]);;
  91
  92 let gen_list_ineq simplify_all_flag th =
  93   let th0 = add_lp_hyp true th in
  94   let tm1, proof_th = mk_lp_ineq th0 in
  95   let raw_data = {name = "tmp"; tm = tm1; proof = Some proof_th; std_only = false} in
  96     generate_ineq1 simplify_all_flag raw_data;;
  97
  98 let tau_split4 = gen_list_ineq false lp_tau_split4;;
  99 let diag4_lo = gen_list_ineq true dart4_y4'_lo;;
 100
 101
 102
 103 let get_all_ineqs hyp_set0 all_ineq_th =
 104   let all_tm, set_tm = dest_comb (concl all_ineq_th) in
 105   let set_eq_th = hyp_set0 ((fst o dest_const o rator) set_tm) in
 106   let ineq1_th = EQ_MP (AP_TERM all_tm set_eq_th) all_ineq_th in
 107     map MY_BETA_RULE (get_all ineq1_th);;
 108
 109
 110 let contravening_conditions hyp_list_tm hyp_set =
 111   let th0 = (MY_RULE_NUM o REWRITE_RULE[Seq.size]) contravening_lp_cond_alt in
 112   let th1 = (UNDISCH_ALL o  ISPEC hyp_list_tm o REWRITE_RULE[GSYM IMP_IMP]) th0 in
 113   let good_list_nodes_th = EQT_ELIM (eval_good_list_nodes_condition hyp_set) in
 114   let lp_cond_th = (MY_PROVE_HYP (hyp_set "good_list") o MY_PROVE_HYP good_list_nodes_th) th1 in
 115   let lp_cond_th' = (SELECT_AND_ABBREV_RULE o SELECT_AND_ABBREV_RULE o ABBREV_RULE "L" hyp_list_tm) lp_cond_th in
 116   let lp_tau_th = (UNDISCH_ALL o SPEC_ALL) contravening_lp_tau in
 117     lp_cond_th', lp_tau_th;;
 118
 119
 120 let split_conditions hyp_list_tm d_tm lp_cond0_th =
 121   let split_eq_th = (ABBREV_RULE "L" hyp_list_tm) (eval_split_list_hyp hyp_list_tm d_tm) in
 122   let split_tm = (rand o concl) split_eq_th in
 123   let lp_cond2_th = (PURE_REWRITE_RULE[split_eq_th] o SPEC d_tm o MATCH_MP lp_cond_trans1) lp_cond0_th in
 124   let e2_tm = (rand o rand o concl) lp_cond2_th in
 125   let lp_cond2_th' = (ABBREV_RULE "L2" split_tm) lp_cond2_th in
 126 (*
 127 let good2_th = MATCH_MP lp_cond_imp_good_list lp_cond2_th;;
 128 let hyp2_set, hyp2_fun = compute_all split_tm (Some good2_th);;
 129 *)
 130   let hyp2_set, hyp2_fun = compute_all split_tm None in
 131     lp_cond2_th', split_eq_th, split_tm, e2_tm, (hyp2_set, hyp2_fun);;
 132
 133
 134 (******************************)
 135 (* Load data *)
 136 loadt "../formal_lp/glpk/ex2/bb2_1_out.hl";;
 137 let p1, c1, t1, v1 = precision, constraints, target_variables, variable_bounds;;
 138
 139 loadt "../formal_lp/glpk/ex2/bb2_2_out.hl";;
 140 let p2, c2, t2, v2 = precision, constraints, target_variables, variable_bounds;;
 141
 142 loadt "../formal_lp/glpk/ex2/bb2_3_out.hl";;
 143 let p3, c3, t3, v3 = precision, constraints, target_variables, variable_bounds;;
 144
 145 loadt "../formal_lp/glpk/ex2/bb2_4_out.hl";;
 146 let p4, c4, t4, v4 = precision, constraints, target_variables, variable_bounds;;
 147
 148 loadt "../formal_lp/glpk/ex2/bb2_5_out.hl";;
 149 let p5, c5, t5, v5 = precision, constraints, target_variables, variable_bounds;;
 150
 151
 152 (******************************)
 153 (* Compute preliminary data *)
 154 let hyp_list0_tm = (to_num o create_hol_list_str) hypermap_string;;
 155 let hyp_set0, hyp_fun0 = compute_all hyp_list0_tm None;;
 156
 157 let d13 = to_num `1,2` and
 158     d24 = to_num `0,1`;;
 159
 160 let lp_cond0, lp_tau0 = contravening_conditions hyp_list0_tm hyp_set0;;
 161 let ye_sym_th = (MY_PROVE_HYP lp_cond0 o INST[`ESTD V`, e_cap_var]) ye_sym0;;
 162
 163 let ye_hi_3 = generate_ineq (find_raw_ineq true "ye_hi");;
 164 let ye_hi_2h0 = generate_ineq (find_raw_ineq true "yy10");;
 165
 166 let ye_ineqs_3, ye_ineqs_2h0, diag4_ineqs, tau_ths =
 167   let estd_refl = REFL `ESTD V` in
 168   let r = get_all_ineqs hyp_set0 o EXPAND_CONCL_RULE "L" o
 169     MY_PROVE_HYP lp_tau0 o MY_PROVE_HYP lp_cond0 o MY_PROVE_HYP estd_refl o INST[`ESTD V`, e_cap_var] in
 170     r ye_hi_3, r ye_hi_2h0, r diag4_lo, r tau_split4;;
 171
 172
 173 let diag4_ths = map (fun th -> EQ_MP (convert_tm hyp_fun0 (concl th)) th) diag4_ineqs;;
 174 let tau_ths2 = map (UNDISCH_ALL o simplify_ineq hyp_fun0) ((fst o chop_list 2) tau_ths);;
 175 let tau_split13 = List.nth tau_ths2 1;;
 176 let tau_split24 = List.nth tau_ths2 0;;
 177
 178 let base_ineqs = ye_ineqs_3 @ ye_ineqs_2h0 @ diag4_ths;;
 179
 180
 181 (******************************)
 182 (* case 1 *)
 183 let lp_cond1, split1_eq, hyp_list1_tm, e1_tm, (hyp1_set, hyp1_fun) = split_conditions hyp_list0_tm d13 lp_cond0;;
 184
 185 let lp1_th0 = prove_flyspeck_lp_step1 hyp_list1_tm hyp1_set hyp1_fun false p1 c1 t1 v1;;
 186 let lp1_th1 = (MY_PROVE_HYP tau_split13 o INST[e1_tm, e_cap_var]) lp1_th0;;
 187 let lp1_th2 = itlist MY_PROVE_HYP base_ineqs lp1_th1;;
 188
 189 let case1_th = (EXPAND_RULE "L2" o MY_PROVE_HYP lp_cond1 o INST[e1_tm, e_cap_var] o ABBREV_RULE "L2" hyp_list1_tm) lp1_th2;;
 190
 191
 192 (******************************)
 193 (* case 2 *)
 194 let lp_cond2, split2_eq, hyp_list2_tm, e2_tm, (hyp2_set, hyp2_fun) = split_conditions hyp_list0_tm d24 lp_cond0;;
 195
 196 let lp2_th0 = prove_flyspeck_lp_step1 hyp_list2_tm hyp2_set hyp2_fun false p2 c2 t2 v2;;
 197 let lp2_th1 = (MY_PROVE_HYP tau_split24 o INST[e2_tm, e_cap_var]) lp2_th0;;
 198 let lp2_th2 = itlist MY_PROVE_HYP base_ineqs lp2_th1;;
 199
 200 let case2_th = (EXPAND_RULE "L2" o MY_PROVE_HYP lp_cond2 o INST[e2_tm, e_cap_var] o ABBREV_RULE "L2" hyp_list2_tm) lp2_th2;;
 201
 202
 203 (******************************)
 204 (* case 3 *)
 205 let lp_cond3, split3_eq, hyp_list3_tm, e3_tm, (hyp3_set, hyp3_fun) = split_conditions hyp_list0_tm d13 lp_cond0;;
 206
 207 let lp3_th0 = prove_flyspeck_lp_step1 hyp_list3_tm hyp3_set hyp3_fun false p3 c3 t3 v3;;
 208 let lp3_th1 = (MY_PROVE_HYP tau_split13 o INST[e3_tm, e_cap_var]) lp3_th0;;
 209 let lp3_th2 = itlist MY_PROVE_HYP base_ineqs lp3_th1;;
 210
 211 let case3_th = (EXPAND_RULE "L2" o MY_PROVE_HYP lp_cond3 o INST[e2_tm, e_cap_var] o ABBREV_RULE "L2" hyp_list3_tm) lp3_th2;;
 212
 213
 214 (******************************)
 215 (* case 4 *)
 216 let lp_cond4, split4_eq, hyp_list4_tm, e4_tm, (hyp4_set, hyp4_fun) = split_conditions hyp_list0_tm d24 lp_cond0;;
 217
 218 let lp4_th0 = prove_flyspeck_lp_step1 hyp_list4_tm hyp4_set hyp4_fun false p4 c4 t4 v4;;
 219 let lp4_th1 = (MY_PROVE_HYP tau_split24 o INST[e2_tm, e_cap_var]) lp4_th0;;
 220 let lp4_th2 = itlist MY_PROVE_HYP base_ineqs lp4_th1;;
 221
 222 let case4_th = (EXPAND_RULE "L2" o MY_PROVE_HYP lp_cond4 o INST[e4_tm, e_cap_var] o ABBREV_RULE "L2" hyp_list4_tm) lp4_th2;;
 223
 224
 225 (******************************)
 226 (* case 5 *)
 227 let lp5_th0 = prove_flyspeck_lp_step1 hyp_list0_tm hyp_set0 hyp_fun0 true p5 c5 t5 v5;;
 228 let lp5_th1 = (MY_PROVE_HYP (REFL `ESTD V`) o INST [`ESTD V`, e_cap_var]) lp5_th0;;
 229 let lp5_th2 = (MY_PROVE_HYP lp_tau0 o MY_PROVE_HYP lp_cond0 o ABBREV_RULE "L" hyp_list0_tm) lp5_th1;;
 230
 231 let case5_th = lp5_th2;;
 232
 233
 234 (******************************)
 235 (* combine all cases *)
 236
 237 let diag2 = to_num `1,3`;;
 238 let diag1 = to_num `0,2`;;
 239
 240 let split_th = INST[diag1, d1_var; diag2, d2_var] split4_lemma';;
 241 let split_cases = striplist dest_disj (concl split_th);;
 242
 243 let case1_tms = striplist dest_conj (List.nth split_cases 0);;
 244 map concl (gen_all_extra_cases ye_sym_th case1_tms);;
 245 let case1_th2 = itlist MY_PROVE_HYP (gen_all_extra_cases ye_sym_th case1_tms) case1_th;;
 246 let case1_th_final = PURE_ONCE_REWRITE_RULE[IMP_IMP] (itlist DISCH case1_tms case1_th2);;
 247
 248 let get_final_case_th ye_sym_th n case_th cases =
 249   let case_tms = striplist dest_conj (List.nth cases n) in
 250   let case_th2 = itlist MY_PROVE_HYP (gen_all_extra_cases ye_sym_th case_tms) case_th in
 251     PURE_REWRITE_RULE[IMP_IMP; GSYM CONJ_ASSOC] (itlist DISCH case_tms case_th2);;
 252
 253 let case1_th_final = get_final_case_th ye_sym_th 0 case1_th split_cases;;
 254 let case2_th_final = get_final_case_th ye_sym_th 1 case2_th split_cases;;
 255 let case3_th_final = get_final_case_th ye_sym_th 2 case3_th split_cases;;
 256 let case4_th_final = get_final_case_th ye_sym_th 3 case4_th split_cases;;
 257 let case5_th_final = get_final_case_th ye_sym_th 4 case5_th split_cases;;
 258
 259 let combine_cases =
 260   let combine_th = TAUT `(A ==> C) /\ (B ==> C) ==> (A \/ B ==> C)` in
 261     fun case1_th case2_th ->
 262       MATCH_MP combine_th (CONJ case1_th case2_th);;
 263
 264
 265 let final' = itlist combine_cases [case1_th_final; case2_th_final; case3_th_final; case4_th_final] case5_th_final;;
 266 let final = (DISCH `contravening V` o EXPAND_RULE "g" o EXPAND_RULE "h" o EXPAND_RULE "L") (MP final' split_th);;