let pp = 10 and n = 8 and xx = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]` and zz = `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;; let xx1 = convert_to_float_list pp true xx and zz1 = convert_to_float_list pp false zz;; let xx_float = map float_of_float_tm (dest_list xx1) and zz_float = map float_of_float_tm (dest_list zz1);; (* let eval_heart, tf_heart = mk_verification_functions pp heart_poly true heart_min;; *) let certificate = run_test tf_heart xx_float zz_float false 0.0 true false;; result_size certificate;; m_verify_raw n pp eval_heart certificate xx1 zz1;; m_verify_raw_old n pp eval_heart certificate xx1 zz1;; let m_verify_raw n pp eval_taylor certificate xx zz = let r_size = result_size certificate in let k = ref 0 in let domain_th = mk_m_center_domain n pp xx zz in let rec rec_verify = let rec apply_trans sub_ths th0 acc = match sub_ths with | [] -> rev acc | th :: ths -> let th' = eval_subset_trans th th0 in apply_trans ths th' (th' :: acc) in let rec mk_domains mono th0 acc = match mono with | [] -> rev acc | j :: js -> let j, flag = if j < 0 then (-j), true else j, false in let ths = restrict_domain n j flag th0 in mk_domains js (fst ths) (ths :: acc) in let verify_mono mono domain_th certificate = let taylor_th = eval_taylor domain_th in let _, diff2_th, _, _ = dest_m_taylor_thms n taylor_th in let domain_ths = mk_domains mono domain_th [] in let mono_ths = map (fun j -> if j < 0 then eval_m_taylor_upper_partial n pp (-j) taylor_th else eval_m_taylor_lower_partial n pp j taylor_th) mono in let _ = map (fun i -> let j = List.nth mono (i - 1) and th = List.nth mono_ths (i - 1) in let f = if j < 0 then rand else lhand in (string_of_term o f o rand o snd o dest_forall o concl) th) (1--(length mono)) in let pass_th0 = rec_verify ((fst o last) domain_ths) certificate in let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths in let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [] in let th = rev_itlist (fun ((j, mono_th), sub_th) pass_th -> let j, flag = if j < 0 then (-j), true else j, false in m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th) (rev (zip (zip mono mono_ths) sub_ths)) pass_th0 in if hyp th <> [] then failwith ("hyp <> []: "^string_of_thm th) else th in fun domain_th certificate -> match certificate with | Result_pass (mono, xx, zz) -> if mono = [] then let _ = k := !k + 1 in let _ = report (sprintf "Verifying: %d/%d" !k r_size) in let taylor_th = eval_taylor domain_th in m_taylor_cell_pass n pp taylor_th else let _ = report (sprintf "Mono: [%s]" (String.concat ";" (map string_of_int (hd mono)))) in verify_mono (hd mono) domain_th (Result_pass (tl mono, xx, zz)) | Result_glue (mono, i, r1, r2) -> let _ = report "Result_glue" in if mono = [] then let domain1_th, domain2_th = split_domain n pp (i + 1) domain_th in let th1 = rec_verify domain1_th r1 in let th2 = rec_verify domain2_th r2 in m_glue_cells n (i + 1) th1 th2 else let _ = report (sprintf "GlueMono: [%s]" (String.concat ";" (map string_of_int (hd mono)))) in verify_mono (hd mono) domain_th (Result_glue (tl mono, i, r1, r2)) | _ -> failwith "False result" in rec_verify domain_th certificate;; m_verify_raw_old n pp eval_heart certificate xx1 zz1;; m_verify_raw n pp eval_heart certificate xx1 zz1;; let rec test_computations tf x z certificate = let rec mono_test mono ti x z = match mono with | [] -> x,z | j :: js -> let bound = if j < 0 then upper_partial ti (-j - 1) else lower_partial ti (j - 1) in let setj u = if j < 0 then table (fun i -> (if i=j then mth x j else mth u i)) else table (fun i -> (if i=j then mth z j else mth u i)) in let _ = report (sprintf "j = %d, bound = %f" j bound) in mono_test js ti (setj x) (setj z) in match certificate with | Result_pass (mono, _, _) -> let _ = report (sprintf "Pass: |mono| = %d" (length mono)) in let ti = evalf tf x z in let x,z = mono_test mono ti x z in let ti = evalf tf x z in let bound = upper_bound ti in report (sprintf "bound = %f" bound) | Result_glue (mono, j, r1, r2) -> let _ = report (sprintf "Glue: |mono| = %d" (length mono)) in let ( ++ ), ( / ) = up(); upadd, updiv in let yj = (mth x j ++ mth z j) / 2.0 in let delta b v = table (fun i -> if (i = j && b) then yj else mth v i) in let _ = test_computations tf (delta false x) (delta true z) r1 in let _ = test_computations tf (delta true x) (delta false z) r2 in ();; test_computations tf_heart xx_float zz_float certificate;; (***) let rec apply_trans sub_ths th0 acc = match sub_ths with | [] -> rev acc | th :: ths -> let th' = eval_subset_trans th th0 in apply_trans ths th' (th' :: acc);; let rec mk_domains mono th0 acc = match mono with | [] -> rev acc | j :: js -> let j, flag = if j < 0 then (-j), true else j, false in let ths = restrict_domain n j flag th0 in mk_domains js (fst ths) (ths :: acc);; let mono = [-1;-2] and domain_th = mk_m_center_domain n pp xx1 zz1;; let verify_mono mono domain_th certificate = 0;; let taylor_th = eval_taylor domain_th;; let _, diff2_th, _, _ = dest_m_taylor_thms n taylor_th;; let domain_ths = mk_domains mono domain_th [];; let mono_ths = map (fun j -> if j < 0 then eval_m_taylor_upper_partial n pp (-j) taylor_th else eval_m_taylor_lower_partial n pp j taylor_th) mono;; let domain0 = (fst o last) domain_ths;; let taylor0 = eval_taylor domain0;; let pass_th0 = m_taylor_cell_pass n pp taylor0;; let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths;; let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [];; zip (zip mono mono_ths) sub_ths;; rev_itlist (fun ((j, mono_th), sub_th) pass_th -> let j, flag = if j < 0 then (-j), true else j, false in m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th) (rev (zip (zip mono mono_ths) sub_ths)) pass_th0;;