1 needs "verifier/m_verifier_main.hl";;
3 needs "nonlinear/lemma.hl";;
4 needs "nonlinear/functional_equation.hl";;
5 needs "nonlinear/ineq.hl";;
7 needs "nonlinear/prep.hl";;
8 let add_inequality = Prep.add_inequality;;
9 let find_ineqs idv = filter (fun t -> (String.length idv <= String.length t.idv) &&
10 (String.sub t.idv 0 (String.length idv) = idv)) (!Prep.prep_ineqs);;
12 needs "nonlinear/formal_tests/ineq_ids.hl";;
14 needs "nonlinear/formal_tests/hminus.hl";;
17 open M_verifier_main;;
20 (*************************)
22 let dih_x_pos_eq = prove (`let d_x4 = delta_x4 x1 x2 x3 x4 x5 x6 in
23 let d = delta_x x1 x2 x3 x4 x5 x6 in
25 dih_x x1 x2 x3 x4 x5 x6 = pi / &2 + atn(--d_x4 / sqrt (&4 * x1 * d))`,
26 REPEAT (CONV_TAC let_CONV) THEN STRIP_TAC THEN
27 REWRITE_TAC[dih_x] THEN CONV_TAC (DEPTH_CONV let_CONV) THEN
28 new_rewrite [] [] Trigonometry1.ATN2_BREAKDOWN THEN ASM_REWRITE_TAC[] THEN
29 MATCH_MP_TAC SQRT_POS_LT THEN
30 MATCH_MP_TAC REAL_LT_MUL THEN STRIP_TAC THENL [ REAL_ARITH_TAC; ALL_TAC] THEN
31 MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]);;
34 let arclength_pos_eq = prove(`&0 < ups_x (a * a) (b * b) (c * c) ==>
35 arclength a b c = pi / &2 + atn ((c * c - a * a - b * b) / sqrt (ups_x (a * a) (b * b) (c * c)))`,
36 STRIP_TAC THEN REWRITE_TAC[arclength] THEN
37 new_rewrite [] [] Trigonometry1.ATN2_BREAKDOWN THEN ASM_REWRITE_TAC[] THEN
38 MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);;
40 let sqrt_pos_eq = prove(`&0 < x ==> sqrt x * sqrt x = x`,
41 DISCH_TAC THEN REWRITE_TAC[GSYM REAL_POW_2] THEN
42 MATCH_MP_TAC SQRT_POW_2 THEN
43 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]);;
46 let dummy = `ineq [] (P \/ Q)` in
48 let data = find_ineqs id in
49 (snd o strip_forall) (if data = [] then dummy else (hd data).ineq) in
50 let all_ineqs = map (fun id, t -> find id, (id, t)) ineq_ids in
51 let filter1 = filter (fun ineq, _ -> not (is_disj (rand ineq))) all_ineqs in
52 filter (fun ineq, _ -> not (is_binary "real_le" (rand ineq))) filter1;;
57 let get_constants tm =
61 | Comb (tm1, tm2) -> find tm1 @ find tm2
62 | Abs (_, tm2) -> find tm2
68 let c1 = "asn797k" and
70 filter (fun ineq, _ ->
71 let cs = get_constants ineq in
72 let l = map (fst o dest_const) cs in
73 not (mem c1 l or mem c2 l)) ineqs;;
75 let consts = end_itlist union (map (get_constants o fst) ineqs);;
79 let all_ids = map (fst o snd) ineqs;;
81 open Functional_equation;;
82 open Nonlinear_lemma;;
85 gamma3f_x_div_sqrtdelta; promote_pow3;
86 proj_x1; proj_x2; proj_x3; proj_x4; proj_x5; proj_x6;
87 delta_x4; delta_x; eulerA_x; num1; acs_sqrt_x1_d4;
88 arclength_x_123; arc_hhn; arclength_x1;
89 lfun_y1; gchi1_x; rhazim2_x; rhazim3_x; rhazim_x;
90 taum_sub345_x; dih4_x; halfbump_x1; halfbump_x4;
91 gchi2_x; gchi3_x; gchi4_x; gchi5_x; gchi6_x;
92 sqrt8; vol_x; dih2_x; dih3_x;
93 sqrt_x1; sqrt_x2; sqrt_x3; sqrt_x4; sqrt_x5; sqrt_x6;
96 mm1; mm2; arclength_y1; h0; lfun;
97 rhazim2; rhazim3; taum_x; rhazim;
98 halfbump_x; dih4_y; dih5_x; dih6_x; gchi;
99 sol_y; rho_x; sol0; tau0;
100 node2_y; node3_y; rho;
101 bump; dih5_y; dih6_y; dih_y;
102 ly; interp; hplus; ups_x;
103 GSYM sol0_over_pi_EQ_const1;
107 let conv = UNDISCH_ALL o CONV_RULE (DEPTH_CONV let_CONV) in
113 (* A temporary cheating *)
115 let conv = UNDISCH_ALL o CONV_RULE (DEPTH_CONV let_CONV) in
116 let conv = Hol.new_axiom o concl o conv in
123 let ineq_conv = REWRITE_CONV[Sphere.ineq; IMP_IMP] THENC REWRITE_CONV flyspeck_defs
124 THENC DEPTH_CONV let_CONV THENC REWRITE_CONV cond_defs THENC REWRITE_CONV flyspeck_defs;;
125 (* let consts2 = end_itlist union (map (get_constants o rand o concl o ineq_conv o fst) ineqs);; *)
128 let verify_all pp ineqs =
129 let n = length ineqs in
132 let _ = k := !k + 1 in
133 let _ = report (sprintf "Verifying: %d/%d" !k n) in
134 let eq_th = ineq_conv ineq_tm in
135 let ineq_tm1 = (rand o concl) eq_th in
137 verify_ineq default_params pp ineq_tm1
140 TRUTH, {total_time = 0.0; formal_verification_time = 0.0; certificate = Verifier.dummy_stats} in
141 map (verify o fst) ineqs;;
144 let sum_time ineqs result =
145 let original_time = itlist (fun (_,(_,x)) y -> x + y) ineqs 0 in
146 let failures = length (filter (fun x, _ -> x = TRUTH) result) in
147 let times = snd (unzip result) in
149 itlist (fun x y -> x.total_time +. y) times 0.0,
150 itlist (fun x y -> x.formal_verification_time +. y) times 0.0,
154 (* Returns inequalities with the given informal verification time (bounds are inclusive) *)
155 let get_ineqs t_min t_max =
156 filter (fun (_, (_, t)) -> t_min <= t && t <= t_max) ineqs;;
161 let ineqs0 = get_ineqs 0 0;;
166 let result0 = verify_all 4 ineqs0;;
167 (* base = 200, pp = 4: 422.494, 2.159; informal = 0 *)
168 sum_time ineqs0 result0;;
170 (*******************)
172 let ineqs100 = get_ineqs 1 100;;
176 let result100 = verify_all 4 ineqs100;;
177 (* base = 200, pp = 4: 5546, 3854; informal = 1134 *)
178 sum_time ineqs100 result100;;
181 (***********************************)
182 (* 101 ms -- 500 ms, 501 -- 700 ms *)
183 let ineqs500 = get_ineqs 101 500;;
187 let ineqs700 = get_ineqs 501 700;;
191 let result500 = verify_all 4 ineqs500;;
193 let result700 = verify_all 4 ineqs700;;
195 (* base = 200, pp = 4: 12098, 10451; informal = 3944 *)
196 sum_time ineqs500 result500;;
198 (* base = 200, pp = 4: 32065, 28705; informal = 8423 *)
199 sum_time ineqs700 result700;;
204 let ineqs1000 = get_ineqs 701 1000;;
208 let result1000 = verify_all 4 ineqs1000;;
210 (* base = 200, pp = 4: 19040, 16688; informal = 7274 *)
211 sum_time ineqs1000 result1000;;
215 (************************************)
217 let ineqs1, ineqs2 = chop_list 57 ineqs;;
218 let result = verify_all 4 ineqs1;;
220 (* base = 200, pp = 4: 434.977, 2.202 (0) *)
221 sum_time ineqs1 result;;
223 let ineqs1, ineqs2 = chop_list 20 ineqs2;;
224 let result2 = verify_all 4 ineqs1;;
226 (* base = 200, pp = 4: 1809.949, 997.721 (279) *)
227 sum_time ineqs1 result2;;
229 let ineqs1, ineqs2 = chop_list 30 ineqs2;;
230 let result3 = verify_all 4 ineqs1;;
232 (* base = 200, pp = 4: 26885, 23111 (6863) *)
233 sum_time ineqs1 result3;;
236 let ineqs3, ineqs4 = chop_list 2 ineqs2;;
237 let result4 = verify_all 4 ineqs3;;
239 (* base = 200, pp = 4: 7105, 6439 (1125) *)
240 sum_time ineqs3 result4;;
242 let ineq_tm = List.nth ineqs3 1;;
243 let eq_th = (ineq_conv THENC REWRITE_CONV[REAL_LE_REFL])
244 (subst[`#6.3504`, `x5:real`; `#4.0`, `x6:real`] (fst ineq_tm));;
245 let ineq_tm1 = (rand o concl) eq_th;;
246 (* verification time: 1954 (vs 3299) *)
247 verify_ineq default_params 4 ineq_tm1;;
250 let ineq_tm = List.nth ineqs3 1;;
252 (REWRITE_CONV[REAL_ARITH `a + b * (-- &1) + c * (-- &1) + d * (-- &1) + e = (a + e) - (b + c + d)`] THENC
253 ineq_conv THENC REWRITE_CONV[REAL_LE_REFL])
254 (subst[`#6.3504`, `x5:real`; `#4.0`, `x6:real`] (fst ineq_tm));;
255 let ineq_tm1 = (rand o concl) eq_th;;
257 (* verification time: 1771 (vs 3299) *)
258 verify_ineq default_params 4 ineq_tm1;;