formal_lp/old/formal_interval/m_test.hl

   1 let pp = 10 and
   2     n = 8 and
   3     xx = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]` and
   4     zz = `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;
   5
   6 let xx1 = convert_to_float_list pp true xx and
   7     zz1 = convert_to_float_list pp false zz;;
   8 let xx_float = map float_of_float_tm (dest_list xx1) and
   9     zz_float = map float_of_float_tm (dest_list zz1);;
  10
  11 (* let eval_heart, tf_heart = mk_verification_functions pp heart_poly true heart_min;; *)
  12 let certificate = run_test tf_heart xx_float zz_float false 0.0 true false;;
  13 result_size certificate;;
  14 m_verify_raw n pp eval_heart certificate xx1 zz1;;
  15 m_verify_raw_old n pp eval_heart certificate xx1 zz1;;
  16
  17
  18
  19
  20 let m_verify_raw n pp eval_taylor certificate xx zz =
  21   let r_size = result_size certificate in
  22   let k = ref 0 in
  23   let domain_th = mk_m_center_domain n pp xx zz in
  24
  25
  26   let rec rec_verify =
  27     let rec apply_trans sub_ths th0 acc =
  28       match sub_ths with
  29         | [] -> rev acc
  30         | th :: ths ->
  31             let th' = eval_subset_trans th th0 in
  32               apply_trans ths th' (th' :: acc) in
  33
  34     let rec mk_domains mono th0 acc =
  35       match mono with
  36         | [] -> rev acc
  37         | j :: js ->
  38             let j, flag = if j < 0 then (-j), true else j, false in
  39             let ths = restrict_domain n j flag th0 in
  40               mk_domains js (fst ths) (ths :: acc) in
  41
  42
  43     let verify_mono mono domain_th certificate =
  44       let taylor_th = eval_taylor domain_th in
  45       let _, diff2_th, _, _ = dest_m_taylor_thms n taylor_th in
  46       let domain_ths = mk_domains mono domain_th [] in
  47
  48       let mono_ths = map (fun j -> if j < 0 then
  49                             eval_m_taylor_upper_partial n pp (-j) taylor_th else
  50                               eval_m_taylor_lower_partial n pp j taylor_th) mono in
  51       let _ = map (fun i ->
  52                      let j = List.nth mono (i - 1) and
  53                          th = List.nth mono_ths (i - 1) in
  54                      let f = if j < 0 then rand else lhand in
  55                        (string_of_term o f o rand o snd o dest_forall o concl) th) (1--(length mono)) in
  56
  57       let pass_th0 = rec_verify ((fst o last) domain_ths) certificate in
  58       let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths in
  59       let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [] in
  60       let th = rev_itlist (fun ((j, mono_th), sub_th) pass_th ->
  61                              let j, flag = if j < 0 then (-j), true else j, false in
  62                                m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th)
  63         (rev (zip (zip mono mono_ths) sub_ths)) pass_th0 in
  64         if hyp th <> [] then failwith ("hyp <> []: "^string_of_thm th) else th in
  65
  66
  67
  68
  69       fun domain_th certificate ->
  70         match certificate with
  71           | Result_pass (mono, xx, zz) ->
  72               if mono = [] then
  73                 let _ = k := !k + 1 in
  74                 let _ = report (sprintf "Verifying: %d/%d" !k r_size) in
  75                 let taylor_th = eval_taylor domain_th in
  76                   m_taylor_cell_pass n pp taylor_th
  77               else
  78                 let _ = report (sprintf "Mono: [%s]" (String.concat ";" (map string_of_int (hd mono)))) in
  79                   verify_mono (hd mono) domain_th (Result_pass (tl mono, xx, zz))
  80
  81           | Result_glue (mono, i, r1, r2) ->
  82               let _ = report "Result_glue" in
  83               if mono = [] then
  84                 let domain1_th, domain2_th = split_domain n pp (i + 1) domain_th in
  85                 let th1 = rec_verify domain1_th r1 in
  86                 let th2 = rec_verify domain2_th r2 in
  87                   m_glue_cells n (i + 1) th1 th2
  88               else
  89                 let _ = report (sprintf "GlueMono: [%s]" (String.concat ";" (map string_of_int (hd mono)))) in
  90                   verify_mono (hd mono) domain_th (Result_glue (tl mono, i, r1, r2))
  91
  92           | _ -> failwith "False result" in
  93
  94     rec_verify domain_th certificate;;
  95
  96
  97 m_verify_raw_old n pp eval_heart certificate xx1 zz1;;
  98 m_verify_raw n pp eval_heart certificate xx1 zz1;;
  99
 100
 101
 102 let rec test_computations tf x z certificate =
 103   let rec mono_test mono ti x z =
 104     match mono with
 105       | [] -> x,z
 106       | j :: js ->
 107           let bound = if j < 0 then upper_partial ti (-j - 1) else lower_partial ti (j - 1) in
 108           let setj u =
 109             if j < 0 then
 110               table (fun i -> (if i=j then mth x j else mth u i))
 111             else
 112               table (fun i -> (if i=j then mth z j else mth u i)) in
 113
 114           let _ = report (sprintf "j = %d, bound = %f" j bound) in
 115             mono_test js ti (setj x) (setj z) in
 116
 117
 118   match certificate with
 119     | Result_pass (mono, _, _) ->
 120         let _ = report (sprintf "Pass: |mono| = %d" (length mono)) in
 121         let ti = evalf tf x z in
 122         let x,z = mono_test mono ti x z in
 123
 124         let ti = evalf tf x z in
 125         let bound = upper_bound ti in
 126           report (sprintf "bound = %f" bound)
 127     | Result_glue (mono, j, r1, r2) ->
 128         let _ = report (sprintf "Glue: |mono| = %d" (length mono)) in
 129         let ( ++ ), ( / ) = up(); upadd, updiv in
 130         let yj = (mth x j ++ mth z j) / 2.0 in
 131         let delta b v = table (fun i -> if (i = j && b) then yj else mth v i) in
 132         let _ = test_computations tf (delta false x) (delta true z) r1 in
 133         let _ = test_computations tf (delta true x) (delta false z) r2 in
 134           ();;
 135
 136
 137 test_computations tf_heart xx_float zz_float certificate;;
 138
 139
 140
 141 (***)
 142
 143
 144 let rec apply_trans sub_ths th0 acc =
 145   match sub_ths with
 146     | [] -> rev acc
 147     | th :: ths ->
 148         let th' = eval_subset_trans th th0 in
 149           apply_trans ths th' (th' :: acc);;
 150
 151 let rec mk_domains mono th0 acc =
 152   match mono with
 153     | [] -> rev acc
 154     | j :: js ->
 155         let j, flag = if j < 0 then (-j), true else j, false in
 156         let ths = restrict_domain n j flag th0 in
 157           mk_domains js (fst ths) (ths :: acc);;
 158
 159
 160 let mono = [-1;-2] and domain_th = mk_m_center_domain n pp xx1 zz1;;
 161
 162 let verify_mono mono domain_th certificate = 0;;
 163 let taylor_th = eval_taylor domain_th;;
 164 let _, diff2_th, _, _ = dest_m_taylor_thms n taylor_th;;
 165 let domain_ths = mk_domains mono domain_th [];;
 166
 167 let mono_ths = map (fun j -> if j < 0 then
 168                       eval_m_taylor_upper_partial n pp (-j) taylor_th else
 169                         eval_m_taylor_lower_partial n pp j taylor_th) mono;;
 170
 171 let domain0 = (fst o last) domain_ths;;
 172 let taylor0 = eval_taylor domain0;;
 173 let pass_th0 = m_taylor_cell_pass n pp taylor0;;
 174
 175 let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths;;
 176 let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [];;
 177 zip (zip mono mono_ths) sub_ths;;
 178
 179 rev_itlist (fun ((j, mono_th), sub_th) pass_th ->
 180               let j, flag = if j < 0 then (-j), true else j, false in
 181                 m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th)
 182   (rev (zip (zip mono mono_ths) sub_ths)) pass_th0;;
 183