needs "verifier/m_verifier_main.hl";;

needs "nonlinear/lemma.hl";;
needs "nonlinear/functional_equation.hl";;
needs "nonlinear/ineq.hl";;

needs "nonlinear/prep.hl";;
let add_inequality = Prep.add_inequality;;
let find_ineqs idv = filter (fun t -> (String.length idv <= String.length t.idv) &&
			     (String.sub t.idv 0 (String.length idv) = idv)) (!Prep.prep_ineqs);;

needs "nonlinear/formal_tests/ineq_ids.hl";;

needs "nonlinear/formal_tests/hminus.hl";;


open M_verifier_main;;
open Sphere;;

(*************************)

let dih_x_pos_eq = 
prove (`let d_x4 = delta_x4 x1 x2 x3 x4 x5 x6 in let d = delta_x x1 x2 x3 x4 x5 x6 in &0 < x1 /\ &0 < d ==> dih_x x1 x2 x3 x4 x5 x6 = pi / &2 + atn(--d_x4 / sqrt (&4 * x1 * d))`,
REPEAT (CONV_TAC let_CONV) THEN STRIP_TAC THEN REWRITE_TAC[dih_x] THEN CONV_TAC (DEPTH_CONV let_CONV) THEN new_rewrite [] [] Trigonometry1.ATN2_BREAKDOWN THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SQRT_POS_LT THEN MATCH_MP_TAC REAL_LT_MUL THEN STRIP_TAC THENL [ REAL_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]);;
let arclength_pos_eq = 
prove(`&0 < ups_x (a * a) (b * b) (c * c) ==> arclength a b c = pi / &2 + atn ((c * c - a * a - b * b) / sqrt (ups_x (a * a) (b * b) (c * c)))`,
STRIP_TAC THEN REWRITE_TAC[arclength] THEN new_rewrite [] [] Trigonometry1.ATN2_BREAKDOWN THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);;
let sqrt_pos_eq = 
prove(`&0 < x ==> sqrt x * sqrt x = x`,
DISCH_TAC THEN REWRITE_TAC[GSYM REAL_POW_2] THEN MATCH_MP_TAC SQRT_POW_2 THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]);;
let ineqs = let dummy = `ineq [] (P \/ Q)` in let find id = let data = find_ineqs id in (snd o strip_forall) (if data = [] then dummy else (hd data).ineq) in let all_ineqs = map (fun id, t -> find id, (id, t)) ineq_ids in let filter1 = filter (fun ineq, _ -> not (is_disj (rand ineq))) all_ineqs in filter (fun ineq, _ -> not (is_binary "real_le" (rand ineq))) filter1;; (* 195 *) length ineqs;; let get_constants tm = let rec find tm = match tm with | Const _ -> [tm] | Comb (tm1, tm2) -> find tm1 @ find tm2 | Abs (_, tm2) -> find tm2 | _ -> [] in setify (find tm);; let ineqs = let c1 = "asn797k" and c2 = "asnFnhk" in filter (fun ineq, _ -> let cs = get_constants ineq in let l = map (fst o dest_const) cs in not (mem c1 l or mem c2 l)) ineqs;; let consts = end_itlist union (map (get_constants o fst) ineqs);; (* 193 *) length ineqs;; let all_ids = map (fst o snd) ineqs;; open Functional_equation;; open Nonlinear_lemma;; let flyspeck_defs = [ gamma3f_x_div_sqrtdelta; promote_pow3; proj_x1; proj_x2; proj_x3; proj_x4; proj_x5; proj_x6; delta_x4; delta_x; eulerA_x; num1; acs_sqrt_x1_d4; arclength_x_123; arc_hhn; arclength_x1; lfun_y1; gchi1_x; rhazim2_x; rhazim3_x; rhazim_x; taum_sub345_x; dih4_x; halfbump_x1; halfbump_x4; gchi2_x; gchi3_x; gchi4_x; gchi5_x; gchi6_x; sqrt8; vol_x; dih2_x; dih3_x; sqrt_x1; sqrt_x2; sqrt_x3; sqrt_x4; sqrt_x5; sqrt_x6; rad2_x; unit6; promote1_to_6; mm1; mm2; arclength_y1; h0; lfun; rhazim2; rhazim3; taum_x; rhazim; halfbump_x; dih4_y; dih5_x; dih6_x; gchi; sol_y; rho_x; sol0; tau0; node2_y; node3_y; rho; bump; dih5_y; dih6_y; dih_y; ly; interp; hplus; ups_x; GSYM sol0_over_pi_EQ_const1; ];; let cond_defs = let conv = UNDISCH_ALL o CONV_RULE (DEPTH_CONV let_CONV) in map conv [ dih_x_pos_eq; arclength_pos_eq ];; (* A temporary cheating *) let cond_defs = let conv = UNDISCH_ALL o CONV_RULE (DEPTH_CONV let_CONV) in let conv = Hol.new_axiom o concl o conv in map conv [ dih_x_pos_eq; arclength_pos_eq; sqrt_pos_eq; ];; let ineq_conv = REWRITE_CONV[Sphere.ineq; IMP_IMP] THENC REWRITE_CONV flyspeck_defs THENC DEPTH_CONV let_CONV THENC REWRITE_CONV cond_defs THENC REWRITE_CONV flyspeck_defs;; (* let consts2 = end_itlist union (map (get_constants o rand o concl o ineq_conv o fst) ineqs);; *) let verify_all pp ineqs = let n = length ineqs in let k = ref 0 in let verify ineq_tm = let _ = k := !k + 1 in let _ = report (sprintf "Verifying: %d/%d" !k n) in let eq_th = ineq_conv ineq_tm in let ineq_tm1 = (rand o concl) eq_th in try verify_ineq default_params pp ineq_tm1 with Failure s -> let _ = report s in TRUTH, {total_time = 0.0; formal_verification_time = 0.0; certificate = Verifier.dummy_stats} in map (verify o fst) ineqs;; let sum_time ineqs result = let original_time = itlist (fun (_,(_,x)) y -> x + y) ineqs 0 in let failures = length (filter (fun x, _ -> x = TRUTH) result) in let times = snd (unzip result) in failures, itlist (fun x y -> x.total_time +. y) times 0.0, itlist (fun x y -> x.formal_verification_time +. y) times 0.0, original_time;; (* Returns inequalities with the given informal verification time (bounds are inclusive) *) let get_ineqs t_min t_max = filter (fun (_, (_, t)) -> t_min <= t && t <= t_max) ineqs;; (**************) (* 0 ms *) let ineqs0 = get_ineqs 0 0;; (* 55 *) length ineqs0;; let result0 = verify_all 4 ineqs0;; (* base = 200, pp = 4: 422.494, 2.159; informal = 0 *) sum_time ineqs0 result0;; (*******************) (* 1 ms -- 100 ms *) let ineqs100 = get_ineqs 1 100;; (* 35 *) length ineqs100;; let result100 = verify_all 4 ineqs100;; (* base = 200, pp = 4: 5546, 3854; informal = 1134 *) sum_time ineqs100 result100;; (***********************************) (* 101 ms -- 500 ms, 501 -- 700 ms *) let ineqs500 = get_ineqs 101 500;; (* 11 *) length ineqs500;; let ineqs700 = get_ineqs 501 700;; (* 14 *) length ineqs700;; let result500 = verify_all 4 ineqs500;; let result700 = verify_all 4 ineqs700;; (* base = 200, pp = 4: 12098, 10451; informal = 3944 *) sum_time ineqs500 result500;; (* base = 200, pp = 4: 32065, 28705; informal = 8423 *) sum_time ineqs700 result700;; (******************) (* 701 -- 1000 ms *) let ineqs1000 = get_ineqs 701 1000;; (* 9 *) length ineqs1000;; let result1000 = verify_all 4 ineqs1000;; (* base = 200, pp = 4: 19040, 16688; informal = 7274 *) sum_time ineqs1000 result1000;; let x = 2;; (************************************) let ineqs1, ineqs2 = chop_list 57 ineqs;; let result = verify_all 4 ineqs1;; (* base = 200, pp = 4: 434.977, 2.202 (0) *) sum_time ineqs1 result;; let ineqs1, ineqs2 = chop_list 20 ineqs2;; let result2 = verify_all 4 ineqs1;; (* base = 200, pp = 4: 1809.949, 997.721 (279) *) sum_time ineqs1 result2;; let ineqs1, ineqs2 = chop_list 30 ineqs2;; let result3 = verify_all 4 ineqs1;; (* base = 200, pp = 4: 26885, 23111 (6863) *) sum_time ineqs1 result3;; let ineqs3, ineqs4 = chop_list 2 ineqs2;; let result4 = verify_all 4 ineqs3;; (* base = 200, pp = 4: 7105, 6439 (1125) *) sum_time ineqs3 result4;; let ineq_tm = List.nth ineqs3 1;; let eq_th = (ineq_conv THENC REWRITE_CONV[REAL_LE_REFL]) (subst[`#6.3504`, `x5:real`; `#4.0`, `x6:real`] (fst ineq_tm));; let ineq_tm1 = (rand o concl) eq_th;; (* verification time: 1954 (vs 3299) *) verify_ineq default_params 4 ineq_tm1;; let ineq_tm = List.nth ineqs3 1;; let eq_th = (REWRITE_CONV[REAL_ARITH `a + b * (-- &1) + c * (-- &1) + d * (-- &1) + e = (a + e) - (b + c + d)`] THENC ineq_conv THENC REWRITE_CONV[REAL_LE_REFL]) (subst[`#6.3504`, `x5:real`; `#4.0`, `x6:real`] (fst ineq_tm));; let ineq_tm1 = (rand o concl) eq_th;; (* verification time: 1771 (vs 3299) *) verify_ineq default_params 4 ineq_tm1;;