1 needs "../formal_lp/formal_interval/m_taylor.hl";;
2 needs "../formal_lp/formal_interval/m_verifier0.hl";;
3 needs "../formal_lp/arith/informal/informal_m_verifier.hl";;
6 let mk_real_vars n name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n);;
9 (*************************************)
11 let BOUNDED_INTERVAL_ARITH_IMP_HI' = (MY_RULE o prove)
12 (`(!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi)) ==>
13 (!x. x IN interval [domain] ==> f x <= hi)`, SIMP_TAC[interval_arith]);;
15 let BOUNDED_INTERVAL_ARITH_IMP_LO' = (MY_RULE o prove)
16 (`(!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi)) ==>
17 (!x. x IN interval [domain] ==> lo <= f x)`, SIMP_TAC[interval_arith]);;
20 let eval_interval_arith_hi n bound_th =
21 let tm0 = (snd o dest_forall o concl) bound_th in
22 let int_tm, concl_tm = dest_comb tm0 in
23 let domain_tm = (rand o rator o rand o rand o rand) int_tm in
24 let ltm, bounds_tm = dest_interval_arith concl_tm in
25 let f_tm, (lo_tm, hi_tm) = rator ltm, dest_pair bounds_tm in
26 let f_var = mk_var ("f", type_of f_tm) and
27 domain_var = mk_var ("domain", type_of domain_tm) in
28 (MY_PROVE_HYP bound_th o
29 INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real; lo_tm, lo_var_real] o
30 inst_first_type_var n_type_array.(n)) BOUNDED_INTERVAL_ARITH_IMP_HI';;
33 let eval_interval_arith_lo n bound_th =
34 let tm0 = (snd o dest_forall o concl) bound_th in
35 let int_tm, concl_tm = dest_comb tm0 in
36 let domain_tm = (rand o rator o rand o rand o rand) int_tm in
37 let ltm, bounds_tm = dest_interval_arith concl_tm in
38 let f_tm, (lo_tm, hi_tm) = rator ltm, dest_pair bounds_tm in
39 let f_var = mk_var ("f", type_of f_tm) and
40 domain_var = mk_var ("domain", type_of domain_tm) in
41 (MY_PROVE_HYP bound_th o
42 INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real; lo_tm, lo_var_real] o
43 inst_first_type_var n_type_array.(n)) BOUNDED_INTERVAL_ARITH_IMP_LO';;
47 (*************************************)
50 let eval_subset_trans =
51 let SUBSET_TRANS' = MY_RULE SUBSET_TRANS in
53 let ltm, t_tm = dest_comb (concl st_th) in
54 let s_tm = rand ltm and
55 u_tm = rand (concl tu_th) in
56 let ty = (hd o snd o dest_type o type_of) s_tm and
57 s_var = mk_var ("s", type_of s_tm) and
58 t_var = mk_var ("t", type_of t_tm) and
59 u_var = mk_var ("u", type_of u_tm) in
60 (MY_PROVE_HYP st_th o MY_PROVE_HYP tu_th o
61 INST[s_tm, s_var; t_tm, t_var; u_tm, u_var] o inst_first_type_var ty) SUBSET_TRANS';;
63 let eval_subset_refl =
64 let SUBSET_REFL' = MY_RULE SUBSET_REFL in
66 let ty = (hd o snd o dest_type o type_of) s_tm and
67 s_var = mk_var ("s", type_of s_tm) in
68 (INST[s_tm, s_var] o inst_first_type_var ty) SUBSET_REFL';;
72 let SUBSET_INTERVAL_IMP = prove(`!a b c d. (!i. i IN 1..dimindex (:N) ==> a$i <= c$i /\ d$i <= b$i) ==>
73 interval [c:real^N,d] SUBSET interval [a,b]`,
74 SIMP_TAC[SUBSET_INTERVAL; GSYM IN_NUMSEG]);;
77 let gen_subset_interval_lemma n =
78 let a_vars = mk_real_vars n "a" and
79 b_vars = mk_real_vars n "b" and
80 c_vars = mk_real_vars n "c" and
81 d_vars = mk_real_vars n "d" in
83 let a_tm = mk_vector_list a_vars and
84 b_tm = mk_vector_list b_vars and
85 c_tm = mk_vector_list c_vars and
86 d_tm = mk_vector_list d_vars in
88 let th0 = (SPEC_ALL o ISPECL [a_tm; b_tm; c_tm; d_tm]) SUBSET_INTERVAL_IMP in
89 let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
90 let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
94 let subset_interval_thms_array = Array.init (max_dim + 1)
95 (fun n -> if n < 1 then TRUTH else gen_subset_interval_lemma n);;
99 let m_subset_interval n a_tm b_tm c_tm d_tm =
100 let a_vars = mk_real_vars n "a" and
101 b_vars = mk_real_vars n "b" and
102 c_vars = mk_real_vars n "c" and
103 d_vars = mk_real_vars n "d" in
105 let a_s = dest_vector a_tm and
106 b_s = dest_vector b_tm and
107 c_s = dest_vector c_tm and
108 d_s = dest_vector d_tm in
110 let th0 = (INST (zip a_s a_vars) o INST (zip b_s b_vars) o
111 INST (zip c_s c_vars) o INST (zip d_s d_vars)) subset_interval_thms_array.(n) in
113 let ltm, rtm = dest_binop le_op_real tm in
114 EQT_ELIM (float_le ltm rtm) in
115 let hyp_ths = map prove_le (hyp th0) in
116 itlist (fun hyp_th th -> MY_PROVE_HYP hyp_th th) hyp_ths th0;;
123 let aa = `[&1; &1]` and bb = `[&3; &2]` and
124 cc = `[#1.5; &1]` and dd = `[&3; #1.6]`;;
125 let a_tm = mk_vector (convert_to_float_list pp true aa) and
126 b_tm = mk_vector (convert_to_float_list pp false bb) and
127 c_tm = mk_vector (convert_to_float_list pp true cc) and
128 d_tm = mk_vector (convert_to_float_list pp false dd);;
131 m_subset_interval n a_tm b_tm c_tm d_tm;;
133 test 1000 (m_subset_interval n a_tm b_tm c_tm) d_tm;;
136 (*************************************)
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
146 GEN_TAC THEN DISCH_TAC THEN
147 ASM_CASES_TAC `i = j:num` THENL
149 ASM_REWRITE_TAC[REAL_LE_REFL; REAL_SUB_REFL; real_max];
152 REPEAT (FIRST_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[]);
155 DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
156 ASM_CASES_TAC `i = j:num` THENL
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;
164 REPEAT (FIRST_ASSUM (new_rewrite [] [])) THEN ASM_REWRITE_TAC[REAL_LE_REFL]);;
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
176 GEN_TAC THEN DISCH_TAC THEN
177 ASM_CASES_TAC `i = j:num` THENL
179 ASM_REWRITE_TAC[REAL_LE_REFL; REAL_SUB_REFL; real_max];
182 REPEAT (FIRST_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[]);
185 DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
186 ASM_CASES_TAC `i = j:num` THENL
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;
194 REPEAT (FIRST_ASSUM (new_rewrite [] [])) THEN ASM_REWRITE_TAC[REAL_LE_REFL]);;
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
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
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));;
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));;
231 (******************************)
236 let m_cell_pass = new_definition `m_cell_pass f domain <=> (!x. x IN interval [domain] ==> f x < &0)`;;
238 let dest_m_cell_pass pass_tm =
239 let ltm, domain = dest_comb pass_tm in
243 (*********************************)
245 let M_CELL_PASS_LEMMA = prove(`(!x. x IN interval [domain] ==> f x <= hi) /\ (hi < &0 <=> T) ==>
246 m_cell_pass f domain`,
247 REWRITE_TAC[m_cell_pass] THEN REPEAT STRIP_TAC THEN
248 MATCH_MP_TAC REAL_LET_TRANS THEN
249 EXISTS_TAC `hi:real` THEN ASM_REWRITE_TAC[] THEN
250 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
252 let M_CELL_PASS_LEMMA' = MY_RULE M_CELL_PASS_LEMMA;;
254 let M_CELL_PASS_INTERVAL_LEMMA' = (MY_RULE o prove)
255 (`(!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi)) /\ hi < &0 ==> m_cell_pass f domain`,
256 REWRITE_TAC[interval_arith] THEN STRIP_TAC THEN MATCH_MP_TAC M_CELL_PASS_LEMMA THEN
259 let M_CELL_PASS_SUBSET' = (MY_RULE o prove)(`m_cell_pass f domain /\
260 interval [domain2] SUBSET interval [domain] ==>
261 m_cell_pass f domain2`,
262 REWRITE_TAC[m_cell_pass; SUBSET] THEN REPEAT STRIP_TAC THEN
263 REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);;
265 (* m_cell_pass with taylor_interval *)
266 let m_taylor_cell_pass n pp m_taylor_th =
267 let upper_th = eval_m_taylor_upper_bound n pp m_taylor_th in
268 let tm0 = (snd o dest_forall o concl) upper_th in
269 let int_tm, concl_tm = dest_comb tm0 in
270 let domain_tm = (rand o rator o rand o rand o rand) int_tm in
271 let ltm, hi_tm = dest_comb concl_tm in
272 let f_tm = (rator o rand) ltm in
273 let f_var = mk_var ("f", type_of f_tm) and
274 domain_var = mk_var ("domain", type_of domain_tm) in
276 let hi_lt0_th = float_lt0 hi_tm in
277 if (fst o dest_const o rand o concl) hi_lt0_th = "F" then
278 failwith "m_taylor_cell_pass: hi < &0 <=> F"
280 (MY_PROVE_HYP upper_th o MY_PROVE_HYP hi_lt0_th o
281 INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real] o
282 inst_first_type_var n_type_array.(n)) M_CELL_PASS_LEMMA';;
285 (* m_cell_pass with a raw interval *)
286 let m_taylor_cell_pass0 n bound_th =
287 let tm0 = (snd o dest_forall o concl) bound_th in
288 let int_tm, concl_tm = dest_comb tm0 in
289 let domain_tm = (rand o rator o rand o rand o rand) int_tm in
290 let ltm, bounds_tm = dest_interval_arith concl_tm in
291 let f_tm, (lo_tm, hi_tm) = rator ltm, dest_pair bounds_tm in
292 let f_var = mk_var ("f", type_of f_tm) and
293 domain_var = mk_var ("domain", type_of domain_tm) in
294 let hi_lt0_th = try EQT_ELIM (float_lt0 hi_tm) with Failure _ -> failwith "m_taylor_cell_pass0" in
295 (MY_PROVE_HYP bound_th o MY_PROVE_HYP hi_lt0_th o
296 INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real; lo_tm, lo_var_real] o
297 inst_first_type_var n_type_array.(n)) M_CELL_PASS_INTERVAL_LEMMA';;
300 (**********************)
302 let M_CELL_PASS_SUBDOMAIN' = (MY_RULE o prove)(`interval [domain2] SUBSET interval [domain] /\
303 m_cell_pass f domain ==> m_cell_pass f domain2`,
304 REWRITE_TAC[m_cell_pass; SUBSET] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[]);;
307 let m_cell_pass_subdomain domain2_tm pass_th =
308 let f_tm, domain_tm = dest_m_cell_pass (concl pass_th) in
309 let f_var = mk_var ("f", type_of f_tm) and
310 domain_var = mk_var ("domain", type_of domain_tm) and
311 domain2_var = mk_var ("domain2", type_of domain2_tm) in
312 let a, b = dest_pair domain_tm and
313 c, d = dest_pair domain2_tm in
315 let sub_th = m_subset_interval n a b c d in
316 (MY_PROVE_HYP sub_th o MY_PROVE_HYP pass_th o
317 INST[domain_tm, domain_var; domain2_tm, domain2_var; f_tm, f_var] o
318 inst_first_type_var n_type_array.(n)) M_CELL_PASS_SUBDOMAIN';;
324 (******************************)
326 let M_CELL_PASS_GLUE_LEMMA = prove(`!j x z v u f.
327 (!i. 1 <= i /\ i <= dimindex (:N) ==> ~(i = j) ==>
328 u$i = x$i /\ v$i = z$i) ==>
330 m_cell_pass f (x,v) ==>
331 m_cell_pass f (u,z) ==>
332 m_cell_pass f (x,z:real^N)`,
333 REWRITE_TAC[m_cell_pass; IN_INTERVAL] THEN REPEAT GEN_TAC THEN
334 move ["eq1"; "eq_vu"; "cell1"; "cell2"; "y"; "ineq"] THEN
335 ASM_CASES_TAC `(y:real^N)$j <= (v:real^N)$j` THENL
337 REMOVE_THEN "cell1" MATCH_MP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
338 USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
339 ASM_CASES_TAC `i = j:num` THENL
341 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN SIMP_TAC[];
344 USE_THEN "eq1" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
345 USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[];
349 POP_ASSUM (ASSUME_TAC o MATCH_MP (REAL_ARITH `~(a <= b) ==> b <= a:real`)) THEN
350 REMOVE_THEN "cell2" MATCH_MP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
351 USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
352 ASM_CASES_TAC `i = j:num` THENL
354 ASM_REWRITE_TAC[] THEN USE_THEN "eq_vu" (fun th -> REWRITE_TAC[SYM th]) THEN
355 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN SIMP_TAC[];
358 USE_THEN "eq1" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
359 USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[]);;
362 let gen_glue_lemma n j =
363 let mk_vars name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n) in
364 let xs = mk_vars "x" and
366 t_var = mk_var ("t", real_ty) and
367 j_tm = mk_small_numeral j in
368 let x_tm = mk_vector_list xs and
369 z_tm = mk_vector_list zs and
370 v_tm = mk_vector_list (map (fun i -> if i = j then t_var else List.nth zs (i - 1)) (1--n)) and
371 u_tm = mk_vector_list (map (fun i -> if i = j then t_var else List.nth xs (i - 1)) (1--n)) in
373 let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; v_tm; u_tm]) M_CELL_PASS_GLUE_LEMMA in
374 let th1 = REWRITE_RULE[dimindex_array.(n); gen_in_interval n; ARITH] th0 in
375 let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
379 let glue_thms_array = Array.init (max_dim + 1)
380 (fun n -> Array.init (n + 1)
381 (fun j -> if j < 1 then TRUTH else gen_glue_lemma n j));;
385 (***************************************)
387 let M_CELL_SUP = prove(`!f x z. lift o f continuous_on interval [x,z:real^N] /\ m_cell_pass f (x,z) ==>
388 ?a. a < &0 /\ !y. y IN interval [x,z] ==> f y <= a`,
389 REWRITE_TAC[m_cell_pass] THEN REPEAT STRIP_TAC THEN
390 ASM_CASES_TAC `interval [x:real^N,z] = {}` THENL
392 EXISTS_TAC `-- &1` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN REAL_ARITH_TAC;
395 MP_TAC (SPECL [`f:real^N->real`; `interval [x,z:real^N]`] CONTINUOUS_ATTAINS_SUP) THEN
396 ASM_REWRITE_TAC[COMPACT_INTERVAL] THEN
397 DISCH_THEN (X_CHOOSE_THEN `y:real^N` STRIP_ASSUME_TAC) THEN
398 EXISTS_TAC `(f:real^N->real) y` THEN ASM_REWRITE_TAC[] THEN
399 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
402 let DIFF2_DOMAIN_IMP_CONTINUOUS_ON = prove(`!(f:real^N->real) domain. diff2_domain domain f ==>
403 lift o f continuous_on interval [domain]`,
404 REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
405 MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN REPEAT STRIP_TAC THEN
406 MATCH_MP_TAC DIFFERENTIABLE_IMP_CONTINUOUS_AT THEN
407 MATCH_MP_TAC diff2_imp_diff THEN
412 let M_CELL_INCREASING_PASS_LEMMA = prove(`!j x z u domain lo f.
413 interval [x,z] SUBSET interval [domain] ==>
414 diff2c_domain domain f ==>
415 (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==> u$i = x$i) ==>
418 (!y. y IN interval [domain] ==> lo <= partial j f y) ==>
419 m_cell_pass f (u,z) ==>
420 m_cell_pass f (x,z:real^N)`,
421 REWRITE_TAC[SUBSET] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[m_cell_pass] THEN
422 X_GEN_TAC `y:real^N` THEN
423 ASM_CASES_TAC `~(!i. i IN 1..dimindex (:N) ==> (x:real^N)$i <= (z:real^N)$i)` THENL
425 POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; IN_INTERVAL; GSYM IN_NUMSEG] THEN
426 DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
427 DISCH_THEN (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
428 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
431 POP_ASSUM MP_TAC THEN REWRITE_TAC[negbK] THEN DISCH_TAC THEN
432 SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL
434 UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN
435 SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
438 MP_TAC (SPECL [`f:real^N->real`; `u:real^N`; `z:real^N`] M_CELL_SUP) THEN
441 ASM_REWRITE_TAC[] THEN
442 MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
443 UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN
444 REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
445 REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN
446 POP_ASSUM MP_TAC THEN
447 REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
448 FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
449 FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
450 ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
451 FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
454 DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN DISCH_TAC THEN
455 MP_TAC (SPECL [`f:real^N->real`; `j:num`; `u:real^N`; `x:real^N`; `z:real^N`; `a:real`] partial_increasing_right) THEN
456 ASM_REWRITE_TAC[] THEN
459 REPEAT STRIP_TAC THEN
460 MATCH_MP_TAC diff2_imp_diff THEN
461 UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN REWRITE_TAC[diff2_domain] THEN
462 DISCH_THEN MATCH_MP_TAC THEN
463 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
468 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
469 EXISTS_TAC `lo:real` THEN ASM_REWRITE_TAC[] THEN
470 REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
473 DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
474 EXISTS_TAC `a:real` THEN ASM_REWRITE_TAC[] THEN
475 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
479 let M_CELL_DECREASING_PASS_LEMMA = prove(`!j x z u domain hi f.
480 interval [x,z] SUBSET interval [domain] ==>
481 diff2c_domain domain f ==>
482 (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==> u$i = z$i) ==>
485 (!y. y IN interval [domain] ==> partial j f y <= hi) ==>
486 m_cell_pass f (x,u) ==>
487 m_cell_pass f (x,z:real^N)`,
488 REWRITE_TAC[SUBSET] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[m_cell_pass] THEN X_GEN_TAC `y:real^N` THEN
489 ASM_CASES_TAC `~(!i. i IN 1..dimindex (:N) ==> (x:real^N)$i <= (z:real^N)$i)` THENL
491 POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; IN_INTERVAL; GSYM IN_NUMSEG] THEN
492 DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
493 DISCH_THEN (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
494 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
497 POP_ASSUM MP_TAC THEN REWRITE_TAC[negbK] THEN DISCH_TAC THEN
498 SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL
500 UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN
501 SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
504 MP_TAC (SPECL [`f:real^N->real`; `x:real^N`; `u:real^N`] M_CELL_SUP) THEN
507 ASM_REWRITE_TAC[] THEN
508 MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
509 UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN
510 REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
511 REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN
512 POP_ASSUM MP_TAC THEN
513 REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
514 FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
515 FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
516 ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
517 FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
520 DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN DISCH_TAC THEN
521 MP_TAC (SPECL [`f:real^N->real`; `j:num`; `u:real^N`; `x:real^N`; `z:real^N`; `a:real`] partial_decreasing_left) THEN
522 ASM_REWRITE_TAC[] THEN
525 REPEAT STRIP_TAC THEN
526 MATCH_MP_TAC diff2_imp_diff THEN
527 UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN REWRITE_TAC[diff2_domain] THEN
528 DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
529 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
534 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
535 EXISTS_TAC `hi:real` THEN ASM_REWRITE_TAC[] THEN
536 REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
539 DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
540 EXISTS_TAC `a:real` THEN ASM_REWRITE_TAC[] THEN
541 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
545 let M_CELL_CONVEX_PASS_LEMMA = prove(`!j x z u v lo f.
546 diff2c_domain (x,z) f ==>
547 (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==> u$i = z$i /\ v$i = x$i) ==>
548 u$j = x$j ==> v$j = z$j ==>
550 (!y. y IN interval [x,z] ==> lo <= partial2 j j f y) ==>
551 m_cell_pass f (x,u) ==>
552 m_cell_pass f (v,z) ==>
553 m_cell_pass f (x:real^N,z)`,
554 REPEAT STRIP_TAC THEN REWRITE_TAC[m_cell_pass] THEN
555 X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
556 SUBGOAL_THEN `!i. i IN 1..dimindex (:N) ==> (x:real^N)$i <= (z:real^N)$i` ASSUME_TAC THENL
558 POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_INTERVAL] THEN REPEAT STRIP_TAC THEN
559 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(y:real^N)$i` THEN
560 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[GSYM IN_NUMSEG];
563 SUBGOAL_THEN `diff2_domain (x,z) (f:real^N->real)` ASSUME_TAC THENL
565 UNDISCH_TAC `diff2c_domain (x,z) (f:real^N->real)` THEN
566 SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
569 MP_TAC (SPECL [`f:real^N->real`; `v:real^N`; `z:real^N`] M_CELL_SUP) THEN
572 ASM_REWRITE_TAC[] THEN
573 MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
574 UNDISCH_TAC `diff2_domain (x,z) (f:real^N->real)` THEN
575 REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
576 FIRST_X_ASSUM MATCH_MP_TAC THEN
577 POP_ASSUM MP_TAC THEN
578 REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
579 FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
580 FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
581 ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
582 FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
585 DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
587 MP_TAC (SPECL [`f:real^N->real`; `x:real^N`; `u:real^N`] M_CELL_SUP) THEN
590 ASM_REWRITE_TAC[] THEN
591 MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
592 UNDISCH_TAC `diff2_domain (x,z) (f:real^N->real)` THEN
593 REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
594 FIRST_X_ASSUM MATCH_MP_TAC THEN
595 POP_ASSUM MP_TAC THEN
596 REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
597 FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
598 FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
599 ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
600 FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
603 DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
605 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
606 ASM_REWRITE_TAC[] THEN
609 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
610 EXISTS_TAC `lo:real` THEN ASM_REWRITE_TAC[] THEN
611 REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
616 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
617 EXISTS_TAC `a':real` THEN
618 ASM_SIMP_TAC[] THEN REAL_ARITH_TAC;
623 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
624 EXISTS_TAC `a:real` THEN
625 ASM_SIMP_TAC[] THEN REAL_ARITH_TAC;
629 DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
630 EXISTS_TAC `max a a'` THEN
632 ASM_REAL_ARITH_TAC);;
636 (*********************)
638 let ZERO_EQ_ZERO_CONST = prove(`0 = _0`, REWRITE_TAC[NUMERAL]);;
640 let gen_increasing_lemma n j =
641 let mk_vars name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n) in
642 let xs = mk_vars "x" and
644 j_tm = mk_small_numeral j in
645 let x_tm = mk_vector_list xs and
646 z_tm = mk_vector_list zs and
647 u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then zs else xs) (i - 1)) (1--n)) in
648 let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; u_tm]) M_CELL_INCREASING_PASS_LEMMA in
649 let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
650 let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
651 let th3 = MY_RULE_NUM th2 in
652 (UNDISCH_ALL o ONCE_REWRITE_RULE[GSYM ZERO_EQ_ZERO_CONST] o DISCH (last (hyp th3))) th3;;
655 let gen_mono_lemma0 th =
656 let h2 = List.nth (hyp th) 1 in
657 let domain_tm = (lhand o rand o lhand) h2 in
658 let domain_var = mk_var ("domain", type_of domain_tm) in
659 (UNDISCH_ALL o REWRITE_RULE[SUBSET_REFL] o DISCH_ALL o INST[domain_tm, domain_var]) th;;
661 let incr_gen_thms_array = Array.init (max_dim + 1)
662 (fun n -> Array.init (n + 1)
663 (fun j -> if j < 1 then TRUTH else gen_increasing_lemma n j));;
665 let incr_thms_array = Array.init (max_dim + 1)
666 (fun n -> Array.init (n + 1)
667 (fun j -> if j < 1 then TRUTH else gen_mono_lemma0 incr_gen_thms_array.(n).(j)));;
671 let gen_decreasing_lemma n j =
672 let mk_vars name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n) in
673 let xs = mk_vars "x" and
675 j_tm = mk_small_numeral j in
676 let x_tm = mk_vector_list xs and
677 z_tm = mk_vector_list zs and
678 u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then xs else zs) (i - 1)) (1--n)) in
679 let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; u_tm]) M_CELL_DECREASING_PASS_LEMMA in
680 let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
681 let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
682 let th3 = MY_RULE_NUM th2 in
683 (UNDISCH_ALL o ONCE_REWRITE_RULE[GSYM ZERO_EQ_ZERO_CONST] o DISCH (last (hyp th3))) th3;;
686 let decr_gen_thms_array = Array.init (max_dim + 1)
687 (fun n -> Array.init (n + 1)
688 (fun j -> if j < 1 then TRUTH else gen_decreasing_lemma n j));;
690 let decr_thms_array = Array.init (max_dim + 1)
691 (fun n -> Array.init (n + 1)
692 (fun j -> if j < 1 then TRUTH else gen_mono_lemma0 decr_gen_thms_array.(n).(j)));;
695 (****************************************)
697 let gen_convex_max_lemma n j =
698 let xs = mk_real_vars n "x" and
699 zs = mk_real_vars n "z" and
700 j_tm = mk_small_numeral j in
701 let x_tm = mk_vector_list xs and
702 z_tm = mk_vector_list zs and
703 u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then xs else zs) (i - 1)) (1--n)) and
704 v_tm = mk_vector_list (map (fun i -> List.nth (if i = j then zs else xs) (i - 1)) (1--n)) in
705 let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; u_tm; v_tm]) M_CELL_CONVEX_PASS_LEMMA in
706 let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
707 let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
708 let th3 = MY_RULE_NUM th2 in
709 (UNDISCH_ALL o ONCE_REWRITE_RULE[GSYM ZERO_EQ_ZERO_CONST] o DISCH (last (hyp th3))) th3;;
712 let convex_thms_array = Array.init (max_dim + 1)
713 (fun n -> Array.init (n + 1)
714 (fun j -> if j < 1 then TRUTH else gen_convex_max_lemma n j));;
718 (******************************************)
720 let m_glue_cells n j pass_th1 pass_th2 =
721 let f_tm, domain1 = dest_m_cell_pass (concl pass_th1) and
722 domain2 = rand (concl pass_th2) in
723 let x1, z1 = dest_pair domain1 and
724 x2, z2 = dest_pair domain2 in
726 let x1s = dest_vector x1 and
727 x2s = dest_vector x2 and
728 z2s = dest_vector z2 in
730 let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
731 z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
732 f_var = mk_var ("f", type_of f_tm) and
733 t_tm = List.nth x2s (j - 1) in
735 let th0 = (INST[t_tm, t_var_real; f_tm, f_var] o
736 INST (zip z2s z_vars) o INST (zip x1s x_vars)) glue_thms_array.(n).(j) in
737 (MY_PROVE_HYP pass_th1 o MY_PROVE_HYP pass_th2) th0;;
740 (**********************)
742 let m_mono_pass_gen n j decr_flag diff2_th partial_mono_th sub_th pass_th =
743 let f_tm, domain0 = dest_m_cell_pass (concl pass_th) and
744 domain = (rand o rator o concl) diff2_th and
745 xv, zv = (dest_pair o lhand o rand o lhand o concl) sub_th and
746 bound_tm = ((if decr_flag then rand else lhand) o rand o snd o dest_forall o concl) partial_mono_th in
748 let xs = dest_vector xv and
749 zs = dest_vector zv in
751 let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
752 z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
753 domain_var = mk_var ("domain", type_of domain) and
754 f_var = mk_var ("f", type_of f_tm) and
755 bound_var = mk_var ((if decr_flag then "hi" else "lo"), real_ty) in
757 let le_th0 = (if decr_flag then float_le0 else float_ge0) bound_tm in
758 let le_th = try EQT_ELIM le_th0 with Failure _ ->
759 failwith (sprintf "m_mono_pass_gen: j = %d, th = %s" j (string_of_thm le_th0)) in
761 let th0 = (INST[f_tm, f_var; bound_tm, bound_var; domain, domain_var] o
762 INST (zip xs x_vars) o INST (zip zs z_vars))
763 (if decr_flag then decr_gen_thms_array.(n).(j) else incr_gen_thms_array.(n).(j)) in
764 (MY_PROVE_HYP le_th o MY_PROVE_HYP pass_th o MY_PROVE_HYP diff2_th o
765 MY_PROVE_HYP sub_th o MY_PROVE_HYP partial_mono_th) th0;;
770 let m_incr_pass n pp j m_taylor_th pass_th0 =
771 let _, diff2_th, _, _ = dest_m_taylor_thms n m_taylor_th in
772 let partial_bound = eval_m_taylor_partial_lower n pp j m_taylor_th in
774 let f_tm, domain0 = dest_m_cell_pass (concl pass_th0) and
775 domain = (rand o rator o concl) diff2_th and
776 lo_tm = (lhand o rand o snd o dest_forall o concl) partial_bound in
777 let lo_ge0_th = EQT_ELIM (float_ge0 lo_tm) in
779 let x_tm, z_tm = dest_pair domain in
780 let xs = dest_vector x_tm and
781 zs = dest_vector z_tm in
783 let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
784 z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
785 f_var = mk_var ("f", type_of f_tm) in
786 let th0 = (INST[f_tm, f_var; lo_tm, lo_var_real] o
787 INST (zip zs z_vars) o INST (zip xs x_vars)) incr_thms_array.(n).(j) in
788 (MY_PROVE_HYP lo_ge0_th o MY_PROVE_HYP pass_th0 o
789 MY_PROVE_HYP diff2_th o MY_PROVE_HYP partial_bound) th0;;
793 let m_decr_pass n pp j m_taylor_th pass_th0 =
794 let _, diff2_th, _, _ = dest_m_taylor_thms n m_taylor_th in
795 let partial_bound = eval_m_taylor_partial_upper n pp j m_taylor_th in
797 let f_tm, domain0 = dest_m_cell_pass (concl pass_th0) and
798 domain = (rand o rator o concl) diff2_th and
799 hi_tm = (rand o rand o snd o dest_forall o concl) partial_bound in
800 let hi_le0_th = EQT_ELIM (float_le0 hi_tm) in
802 let x_tm, z_tm = dest_pair domain in
803 let xs = dest_vector x_tm and
804 zs = dest_vector z_tm in
806 let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
807 z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
808 f_var = mk_var ("f", type_of f_tm) in
809 let th0 = (INST[f_tm, f_var; hi_tm, hi_var_real] o
810 INST (zip zs z_vars) o INST (zip xs x_vars)) decr_thms_array.(n).(j) in
811 (MY_PROVE_HYP hi_le0_th o MY_PROVE_HYP pass_th0 o
812 MY_PROVE_HYP diff2_th o MY_PROVE_HYP partial_bound) th0;;
814 (*************************)
817 let m_convex_pass n j diff2_th partial2_bound_th pass1_th pass2_th =
818 let f_tm, domain1 = dest_m_cell_pass (concl pass1_th) and
819 _, domain2 = dest_m_cell_pass (concl pass2_th) in
820 let x_tm, _ = dest_pair domain1 and
821 _, z_tm = dest_pair domain2 and
822 bound_tm = (lhand o rand o snd o dest_forall o concl) partial2_bound_th in
824 let xs = dest_vector x_tm and
825 zs = dest_vector z_tm in
827 let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
828 z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
829 f_var = mk_var ("f", type_of f_tm) in
831 let le_th0 = float_ge0 bound_tm in
833 try EQT_ELIM le_th0 with Failure _ -> failwith ("m_convex_pass: "^string_of_thm le_th0) in
835 let th0 = (INST[f_tm, f_var; bound_tm, lo_var_real] o
836 INST (zip xs x_vars) o INST (zip zs z_vars)) convex_thms_array.(n).(j) in
837 (MY_PROVE_HYP le_th o MY_PROVE_HYP pass1_th o MY_PROVE_HYP pass2_th o
838 MY_PROVE_HYP diff2_th o MY_PROVE_HYP partial2_bound_th) th0;;
843 (***********************)
845 (* mk_verification_functions *)
847 type verification_funs =
849 (* p_lin -> p_second -> domain_th -> taylor_th *)
850 taylor : int -> int -> thm -> thm;
851 (* pp -> lo -> hi -> interval_th *)
852 f : int -> term -> term -> thm;
853 (* i -> pp -> lo -> hi -> interval_th *)
854 df : int -> int -> term -> term -> thm;
855 (* i -> j -> pp -> lo -> hi -> interval_th *)
856 ddf : int -> int -> int -> term -> term -> thm;
857 (* lo -> hi -> diff2_th *)
858 diff2_f : term -> term -> thm;
862 let mk_verification_functions pp0 poly_tm min_flag value_tm =
863 let x_tm, body_tm = dest_abs poly_tm in
865 uncurry (mk_binop sub_op_real) (if min_flag then value_tm, body_tm else body_tm, value_tm) in
866 let new_f = mk_abs (x_tm, new_expr) in
867 let n = get_dim x_tm in
869 let partials = map (fun i ->
870 let _ = report (sprintf "Partial %d/%d" i n) in
871 gen_partial_poly i new_f) (1--n) in
872 let get_partial i eq_th =
873 let partial_i = gen_partial_poly i (rand (concl eq_th)) in
874 let pi = (rator o lhand o concl) partial_i in
875 REWRITE_RULE[GSYM partial2] (TRANS (AP_TERM pi eq_th) partial_i) in
876 let partials2 = map (fun j ->
877 let th = List.nth partials (j - 1) in
878 let _ = report (sprintf "Partial2 %d/%d" j n) in
879 map (fun i -> get_partial i th) (1--j)) (1--n) in
881 let diff_th = gen_diff_poly new_f in
882 let lin_th = gen_lin_approx_poly_thm new_f diff_th partials in
883 let diff2_th = gen_diff2c_domain_poly new_f in
884 let second_th = gen_second_bounded_poly_thm new_f partials2 in
886 let replace_numeral i th =
887 let num_eq = (REWRITE_RULE[Arith_hash.NUM_THM] o NUMERAL_TO_NUM_CONV) (mk_small_numeral i) in
888 GEN_REWRITE_RULE (LAND_CONV o RATOR_CONV o DEPTH_CONV) [num_eq] th in
890 let eval0 = mk_eval_function pp0 new_f in
891 let eval1 = map (fun i ->
892 let d_th = List.nth partials (i - 1) in
893 let eq_th = replace_numeral i d_th in
894 mk_eval_function_eq pp0 eq_th) (1--n) in
896 let eval2 = map (fun i ->
898 let d2_th = List.nth (List.nth partials2 (i - 1)) (j - 1) in
899 let eq_th' = replace_numeral i d2_th in
900 let eq_th = replace_numeral j eq_th' in
901 mk_eval_function_eq pp0 eq_th) (1--i)) (1--n) in
903 let diff2_f = eval_diff2_poly diff2_th in
904 let eval_f = eval_m_taylor pp0 diff2_th lin_th second_th in
905 let taylor_f = build_taylor pp0 lin_th second_th in
908 df = (fun i -> List.nth eval1 (i - 1));
909 ddf = (fun i j -> List.nth (List.nth eval2 (j - 1)) (i - 1));
911 }, taylor_f, Informal_verifier.mk_verification_functions pp0 new_f partials partials2;;
916 let split_domain n pp j domain_th =
917 let domain_tm, y_tm, _ = dest_m_cell_domain (concl domain_th) in
918 let x_tm, z_tm = dest_pair domain_tm in
919 let xs = dest_vector x_tm and
920 zs = dest_vector z_tm and
921 t = List.nth (dest_vector y_tm) (j - 1) in
923 let vv = map (fun i -> if i = j then t else List.nth zs (i - 1)) (1--n) and
924 uu = map (fun i -> if i = j then t else List.nth xs (i - 1)) (1--n) in
926 let domain1_th = mk_m_center_domain n pp (rand x_tm) (mk_list (vv, real_ty)) and
927 domain2_th = mk_m_center_domain n pp (mk_list (uu, real_ty)) (rand z_tm) in
928 domain1_th, domain2_th;;
931 (* restrict_domain *)
933 let restrict_domain n j left_flag domain_th =
934 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
935 let x_tm, z_tm = dest_pair domain_tm in
936 let xs = dest_vector x_tm and
937 zs = dest_vector z_tm and
938 ys = dest_vector y_tm and
939 ws = dest_vector w_tm in
941 let th0 = (INST (zip xs (mk_real_vars n "x")) o INST (zip zs (mk_real_vars n "z")) o
942 INST (zip ys (mk_real_vars n "y")) o INST (zip ws (mk_real_vars n "w")))
943 (if left_flag then left_restrict_thms_array.(n).(j) else right_restrict_thms_array.(n).(j)) in
944 let ths = CONJUNCTS (MY_PROVE_HYP domain_th th0) in
945 hd ths, hd (tl ths);;
948 let convert_to_float_list pp lo_flag list_tm =
949 let tms = dest_list list_tm in
950 let i_funs = map build_interval_fun tms in
951 let ints = map (fun f -> eval_interval_fun pp f [] []) i_funs in
952 let extract = (if lo_flag then fst else snd) o dest_pair o rand o concl in
953 mk_list (map extract ints, real_ty);;
959 (****************************************)
961 (* time test for domain computations *)
962 let m_verify_domain_test n pp certificate xx zz =
963 let r_size = result_size certificate in
965 let domain_th = mk_m_center_domain n pp xx zz in
967 let rec rec_verify domain_th certificate =
968 match certificate with
969 | Result_mono (mono, r1) ->
971 let _ = report (sprintf "Mono: %d (%b)" m.variable m.decr_flag) in
972 let j, left_flag = m.variable, m.decr_flag in
973 let domain1_th, _ = restrict_domain n j left_flag domain_th in
974 let r = if tl mono = [] then r1 else Result_mono (tl mono, r1) in
975 rec_verify domain1_th r
977 | Result_pass (f0_flag, xx, zz) ->
978 let _ = k := !k + 1 in
979 let _ = report (sprintf "Verifying: %d/%d" !k r_size) in ()
981 | Result_glue (i, convex_flag, r1, r2) ->
982 let domain1_th, domain2_th =
984 let d1, _ = restrict_domain n (i + 1) true domain_th and
985 d2, _ = restrict_domain n (i + 1) false domain_th in
988 split_domain n pp (i + 1) domain_th in
989 let _ = rec_verify domain1_th r1 and
990 _ = rec_verify domain2_th r2 in ()
992 | _ -> failwith "False result" in
994 rec_verify domain_th certificate;;
1000 (***************************)
1002 let m_verify_raw n pp fs certificate domain_th0 th_list =
1003 let r_size = result_size certificate in
1006 let rec rec_verify =
1007 let rec apply_trans sub_ths th0 acc =
1011 let th' = eval_subset_trans th th0 in
1012 apply_trans ths th' (th' :: acc) in
1014 let rec mk_domains mono th0 acc =
1018 let j, flag = m.variable, m.decr_flag in
1019 let ths = restrict_domain n j flag th0 in
1020 mk_domains ms (fst ths) (ths :: acc) in
1022 let verify_mono mono domain_th certificate =
1023 let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1024 let xx, zz = dest_pair domain in
1025 let df0_flags = itlist (fun m b -> m.df0_flag & b) mono true in
1026 let _ = report (sprintf "df0_flags = %b" df0_flags) in
1027 let taylor_th, diff2_th =
1029 TRUTH, fs.diff2_f xx zz
1031 let t_th = fs.taylor pp pp domain_th in
1032 let _, d_th, _, _ = dest_m_taylor_thms n t_th in
1035 let domain_ths = mk_domains mono domain_th [] in
1036 (* let domains = domain_th :: map fst (butlast domain_ths) in *)
1038 (* let gen_mono (m, domain_th) = *)
1042 eval_interval_arith_hi n (fs.df m.variable pp xx zz)
1044 eval_interval_arith_lo n (fs.df m.variable pp xx zz)
1047 eval_m_taylor_partial_upper n pp m.variable taylor_th
1049 eval_m_taylor_partial_lower n pp m.variable taylor_th in
1051 (* let mono_ths = map gen_mono (zip mono domains) in *)
1052 let mono_ths = map gen_mono mono in
1053 let pass_th0 = rec_verify ((fst o last) domain_ths) certificate in
1054 let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths in
1055 let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [] in
1056 let th = rev_itlist (fun ((m, mono_th), sub_th) pass_th ->
1057 let j, flag = m.variable, m.decr_flag in
1058 m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th)
1059 (rev (zip (zip mono mono_ths) sub_ths)) pass_th0 in
1060 if hyp th <> [] then failwith ("hyp <> []: "^string_of_thm th) else th in
1064 fun domain_th certificate ->
1065 match certificate with
1066 | Result_mono (mono, r1) ->
1068 map (fun m -> sprintf "%s%d (%b)" (if m.decr_flag then "-" else "")
1069 m.variable m.df0_flag) mono in
1070 let _ = report (sprintf "Mono: [%s]" (String.concat ";" mono_strs)) in
1071 verify_mono mono domain_th r1
1073 | Result_pass (f0_flag, xx, zz) ->
1074 let _ = k := !k + 1 in
1075 let _ = report (sprintf "Verifying: %d/%d (f0_flag = %b)" !k r_size f0_flag) in
1077 let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1078 let xx, zz = dest_pair domain in
1079 m_taylor_cell_pass0 n (fs.f pp xx zz)
1081 let taylor_th = fs.taylor pp pp domain_th in
1082 m_taylor_cell_pass n pp taylor_th
1084 | Result_glue (i, convex_flag, r1, r2) ->
1085 let domain1_th, domain2_th =
1087 let d1, _ = restrict_domain n (i + 1) true domain_th in
1088 let d2, _ = restrict_domain n (i + 1) false domain_th in
1091 split_domain n pp (i + 1) domain_th in
1092 let th1 = rec_verify domain1_th r1 in
1093 let th2 = rec_verify domain2_th r2 in
1095 let _ = report (sprintf "GlueConvex: %d" (i + 1)) in
1096 let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1097 let xx, zz = dest_pair domain in
1098 let diff2_th = fs.diff2_f xx zz in
1099 let partial2_th = fs.ddf (i + 1) (i + 1) pp xx zz in
1100 let lo_partial2_th = eval_interval_arith_lo n partial2_th in
1101 m_convex_pass n (i + 1) diff2_th lo_partial2_th th1 th2
1103 m_glue_cells n (i + 1) th1 th2
1105 | Result_pass_ref i ->
1106 let _ = report (sprintf "Ref: %d" i) in
1108 List.nth th_list (i - 1)
1110 let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1111 let pass_th = List.nth th_list (-i - 1) in
1112 m_cell_pass_subdomain domain pass_th
1114 | _ -> failwith "False result" in
1116 rec_verify domain_th0 certificate;;
1122 let m_verify_raw0 n pp fs certificate xx zz =
1123 m_verify_raw n pp fs certificate (mk_m_center_domain n pp xx zz) [];;
1127 let m_verify_list n pp fs certificate_list xx zz =
1128 let domain_hash = Hashtbl.create (length certificate_list * 10) in
1129 let mem, find, add = Hashtbl.mem domain_hash,
1130 Hashtbl.find domain_hash, Hashtbl.add domain_hash in
1132 let get_m_cell_domain n pp domain0 path =
1133 let rec get_rec domain_th path hash =
1137 let hash' = hash^s^(string_of_int j) in
1139 get_rec (find hash') ps hash'
1141 if s = "l" or s = "r" then
1142 let domain1_th, domain2_th = split_domain n pp j domain_th in
1143 let hash1 = hash^"l"^(string_of_int j) and
1144 hash2 = hash^"r"^(string_of_int j) in
1145 let _ = add hash1 domain1_th; add hash2 domain2_th in
1147 get_rec domain1_th ps hash'
1149 get_rec domain2_th ps hash'
1151 let l_flag = (s = "ml") in
1152 let domain_th', _ = restrict_domain n j l_flag domain_th in
1153 let _ = add hash' domain_th' in
1154 get_rec domain_th' ps hash' in
1155 get_rec domain0 path "" in
1157 let domain_th0 = mk_m_center_domain n pp xx zz in
1158 let size = length certificate_list in
1160 let rec rec_verify certificate_list th_list =
1161 match certificate_list with
1162 | [] -> last th_list
1163 | (path, certificate) :: cs ->
1164 let _ = k := !k + 1; report (sprintf "List: %d/%d" !k size) in
1165 let domain_th = get_m_cell_domain n pp domain_th0 path in
1166 let th = m_verify_raw n pp fs certificate domain_th th_list in
1167 rec_verify cs (th_list @ [th]) in
1168 rec_verify certificate_list [];;
1171 (***************************)
1172 (* Verification based on a p_result_tree *)
1174 let m_p_verify_raw n p_split fs certificate domain_th0 th_list =
1175 let r_size = p_result_size certificate in
1178 let rec rec_verify =
1179 let rec apply_trans sub_ths th0 acc =
1183 let th' = eval_subset_trans th th0 in
1184 apply_trans ths th' (th' :: acc) in
1186 let rec mk_domains mono th0 acc =
1190 let j, flag = m.variable, m.decr_flag in
1191 let ths = restrict_domain n j flag th0 in
1192 mk_domains ms (fst ths) (ths :: acc) in
1194 let verify_mono p_stat mono domain_th certificate =
1195 let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1196 let xx, zz = dest_pair domain in
1197 let df0_flags = itlist (fun m b -> m.df0_flag & b) mono true in
1198 let _ = report (sprintf "df0_flags = %b" df0_flags) in
1199 let taylor_th, diff2_th =
1201 TRUTH, fs.diff2_f xx zz
1203 let t_th = fs.taylor p_stat.pp p_stat.pp domain_th in
1204 let _, d_th, _, _ = dest_m_taylor_thms n t_th in
1207 let domain_ths = mk_domains mono domain_th [] in
1211 eval_interval_arith_hi n (fs.df m.variable p_stat.pp xx zz)
1213 eval_interval_arith_lo n (fs.df m.variable p_stat.pp xx zz)
1216 eval_m_taylor_partial_upper n p_stat.pp m.variable taylor_th
1218 eval_m_taylor_partial_lower n p_stat.pp m.variable taylor_th in
1219 let mono_ths = map gen_mono mono in
1220 let pass_th0 = rec_verify ((fst o last) domain_ths) certificate in
1221 let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths in
1222 let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [] in
1223 let th = rev_itlist (fun ((m, mono_th), sub_th) pass_th ->
1224 let j, flag = m.variable, m.decr_flag in
1225 m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th)
1226 (rev (zip (zip mono mono_ths) sub_ths)) pass_th0 in
1227 if hyp th <> [] then failwith ("hyp <> []: "^string_of_thm th) else th in
1231 fun domain_th certificate ->
1232 match certificate with
1233 | P_result_mono (p_stat, mono, r1) ->
1235 map (fun m -> sprintf "%s%d (%b)" (if m.decr_flag then "-" else "")
1236 m.variable m.df0_flag) mono in
1237 let _ = report (sprintf "Mono: [%s]" (String.concat ";" mono_strs)) in
1238 verify_mono p_stat mono domain_th r1
1240 | P_result_pass (p_stat, f0_flag) ->
1241 let _ = k := !k + 1 in
1242 let _ = report (sprintf "Verifying: %d/%d (f0_flag = %b)" !k r_size f0_flag) in
1244 let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1245 let xx, zz = dest_pair domain in
1246 m_taylor_cell_pass0 n (fs.f p_stat.pp xx zz)
1248 let taylor_th = fs.taylor p_stat.pp p_stat.pp domain_th in
1249 m_taylor_cell_pass n p_stat.pp taylor_th
1251 | P_result_glue (p_stat, i, convex_flag, r1, r2) ->
1252 let domain1_th, domain2_th =
1254 let d1, _ = restrict_domain n (i + 1) true domain_th in
1255 let d2, _ = restrict_domain n (i + 1) false domain_th in
1258 split_domain n p_split (i + 1) domain_th in
1259 let th1 = rec_verify domain1_th r1 in
1260 let th2 = rec_verify domain2_th r2 in
1262 let _ = report (sprintf "GlueConvex: %d" (i + 1)) in
1263 let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1264 let xx, zz = dest_pair domain in
1265 let diff2_th = fs.diff2_f xx zz in
1266 let partial2_th = fs.ddf (i + 1) (i + 1) p_stat.pp xx zz in
1267 let lo_partial2_th = eval_interval_arith_lo n partial2_th in
1268 m_convex_pass n (i + 1) diff2_th lo_partial2_th th1 th2
1270 m_glue_cells n (i + 1) th1 th2
1273 let _ = report (sprintf "Ref: %d" i) in
1275 List.nth th_list (i - 1)
1277 let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1278 let pass_th = List.nth th_list (-i - 1) in
1279 m_cell_pass_subdomain domain pass_th in
1281 rec_verify domain_th0 certificate;;
1285 let m_p_verify_raw0 n p_split fs certificate xx zz =
1286 m_p_verify_raw n p_split fs certificate (mk_m_center_domain n p_split xx zz) [];;
1290 let m_p_verify_list n p_split fs certificate_list xx zz =
1291 let domain_hash = Hashtbl.create (length certificate_list * 10) in
1292 let mem, find, add = Hashtbl.mem domain_hash,
1293 Hashtbl.find domain_hash, Hashtbl.add domain_hash in
1295 let get_m_cell_domain n pp domain0 path =
1296 let rec get_rec domain_th path hash =
1300 let hash' = hash^s^(string_of_int j) in
1302 get_rec (find hash') ps hash'
1304 if s = "l" or s = "r" then
1305 let domain1_th, domain2_th = split_domain n pp j domain_th in
1306 let hash1 = hash^"l"^(string_of_int j) and
1307 hash2 = hash^"r"^(string_of_int j) in
1308 let _ = add hash1 domain1_th; add hash2 domain2_th in
1310 get_rec domain1_th ps hash'
1312 get_rec domain2_th ps hash'
1314 let l_flag = (s = "ml") in
1315 let domain_th', _ = restrict_domain n j l_flag domain_th in
1316 let _ = add hash' domain_th' in
1317 get_rec domain_th' ps hash' in
1318 get_rec domain0 path "" in
1320 let domain_th0 = mk_m_center_domain n p_split xx zz in
1321 let size = length certificate_list in
1323 let rec rec_verify certificate_list th_list =
1324 match certificate_list with
1325 | [] -> last th_list
1326 | (path, certificate) :: cs ->
1327 let _ = k := !k + 1; report (sprintf "List: %d/%d" !k size) in
1328 let domain_th = get_m_cell_domain n p_split domain_th0 path in
1329 let th = m_p_verify_raw n p_split fs certificate domain_th th_list in
1330 rec_verify cs (th_list @ [th]) in
1331 rec_verify certificate_list [];;