needs "../formal_lp/hypermap/ineqs/lp_gen_ineqs.hl";; needs "../formal_lp/hypermap/ineqs/lp_approx_ineqs.hl";; needs "../formal_lp/hypermap/ineqs/lp_ineqs_defs.hl";; needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";; needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs2-compiled.hl";; needs "../formal_lp/hypermap/ineqs/lp_main_estimate-compiled.hl";; needs "../formal_lp/hypermap/arith_link.hl";; module Lp_ineqs = struct open Lp_ineqs_proofs;; type raw_lp_ineq = { name : string; tm : term; proof: thm option; std_only: bool; };; type lp_ineq = { ineq_th : thm; pair_flag : bool; };; let raw_ineq_list, add_raw_ineq, find_raw_ineq = let table = ref [] in (fun () -> !table), (fun name std tm th -> table := {name = name; tm = tm; proof = th; std_only = std} :: !table), (fun std_flag name -> find (fun x -> x.name = name && x.std_only = std_flag) !table);; (* Combine all nonlinear inequalities related to linear programs into one definition *) let lp_ineqs_def = let check_lp_tags = let rec check tags = match tags with | Lp :: _ -> true | Tablelp :: _ -> true | Lp_aux _ :: _ -> true | h :: t -> check t | [] -> false in fun ineq -> check ineq.tags in let ineq_ids = ["6170936724"] in let lp_ineqs = filter (fun ineq -> check_lp_tags ineq or mem ineq.idv ineq_ids) !Ineq.ineqs in let lp_tms = setify (map (fun t -> t.ineq) lp_ineqs) in let lp_tm = end_itlist (curry mk_conj) lp_tms in new_definition (mk_eq (`lp_ineqs:bool`, lp_tm));; let add_lp_ineqs_hyp = let imp_th = (UNDISCH o MATCH_MP EQ_IMP) lp_ineqs_def in let ths = CONJUNCTS imp_th in fun th -> itlist PROVE_HYP ths th;; (* Replaces all general hypotheses with lp_cond *) let add_lp_hyp = let lp_fan_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL) Lp_ineqs_proofs.lp_fan in 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 let lp_main_estimate_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL) Lp_main_estimate.lp_main_estimate in fun lp_ineq_flag th -> let th' = (UNDISCH_ALL o SPEC_ALL) th in let th0 = if (not lp_ineq_flag) or is_forall (concl th') or is_binary "ALL" (concl th') then th' else th in let th1 = itlist PROVE_HYP lp_fan_ths th0 in let th2 = itlist PROVE_HYP lp_cond_ths th1 in let th3 = itlist PROVE_HYP lp_main_estimate_ths th2 in add_lp_ineqs_hyp th3;; let parse_lp_ineq s type_hints = let hints = map (fun var, ty -> var, pretype_of_type ty) type_hints in let ptm, l = (parse_preterm o lex o explode) s in if l = [] then (term_of_preterm o retypecheck hints) ptm else failwith "Unparsed input following term";; let add_lp_ineq_str (name, std_flag, s_tm, th) = let tm = parse_lp_ineq s_tm ["H", `:(A)hypermap`; "V", `:C->bool`; "node_mod", `:A->C`] in let proof = match th with | None -> None | Some th -> Some (PURE_REWRITE_RULE[GSYM IMP_IMP] (add_lp_hyp true th)) in add_raw_ineq name std_flag tm proof;; let mk_lp_ineq = let subst_list = [ `dart (H:(real^3#real^3)hypermap)`, `dart_of_fan (V:real^3->bool,E)`; `H:(real^3#real^3)hypermap`, `hypermap_of_fan (V:real^3->bool,E)`; `face_map (H:(real^3#real^3)hypermap)`, `f_fan_pair_ext (V:real^3->bool,E)`; `azim_mod:real^3#real^3->real`, `azim_dart (V:real^3->bool,E)`; `azim2_mod:real^3#real^3->real`, `azim2_fan (V:real^3->bool,E)`; `azim3_mod:real^3#real^3->real`, `azim3_fan (V:real^3->bool,E)`; `rhazim_mod:real^3#real^3->real`, `rhazim_fan (V:real^3->bool,E)`; `rhazim2_mod:real^3#real^3->real`, `rhazim2_fan (V:real^3->bool,E)`; `rhazim3_mod:real^3#real^3->real`, `rhazim3_fan (V:real^3->bool,E)`; `sol_mod:(real^3#real^3->bool)->real`, `sol_fan (V:real^3->bool,E)`; `tau_mod:(real^3#real^3->bool)->real`, `tau_fan (V:real^3->bool,E)`; `y1_mod:real^3#real^3->real`, `y1_fan`; `y2_mod:real^3#real^3->real`, `y2_fan`; `y3_mod:real^3#real^3->real`, `y3_fan (V,E)`; `y4_mod:real^3#real^3->real`, `y4_fan (V,E)`; `y5_mod:real^3#real^3->real`, `y5_fan (V,E)`; `y6_mod:real^3#real^3->real`, `y6_fan`; `y7_mod:real^3#real^3->real`, `y7_fan (V,E)`; `y8_mod:real^3#real^3->real`, `y8_fan (V,E)`; `y9_mod:real^3#real^3->real`, `y9_fan (V,E)`; `y4'_mod:real^3#real^3->real`, `y4'_fan (V,E)`; `ye_mod:real^3#real^3->real`, `ye_fan`; `yn_mod:real^3->real`, `yn_fan`; ] in fun ineq_th -> let proof = PURE_REWRITE_RULE[GSYM IMP_IMP] (add_lp_hyp true ineq_th) in let tm0 = concl proof in let tm1 = subst subst_list tm0 in tm1, proof;; let add_lp_ineq_th (name, std_flag, ineq_th) = let tm1, proof = mk_lp_ineq ineq_th in add_raw_ineq name std_flag tm1 (Some proof);; let gen_raw_ineq_data_str name std_flag str = let tm = parse_lp_ineq str ["H", `:(A)hypermap`; "V", `:C->bool`; "node_mod", `:A->C`] in {name = name; tm = tm; proof = None; std_only = std_flag};; let gen_raw_ineq_data name std_flag ineq_th = let tm1, proof = mk_lp_ineq ineq_th in {name = name; tm = tm1; proof = Some proof; std_only = std_flag};; (******************************) (* Generates a general form of an inequality *) let generate_ineq0 ineq = let th0 = Lp_gen_ineqs.generate_ineq ineq.tm in let th1 = add_lp_hyp true th0 in let proof = match ineq.proof with | Some th -> th | None -> TRUTH in PROVE_HYP proof th1;; let generate_ineq1 = let power_th = prove(`!f (x:A). (f POWER 2) x = f (f x) /\ (f POWER 3) x = f (f (f x))`, REWRITE_TAC[Hypermap.POWER_2; Hypermap.THREE; Hypermap.POWER; o_THM]) in let mk_list_th th = let tm, proof = mk_lp_ineq th in generate_ineq0 {name = "tmp"; std_only = false; tm = tm; proof = Some proof} in let strip_ALL th = let ltm, set_tm = dest_comb (concl th) in let p_tm = rand ltm in let var_tm, _ = dest_abs p_tm in let th1 = (BETA_RULE o SPEC var_tm o PURE_REWRITE_RULE[GSYM ALL_MEM]) th in let mem_tm = (fst o dest_imp o concl) th1 in UNDISCH th1, (var_tm, mem_tm) in let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty; `:num`, `:D`; `:real^3`, `:C`] o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP; RIGHT_IMP_FORALL_THM]) in let def_ths = let defs = map (fst o strip_ALL o mk_list_th) [y1_def; y2_def; y3_def; y4_def; y5_def; y6_def; y9_def] in let r = (fst o strip_ALL o add_lp_hyp true o REWRITE_RULE[GSYM IMP_IMP]) in let extra_defs = map r [ y8_list_def; y4'_list_def; y4'_list_f_def; y4'_list_inv_f_def; y4'_list_ff_def; y4'_list_fff_def; ] in extra_defs @ defs in let mem_ths = [ `MEM (d:num#num) (list_of_darts3 L)`, th_rule Lp_gen_theory.list_of_darts3_subset; `MEM (d:num#num) (list_of_darts4 L)`, th_rule Lp_gen_theory.list_of_darts4_subset; `MEM (d:num#num) (list_of_darts5 L)`, th_rule Lp_gen_theory.list_of_darts5_subset; `MEM (d:num#num) (list_of_darts6 L)`, th_rule Lp_gen_theory.list_of_darts6_subset; ] in let rec simplify tm = if is_imp tm then let ltm, q_tm = dest_comb tm in let imp_tm, p_tm = dest_comb ltm in let p_tm, q_tm = dest_imp tm in let p_th = (PURE_REWRITE_CONV def_ths THENC PURE_REWRITE_CONV[power_th]) p_tm in let q_th = simplify q_tm in MK_COMB (AP_TERM imp_tm p_th, q_th) else REFL tm in fun simplify_all_flag ineq -> let th1 = generate_ineq0 ineq in let th2, (var_tm, mem_tm) = strip_ALL th1 in let eq_th = if simplify_all_flag then (PURE_REWRITE_CONV def_ths THENC PURE_REWRITE_CONV[power_th]) (concl th2) else simplify (concl th2) in let th3 = EQ_MP eq_th th2 in let th4 = try let mem_th = assoc mem_tm mem_ths in PROVE_HYP mem_th th3 with Failure _ -> th3 in let th5 = (GEN var_tm o DISCH mem_tm) th4 in PURE_REWRITE_RULE[ALL_MEM] th5;; let generate_ineq = generate_ineq1 false;; let add_lp_list_ineq, find_ineq = let ineq_table = Array.init 8 (fun i -> Hashtbl.create 10) in let std_ineq_table = Array.init 8 (fun i -> Hashtbl.create 10) in let add std_flag i pair_flag name ineq_th = let table = if std_flag then std_ineq_table.(i) else ineq_table.(i) in Hashtbl.add table name {ineq_th = ineq_th; pair_flag = pair_flag} in let DECIMAL_INT = prove(`!n. DECIMAL n 1 = &n`, REWRITE_TAC[DECIMAL; REAL_DIV_1]) in let pos_thms = let inst = INST[`V:real^3->bool,E:(real^3->bool)->bool`, `fan:(real^3->bool)#((real^3->bool)->bool)`] in map inst Lp_ineqs_def.list_var_pos in let rec rewrite_num_conv real_flag tm = match tm with | Var _ -> REFL tm | Const _ -> REFL tm | Abs (v_tm, b_tm) -> ABS v_tm (rewrite_num_conv real_flag b_tm) | Comb (Const ("NUMERAL", _), _) -> Arith_nat.NUMERAL_TO_NUM_CONV tm | Comb (Const ("real_of_num", _) as ltm, rtm) -> if real_flag then AP_TERM ltm (rewrite_num_conv real_flag rtm) else REFL tm | Comb (Comb (Const ("DECIMAL", _), _), _) -> REFL tm | Comb (ltm, rtm) -> MK_COMB (rewrite_num_conv real_flag ltm, rewrite_num_conv real_flag rtm) in let rewrite_num ineq_th = let th1 = PURE_REWRITE_RULE[DECIMAL_INT] ineq_th in let imp_flag = (is_imp o snd o dest_abs o lhand o concl) th1 in if imp_flag then let th2 = PURE_REWRITE_RULE[IMP_IMP] th1 in let th3 = CONV_RULE ((LAND_CONV o ABS_CONV o RAND_CONV) (rewrite_num_conv true)) th2 in let th4 = CONV_RULE ((LAND_CONV o ABS_CONV o LAND_CONV) (rewrite_num_conv false)) th3 in PURE_REWRITE_RULE[GSYM IMP_IMP] th4 else CONV_RULE (rewrite_num_conv true) th1 in (* add_lp_list_ineq *) (fun (name, std_only, list_ineq_th) -> let approx_ths, neg_approx_ths = Lp_approx_ineqs.generate_ineqs pos_thms [3;4;5;6;7] list_ineq_th in let set_name = (fst o dest_const o rator o rand o concl o hd) approx_ths in let pair_flag, approx_ths, neg_approx_ths = if set_name = "list_dart_pairs" then let r = PURE_REWRITE_RULE[Lp_gen_theory.ALL_list_dart_pairs_split; BETA_THM; FST; SND] in true, map r approx_ths, map r neg_approx_ths else false, approx_ths, neg_approx_ths in let approx_ths = zip (3--7) approx_ths in let neg_approx_ths = if (neg_approx_ths = []) then [] else zip (3--7) neg_approx_ths in let r = rewrite_num in if std_only then let _ = map (fun (i, t) -> add true i pair_flag name (r t)) approx_ths in let _ = map (fun (i, t) -> add true i pair_flag (name^"_neg") (r t)) neg_approx_ths in () else let _ = map (fun (i, t) -> add false i pair_flag name (r t)) approx_ths in let _ = map (fun (i, t) -> add false i pair_flag (name^"_neg") (r t)) neg_approx_ths in ()), (* find_ineq *) (fun std_flag precision name -> if std_flag then try Hashtbl.find std_ineq_table.(precision) name with Not_found -> Hashtbl.find ineq_table.(precision) name else Hashtbl.find ineq_table.(precision) name);; (* Generates all list inequalities from raw inequalities *) let process_raw_ineqs = let report s = Format.print_string s; Format.print_newline(); Format.print_flush() in let counter = ref 0 and total = ref 0 in let process_ineq ineq = let _ = counter := !counter + 1 in let _ = report (sprintf "Processing: %s (%d / %d)" ineq.name !counter !total) in let th = generate_ineq ineq in add_lp_list_ineq (ineq.name, ineq.std_only, th) in fun () -> let ineqs = raw_ineq_list() in let _ = counter := 0 in let _ = total := length ineqs in let _ = map process_ineq (raw_ineq_list()) in ();; end;;