text_formalization/nonlinear/formal_tests/test1.hl

   1 needs "verifier/m_verifier_main.hl";;
   2
   3 needs "nonlinear/lemma.hl";;
   4 needs "nonlinear/functional_equation.hl";;
   5 needs "nonlinear/ineq.hl";;
   6
   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);;
  11
  12 needs "nonlinear/formal_tests/ineq_ids.hl";;
  13
  14 needs "nonlinear/formal_tests/hminus.hl";;
  15
  16
  17 open M_verifier_main;;
  18 open Sphere;;
  19
  20 (*************************)
  21
  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
  24      &0 < x1 /\ &0 < d ==>
  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[]);;
  32
  33
  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[]);;
  39
  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[]);;
  44
  45 let ineqs =
  46   let dummy = `ineq [] (P \/ Q)` in
  47   let find id =
  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;;
  53
  54 (* 195 *)
  55 length ineqs;;
  56
  57 let get_constants tm =
  58   let rec find tm =
  59     match tm with
  60       | Const _ -> [tm]
  61       | Comb (tm1, tm2) -> find tm1 @ find tm2
  62       | Abs (_, tm2) -> find tm2
  63       | _ -> [] in
  64     setify (find tm);;
  65
  66
  67 let ineqs =
  68   let c1 = "asn797k" and
  69       c2 = "asnFnhk" in
  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;;
  74
  75 let consts = end_itlist union (map (get_constants o fst) ineqs);;
  76 (* 193 *)
  77 length ineqs;;
  78
  79 let all_ids = map (fst o snd) ineqs;;
  80
  81 open Functional_equation;;
  82 open Nonlinear_lemma;;
  83
  84 let flyspeck_defs = [
  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;
  94   rad2_x; unit6;
  95   promote1_to_6;
  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;
 104 ];;
 105
 106 let cond_defs =
 107   let conv = UNDISCH_ALL o CONV_RULE (DEPTH_CONV let_CONV) in
 108     map conv [
 109       dih_x_pos_eq;
 110       arclength_pos_eq
 111     ];;
 112
 113 (* A temporary cheating *)
 114 let cond_defs =
 115   let conv = UNDISCH_ALL o CONV_RULE (DEPTH_CONV let_CONV) in
 116   let conv = Hol.new_axiom o concl o conv in
 117     map conv [
 118       dih_x_pos_eq;
 119       arclength_pos_eq;
 120       sqrt_pos_eq;
 121     ];;
 122
 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);; *)
 126
 127
 128 let verify_all pp ineqs =
 129   let n = length ineqs in
 130   let k = ref 0 in
 131   let verify ineq_tm =
 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
 136       try
 137         verify_ineq default_params pp ineq_tm1
 138       with Failure s ->
 139         let _ = report s in
 140           TRUTH, {total_time = 0.0; formal_verification_time = 0.0; certificate = Verifier.dummy_stats} in
 141     map (verify o fst) ineqs;;
 142
 143
 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
 148     failures,
 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,
 151   original_time;;
 152
 153
 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;;
 157
 158
 159 (**************)
 160 (* 0 ms *)
 161 let ineqs0 = get_ineqs 0 0;;
 162 (* 55 *)
 163 length ineqs0;;
 164
 165
 166 let result0 = verify_all 4 ineqs0;;
 167 (* base = 200, pp = 4: 422.494, 2.159; informal = 0 *)
 168 sum_time ineqs0 result0;;
 169
 170 (*******************)
 171 (* 1 ms -- 100 ms *)
 172 let ineqs100 = get_ineqs 1 100;;
 173 (* 35 *)
 174 length ineqs100;;
 175
 176 let result100 = verify_all 4 ineqs100;;
 177 (* base = 200, pp = 4: 5546, 3854; informal = 1134 *)
 178 sum_time ineqs100 result100;;
 179
 180
 181 (***********************************)
 182 (* 101 ms -- 500 ms, 501 -- 700 ms *)
 183 let ineqs500 = get_ineqs 101 500;;
 184 (* 11 *)
 185 length ineqs500;;
 186
 187 let ineqs700 = get_ineqs 501 700;;
 188 (* 14 *)
 189 length ineqs700;;
 190
 191 let result500 = verify_all 4 ineqs500;;
 192
 193 let result700 = verify_all 4 ineqs700;;
 194
 195 (* base = 200, pp = 4: 12098, 10451; informal = 3944 *)
 196 sum_time ineqs500 result500;;
 197
 198 (* base = 200, pp = 4: 32065, 28705; informal = 8423 *)
 199 sum_time ineqs700 result700;;
 200
 201
 202 (******************)
 203 (* 701 -- 1000 ms *)
 204 let ineqs1000 = get_ineqs 701 1000;;
 205 (* 9 *)
 206 length ineqs1000;;
 207
 208 let result1000 = verify_all 4 ineqs1000;;
 209
 210 (* base = 200, pp = 4: 19040, 16688; informal = 7274 *)
 211 sum_time ineqs1000 result1000;;
 212
 213 let x = 2;;
 214
 215 (************************************)
 216
 217 let ineqs1, ineqs2 = chop_list 57 ineqs;;
 218 let result = verify_all 4 ineqs1;;
 219
 220 (* base = 200, pp = 4: 434.977, 2.202 (0) *)
 221 sum_time ineqs1 result;;
 222
 223 let ineqs1, ineqs2 = chop_list 20 ineqs2;;
 224 let result2 = verify_all 4 ineqs1;;
 225
 226 (* base = 200, pp = 4: 1809.949, 997.721 (279) *)
 227 sum_time ineqs1 result2;;
 228
 229 let ineqs1, ineqs2 = chop_list 30 ineqs2;;
 230 let result3 = verify_all 4 ineqs1;;
 231
 232 (* base = 200, pp = 4: 26885, 23111 (6863) *)
 233 sum_time ineqs1 result3;;
 234
 235
 236 let ineqs3, ineqs4 = chop_list 2 ineqs2;;
 237 let result4 = verify_all 4 ineqs3;;
 238
 239 (* base = 200, pp = 4: 7105, 6439 (1125) *)
 240 sum_time ineqs3 result4;;
 241
 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;;
 248
 249
 250 let ineq_tm = List.nth ineqs3 1;;
 251 let eq_th =
 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;;
 256
 257 (* verification time: 1771 (vs 3299) *)
 258 verify_ineq default_params 4 ineq_tm1;;