formal_ineqs/verifier/m_verifier.hl

   1 (* =========================================================== *)
   2 (* Formal verification functions                               *)
   3 (* Author: Alexey Solovyev                                     *)
   4 (* Date: 2012-10-27                                            *)
   5 (* =========================================================== *)
   6
   7 needs "taylor/m_taylor.hl";;
   8 (* needs "verifier/interval_m/verifier.ml";; *)
   9 needs "verifier/interval_m/verifier.hl";;
  10 needs "misc/vars.hl";;
  11 needs "verifier_options.hl";;
  12 needs "verifier/m_verifier_build.hl";;
  13
  14 (* module M_verifier = struct *)
  15
  16 open Arith_misc;;
  17 open Arith_float;;
  18 open M_taylor;;
  19 open Misc_vars;;
  20 open Verifier_options;;
  21 open M_verifier_build;;
  22
  23
  24 let mk_real_vars n name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n);;
  25
  26 (*************************************)
  27
  28 let BOUNDED_INTERVAL_ARITH_IMP_HI' = (MY_RULE o prove)
  29   (`(!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi)) ==>
  30      (!x. x IN interval [domain] ==> f x <= hi)`, SIMP_TAC[interval_arith]);;
  31
  32 let BOUNDED_INTERVAL_ARITH_IMP_LO' = (MY_RULE o prove)
  33   (`(!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi)) ==>
  34      (!x. x IN interval [domain] ==> lo <= f x)`, SIMP_TAC[interval_arith]);;
  35
  36
  37 let eval_interval_arith_hi n bound_th =
  38   let tm0 = (snd o dest_forall o concl) bound_th in
  39   let int_tm, concl_tm = dest_comb tm0 in
  40   let domain_tm = (rand o rator o rand o rand o rand) int_tm in
  41   let ltm, bounds_tm = dest_interval_arith concl_tm in
  42   let f_tm, (lo_tm, hi_tm) = rator ltm, dest_pair bounds_tm in
  43   let f_var = mk_var ("f", type_of f_tm) and
  44       domain_var = mk_var ("domain", type_of domain_tm) in
  45     (MY_PROVE_HYP bound_th o
  46        INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real; lo_tm, lo_var_real] o
  47        inst_first_type_var n_type_array.(n)) BOUNDED_INTERVAL_ARITH_IMP_HI';;
  48
  49
  50 let eval_interval_arith_lo n bound_th =
  51   let tm0 = (snd o dest_forall o concl) bound_th in
  52   let int_tm, concl_tm = dest_comb tm0 in
  53   let domain_tm = (rand o rator o rand o rand o rand) int_tm in
  54   let ltm, bounds_tm = dest_interval_arith concl_tm in
  55   let f_tm, (lo_tm, hi_tm) = rator ltm, dest_pair bounds_tm in
  56   let f_var = mk_var ("f", type_of f_tm) and
  57       domain_var = mk_var ("domain", type_of domain_tm) in
  58     (MY_PROVE_HYP bound_th o
  59        INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real; lo_tm, lo_var_real] o
  60        inst_first_type_var n_type_array.(n)) BOUNDED_INTERVAL_ARITH_IMP_LO';;
  61
  62
  63
  64 (*************************************)
  65 (* subdomains *)
  66
  67 let eval_subset_trans =
  68   let SUBSET_TRANS' = MY_RULE SUBSET_TRANS in
  69     fun st_th tu_th ->
  70       let ltm, t_tm = dest_comb (concl st_th) in
  71       let s_tm = rand ltm and
  72           u_tm = rand (concl tu_th) in
  73       let ty = (hd o snd o dest_type o type_of) s_tm and
  74           s_var = mk_var ("s", type_of s_tm) and
  75           t_var = mk_var ("t", type_of t_tm) and
  76           u_var = mk_var ("u", type_of u_tm) in
  77         (MY_PROVE_HYP st_th o MY_PROVE_HYP tu_th o
  78            INST[s_tm, s_var; t_tm, t_var; u_tm, u_var] o inst_first_type_var ty) SUBSET_TRANS';;
  79
  80 let eval_subset_refl =
  81   let SUBSET_REFL' = MY_RULE SUBSET_REFL in
  82     fun s_tm ->
  83       let ty = (hd o snd o dest_type o type_of) s_tm and
  84           s_var = mk_var ("s", type_of s_tm) in
  85         (INST[s_tm, s_var] o inst_first_type_var ty) SUBSET_REFL';;
  86
  87
  88
  89 let SUBSET_INTERVAL_IMP = prove(`!a b c d. (!i. i IN 1..dimindex (:N) ==> a$i <= c$i /\ d$i <= b$i) ==>
  90                                   interval [c:real^N,d] SUBSET interval [a,b]`,
  91                                 SIMP_TAC[SUBSET_INTERVAL; GSYM IN_NUMSEG]);;
  92
  93
  94 let gen_subset_interval_lemma n =
  95   let a_vars = mk_real_vars n "a" and
  96       b_vars = mk_real_vars n "b" and
  97       c_vars = mk_real_vars n "c" and
  98       d_vars = mk_real_vars n "d" in
  99
 100   let a_tm = mk_vector_list a_vars and
 101       b_tm = mk_vector_list b_vars and
 102       c_tm = mk_vector_list c_vars and
 103       d_tm = mk_vector_list d_vars in
 104
 105   let th0 = (SPEC_ALL o ISPECL [a_tm; b_tm; c_tm; d_tm]) SUBSET_INTERVAL_IMP in
 106   let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
 107   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 108     MY_RULE th2;;
 109
 110
 111 let subset_interval_thms_array = Array.init (max_dim + 1)
 112   (fun n -> if n < 1 then TRUTH else gen_subset_interval_lemma n);;
 113
 114
 115
 116 let m_subset_interval n a_tm b_tm c_tm d_tm =
 117   let a_vars = mk_real_vars n "a" and
 118       b_vars = mk_real_vars n "b" and
 119       c_vars = mk_real_vars n "c" and
 120       d_vars = mk_real_vars n "d" in
 121
 122   let a_s = dest_vector a_tm and
 123       b_s = dest_vector b_tm and
 124       c_s = dest_vector c_tm and
 125       d_s = dest_vector d_tm in
 126
 127   let th0 = (INST (zip a_s a_vars) o INST (zip b_s b_vars) o
 128                INST (zip c_s c_vars) o INST (zip d_s d_vars)) subset_interval_thms_array.(n) in
 129   let prove_le tm =
 130     let ltm, rtm = dest_binop le_op_real tm in
 131       EQT_ELIM (float_le ltm rtm) in
 132   let hyp_ths = map prove_le (hyp th0) in
 133     itlist (fun hyp_th th -> MY_PROVE_HYP hyp_th th) hyp_ths th0;;
 134
 135
 136 (*************************************)
 137
 138 let M_RESTRICT_RIGHT_LEMMA = prove(`!j x z y w u y' w'. m_cell_domain (x:real^N,z) y w /\
 139                                     (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==>
 140                                        u$i = x$i /\ y'$i = y$i /\ w'$i = w$i) /\
 141                                     u$j = z$j /\ y'$j = z$j /\ w'$j = &0 ==>
 142     m_cell_domain (u,z) y' w' /\ interval [u,z] SUBSET interval [x,z]`,
 143    REWRITE_TAC[m_cell_domain; SUBSET_INTERVAL; GSYM IN_NUMSEG] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 144      CONJ_TAC THENL
 145      [
 146        GEN_TAC THEN DISCH_TAC THEN
 147          ASM_CASES_TAC `i = j:num` THENL
 148          [
 149            ASM_REWRITE_TAC[REAL_LE_REFL; REAL_SUB_REFL; real_max];
 150            ALL_TAC
 151          ] THEN
 152          REPEAT (FIRST_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[]);
 153        ALL_TAC
 154      ] THEN
 155      DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 156      ASM_CASES_TAC `i = j:num` THENL
 157      [
 158        ASM_REWRITE_TAC[REAL_LE_REFL] THEN
 159          REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `j:num`)) THEN
 160          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 161          ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
 162        ALL_TAC
 163      ] THEN
 164      REPEAT (FIRST_ASSUM (new_rewrite [] [])) THEN ASM_REWRITE_TAC[REAL_LE_REFL]);;
 165
 166
 167
 168 let M_RESTRICT_LEFT_LEMMA = prove(`!j x z y w u y' w'. m_cell_domain (x:real^N,z) y w /\
 169                                     (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==>
 170                                        u$i = z$i /\ y'$i = y$i /\ w'$i = w$i) /\
 171                                     u$j = x$j /\ y'$j = x$j /\ w'$j = &0 ==>
 172     m_cell_domain (x,u) y' w' /\ interval [x,u] SUBSET interval [x,z]`,
 173    REWRITE_TAC[m_cell_domain; SUBSET_INTERVAL; GSYM IN_NUMSEG] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 174      CONJ_TAC THENL
 175      [
 176        GEN_TAC THEN DISCH_TAC THEN
 177          ASM_CASES_TAC `i = j:num` THENL
 178          [
 179            ASM_REWRITE_TAC[REAL_LE_REFL; REAL_SUB_REFL; real_max];
 180            ALL_TAC
 181          ] THEN
 182          REPEAT (FIRST_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[]);
 183        ALL_TAC
 184      ] THEN
 185      DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 186      ASM_CASES_TAC `i = j:num` THENL
 187      [
 188        ASM_REWRITE_TAC[REAL_LE_REFL] THEN
 189          REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `j:num`)) THEN
 190          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 191          ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
 192        ALL_TAC
 193      ] THEN
 194      REPEAT (FIRST_ASSUM (new_rewrite [] [])) THEN ASM_REWRITE_TAC[REAL_LE_REFL]);;
 195
 196
 197 let gen_restrict_lemma n j left_flag =
 198   let xs = mk_real_vars n "x" and
 199       zs = mk_real_vars n "z" and
 200       ys = mk_real_vars n "y" and
 201       ws = mk_real_vars n "w" and
 202       j_tm = mk_small_numeral j in
 203   let a, b = if left_flag then zs, xs else xs, zs in
 204   let x_tm = mk_vector_list xs and
 205       z_tm = mk_vector_list zs and
 206       y_tm = mk_vector_list ys and
 207       w_tm = mk_vector_list ws and
 208       u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then b else a) (i - 1)) (1--n)) and
 209       y'_tm = mk_vector_list (map (fun i -> List.nth (if i = j then b else ys) (i - 1)) (1--n)) and
 210       w'_tm = mk_vector_list (map (fun i -> if i = j then `&0` else List.nth ws (i - 1)) (1--n)) in
 211
 212   let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; y_tm; w_tm; u_tm; y'_tm; w'_tm])
 213     (if left_flag then M_RESTRICT_LEFT_LEMMA else M_RESTRICT_RIGHT_LEMMA) in
 214   let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
 215   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 216     MY_RULE_FLOAT th2;;
 217
 218
 219 let left_restrict_thms_array = Array.init (max_dim + 1)
 220   (fun n -> Array.init (n + 1)
 221      (fun j -> if j < 1 then TRUTH else gen_restrict_lemma n j true));;
 222
 223
 224 let right_restrict_thms_array = Array.init (max_dim + 1)
 225   (fun n -> Array.init (n + 1)
 226      (fun j -> if j < 1 then TRUTH else gen_restrict_lemma n j false));;
 227
 228
 229
 230
 231 (******************************)
 232 (* m_cell_pass *)
 233
 234 let m_cell_pass = new_definition `m_cell_pass f domain <=> (!x. x IN interval [domain] ==> f x < &0)`;;
 235
 236 let m_cell_list_pass = new_definition `m_cell_list_pass fs domain <=>
 237   (!x:real^N. x IN interval [domain] ==> ITLIST (\f r. f x < &0 \/ r) fs F)`;;
 238
 239 let dest_m_cell_pass pass_tm =
 240   let ltm, domain = dest_comb pass_tm in
 241     rand ltm, domain;;
 242
 243 let dest_m_cell_list_pass pass_tm =
 244   let ltm, domain = dest_comb pass_tm in
 245     dest_list (rand ltm), domain;;
 246
 247
 248 (*********************************)
 249
 250 let M_CELL_PASS_EQ_LIST_PASS1 = prove(`m_cell_pass f domain <=> m_cell_list_pass [f] domain`,
 251                                       REWRITE_TAC[m_cell_pass; m_cell_list_pass; ITLIST]);;
 252
 253 let M_CELL_PASS_IMP_LIST_PASS1 = prove(`m_cell_pass f domain ==> m_cell_list_pass [f] domain`,
 254                                       REWRITE_TAC[M_CELL_PASS_EQ_LIST_PASS1]);;
 255
 256 let M_CELL_PASS_LEMMA = prove(`(!x. x IN interval [domain] ==> f x <= hi) /\ (hi < &0 <=> T) ==>
 257                                 m_cell_pass f domain`,
 258                               REWRITE_TAC[m_cell_pass] THEN REPEAT STRIP_TAC THEN
 259                                 MATCH_MP_TAC REAL_LET_TRANS THEN
 260                                 EXISTS_TAC `hi:real` THEN ASM_REWRITE_TAC[] THEN
 261                                 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 262
 263 let M_CELL_LIST_PASS1_LEMMA = prove(`(!x. x IN interval [domain] ==> f x <= hi) /\ (hi < &0 <=> T) ==>
 264                                 m_cell_list_pass [f] domain`,
 265                                     DISCH_THEN (MP_TAC o MATCH_MP M_CELL_PASS_LEMMA) THEN
 266                                       REWRITE_TAC[M_CELL_PASS_EQ_LIST_PASS1]);;
 267
 268
 269 let M_CELL_PASS_LEMMA' = MY_RULE M_CELL_PASS_LEMMA and
 270     M_CELL_LIST_PASS1_LEMMA' = MY_RULE M_CELL_LIST_PASS1_LEMMA;;
 271
 272 let M_CELL_PASS_INTERVAL_LEMMA' = (MY_RULE o prove)
 273   (`(!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi)) /\ hi < &0 ==> m_cell_pass f domain`,
 274    REWRITE_TAC[interval_arith] THEN STRIP_TAC THEN MATCH_MP_TAC M_CELL_PASS_LEMMA THEN
 275      ASM_SIMP_TAC[]);;
 276
 277 let M_CELL_LIST_PASS1_INTERVAL_LEMMA' = (MY_RULE o prove)
 278   (`(!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi)) /\ hi < &0 ==> m_cell_list_pass [f] domain`,
 279    REWRITE_TAC[interval_arith] THEN STRIP_TAC THEN MATCH_MP_TAC M_CELL_LIST_PASS1_LEMMA THEN
 280      ASM_SIMP_TAC[]);;
 281
 282
 283 (* m_cell_pass with taylor_interval *)
 284 let m_taylor_cell_pass n pp m_taylor_th =
 285   let upper_th = eval_m_taylor_upper_bound n pp m_taylor_th in
 286   let tm0 = (snd o dest_forall o concl) upper_th in
 287   let int_tm, concl_tm = dest_comb tm0 in
 288   let domain_tm = (rand o rator o rand o rand o rand) int_tm in
 289   let ltm, hi_tm = dest_comb concl_tm in
 290   let f_tm = (rator o rand) ltm in
 291   let f_var = mk_var ("f", type_of f_tm) and
 292       domain_var = mk_var ("domain", type_of domain_tm) in
 293
 294   let hi_lt0_th = float_lt0 hi_tm in
 295     if (fst o dest_const o rand o concl) hi_lt0_th = "F" then
 296       failwith "m_taylor_cell_pass: hi < &0 <=> F"
 297     else
 298       (MY_PROVE_HYP upper_th o MY_PROVE_HYP hi_lt0_th o
 299          INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real] o
 300          inst_first_type_var n_type_array.(n)) M_CELL_PASS_LEMMA';;
 301
 302 let m_taylor_cell_list_pass n pp m_taylor_th =
 303   let upper_th = eval_m_taylor_upper_bound n pp m_taylor_th in
 304   let tm0 = (snd o dest_forall o concl) upper_th in
 305   let int_tm, concl_tm = dest_comb tm0 in
 306   let domain_tm = (rand o rator o rand o rand o rand) int_tm in
 307   let ltm, hi_tm = dest_comb concl_tm in
 308   let f_tm = (rator o rand) ltm in
 309   let f_var = mk_var ("f", type_of f_tm) and
 310       domain_var = mk_var ("domain", type_of domain_tm) in
 311
 312   let hi_lt0_th = float_lt0 hi_tm in
 313     if (fst o dest_const o rand o concl) hi_lt0_th = "F" then
 314       failwith "m_taylor_cell_list_pass: hi < &0 <=> F"
 315     else
 316       (MY_PROVE_HYP upper_th o MY_PROVE_HYP hi_lt0_th o
 317          INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real] o
 318          inst_first_type_var n_type_array.(n)) M_CELL_LIST_PASS1_LEMMA';;
 319
 320
 321 (* m_cell_pass with a raw interval *)
 322 let m_taylor_cell_pass0 n bound_th =
 323   let tm0 = (snd o dest_forall o concl) bound_th in
 324   let int_tm, concl_tm = dest_comb tm0 in
 325   let domain_tm = (rand o rator o rand o rand o rand) int_tm in
 326   let ltm, bounds_tm = dest_interval_arith concl_tm in
 327   let f_tm, (lo_tm, hi_tm) = rator ltm, dest_pair bounds_tm in
 328   let f_var = mk_var ("f", type_of f_tm) and
 329       domain_var = mk_var ("domain", type_of domain_tm) in
 330   let hi_lt0_th = try EQT_ELIM (float_lt0 hi_tm) with Failure _ -> failwith "m_taylor_cell_pass0" in
 331     (MY_PROVE_HYP bound_th o MY_PROVE_HYP hi_lt0_th o
 332        INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real; lo_tm, lo_var_real] o
 333        inst_first_type_var n_type_array.(n)) M_CELL_PASS_INTERVAL_LEMMA';;
 334
 335 let m_taylor_cell_list_pass0 n bound_th =
 336   let tm0 = (snd o dest_forall o concl) bound_th in
 337   let int_tm, concl_tm = dest_comb tm0 in
 338   let domain_tm = (rand o rator o rand o rand o rand) int_tm in
 339   let ltm, bounds_tm = dest_interval_arith concl_tm in
 340   let f_tm, (lo_tm, hi_tm) = rator ltm, dest_pair bounds_tm in
 341   let f_var = mk_var ("f", type_of f_tm) and
 342       domain_var = mk_var ("domain", type_of domain_tm) in
 343   let hi_lt0_th = try EQT_ELIM (float_lt0 hi_tm) with Failure _ -> failwith "m_taylor_cell_list_pass0" in
 344     (MY_PROVE_HYP bound_th o MY_PROVE_HYP hi_lt0_th o
 345        INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real; lo_tm, lo_var_real] o
 346        inst_first_type_var n_type_array.(n)) M_CELL_LIST_PASS1_INTERVAL_LEMMA';;
 347
 348
 349
 350 (**********************)
 351
 352 let M_CELL_PASS_SUBDOMAIN' = (MY_RULE o prove)(`interval [domain2] SUBSET interval [domain] /\
 353                                                  m_cell_pass f domain ==> m_cell_pass f domain2`,
 354    REWRITE_TAC[m_cell_pass; SUBSET] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[]);;
 355
 356 let M_CELL_LIST_PASS_SUBDOMAIN' = (MY_RULE o prove)(`interval [domain2] SUBSET interval [domain] /\
 357                                                  m_cell_list_pass fs domain ==> m_cell_list_pass fs domain2`,
 358    REWRITE_TAC[m_cell_list_pass; SUBSET] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[]);;
 359
 360
 361 let m_cell_pass_subdomain domain2_tm pass_th =
 362   let f_tm, domain_tm = dest_m_cell_pass (concl pass_th) in
 363   let f_var = mk_var ("f", type_of f_tm) and
 364       domain_var = mk_var ("domain", type_of domain_tm) and
 365       domain2_var = mk_var ("domain2", type_of domain2_tm) in
 366   let a, b = dest_pair domain_tm and
 367       c, d = dest_pair domain2_tm in
 368   let n = get_dim a in
 369   let sub_th = m_subset_interval n a b c d in
 370     (MY_PROVE_HYP sub_th o MY_PROVE_HYP pass_th o
 371        INST[domain_tm, domain_var; domain2_tm, domain2_var; f_tm, f_var] o
 372        inst_first_type_var n_type_array.(n)) M_CELL_PASS_SUBDOMAIN';;
 373
 374
 375 let m_cell_list_pass_subdomain domain2_tm pass_th =
 376   let fs_tm, domain_tm = dest_m_cell_pass (concl pass_th) in
 377   let fs_var = mk_var ("fs", type_of fs_tm) and
 378       domain_var = mk_var ("domain", type_of domain_tm) and
 379       domain2_var = mk_var ("domain2", type_of domain2_tm) in
 380   let a, b = dest_pair domain_tm and
 381       c, d = dest_pair domain2_tm in
 382   let n = get_dim a in
 383   let sub_th = m_subset_interval n a b c d in
 384     (MY_PROVE_HYP sub_th o MY_PROVE_HYP pass_th o
 385        INST[domain_tm, domain_var; domain2_tm, domain2_var; fs_tm, fs_var] o
 386        inst_first_type_var n_type_array.(n)) M_CELL_LIST_PASS_SUBDOMAIN';;
 387
 388
 389
 390
 391
 392 (******************************)
 393
 394 let GLUE_LEMMA = prove(`!j x z v u P Q.
 395                          (!i. 1 <= i /\ i <= dimindex (:N) ==> ~(i = j) ==>
 396                             u$i = x$i /\ v$i = z$i) ==>
 397                          v$j = u$j ==>
 398                              (!p. p IN interval [x,v] ==> P p) ==>
 399                              (!p. p IN interval [u,z] ==> Q p) ==>
 400                              (!p. p IN interval [x,z:real^N] ==> P p \/ Q p)`,
 401    REWRITE_TAC[IN_INTERVAL] THEN REPEAT GEN_TAC THEN
 402      move ["eq1"; "eq_vu"; "cell1"; "cell2"; "y"; "ineq"] THEN
 403      ASM_CASES_TAC `(y:real^N)$j <= (v:real^N)$j` THENL
 404      [
 405        DISJ1_TAC THEN REMOVE_THEN "cell1" MATCH_MP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 406          USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
 407          ASM_CASES_TAC `i = j:num` THENL
 408          [
 409            REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN SIMP_TAC[];
 410            ALL_TAC
 411          ] THEN
 412          USE_THEN "eq1" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
 413          USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[];
 414        ALL_TAC
 415      ] THEN
 416
 417      POP_ASSUM (ASSUME_TAC o MATCH_MP (REAL_ARITH `~(a <= b) ==> b <= a:real`)) THEN
 418      DISJ2_TAC THEN REMOVE_THEN "cell2" MATCH_MP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 419      USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
 420      ASM_CASES_TAC `i = j:num` THENL
 421      [
 422        ASM_REWRITE_TAC[] THEN USE_THEN "eq_vu" (fun th -> REWRITE_TAC[SYM th]) THEN
 423          REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN SIMP_TAC[];
 424        ALL_TAC
 425      ] THEN
 426      USE_THEN "eq1" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
 427      USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[]);;
 428
 429 let M_CELL_PASS_GLUE_LEMMA = prove(`!j x z v u f.
 430                                      (!i. 1 <= i /\ i <= dimindex (:N) ==> ~(i = j) ==>
 431                                         u$i = x$i /\ v$i = z$i) ==>
 432                                      v$j = u$j ==>
 433                                          m_cell_pass f (x,v) ==>
 434                                          m_cell_pass f (u,z) ==>
 435                                          m_cell_pass f (x,z:real^N)`,
 436                                    REPEAT GEN_TAC THEN REWRITE_TAC[m_cell_pass] THEN
 437                                      DISCH_THEN (MP_TAC o MATCH_MP GLUE_LEMMA) THEN
 438                                      DISCH_THEN (MP_TAC o SPECL [`\x:real^N. f x < &0`; `\x:real^N. f x < &0`]) THEN
 439                                      REWRITE_TAC[]);;
 440
 441 let ITLIST_DISJ_APPEND = prove(`!P l1 l2. ITLIST (\a r. P a \/ r) (APPEND l1 l2) F
 442                                <=> ITLIST (\a r. P a \/ r) l1 F \/ ITLIST (\a r. P a \/ r) l2 F`,
 443                                GEN_TAC THEN LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[APPEND; ITLIST; APPEND_NIL] THEN
 444                                  ASM_REWRITE_TAC[ITLIST; DISJ_ACI]);;
 445
 446 let M_CELL_LIST_PASS_GLUE_LEMMA = prove(`!j x z v u fs1 fs2.
 447                                      (!i. 1 <= i /\ i <= dimindex (:N) ==> ~(i = j) ==>
 448                                         u$i = x$i /\ v$i = z$i) ==>
 449                                      v$j = u$j ==>
 450                                          m_cell_list_pass fs1 (x,v) ==>
 451                                          m_cell_list_pass fs2 (u,z) ==>
 452                                          m_cell_list_pass (APPEND fs1 fs2) (x,z:real^N)`,
 453                                    REPEAT GEN_TAC THEN REWRITE_TAC[m_cell_list_pass; ITLIST_DISJ_APPEND] THEN
 454                                      apply_tac GLUE_LEMMA);;
 455
 456
 457 let gen_glue_lemma n j =
 458   let mk_vars name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n) in
 459   let xs = mk_vars "x" and
 460       zs = mk_vars "z" and
 461       t_var = mk_var ("t", real_ty) and
 462       j_tm = mk_small_numeral j in
 463   let x_tm = mk_vector_list xs and
 464       z_tm = mk_vector_list zs and
 465       v_tm = mk_vector_list (map (fun i -> if i = j then t_var else List.nth zs (i - 1)) (1--n)) and
 466       u_tm = mk_vector_list (map (fun i -> if i = j then t_var else List.nth xs (i - 1)) (1--n)) in
 467   let gen_th lemma =
 468     let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; v_tm; u_tm]) lemma in
 469     let th1 = REWRITE_RULE[dimindex_array.(n); gen_in_interval n; ARITH] th0 in
 470     let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 471       MY_RULE th2 in
 472     gen_th M_CELL_PASS_GLUE_LEMMA, gen_th M_CELL_LIST_PASS_GLUE_LEMMA;;
 473
 474
 475 let glue_thms_array = Array.init (max_dim + 1)
 476   (fun n -> Array.init (n + 1)
 477      (fun j -> if j < 1 then TRUTH, TRUTH else gen_glue_lemma n j));;
 478
 479
 480 (***************************************)
 481 (* m_cell_list_pass reduction *)
 482
 483 let CELL_LIST_PASS_ACC_INTRO = prove(`m_cell_list_pass fs1 domain <=> m_cell_list_pass (APPEND fs1 []) domain`,
 484                                      REWRITE_TAC[APPEND_NIL]);;
 485
 486 let CELL_LIST_PASS_ACC_ELIM = SYM CELL_LIST_PASS_ACC_INTRO;;
 487
 488 let CELL_LIST_PASS_ACC_REV = prove(`m_cell_list_pass (APPEND acc (CONS h fs2)) domain
 489                                    <=> m_cell_list_pass (APPEND (CONS h acc) fs2) domain`,
 490                                    REWRITE_TAC[m_cell_list_pass; ITLIST_DISJ_APPEND; ITLIST; DISJ_ACI]);;
 491
 492 let CELL_LIST_PASS_NIL1 = prove(`m_cell_list_pass (APPEND (APPEND [] fs2) acc) domain
 493                                 <=> m_cell_list_pass (APPEND fs2 acc) domain`,
 494                                 REWRITE_TAC[APPEND]);;
 495
 496 let CELL_LIST_PASS_NIL2 = prove(`m_cell_list_pass (APPEND (APPEND fs1 []) acc) domain
 497                                 <=> m_cell_list_pass (APPEND fs1 acc) domain`,
 498                                 REWRITE_TAC[APPEND_NIL]);;
 499
 500 let CELL_LIST_PASS_SAME_HD = prove(`m_cell_list_pass (APPEND (APPEND (CONS h fs1) (CONS h fs2)) acc) domain
 501                                      <=> m_cell_list_pass (APPEND (APPEND fs1 fs2) (CONS h acc)) domain`,
 502                                    REWRITE_TAC[m_cell_list_pass; ITLIST_DISJ_APPEND; ITLIST; DISJ_ACI]);;
 503
 504 let CELL_LIST_PASS_MOVE1 = prove(`m_cell_list_pass (APPEND (APPEND (CONS h fs1) fs2) acc) domain
 505                                    <=> m_cell_list_pass (APPEND (APPEND fs1 fs2) (CONS h acc)) domain`,
 506                                  REWRITE_TAC[m_cell_list_pass; ITLIST_DISJ_APPEND; ITLIST; DISJ_ACI]);;
 507
 508 let CELL_LIST_PASS_MOVE2 = prove(`m_cell_list_pass (APPEND (APPEND fs1 (CONS h fs2)) acc) domain
 509                                    <=> m_cell_list_pass (APPEND (APPEND fs1 fs2) (CONS h acc)) domain`,
 510                                  REWRITE_TAC[m_cell_list_pass; ITLIST_DISJ_APPEND; ITLIST; DISJ_ACI]);;
 511
 512 (* pass_th should be in the form |- m_cell_list_pass (APPEND fs1 fs2) dom *)
 513 let merge_m_cell_list_pass n pass_th =
 514   let append_tm, dom_tm = dest_m_cell_pass (concl pass_th) in
 515   let list_ty = type_of append_tm in
 516   let dom_var = mk_var ("domain", type_of dom_tm) and
 517       fs1_var = mk_var ("fs1", list_ty) and
 518       fs2_var = mk_var ("fs2", list_ty) and
 519       acc_var = mk_var ("acc", list_ty) and
 520       h_var = mk_var ("h", (hd o snd o dest_type) list_ty) in
 521   let acc_intro, acc_elim, acc_rev, pass_nil1, pass_nil2, same_hd, pass_move1, pass_move2 =
 522     let r = inst_first_type_var n_type_array.(n) in
 523       r CELL_LIST_PASS_ACC_INTRO,
 524     r CELL_LIST_PASS_ACC_ELIM,
 525     r CELL_LIST_PASS_ACC_REV,
 526     r CELL_LIST_PASS_NIL1,
 527     r CELL_LIST_PASS_NIL2,
 528     r CELL_LIST_PASS_SAME_HD,
 529     r CELL_LIST_PASS_MOVE1,
 530     r CELL_LIST_PASS_MOVE2 in
 531
 532     (* Reverses the result list to preserve ordering *)
 533   let rec rev_acc th =
 534     let ltm, s_tm = (dest_comb o rand o rator o concl) th in
 535     let acc_tm = rand ltm in
 536       if is_comb s_tm then
 537         let h_tm, fs2_tm = dest_binary "CONS" s_tm in
 538         let th1 = INST[h_tm, h_var; fs2_tm, fs2_var; acc_tm, acc_var; dom_tm, dom_var] acc_rev in
 539         let th2 = EQ_MP th1 th in
 540           rev_acc th2
 541       else
 542         let th1 = INST[acc_tm, fs1_var; dom_tm, dom_var] acc_elim in
 543           EQ_MP th1 th in
 544
 545     (* Computes a merged list *)
 546   let rec merge_append th =
 547     let ltm, acc_tm = (dest_comb o rand o rator o concl) th in
 548     let fs1_tm, fs2_tm = dest_binary "APPEND" (rand ltm) in
 549       if not (is_comb fs1_tm) then
 550         let th1 = INST[fs2_tm, fs2_var; acc_tm, acc_var; dom_tm, dom_var] pass_nil1 in
 551           EQ_MP th1 th
 552       else if not (is_comb fs2_tm) then
 553         let th1 = INST[fs1_tm, fs1_var; acc_tm, acc_var; dom_tm, dom_var] pass_nil2 in
 554           EQ_MP th1 th
 555       else
 556         let h1_tm, t1_tm = dest_binary "CONS" fs1_tm and
 557             h2_tm, t2_tm = dest_binary "CONS" fs2_tm in
 558         let th1 =
 559           match (compare h1_tm h2_tm) with
 560             | -1 -> INST[h1_tm, h_var; t1_tm, fs1_var; fs2_tm, fs2_var; acc_tm, acc_var; dom_tm, dom_var] pass_move1
 561             | 1 -> INST[h2_tm, h_var; t2_tm, fs2_var; fs1_tm, fs1_var; acc_tm, acc_var; dom_tm, dom_var] pass_move2
 562             | _ -> INST[h1_tm, h_var; t1_tm, fs1_var; t2_tm, fs2_var; acc_tm, acc_var; dom_tm, dom_var] same_hd in
 563         let th2 = EQ_MP th1 th in
 564           merge_append th2 in
 565
 566   let th0 = EQ_MP (INST[append_tm, fs1_var; dom_tm, dom_var] acc_intro) pass_th in
 567   let th1 = merge_append th0 in
 568     rev_acc th1;;
 569
 570 (*
 571 compare `\x:real^2. x$1` `\x:real^2. x$1 + x$2`;;
 572
 573 let test_th = ASSUME `m_cell_list_pass (APPEND [\x:real^2. x$1; \x:real^2. x$1 + x$2] [\x:real^2. x$1 + x$2; \x:real^2. x$1 * x$2]) dom`;;
 574 merge_m_cell_list_pass 2 test_th;;
 575
 576
 577 (rand o rator o concl) test_th;;
 578 test 1000 (merge_m_cell_list_pass 2) test_th;;
 579
 580 *)
 581
 582 (***************************************)
 583
 584 let M_CELL_SUP = prove(`!f x z. lift o f continuous_on interval [x,z:real^N] /\ m_cell_pass f (x,z) ==>
 585                          ?a. a < &0 /\ !y. y IN interval [x,z] ==> f y <= a`,
 586    REWRITE_TAC[m_cell_pass] THEN REPEAT STRIP_TAC THEN
 587      ASM_CASES_TAC `interval [x:real^N,z] = {}` THENL
 588      [
 589        EXISTS_TAC `-- &1` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN REAL_ARITH_TAC;
 590        ALL_TAC
 591      ] THEN
 592      MP_TAC (SPECL [`f:real^N->real`; `interval [x,z:real^N]`] CONTINUOUS_ATTAINS_SUP) THEN
 593      ASM_REWRITE_TAC[COMPACT_INTERVAL] THEN
 594      DISCH_THEN (X_CHOOSE_THEN `y:real^N` STRIP_ASSUME_TAC) THEN
 595      EXISTS_TAC `(f:real^N->real) y` THEN ASM_REWRITE_TAC[] THEN
 596      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 597
 598
 599 let DIFF2_DOMAIN_IMP_CONTINUOUS_ON = prove(`!(f:real^N->real) domain. diff2_domain domain f ==>
 600                                              lift o f continuous_on interval [domain]`,
 601    REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
 602      MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN REPEAT STRIP_TAC THEN
 603      MATCH_MP_TAC DIFFERENTIABLE_IMP_CONTINUOUS_AT THEN
 604      MATCH_MP_TAC diff2_imp_diff THEN
 605      ASM_SIMP_TAC[]);;
 606
 607
 608
 609 let M_CELL_INCREASING_PASS_LEMMA = prove(`!j x z u domain lo f.
 610                                            interval [x,z] SUBSET interval [domain] ==>
 611                                            diff2c_domain domain f ==>
 612                                            (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==> u$i = x$i) ==>
 613                                            u$j = z$j ==>
 614                                                &0 <= lo ==>
 615                                                (!y. y IN interval [domain] ==> lo <= partial j f y) ==>
 616                                                m_cell_pass f (u,z) ==>
 617                                                m_cell_pass f (x,z:real^N)`,
 618    REWRITE_TAC[SUBSET] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[m_cell_pass] THEN
 619      X_GEN_TAC `y:real^N` THEN
 620      ASM_CASES_TAC `~(!i. i IN 1..dimindex (:N) ==> (x:real^N)$i <= (z:real^N)$i)` THENL
 621      [
 622        POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; IN_INTERVAL; GSYM IN_NUMSEG] THEN
 623          DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
 624          DISCH_THEN (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 625          POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 626        ALL_TAC
 627      ] THEN
 628      POP_ASSUM MP_TAC THEN REWRITE_TAC[negbK] THEN DISCH_TAC THEN
 629      SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL
 630      [
 631        UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN
 632          SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
 633        ALL_TAC
 634      ] THEN
 635      MP_TAC (SPECL [`f:real^N->real`; `u:real^N`; `z:real^N`] M_CELL_SUP) THEN
 636      ANTS_TAC THENL
 637      [
 638        ASM_REWRITE_TAC[] THEN
 639          MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
 640          UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN
 641          REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
 642          REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN
 643          POP_ASSUM MP_TAC THEN
 644          REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 645          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 646          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
 647          ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 648          FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
 649        ALL_TAC
 650      ] THEN
 651      DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN DISCH_TAC THEN
 652      MP_TAC (SPECL [`f:real^N->real`; `j:num`; `u:real^N`; `x:real^N`; `z:real^N`; `a:real`] partial_increasing_right) THEN
 653      ASM_REWRITE_TAC[] THEN
 654      ANTS_TAC THENL
 655      [
 656        REPEAT STRIP_TAC THEN
 657          MATCH_MP_TAC diff2_imp_diff THEN
 658          UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN REWRITE_TAC[diff2_domain] THEN
 659          DISCH_THEN MATCH_MP_TAC THEN
 660          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
 661        ALL_TAC
 662      ] THEN
 663      ANTS_TAC THENL
 664      [
 665        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 666          EXISTS_TAC `lo:real` THEN ASM_REWRITE_TAC[] THEN
 667          REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
 668        ALL_TAC
 669      ] THEN
 670      DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
 671      EXISTS_TAC `a:real` THEN ASM_REWRITE_TAC[] THEN
 672      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 673
 674
 675
 676 let M_CELL_DECREASING_PASS_LEMMA = prove(`!j x z u domain hi f.
 677                                            interval [x,z] SUBSET interval [domain] ==>
 678                                            diff2c_domain domain f ==>
 679                                            (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==> u$i = z$i) ==>
 680                                            u$j = x$j ==>
 681                                                hi <= &0 ==>
 682                                                (!y. y IN interval [domain] ==> partial j f y <= hi) ==>
 683                                                m_cell_pass f (x,u) ==>
 684                                                m_cell_pass f (x,z:real^N)`,
 685    REWRITE_TAC[SUBSET] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[m_cell_pass] THEN X_GEN_TAC `y:real^N` THEN
 686      ASM_CASES_TAC `~(!i. i IN 1..dimindex (:N) ==> (x:real^N)$i <= (z:real^N)$i)` THENL
 687      [
 688        POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; IN_INTERVAL; GSYM IN_NUMSEG] THEN
 689          DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
 690          DISCH_THEN (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 691          POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 692        ALL_TAC
 693      ] THEN
 694      POP_ASSUM MP_TAC THEN REWRITE_TAC[negbK] THEN DISCH_TAC THEN
 695      SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL
 696      [
 697        UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN
 698          SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
 699        ALL_TAC
 700      ] THEN
 701      MP_TAC (SPECL [`f:real^N->real`; `x:real^N`; `u:real^N`] M_CELL_SUP) THEN
 702      ANTS_TAC THENL
 703      [
 704        ASM_REWRITE_TAC[] THEN
 705          MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
 706          UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN
 707          REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
 708          REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN
 709          POP_ASSUM MP_TAC THEN
 710          REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 711          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 712          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
 713          ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 714          FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
 715        ALL_TAC
 716      ] THEN
 717      DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN DISCH_TAC THEN
 718      MP_TAC (SPECL [`f:real^N->real`; `j:num`; `u:real^N`; `x:real^N`; `z:real^N`; `a:real`] partial_decreasing_left) THEN
 719      ASM_REWRITE_TAC[] THEN
 720      ANTS_TAC THENL
 721      [
 722        REPEAT STRIP_TAC THEN
 723          MATCH_MP_TAC diff2_imp_diff THEN
 724          UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN REWRITE_TAC[diff2_domain] THEN
 725          DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
 726          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
 727        ALL_TAC
 728      ] THEN
 729      ANTS_TAC THENL
 730      [
 731        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 732          EXISTS_TAC `hi:real` THEN ASM_REWRITE_TAC[] THEN
 733          REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
 734        ALL_TAC
 735      ] THEN
 736      DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
 737      EXISTS_TAC `a:real` THEN ASM_REWRITE_TAC[] THEN
 738      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 739
 740
 741
 742 let M_CELL_CONVEX_PASS_LEMMA = prove(`!j x z u v lo f.
 743                 diff2c_domain (x,z) f ==>
 744                 (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==> u$i = z$i /\ v$i = x$i) ==>
 745                 u$j = x$j ==> v$j = z$j ==>
 746                     &0 <= lo ==>
 747                     (!y. y IN interval [x,z] ==> lo <= partial2 j j f y) ==>
 748                     m_cell_pass f (x,u) ==>
 749                     m_cell_pass f (v,z) ==>
 750                     m_cell_pass f (x:real^N,z)`,
 751    REPEAT STRIP_TAC THEN REWRITE_TAC[m_cell_pass] THEN
 752      X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
 753      SUBGOAL_THEN `!i. i IN 1..dimindex (:N) ==> (x:real^N)$i <= (z:real^N)$i` ASSUME_TAC THENL
 754      [
 755        POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_INTERVAL] THEN REPEAT STRIP_TAC THEN
 756          MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(y:real^N)$i` THEN
 757          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[GSYM IN_NUMSEG];
 758        ALL_TAC
 759      ] THEN
 760      SUBGOAL_THEN `diff2_domain (x,z) (f:real^N->real)` ASSUME_TAC THENL
 761      [
 762        UNDISCH_TAC `diff2c_domain (x,z) (f:real^N->real)` THEN
 763          SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
 764        ALL_TAC
 765      ] THEN
 766      MP_TAC (SPECL [`f:real^N->real`; `v:real^N`; `z:real^N`] M_CELL_SUP) THEN
 767      ANTS_TAC THENL
 768      [
 769        ASM_REWRITE_TAC[] THEN
 770          MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
 771          UNDISCH_TAC `diff2_domain (x,z) (f:real^N->real)` THEN
 772          REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
 773          FIRST_X_ASSUM MATCH_MP_TAC THEN
 774          POP_ASSUM MP_TAC THEN
 775          REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 776          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 777          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
 778          ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 779          FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
 780        ALL_TAC
 781      ] THEN
 782      DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
 783
 784      MP_TAC (SPECL [`f:real^N->real`; `x:real^N`; `u:real^N`] M_CELL_SUP) THEN
 785      ANTS_TAC THENL
 786      [
 787        ASM_REWRITE_TAC[] THEN
 788          MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
 789          UNDISCH_TAC `diff2_domain (x,z) (f:real^N->real)` THEN
 790          REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
 791          FIRST_X_ASSUM MATCH_MP_TAC THEN
 792          POP_ASSUM MP_TAC THEN
 793          REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 794          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 795          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
 796          ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 797          FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
 798        ALL_TAC
 799      ] THEN
 800      DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
 801
 802      MP_TAC (SPECL [`f:real^N->real`; `j:num`; `x:real^N`; `z:real^N`; `u:real^N`; `v:real^N`; `max a a'`] partial_convex_max) THEN
 803      ASM_REWRITE_TAC[] THEN
 804      ANTS_TAC THENL
 805      [
 806        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 807          EXISTS_TAC `lo:real` THEN ASM_REWRITE_TAC[] THEN
 808          REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
 809        ALL_TAC
 810      ] THEN
 811      ANTS_TAC THENL
 812      [
 813        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 814          EXISTS_TAC `a':real` THEN
 815          ASM_SIMP_TAC[] THEN REAL_ARITH_TAC;
 816        ALL_TAC
 817      ] THEN
 818      ANTS_TAC THENL
 819      [
 820        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 821          EXISTS_TAC `a:real` THEN
 822          ASM_SIMP_TAC[] THEN REAL_ARITH_TAC;
 823        ALL_TAC
 824      ] THEN
 825
 826      DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
 827      EXISTS_TAC `max a a'` THEN
 828      ASM_SIMP_TAC[] THEN
 829      ASM_REAL_ARITH_TAC);;
 830
 831
 832
 833 (*********************)
 834
 835 let ZERO_EQ_ZERO_CONST = prove(`0 = _0`, REWRITE_TAC[NUMERAL]);;
 836
 837 let gen_increasing_lemma n j =
 838   let mk_vars name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n) in
 839   let xs = mk_vars "x" and
 840       zs = mk_vars "z" and
 841       j_tm = mk_small_numeral j in
 842   let x_tm = mk_vector_list xs and
 843       z_tm = mk_vector_list zs and
 844       u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then zs else xs) (i - 1)) (1--n)) in
 845   let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; u_tm]) M_CELL_INCREASING_PASS_LEMMA in
 846   let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
 847   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 848   let th3 = MY_RULE_NUM th2 in
 849     (UNDISCH_ALL o ONCE_REWRITE_RULE[GSYM ZERO_EQ_ZERO_CONST] o DISCH (last (hyp th3))) th3;;
 850
 851
 852 let gen_mono_lemma0 th =
 853   let h2 = List.nth (hyp th) 1 in
 854   let domain_tm = (lhand o rand o lhand) h2 in
 855   let domain_var = mk_var ("domain", type_of domain_tm) in
 856     (UNDISCH_ALL o REWRITE_RULE[SUBSET_REFL] o DISCH_ALL o INST[domain_tm, domain_var]) th;;
 857
 858 let incr_gen_thms_array = Array.init (max_dim + 1)
 859   (fun n -> Array.init (n + 1)
 860      (fun j -> if j < 1 then TRUTH else gen_increasing_lemma n j));;
 861
 862 let incr_thms_array = Array.init (max_dim + 1)
 863   (fun n -> Array.init (n + 1)
 864      (fun j -> if j < 1 then TRUTH else gen_mono_lemma0 incr_gen_thms_array.(n).(j)));;
 865
 866
 867
 868 let gen_decreasing_lemma n j =
 869   let mk_vars name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n) in
 870   let xs = mk_vars "x" and
 871       zs = mk_vars "z" and
 872       j_tm = mk_small_numeral j in
 873   let x_tm = mk_vector_list xs and
 874       z_tm = mk_vector_list zs and
 875       u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then xs else zs) (i - 1)) (1--n)) in
 876   let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; u_tm]) M_CELL_DECREASING_PASS_LEMMA in
 877   let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
 878   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 879   let th3 = MY_RULE_NUM th2 in
 880     (UNDISCH_ALL o ONCE_REWRITE_RULE[GSYM ZERO_EQ_ZERO_CONST] o DISCH (last (hyp th3))) th3;;
 881
 882
 883 let decr_gen_thms_array = Array.init (max_dim + 1)
 884   (fun n -> Array.init (n + 1)
 885      (fun j -> if j < 1 then TRUTH else gen_decreasing_lemma n j));;
 886
 887 let decr_thms_array = Array.init (max_dim + 1)
 888   (fun n -> Array.init (n + 1)
 889      (fun j -> if j < 1 then TRUTH else gen_mono_lemma0 decr_gen_thms_array.(n).(j)));;
 890
 891
 892 (****************************************)
 893
 894 let gen_convex_max_lemma n j =
 895   let xs = mk_real_vars n "x" and
 896       zs = mk_real_vars n "z" and
 897       j_tm = mk_small_numeral j in
 898   let x_tm = mk_vector_list xs and
 899       z_tm = mk_vector_list zs and
 900       u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then xs else zs) (i - 1)) (1--n)) and
 901       v_tm = mk_vector_list (map (fun i -> List.nth (if i = j then zs else xs) (i - 1)) (1--n)) in
 902   let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; u_tm; v_tm]) M_CELL_CONVEX_PASS_LEMMA in
 903   let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
 904   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 905   let th3 = MY_RULE_NUM th2 in
 906     (UNDISCH_ALL o ONCE_REWRITE_RULE[GSYM ZERO_EQ_ZERO_CONST] o DISCH (last (hyp th3))) th3;;
 907
 908
 909 let convex_thms_array = Array.init (max_dim + 1)
 910   (fun n -> Array.init (n + 1)
 911      (fun j -> if j < 1 then TRUTH else gen_convex_max_lemma n j));;
 912
 913
 914
 915 (******************************************)
 916
 917 let m_glue_cells n j pass_th1 pass_th2 =
 918   let f_tm, domain1 = dest_m_cell_pass (concl pass_th1) and
 919       domain2 = rand (concl pass_th2) in
 920   let x1, z1 = dest_pair domain1 and
 921       x2, z2 = dest_pair domain2 in
 922
 923   let x1s = dest_vector x1 and
 924       x2s = dest_vector x2 and
 925       z2s = dest_vector z2 in
 926
 927   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
 928       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
 929       f_var = mk_var ("f", type_of f_tm) and
 930       t_tm = List.nth x2s (j - 1) in
 931
 932   let th0 = (INST[t_tm, t_var_real; f_tm, f_var] o
 933                INST (zip z2s z_vars) o INST (zip x1s x_vars)) (fst glue_thms_array.(n).(j)) in
 934     (MY_PROVE_HYP pass_th1 o MY_PROVE_HYP pass_th2) th0;;
 935
 936
 937 let m_glue_cells_list n j pass_th1 pass_th2 =
 938   let fs1_tm, domain1 = dest_m_cell_pass (concl pass_th1) and
 939       fs2_tm, domain2 = dest_m_cell_pass (concl pass_th2) in
 940   let x1, z1 = dest_pair domain1 and
 941       x2, z2 = dest_pair domain2 in
 942
 943   let x1s = dest_vector x1 and
 944       x2s = dest_vector x2 and
 945       z2s = dest_vector z2 in
 946
 947   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
 948       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
 949       fs1_var = mk_var ("fs1", type_of fs1_tm) and
 950       fs2_var = mk_var ("fs2", type_of fs2_tm) and
 951       t_tm = List.nth x2s (j - 1) in
 952
 953   let th0 = (INST[t_tm, t_var_real; fs1_tm, fs1_var; fs2_tm, fs2_var] o
 954                INST (zip z2s z_vars) o INST (zip x1s x_vars)) (snd glue_thms_array.(n).(j)) in
 955     (MY_PROVE_HYP pass_th1 o MY_PROVE_HYP pass_th2) th0;;
 956
 957
 958 (**********************)
 959
 960 let m_mono_pass_gen n j decr_flag diff2_th partial_mono_th sub_th pass_th =
 961   let f_tm, domain0 = dest_m_cell_pass (concl pass_th) and
 962       domain = (rand o rator o concl) diff2_th and
 963       xv, zv = (dest_pair o lhand o rand o lhand o concl) sub_th and
 964       bound_tm = ((if decr_flag then rand else lhand) o rand o snd o dest_forall o concl) partial_mono_th in
 965
 966   let xs = dest_vector xv and
 967       zs = dest_vector zv in
 968
 969   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
 970       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
 971       domain_var = mk_var ("domain", type_of domain) and
 972       f_var = mk_var ("f", type_of f_tm) and
 973       bound_var = mk_var ((if decr_flag then "hi" else "lo"), real_ty) in
 974
 975   let le_th0 = (if decr_flag then float_le0 else float_ge0) bound_tm in
 976   let le_th = try EQT_ELIM le_th0 with Failure _ ->
 977     failwith (sprintf "m_mono_pass_gen: j = %d, th = %s" j (string_of_thm le_th0)) in
 978
 979   let th0 = (INST[f_tm, f_var; bound_tm, bound_var; domain, domain_var] o
 980           INST (zip xs x_vars) o INST (zip zs z_vars))
 981     (if decr_flag then decr_gen_thms_array.(n).(j) else incr_gen_thms_array.(n).(j)) in
 982     (MY_PROVE_HYP le_th o MY_PROVE_HYP pass_th o MY_PROVE_HYP diff2_th o
 983        MY_PROVE_HYP sub_th o MY_PROVE_HYP partial_mono_th) th0;;
 984
 985
 986
 987 (* m_incr_pass *)
 988 let m_incr_pass n pp j m_taylor_th pass_th0 =
 989   let _, diff2_th, _, _ = dest_m_taylor_thms n m_taylor_th in
 990   let partial_bound = eval_m_taylor_partial_lower n pp j m_taylor_th in
 991
 992   let f_tm, domain0 = dest_m_cell_pass (concl pass_th0) and
 993       domain = (rand o rator o concl) diff2_th and
 994       lo_tm = (lhand o rand o snd o dest_forall o concl) partial_bound in
 995   let lo_ge0_th = EQT_ELIM (float_ge0 lo_tm) in
 996
 997   let x_tm, z_tm = dest_pair domain in
 998   let xs = dest_vector x_tm and
 999       zs = dest_vector z_tm in
1000
1001   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
1002       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
1003       f_var = mk_var ("f", type_of f_tm) in
1004   let th0 = (INST[f_tm, f_var; lo_tm, lo_var_real] o
1005                INST (zip zs z_vars) o INST (zip xs x_vars)) incr_thms_array.(n).(j) in
1006     (MY_PROVE_HYP lo_ge0_th o MY_PROVE_HYP pass_th0 o
1007        MY_PROVE_HYP diff2_th o MY_PROVE_HYP partial_bound) th0;;
1008
1009
1010 (* m_decr_pass *)
1011 let m_decr_pass n pp j m_taylor_th pass_th0 =
1012   let _, diff2_th, _, _ = dest_m_taylor_thms n m_taylor_th in
1013   let partial_bound = eval_m_taylor_partial_upper n pp j m_taylor_th in
1014
1015   let f_tm, domain0 = dest_m_cell_pass (concl pass_th0) and
1016       domain = (rand o rator o concl) diff2_th and
1017       hi_tm = (rand o rand o snd o dest_forall o concl) partial_bound in
1018   let hi_le0_th = EQT_ELIM (float_le0 hi_tm) in
1019
1020   let x_tm, z_tm = dest_pair domain in
1021   let xs = dest_vector x_tm and
1022       zs = dest_vector z_tm in
1023
1024   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
1025       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
1026       f_var = mk_var ("f", type_of f_tm) in
1027   let th0 = (INST[f_tm, f_var; hi_tm, hi_var_real] o
1028                INST (zip zs z_vars) o INST (zip xs x_vars)) decr_thms_array.(n).(j) in
1029     (MY_PROVE_HYP hi_le0_th o MY_PROVE_HYP pass_th0 o
1030        MY_PROVE_HYP diff2_th o MY_PROVE_HYP partial_bound) th0;;
1031
1032 (*************************)
1033
1034 (* m_convex_pass *)
1035 let m_convex_pass n j diff2_th partial2_bound_th pass1_th pass2_th =
1036   let f_tm, domain1 = dest_m_cell_pass (concl pass1_th) and
1037       _, domain2 = dest_m_cell_pass (concl pass2_th) in
1038   let x_tm, _ = dest_pair domain1 and
1039       _, z_tm = dest_pair domain2 and
1040       bound_tm = (lhand o rand o snd o dest_forall o concl) partial2_bound_th in
1041
1042   let xs = dest_vector x_tm and
1043       zs = dest_vector z_tm in
1044
1045   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
1046       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
1047       f_var = mk_var ("f", type_of f_tm) in
1048
1049   let le_th0 = float_ge0 bound_tm in
1050   let le_th =
1051     try EQT_ELIM le_th0 with Failure _ -> failwith ("m_convex_pass: "^string_of_thm le_th0) in
1052
1053   let th0 = (INST[f_tm, f_var; bound_tm, lo_var_real] o
1054                INST (zip xs x_vars) o INST (zip zs z_vars)) convex_thms_array.(n).(j) in
1055     (MY_PROVE_HYP le_th o MY_PROVE_HYP pass1_th o MY_PROVE_HYP pass2_th o
1056        MY_PROVE_HYP diff2_th o MY_PROVE_HYP partial2_bound_th) th0;;
1057
1058
1059
1060
1061 (***********************)
1062
1063 (* split_domain *)
1064
1065 let split_domain n pp j domain_th =
1066   let domain_tm, y_tm, _ = dest_m_cell_domain (concl domain_th) in
1067   let x_tm, z_tm = dest_pair domain_tm in
1068   let xs = dest_vector x_tm and
1069       zs = dest_vector z_tm and
1070       t = List.nth (dest_vector y_tm) (j - 1) in
1071
1072   let vv = map (fun i -> if i = j then t else List.nth zs (i - 1)) (1--n) and
1073       uu = map (fun i -> if i = j then t else List.nth xs (i - 1)) (1--n) in
1074
1075   let domain1_th = mk_m_center_domain n pp (rand x_tm) (mk_list (vv, real_ty)) and
1076       domain2_th = mk_m_center_domain n pp (mk_list (uu, real_ty)) (rand z_tm) in
1077     domain1_th, domain2_th;;
1078
1079
1080 (* restrict_domain *)
1081
1082 let restrict_domain n j left_flag domain_th =
1083   let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
1084   let x_tm, z_tm = dest_pair domain_tm in
1085   let xs = dest_vector x_tm and
1086       zs = dest_vector z_tm and
1087       ys = dest_vector y_tm and
1088       ws = dest_vector w_tm in
1089
1090   let th0 = (INST (zip xs (mk_real_vars n "x")) o INST (zip zs (mk_real_vars n "z")) o
1091                INST (zip ys (mk_real_vars n "y")) o INST (zip ws (mk_real_vars n "w")))
1092     (if left_flag then left_restrict_thms_array.(n).(j) else right_restrict_thms_array.(n).(j)) in
1093   let ths = CONJUNCTS (MY_PROVE_HYP domain_th th0) in
1094     hd ths, hd (tl ths);;
1095
1096
1097
1098
1099 (****************************************)
1100
1101 open Verifier;;
1102 open Recurse;;
1103
1104 let m_verify_raw (report_start, total_size) n pp fs certificate domain_th0 th_list =
1105   let r_size = result_size certificate in
1106   let r_size2 = float_of_int (if total_size > 0 then total_size else (if r_size > 0 then r_size else 1)) in
1107   let k = ref 0 in
1108   let kk = ref report_start in
1109   let last_report = ref (int_of_float (float_of_int !kk /. r_size2 *. 100.0)) in
1110
1111   let rec rec_verify =
1112     let rec apply_trans sub_ths th0 acc =
1113       match sub_ths with
1114         | [] -> rev acc
1115         | th :: ths ->
1116             let th' = eval_subset_trans th th0 in
1117               apply_trans ths th' (th' :: acc) in
1118
1119     let rec mk_domains mono th0 acc =
1120       match mono with
1121         | [] -> rev acc
1122         | m :: ms ->
1123             let j, flag = m.variable, m.decr_flag in
1124             let ths = restrict_domain n j flag th0 in
1125               mk_domains ms (fst ths) (ths :: acc) in
1126
1127     let verify_mono mono domain_th certificate =
1128       let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1129       let xx, zz = dest_pair domain in
1130       let df0_flags = itlist (fun m b -> m.df0_flag & b) mono true in
1131       let _ = !info_print_level < 2 or (report (sprintf "df0_flags = %b" df0_flags); true) in
1132       let taylor_th, diff2_th =
1133         if df0_flags then
1134           TRUTH, fs.diff2_f xx zz
1135         else
1136           let t_th = fs.taylor pp pp domain_th in
1137           let _, d_th, _, _ = dest_m_taylor_thms n t_th in
1138             t_th, d_th in
1139
1140       let domain_ths = mk_domains mono domain_th [] in
1141 (*      let domains = domain_th :: map fst (butlast domain_ths) in *)
1142
1143 (*      let gen_mono (m, domain_th) = *)
1144       let gen_mono m =
1145         if m.df0_flag then
1146           if m.decr_flag then
1147             eval_interval_arith_hi n (fs.df m.variable pp xx zz)
1148           else
1149             eval_interval_arith_lo n (fs.df m.variable pp xx zz)
1150         else
1151           if m.decr_flag then
1152             eval_m_taylor_partial_upper n pp m.variable taylor_th
1153           else
1154             eval_m_taylor_partial_lower n pp m.variable taylor_th in
1155
1156 (*      let mono_ths = map gen_mono (zip mono domains) in *)
1157       let mono_ths = map gen_mono mono in
1158       let pass_th0 = rec_verify ((fst o last) domain_ths) certificate in
1159       let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths in
1160       let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [] in
1161       let th = rev_itlist (fun ((m, mono_th), sub_th) pass_th ->
1162                              let j, flag = m.variable, m.decr_flag in
1163                                m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th)
1164         (rev (zip (zip mono mono_ths) sub_ths)) pass_th0 in
1165         if hyp th <> [] then failwith ("hyp <> []: "^string_of_thm th) else th in
1166
1167
1168
1169       fun domain_th certificate ->
1170         match certificate with
1171           | Result_mono (mono, r1) ->
1172               let _ = !info_print_level < 2 or
1173                 (let mono_strs =
1174                    map (fun m -> sprintf "%s%d (%b)" (if m.decr_flag then "-" else "")
1175                           m.variable m.df0_flag) mono in
1176                    report (sprintf "Mono: [%s]" (String.concat ";" mono_strs)); true) in
1177                 verify_mono mono domain_th r1
1178
1179           | Result_pass (_, f0_flag) ->
1180               let _ = k := !k + 1 in
1181               let _ = !info_print_level < 2 or
1182                 (report (sprintf "Verifying: %d/%d (f0_flag = %b)" !k r_size f0_flag); true) in
1183               let _ = !info_print_level < 1 or
1184                 (let r = int_of_float (float_of_int !kk /. r_size2 *. 100.0) in
1185                  let _ = if r <> !last_report then (last_report := r; report0 (sprintf "%d " r)) else () in true) in
1186                 if f0_flag then
1187                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1188                   let xx, zz = dest_pair domain in
1189                     m_taylor_cell_pass0 n (fs.f pp xx zz)
1190                 else
1191                   let taylor_th = fs.taylor pp pp domain_th in
1192                     m_taylor_cell_pass n pp taylor_th
1193
1194           | Result_glue (i, convex_flag, r1, r2) ->
1195               let domain1_th, domain2_th =
1196                 if convex_flag then
1197                   let d1, _ = restrict_domain n (i + 1) true domain_th in
1198                   let d2, _ = restrict_domain n (i + 1) false domain_th in
1199                     d1, d2
1200                 else
1201                   split_domain n pp (i + 1) domain_th in
1202               let th1 = rec_verify domain1_th r1 in
1203               let th2 = rec_verify domain2_th r2 in
1204                 if convex_flag then
1205                   let _ = !info_print_level < 2 or (report (sprintf "GlueConvex: %d" (i + 1)); true) in
1206                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1207                   let xx, zz = dest_pair domain in
1208                   let diff2_th = fs.diff2_f xx zz in
1209                   let partial2_th = fs.ddf (i + 1) (i + 1) pp xx zz in
1210                   let lo_partial2_th = eval_interval_arith_lo n partial2_th in
1211                     m_convex_pass n (i + 1) diff2_th lo_partial2_th th1 th2
1212                 else
1213                   m_glue_cells n (i + 1) th1 th2
1214
1215           | Result_pass_ref i ->
1216               let _ = !info_print_level < 2 or (report (sprintf "Ref: %d" i); true) in
1217                 if i > 0 then
1218                   List.nth th_list (i - 1)
1219                 else
1220                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1221                   let pass_th = List.nth th_list (-i - 1) in
1222                     m_cell_pass_subdomain domain pass_th
1223
1224           | _ -> failwith "False result" in
1225
1226     rec_verify domain_th0 certificate;;
1227
1228
1229 (*****************)
1230
1231
1232 let m_verify_raw0 n pp fs certificate xx zz =
1233   m_verify_raw (0, 0) n pp fs certificate (mk_m_center_domain n pp xx zz) [];;
1234
1235
1236
1237 let m_verify_list n pp fs certificate_list xx zz =
1238   let domain_hash = Hashtbl.create (length certificate_list * 10) in
1239   let mem, find, add = Hashtbl.mem domain_hash,
1240     Hashtbl.find domain_hash, Hashtbl.add domain_hash in
1241
1242   let get_m_cell_domain n pp domain0 path =
1243     let rec get_rec domain_th path hash =
1244       match path with
1245         | [] -> domain_th
1246         | (s, j) :: ps ->
1247             let hash' = hash^s^(string_of_int j) in
1248               if mem hash' then
1249                 get_rec (find hash') ps hash'
1250               else
1251                 if s = "l" or s = "r" then
1252                   let domain1_th, domain2_th = split_domain n pp j domain_th in
1253                   let hash1 = hash^"l"^(string_of_int j) and
1254                       hash2 = hash^"r"^(string_of_int j) in
1255                   let _ = add hash1 domain1_th; add hash2 domain2_th in
1256                     if s = "l" then
1257                       get_rec domain1_th ps hash'
1258                     else
1259                       get_rec domain2_th ps hash'
1260                 else
1261                   let l_flag = (s = "ml") in
1262                   let domain_th', _ = restrict_domain n j l_flag domain_th in
1263                   let _ = add hash' domain_th' in
1264                     get_rec domain_th' ps hash' in
1265       get_rec domain0 path "" in
1266
1267   let domain_th0 = mk_m_center_domain n pp xx zz in
1268   let size = length certificate_list in
1269   let k = ref 0 in
1270   let kk = ref 0 in
1271   let total_size = end_itlist (+) (map (result_size o snd) certificate_list) in
1272
1273   let rec rec_verify certificate_list th_list =
1274     match certificate_list with
1275       | [] -> last th_list
1276       | (path, certificate) :: cs ->
1277           let _ = k := !k + 1 in
1278           let _ = !info_print_level < 2 or (report (sprintf "List: %d/%d" !k size); true) in
1279           let domain_th = get_m_cell_domain n pp domain_th0 path in
1280           let th = m_verify_raw (!kk, total_size) n pp fs certificate domain_th th_list in
1281           let _ = kk := !kk + result_size certificate in
1282             rec_verify cs (th_list @ [th]) in
1283     rec_verify certificate_list [];;
1284
1285
1286 (***************************)
1287 (* Verification based on a p_result_tree *)
1288
1289 let m_p_verify_raw (report_start, total_size) n p_split fs certificate domain_th0 th_list =
1290   let r_size = p_result_size certificate in
1291   let r_size2 = float_of_int (if total_size > 0 then total_size else (if r_size > 0 then r_size else 1)) in
1292   let k = ref 0 in
1293   let kk = ref report_start in
1294   let last_report = ref (int_of_float (float_of_int !kk /. r_size2 *. 100.0)) in
1295
1296   let rec rec_verify =
1297     let rec apply_trans sub_ths th0 acc =
1298       match sub_ths with
1299         | [] -> rev acc
1300         | th :: ths ->
1301             let th' = eval_subset_trans th th0 in
1302               apply_trans ths th' (th' :: acc) in
1303
1304     let rec mk_domains mono th0 acc =
1305       match mono with
1306         | [] -> rev acc
1307         | m :: ms ->
1308             let j, flag = m.variable, m.decr_flag in
1309             let ths = restrict_domain n j flag th0 in
1310               mk_domains ms (fst ths) (ths :: acc) in
1311
1312     let verify_mono p_stat mono domain_th certificate =
1313       let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1314       let xx, zz = dest_pair domain in
1315       let df0_flags = itlist (fun m b -> m.df0_flag & b) mono true in
1316       let _ = !info_print_level < 2 or (report (sprintf "df0_flags = %b" df0_flags); true) in
1317       let taylor_th, diff2_th =
1318         if df0_flags then
1319           TRUTH, fs.diff2_f xx zz
1320         else
1321           let t_th = fs.taylor p_stat.pp p_stat.pp domain_th in
1322           let _, d_th, _, _ = dest_m_taylor_thms n t_th in
1323             t_th, d_th in
1324
1325       let domain_ths = mk_domains mono domain_th [] in
1326       let gen_mono m =
1327         if m.df0_flag then
1328           if m.decr_flag then
1329             eval_interval_arith_hi n (fs.df m.variable p_stat.pp xx zz)
1330           else
1331             eval_interval_arith_lo n (fs.df m.variable p_stat.pp xx zz)
1332         else
1333           if m.decr_flag then
1334             eval_m_taylor_partial_upper n p_stat.pp m.variable taylor_th
1335           else
1336             eval_m_taylor_partial_lower n p_stat.pp m.variable taylor_th in
1337       let mono_ths = map gen_mono mono in
1338       let pass_th0 = rec_verify ((fst o last) domain_ths) certificate in
1339       let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths in
1340       let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [] in
1341       let th = rev_itlist (fun ((m, mono_th), sub_th) pass_th ->
1342                              let j, flag = m.variable, m.decr_flag in
1343                                m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th)
1344         (rev (zip (zip mono mono_ths) sub_ths)) pass_th0 in
1345         if hyp th <> [] then failwith ("hyp <> []: "^string_of_thm th) else th in
1346
1347
1348
1349       fun domain_th certificate ->
1350         match certificate with
1351           | P_result_mono (p_stat, mono, r1) ->
1352               let _ = !info_print_level < 2 or
1353                 (let mono_strs =
1354                    map (fun m -> sprintf "%s%d (%b)" (if m.decr_flag then "-" else "")
1355                           m.variable m.df0_flag) mono in
1356                    report (sprintf "Mono: [%s]" (String.concat ";" mono_strs)); true) in
1357                 verify_mono p_stat mono domain_th r1
1358
1359           | P_result_pass (p_stat, _, f0_flag) ->
1360               let _ = k := !k + 1; kk := !kk + 1 in
1361               let _ = !info_print_level < 2 or
1362                 (report (sprintf "Verifying: %d/%d (f0_flag = %b)" !k r_size f0_flag); true) in
1363               let _ = !info_print_level <> 1 or
1364                 (let r = int_of_float (float_of_int !kk /. r_size2 *. 100.0) in
1365                  let _ = if r <> !last_report then (last_report := r; report0 (sprintf "%d " r)) else () in true) in
1366                 if f0_flag then
1367                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1368                   let xx, zz = dest_pair domain in
1369                     m_taylor_cell_pass0 n (fs.f p_stat.pp xx zz)
1370                 else
1371                   let taylor_th = fs.taylor p_stat.pp p_stat.pp domain_th in
1372                     m_taylor_cell_pass n p_stat.pp taylor_th
1373
1374           | P_result_glue (p_stat, i, convex_flag, r1, r2) ->
1375               let domain1_th, domain2_th =
1376                 if convex_flag then
1377                   let d1, _ = restrict_domain n (i + 1) true domain_th in
1378                   let d2, _ = restrict_domain n (i + 1) false domain_th in
1379                     d1, d2
1380                 else
1381                   split_domain n p_split (i + 1) domain_th in
1382               let th1 = rec_verify domain1_th r1 in
1383               let th2 = rec_verify domain2_th r2 in
1384                 if convex_flag then
1385                   let _ = !info_print_level < 2 or (report (sprintf "GlueConvex: %d" (i + 1)); true) in
1386                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1387                   let xx, zz = dest_pair domain in
1388                   let diff2_th = fs.diff2_f xx zz in
1389                   let partial2_th = fs.ddf (i + 1) (i + 1) p_stat.pp xx zz in
1390                   let lo_partial2_th = eval_interval_arith_lo n partial2_th in
1391                     m_convex_pass n (i + 1) diff2_th lo_partial2_th th1 th2
1392                 else
1393                   m_glue_cells n (i + 1) th1 th2
1394
1395           | P_result_ref i ->
1396               let _ = !info_print_level < 2 or (report (sprintf "Ref: %d" i); true) in
1397                 if i > 0 then
1398                   List.nth th_list (i - 1)
1399                 else
1400                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1401                   let pass_th = List.nth th_list (-i - 1) in
1402                     m_cell_pass_subdomain domain pass_th in
1403
1404     rec_verify domain_th0 certificate;;
1405
1406 (*****************)
1407
1408 let m_p_verify_raw0 n p_split fs certificate xx zz =
1409   m_p_verify_raw (0, 0) n p_split fs certificate (mk_m_center_domain n p_split xx zz) [];;
1410
1411
1412
1413 let m_p_verify_list n p_split fs certificate_list xx zz =
1414   let domain_hash = Hashtbl.create (length certificate_list * 10) in
1415   let mem, find, add = Hashtbl.mem domain_hash,
1416     Hashtbl.find domain_hash, Hashtbl.add domain_hash in
1417
1418   let get_m_cell_domain n pp domain0 path =
1419     let rec get_rec domain_th path hash =
1420       match path with
1421         | [] -> domain_th
1422         | (s, j) :: ps ->
1423             let hash' = hash^s^(string_of_int j) in
1424               if mem hash' then
1425                 get_rec (find hash') ps hash'
1426               else
1427                 if s = "l" or s = "r" then
1428                   let domain1_th, domain2_th = split_domain n pp j domain_th in
1429                   let hash1 = hash^"l"^(string_of_int j) and
1430                       hash2 = hash^"r"^(string_of_int j) in
1431                   let _ = add hash1 domain1_th; add hash2 domain2_th in
1432                     if s = "l" then
1433                       get_rec domain1_th ps hash'
1434                     else
1435                       get_rec domain2_th ps hash'
1436                 else
1437                   let l_flag = (s = "ml") in
1438                   let domain_th', _ = restrict_domain n j l_flag domain_th in
1439                   let _ = add hash' domain_th' in
1440                     get_rec domain_th' ps hash' in
1441       get_rec domain0 path "" in
1442
1443   let domain_th0 = mk_m_center_domain n p_split xx zz in
1444   let size = length certificate_list in
1445   let k = ref 0 in
1446   let kk = ref 0 in
1447   let total_size = end_itlist (+) (map (p_result_size o snd) certificate_list) in
1448
1449   let rec rec_verify certificate_list th_list =
1450     match certificate_list with
1451       | [] -> last th_list
1452       | (path, certificate) :: cs ->
1453           let _ = k := !k + 1 in
1454           let _ = !info_print_level < 2 or (report (sprintf "List: %d/%d" !k size); true) in
1455           let domain_th = get_m_cell_domain n p_split domain_th0 path in
1456           let th = m_p_verify_raw (!kk, total_size) n p_split fs certificate domain_th th_list in
1457           let _ = kk := !kk + p_result_size certificate in
1458             rec_verify cs (th_list @ [th]) in
1459     rec_verify certificate_list [];;
1460
1461
1462 (*************************************)
1463 (* disjunctions *)
1464
1465
1466 let m_verify_list_raw (report_start, total_size) n pp fs_list certificate domain_th0 th_list =
1467   let r_size = result_size certificate in
1468   let r_size2 = float_of_int (if total_size > 0 then total_size else (if r_size > 0 then r_size else 1)) in
1469   let k = ref 0 in
1470   let kk = ref report_start in
1471   let last_report = ref (int_of_float (float_of_int !kk /. r_size2 *. 100.0)) in
1472
1473   let rec rec_verify =
1474     let rec apply_trans sub_ths th0 acc =
1475       match sub_ths with
1476         | [] -> rev acc
1477         | th :: ths ->
1478             let th' = eval_subset_trans th th0 in
1479               apply_trans ths th' (th' :: acc) in
1480
1481     let rec mk_domains mono th0 acc =
1482       match mono with
1483         | [] -> rev acc
1484         | m :: ms ->
1485             let j, flag = m.variable, m.decr_flag in
1486             let ths = restrict_domain n j flag th0 in
1487               mk_domains ms (fst ths) (ths :: acc) in
1488 (*
1489     let verify_mono mono domain_th certificate =
1490       let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1491       let xx, zz = dest_pair domain in
1492       let df0_flags = itlist (fun m b -> m.df0_flag & b) mono true in
1493       let _ = !info_print_level < 2 or (report (sprintf "df0_flags = %b" df0_flags); true) in
1494       let taylor_th, diff2_th =
1495         if df0_flags then
1496           TRUTH, fs.diff2_f xx zz
1497         else
1498           let t_th = fs.taylor pp pp domain_th in
1499           let _, d_th, _, _ = dest_m_taylor_thms n t_th in
1500             t_th, d_th in
1501
1502       let domain_ths = mk_domains mono domain_th [] in
1503 (*      let domains = domain_th :: map fst (butlast domain_ths) in *)
1504
1505 (*      let gen_mono (m, domain_th) = *)
1506       let gen_mono m =
1507         if m.df0_flag then
1508           if m.decr_flag then
1509             eval_interval_arith_hi n (fs.df m.variable pp xx zz)
1510           else
1511             eval_interval_arith_lo n (fs.df m.variable pp xx zz)
1512         else
1513           if m.decr_flag then
1514             eval_m_taylor_partial_upper n pp m.variable taylor_th
1515           else
1516             eval_m_taylor_partial_lower n pp m.variable taylor_th in
1517
1518 (*      let mono_ths = map gen_mono (zip mono domains) in *)
1519       let mono_ths = map gen_mono mono in
1520       let pass_th0 = rec_verify ((fst o last) domain_ths) certificate in
1521       let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths in
1522       let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [] in
1523       let th = rev_itlist (fun ((m, mono_th), sub_th) pass_th ->
1524                              let j, flag = m.variable, m.decr_flag in
1525                                m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th)
1526         (rev (zip (zip mono mono_ths) sub_ths)) pass_th0 in
1527         if hyp th <> [] then failwith ("hyp <> []: "^string_of_thm th) else th in
1528 *)
1529
1530
1531       fun domain_th certificate ->
1532         match certificate with
1533           | Result_mono (mono, r1) ->
1534               failwith "Mono: not implemented"
1535               (*
1536               let _ = !info_print_level < 2 or
1537                 (let mono_strs =
1538                    map (fun m -> sprintf "%s%d (%b)" (if m.decr_flag then "-" else "")
1539                           m.variable m.df0_flag) mono in
1540                    report (sprintf "Mono: [%s]" (String.concat ";" mono_strs)); true) in
1541                 verify_mono mono domain_th r1
1542               *)
1543
1544           | Result_pass (j, f0_flag) ->
1545               let _ = k := !k + 1 in
1546               let _ = !info_print_level < 2 or
1547                 (report (sprintf "Verifying: %d/%d (f0_flag = %b)" !k r_size f0_flag); true) in
1548               let _ = !info_print_level < 1 or
1549                 (let r = int_of_float (float_of_int !kk /. r_size2 *. 100.0) in
1550                  let _ = if r <> !last_report then (last_report := r; report0 (sprintf "%d " r)) else () in true) in
1551               let fs = List.nth fs_list j in
1552                 if f0_flag then
1553                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1554                   let xx, zz = dest_pair domain in
1555                     m_taylor_cell_list_pass0 n (fs.f pp xx zz)
1556                 else
1557                   let taylor_th = fs.taylor pp pp domain_th in
1558                     m_taylor_cell_list_pass n pp taylor_th
1559
1560           | Result_glue (i, convex_flag, r1, r2) ->
1561               let domain1_th, domain2_th =
1562                 if convex_flag then
1563                   let d1, _ = restrict_domain n (i + 1) true domain_th in
1564                   let d2, _ = restrict_domain n (i + 1) false domain_th in
1565                     d1, d2
1566                 else
1567                   split_domain n pp (i + 1) domain_th in
1568               let th1 = rec_verify domain1_th r1 in
1569               let th2 = rec_verify domain2_th r2 in
1570                 if convex_flag then
1571                   failwith "convexity: not implemented"
1572                   (*
1573                   let _ = !info_print_level < 2 or (report (sprintf "GlueConvex: %d" (i + 1)); true) in
1574                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1575                   let xx, zz = dest_pair domain in
1576                   let diff2_th = fs.diff2_f xx zz in
1577                   let partial2_th = fs.ddf (i + 1) (i + 1) pp xx zz in
1578                   let lo_partial2_th = eval_interval_arith_lo n partial2_th in
1579                     m_convex_pass n (i + 1) diff2_th lo_partial2_th th1 th2
1580                   *)
1581                 else
1582                   let th0 = m_glue_cells_list n (i + 1) th1 th2 in
1583                     merge_m_cell_list_pass n th0
1584
1585           | Result_pass_ref i ->
1586               let _ = !info_print_level < 2 or (report (sprintf "Ref: %d" i); true) in
1587                 if i > 0 then
1588                   List.nth th_list (i - 1)
1589                 else
1590                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1591                   let pass_th = List.nth th_list (-i - 1) in
1592                     m_cell_list_pass_subdomain domain pass_th
1593
1594           | _ -> failwith "False result" in
1595
1596     rec_verify domain_th0 certificate;;
1597
1598
1599 (*****************)
1600
1601
1602 let m_verify_list_raw0 n pp fs_list certificate xx zz =
1603   m_verify_list_raw (0, 0) n pp fs_list certificate (mk_m_center_domain n pp xx zz) [];;
1604
1605
1606
1607
1608 (* end;; *)
1609
1610 m_verify_list_raw0 2 pp [formal_f1; formal_f2] cert xx_float_tm zz_float_tm;;