formal_lp/hypermap/ineqs/lp_ineqs.hl

   1 needs "../formal_lp/hypermap/ineqs/lp_gen_ineqs.hl";;
   2 needs "../formal_lp/hypermap/ineqs/lp_approx_ineqs.hl";;
   3 needs "../formal_lp/hypermap/ineqs/lp_ineqs_defs.hl";;
   4 needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";;
   5 needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs2-compiled.hl";;
   6 needs "../formal_lp/hypermap/ineqs/lp_main_estimate-compiled.hl";;
   7 needs "../formal_lp/hypermap/arith_link.hl";;
   8
   9 module Lp_ineqs = struct
  10
  11 open Lp_ineqs_proofs;;
  12
  13 type raw_lp_ineq = {
  14   name : string;
  15   tm : term;
  16   proof: thm option;
  17   std_only: bool;
  18 };;
  19
  20
  21 type lp_ineq = {
  22   ineq_th : thm;
  23   pair_flag : bool;
  24 };;
  25
  26
  27 let raw_ineq_list, add_raw_ineq, find_raw_ineq =
  28   let table = ref [] in
  29     (fun () -> !table),
  30   (fun name std tm th ->
  31      table := {name = name; tm = tm; proof = th; std_only = std} :: !table),
  32   (fun std_flag name -> find (fun x -> x.name = name && x.std_only = std_flag) !table);;
  33
  34
  35 (* Combine all nonlinear inequalities related to linear programs into one definition *)
  36 let lp_ineqs_def =
  37   let check_lp_tags =
  38     let rec check tags =
  39       match tags with
  40         | Lp :: _ -> true
  41         | Tablelp :: _ -> true
  42         | Lp_aux _ :: _ -> true
  43         | h :: t -> check t
  44         | [] -> false in
  45       fun ineq -> check ineq.tags in
  46   let ineq_ids = ["6170936724"] in
  47   let lp_ineqs = filter (fun ineq -> check_lp_tags ineq or mem ineq.idv ineq_ids) !Ineq.ineqs in
  48   let lp_tms = setify (map (fun t -> t.ineq) lp_ineqs) in
  49   let lp_tm = end_itlist (curry mk_conj) lp_tms in
  50     new_definition (mk_eq (`lp_ineqs:bool`, lp_tm));;
  51
  52
  53 let add_lp_ineqs_hyp =
  54   let imp_th = (UNDISCH o MATCH_MP EQ_IMP) lp_ineqs_def in
  55   let ths = CONJUNCTS imp_th in
  56     fun th ->
  57       itlist PROVE_HYP ths th;;
  58
  59
  60 (* Replaces all general hypotheses with lp_cond *)
  61 let add_lp_hyp =
  62   let lp_fan_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL) Lp_ineqs_proofs.lp_fan in
  63   let lp_cond_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL o INST_TYPE[`:num`, aty]) Lp_ineqs_proofs.lp_cond in
  64   let lp_main_estimate_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL) Lp_main_estimate.lp_main_estimate in
  65     fun lp_ineq_flag th ->
  66       let th' = (UNDISCH_ALL o SPEC_ALL) th in
  67       let th0 = if (not lp_ineq_flag) or is_forall (concl th') or is_binary "ALL" (concl th') then th' else th in
  68       let th1 = itlist PROVE_HYP lp_fan_ths th0 in
  69       let th2 = itlist PROVE_HYP lp_cond_ths th1 in
  70           let th3 = itlist PROVE_HYP lp_main_estimate_ths th2 in
  71                 add_lp_ineqs_hyp th3;;
  72
  73
  74 let parse_lp_ineq s type_hints =
  75   let hints = map (fun var, ty -> var, pretype_of_type ty) type_hints in
  76   let ptm, l = (parse_preterm o lex o explode) s in
  77     if l = [] then
  78       (term_of_preterm o retypecheck hints) ptm
  79     else
  80       failwith "Unparsed input following term";;
  81
  82
  83 let add_lp_ineq_str (name, std_flag, s_tm, th) =
  84   let tm = parse_lp_ineq s_tm ["H", `:(A)hypermap`; "V", `:C->bool`; "node_mod", `:A->C`] in
  85   let proof = match th with
  86     | None -> None
  87     | Some th -> Some (PURE_REWRITE_RULE[GSYM IMP_IMP] (add_lp_hyp true th)) in
  88     add_raw_ineq name std_flag tm proof;;
  89
  90
  91 let mk_lp_ineq =
  92   let subst_list = [
  93     `dart (H:(real^3#real^3)hypermap)`, `dart_of_fan (V:real^3->bool,E)`;
  94     `H:(real^3#real^3)hypermap`, `hypermap_of_fan (V:real^3->bool,E)`;
  95     `face_map (H:(real^3#real^3)hypermap)`, `f_fan_pair_ext (V:real^3->bool,E)`;
  96     `azim_mod:real^3#real^3->real`, `azim_dart (V:real^3->bool,E)`;
  97     `azim2_mod:real^3#real^3->real`, `azim2_fan (V:real^3->bool,E)`;
  98     `azim3_mod:real^3#real^3->real`, `azim3_fan (V:real^3->bool,E)`;
  99     `rhazim_mod:real^3#real^3->real`, `rhazim_fan (V:real^3->bool,E)`;
 100     `rhazim2_mod:real^3#real^3->real`, `rhazim2_fan (V:real^3->bool,E)`;
 101     `rhazim3_mod:real^3#real^3->real`, `rhazim3_fan (V:real^3->bool,E)`;
 102     `sol_mod:(real^3#real^3->bool)->real`, `sol_fan (V:real^3->bool,E)`;
 103     `tau_mod:(real^3#real^3->bool)->real`, `tau_fan (V:real^3->bool,E)`;
 104     `y1_mod:real^3#real^3->real`, `y1_fan`;
 105     `y2_mod:real^3#real^3->real`, `y2_fan`;
 106     `y3_mod:real^3#real^3->real`, `y3_fan (V,E)`;
 107     `y4_mod:real^3#real^3->real`, `y4_fan (V,E)`;
 108     `y5_mod:real^3#real^3->real`, `y5_fan (V,E)`;
 109     `y6_mod:real^3#real^3->real`, `y6_fan`;
 110     `y7_mod:real^3#real^3->real`, `y7_fan (V,E)`;
 111     `y8_mod:real^3#real^3->real`, `y8_fan (V,E)`;
 112     `y9_mod:real^3#real^3->real`, `y9_fan (V,E)`;
 113     `y4'_mod:real^3#real^3->real`, `y4'_fan (V,E)`;
 114     `ye_mod:real^3#real^3->real`, `ye_fan`;
 115     `yn_mod:real^3->real`, `yn_fan`;
 116   ] in
 117     fun ineq_th ->
 118       let proof = PURE_REWRITE_RULE[GSYM IMP_IMP] (add_lp_hyp true ineq_th) in
 119       let tm0 = concl proof in
 120       let tm1 = subst subst_list tm0 in
 121         tm1, proof;;
 122
 123
 124 let add_lp_ineq_th (name, std_flag, ineq_th) =
 125   let tm1, proof = mk_lp_ineq ineq_th in
 126     add_raw_ineq name std_flag tm1 (Some proof);;
 127
 128 let gen_raw_ineq_data_str name std_flag str =
 129   let tm = parse_lp_ineq str ["H", `:(A)hypermap`; "V", `:C->bool`; "node_mod", `:A->C`] in
 130     {name = name; tm = tm; proof = None; std_only = std_flag};;
 131
 132 let gen_raw_ineq_data name std_flag ineq_th =
 133   let tm1, proof = mk_lp_ineq ineq_th in
 134     {name = name; tm = tm1; proof = Some proof; std_only = std_flag};;
 135
 136 (******************************)
 137
 138
 139 (* Generates a general form of an inequality *)
 140 let generate_ineq0 ineq =
 141   let th0 = Lp_gen_ineqs.generate_ineq ineq.tm in
 142   let th1 = add_lp_hyp true th0 in
 143   let proof =
 144     match ineq.proof with
 145       | Some th -> th
 146       | None -> TRUTH in
 147     PROVE_HYP proof th1;;
 148
 149
 150 let generate_ineq1 =
 151   let power_th = prove(`!f (x:A). (f POWER 2) x = f (f x) /\ (f POWER 3) x = f (f (f x))`,
 152                        REWRITE_TAC[Hypermap.POWER_2; Hypermap.THREE; Hypermap.POWER; o_THM]) in
 153
 154   let mk_list_th th =
 155     let tm, proof = mk_lp_ineq th in
 156       generate_ineq0 {name = "tmp"; std_only = false; tm = tm; proof = Some proof} in
 157
 158   let strip_ALL th =
 159     let ltm, set_tm = dest_comb (concl th) in
 160     let p_tm = rand ltm in
 161     let var_tm, _ = dest_abs p_tm in
 162     let th1 = (BETA_RULE o SPEC var_tm o PURE_REWRITE_RULE[GSYM ALL_MEM]) th in
 163     let mem_tm = (fst o dest_imp o concl) th1 in
 164       UNDISCH th1, (var_tm, mem_tm) in
 165
 166   let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty; `:num`, `:D`; `:real^3`, `:C`] o
 167                    SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP; RIGHT_IMP_FORALL_THM]) in
 168
 169   let def_ths =
 170     let defs =
 171       map (fst o strip_ALL o mk_list_th)
 172         [y1_def; y2_def; y3_def; y4_def; y5_def; y6_def; y9_def] in
 173     let r = (fst o strip_ALL o add_lp_hyp true o REWRITE_RULE[GSYM IMP_IMP]) in
 174     let extra_defs = map r
 175       [
 176         y8_list_def; y4'_list_def; y4'_list_f_def;
 177         y4'_list_inv_f_def; y4'_list_ff_def; y4'_list_fff_def;
 178       ] in
 179       extra_defs @ defs in
 180
 181   let mem_ths =
 182     [
 183       `MEM (d:num#num) (list_of_darts3 L)`, th_rule Lp_gen_theory.list_of_darts3_subset;
 184       `MEM (d:num#num) (list_of_darts4 L)`, th_rule Lp_gen_theory.list_of_darts4_subset;
 185       `MEM (d:num#num) (list_of_darts5 L)`, th_rule Lp_gen_theory.list_of_darts5_subset;
 186       `MEM (d:num#num) (list_of_darts6 L)`, th_rule Lp_gen_theory.list_of_darts6_subset;
 187     ] in
 188
 189   let rec simplify tm =
 190     if is_imp tm then
 191       let ltm, q_tm = dest_comb tm in
 192       let imp_tm, p_tm = dest_comb ltm in
 193       let p_tm, q_tm = dest_imp tm in
 194       let p_th = (PURE_REWRITE_CONV def_ths THENC PURE_REWRITE_CONV[power_th]) p_tm in
 195       let q_th = simplify q_tm in
 196         MK_COMB (AP_TERM imp_tm p_th, q_th)
 197     else
 198       REFL tm in
 199
 200     fun simplify_all_flag ineq ->
 201       let th1 = generate_ineq0 ineq in
 202       let th2, (var_tm, mem_tm) = strip_ALL th1 in
 203       let eq_th =
 204         if simplify_all_flag then
 205           (PURE_REWRITE_CONV def_ths THENC PURE_REWRITE_CONV[power_th]) (concl th2)
 206         else
 207           simplify (concl th2) in
 208       let th3 = EQ_MP eq_th th2 in
 209       let th4 =
 210         try
 211           let mem_th = assoc mem_tm mem_ths in
 212             PROVE_HYP mem_th th3
 213         with Failure _ -> th3 in
 214       let th5 = (GEN var_tm o DISCH mem_tm) th4 in
 215         PURE_REWRITE_RULE[ALL_MEM] th5;;
 216
 217 let generate_ineq = generate_ineq1 false;;
 218
 219 let add_lp_list_ineq, find_ineq =
 220   let ineq_table = Array.init 8 (fun i -> Hashtbl.create 10) in
 221   let std_ineq_table = Array.init 8 (fun i -> Hashtbl.create 10) in
 222   let add std_flag i pair_flag name ineq_th =
 223     let table = if std_flag then std_ineq_table.(i) else ineq_table.(i) in
 224       Hashtbl.add table name {ineq_th = ineq_th; pair_flag = pair_flag} in
 225   let DECIMAL_INT = prove(`!n. DECIMAL n 1 = &n`, REWRITE_TAC[DECIMAL; REAL_DIV_1]) in
 226
 227   let pos_thms =
 228     let inst = INST[`V:real^3->bool,E:(real^3->bool)->bool`, `fan:(real^3->bool)#((real^3->bool)->bool)`] in
 229       map inst Lp_ineqs_def.list_var_pos in
 230
 231   let rec rewrite_num_conv real_flag tm =
 232     match tm with
 233       | Var _ -> REFL tm
 234       | Const _ -> REFL tm
 235       | Abs (v_tm, b_tm) ->
 236           ABS v_tm (rewrite_num_conv real_flag b_tm)
 237       | Comb (Const ("NUMERAL", _), _) ->
 238           Arith_nat.NUMERAL_TO_NUM_CONV tm
 239       | Comb (Const ("real_of_num", _) as ltm, rtm) ->
 240           if real_flag then
 241             AP_TERM ltm (rewrite_num_conv real_flag rtm)
 242           else
 243             REFL tm
 244       | Comb (Comb (Const ("DECIMAL", _), _), _) ->
 245           REFL tm
 246       | Comb (ltm, rtm) ->
 247           MK_COMB (rewrite_num_conv real_flag ltm, rewrite_num_conv real_flag rtm) in
 248
 249   let rewrite_num ineq_th =
 250     let th1 = PURE_REWRITE_RULE[DECIMAL_INT] ineq_th in
 251     let imp_flag = (is_imp o snd o dest_abs o lhand o concl) th1 in
 252       if imp_flag then
 253         let th2 = PURE_REWRITE_RULE[IMP_IMP] th1 in
 254         let th3 = CONV_RULE ((LAND_CONV o ABS_CONV o RAND_CONV) (rewrite_num_conv true)) th2 in
 255         let th4 = CONV_RULE ((LAND_CONV o ABS_CONV o LAND_CONV) (rewrite_num_conv false)) th3 in
 256           PURE_REWRITE_RULE[GSYM IMP_IMP] th4
 257       else
 258         CONV_RULE (rewrite_num_conv true) th1 in
 259
 260     (* add_lp_list_ineq *)
 261     (fun (name, std_only, list_ineq_th) ->
 262        let approx_ths, neg_approx_ths = Lp_approx_ineqs.generate_ineqs pos_thms [3;4;5;6;7] list_ineq_th in
 263        let set_name = (fst o dest_const o rator o rand o concl o hd) approx_ths in
 264        let pair_flag, approx_ths, neg_approx_ths =
 265          if set_name = "list_dart_pairs" then
 266            let r = PURE_REWRITE_RULE[Lp_gen_theory.ALL_list_dart_pairs_split; BETA_THM; FST; SND] in
 267              true, map r approx_ths, map r neg_approx_ths
 268          else
 269            false, approx_ths, neg_approx_ths in
 270        let approx_ths = zip (3--7) approx_ths in
 271        let neg_approx_ths = if (neg_approx_ths = []) then [] else zip (3--7) neg_approx_ths in
 272
 273        let r = rewrite_num in
 274          if std_only then
 275            let _ = map (fun (i, t) -> add true i pair_flag name (r t)) approx_ths in
 276            let _ = map (fun (i, t) -> add true i pair_flag (name^"_neg") (r t)) neg_approx_ths in
 277              ()
 278          else
 279            let _ = map (fun (i, t) -> add false i pair_flag name (r t)) approx_ths in
 280            let _ = map (fun (i, t) -> add false i pair_flag (name^"_neg") (r t)) neg_approx_ths in
 281              ()),
 282
 283   (* find_ineq *)
 284   (fun std_flag precision name ->
 285      if std_flag then
 286        try
 287          Hashtbl.find std_ineq_table.(precision) name
 288        with Not_found -> Hashtbl.find ineq_table.(precision) name
 289      else
 290        Hashtbl.find ineq_table.(precision) name);;
 291
 292
 293 (* Generates all list inequalities from raw inequalities *)
 294 let process_raw_ineqs =
 295   let report s =
 296     Format.print_string s; Format.print_newline(); Format.print_flush() in
 297   let counter = ref 0 and
 298       total = ref 0 in
 299
 300   let process_ineq ineq =
 301     let _ = counter := !counter + 1 in
 302     let _ = report (sprintf "Processing: %s (%d / %d)" ineq.name !counter !total) in
 303     let th = generate_ineq ineq in
 304       add_lp_list_ineq (ineq.name, ineq.std_only, th) in
 305
 306     fun () ->
 307       let ineqs = raw_ineq_list() in
 308       let _ = counter := 0 in
 309       let _ = total := length ineqs in
 310       let _ = map process_ineq (raw_ineq_list()) in
 311         ();;
 312
 313 end;;
 314