1 (* =========================================================== *)
2 (* Formal verification functions *)
3 (* Author: Alexey Solovyev *)
5 (* =========================================================== *)
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";;
14 (* module M_verifier = struct *)
20 open Verifier_options;;
21 open M_verifier_build;;
24 let mk_real_vars n name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n);;
26 (*************************************)
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]);;
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]);;
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';;
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';;
64 (*************************************)
67 let eval_subset_trans =
68 let SUBSET_TRANS' = MY_RULE SUBSET_TRANS in
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';;
80 let eval_subset_refl =
81 let SUBSET_REFL' = MY_RULE SUBSET_REFL in
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';;
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]);;
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
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
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
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);;
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
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
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
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;;
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 (******************************)
234 let m_cell_pass = new_definition `m_cell_pass f domain <=> (!x. x IN interval [domain] ==> f x < &0)`;;
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)`;;
239 let dest_m_cell_pass pass_tm =
240 let ltm, domain = dest_comb pass_tm in
243 let dest_m_cell_list_pass pass_tm =
244 let ltm, domain = dest_comb pass_tm in
245 dest_list (rand ltm), domain;;
248 (*********************************)
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]);;
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]);;
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[]);;
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]);;
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;;
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
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
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
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"
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';;
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
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"
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';;
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';;
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';;
350 (**********************)
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[]);;
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[]);;
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
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';;
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
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';;
392 (******************************)
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) ==>
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
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
409 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN SIMP_TAC[];
412 USE_THEN "eq1" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
413 USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[];
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
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[];
426 USE_THEN "eq1" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
427 USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[]);;
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) ==>
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
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]);;
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) ==>
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);;
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
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
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
472 gen_th M_CELL_PASS_GLUE_LEMMA, gen_th M_CELL_LIST_PASS_GLUE_LEMMA;;
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));;
480 (***************************************)
481 (* m_cell_list_pass reduction *)
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]);;
486 let CELL_LIST_PASS_ACC_ELIM = SYM CELL_LIST_PASS_ACC_INTRO;;
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]);;
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]);;
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]);;
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]);;
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]);;
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]);;
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
532 (* Reverses the result list to preserve ordering *)
534 let ltm, s_tm = (dest_comb o rand o rator o concl) th in
535 let acc_tm = rand ltm in
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
542 let th1 = INST[acc_tm, fs1_var; dom_tm, dom_var] acc_elim in
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
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
556 let h1_tm, t1_tm = dest_binary "CONS" fs1_tm and
557 h2_tm, t2_tm = dest_binary "CONS" fs2_tm in
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
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
571 compare `\x:real^2. x$1` `\x:real^2. x$1 + x$2`;;
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;;
577 (rand o rator o concl) test_th;;
578 test 1000 (merge_m_cell_list_pass 2) test_th;;
582 (***************************************)
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
589 EXISTS_TAC `-- &1` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN REAL_ARITH_TAC;
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[]);;
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
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) ==>
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
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;
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
631 UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN
632 SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
635 MP_TAC (SPECL [`f:real^N->real`; `u:real^N`; `z:real^N`] M_CELL_SUP) THEN
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];
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
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[];
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[]);
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[]);;
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) ==>
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
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;
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
697 UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN
698 SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
701 MP_TAC (SPECL [`f:real^N->real`; `x:real^N`; `u:real^N`] M_CELL_SUP) THEN
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];
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
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[];
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[]);
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[]);;
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 ==>
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
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];
760 SUBGOAL_THEN `diff2_domain (x,z) (f:real^N->real)` ASSUME_TAC THENL
762 UNDISCH_TAC `diff2c_domain (x,z) (f:real^N->real)` THEN
763 SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
766 MP_TAC (SPECL [`f:real^N->real`; `v:real^N`; `z:real^N`] M_CELL_SUP) THEN
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];
782 DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
784 MP_TAC (SPECL [`f:real^N->real`; `x:real^N`; `u:real^N`] M_CELL_SUP) THEN
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];
800 DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
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
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[]);
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;
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;
826 DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
827 EXISTS_TAC `max a a'` THEN
829 ASM_REAL_ARITH_TAC);;
833 (*********************)
835 let ZERO_EQ_ZERO_CONST = prove(`0 = _0`, REWRITE_TAC[NUMERAL]);;
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
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;;
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;;
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));;
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)));;
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
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;;
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));;
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)));;
892 (****************************************)
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;;
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));;
915 (******************************************)
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
923 let x1s = dest_vector x1 and
924 x2s = dest_vector x2 and
925 z2s = dest_vector z2 in
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
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;;
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
943 let x1s = dest_vector x1 and
944 x2s = dest_vector x2 and
945 z2s = dest_vector z2 in
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
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;;
958 (**********************)
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
966 let xs = dest_vector xv and
967 zs = dest_vector zv in
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
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
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;;
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
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
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
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;;
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
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
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
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;;
1032 (*************************)
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
1042 let xs = dest_vector x_tm and
1043 zs = dest_vector z_tm in
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
1049 let le_th0 = float_ge0 bound_tm in
1051 try EQT_ELIM le_th0 with Failure _ -> failwith ("m_convex_pass: "^string_of_thm le_th0) in
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;;
1061 (***********************)
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
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
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;;
1080 (* restrict_domain *)
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
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);;
1099 (****************************************)
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
1108 let kk = ref report_start in
1109 let last_report = ref (int_of_float (float_of_int !kk /. r_size2 *. 100.0)) in
1111 let rec rec_verify =
1112 let rec apply_trans sub_ths th0 acc =
1116 let th' = eval_subset_trans th th0 in
1117 apply_trans ths th' (th' :: acc) in
1119 let rec mk_domains mono th0 acc =
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
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 =
1134 TRUTH, fs.diff2_f xx zz
1136 let t_th = fs.taylor pp pp domain_th in
1137 let _, d_th, _, _ = dest_m_taylor_thms n t_th in
1140 let domain_ths = mk_domains mono domain_th [] in
1141 (* let domains = domain_th :: map fst (butlast domain_ths) in *)
1143 (* let gen_mono (m, domain_th) = *)
1147 eval_interval_arith_hi n (fs.df m.variable pp xx zz)
1149 eval_interval_arith_lo n (fs.df m.variable pp xx zz)
1152 eval_m_taylor_partial_upper n pp m.variable taylor_th
1154 eval_m_taylor_partial_lower n pp m.variable taylor_th in
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
1169 fun domain_th certificate ->
1170 match certificate with
1171 | Result_mono (mono, r1) ->
1172 let _ = !info_print_level < 2 or
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
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
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)
1191 let taylor_th = fs.taylor pp pp domain_th in
1192 m_taylor_cell_pass n pp taylor_th
1194 | Result_glue (i, convex_flag, r1, r2) ->
1195 let domain1_th, domain2_th =
1197 let d1, _ = restrict_domain n (i + 1) true domain_th in
1198 let d2, _ = restrict_domain n (i + 1) false domain_th in
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
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
1213 m_glue_cells n (i + 1) th1 th2
1215 | Result_pass_ref i ->
1216 let _ = !info_print_level < 2 or (report (sprintf "Ref: %d" i); true) in
1218 List.nth th_list (i - 1)
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
1224 | _ -> failwith "False result" in
1226 rec_verify domain_th0 certificate;;
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) [];;
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
1242 let get_m_cell_domain n pp domain0 path =
1243 let rec get_rec domain_th path hash =
1247 let hash' = hash^s^(string_of_int j) in
1249 get_rec (find hash') ps hash'
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
1257 get_rec domain1_th ps hash'
1259 get_rec domain2_th ps hash'
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
1267 let domain_th0 = mk_m_center_domain n pp xx zz in
1268 let size = length certificate_list in
1271 let total_size = end_itlist (+) (map (result_size o snd) certificate_list) in
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 [];;
1286 (***************************)
1287 (* Verification based on a p_result_tree *)
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
1293 let kk = ref report_start in
1294 let last_report = ref (int_of_float (float_of_int !kk /. r_size2 *. 100.0)) in
1296 let rec rec_verify =
1297 let rec apply_trans sub_ths th0 acc =
1301 let th' = eval_subset_trans th th0 in
1302 apply_trans ths th' (th' :: acc) in
1304 let rec mk_domains mono th0 acc =
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
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 =
1319 TRUTH, fs.diff2_f xx zz
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
1325 let domain_ths = mk_domains mono domain_th [] in
1329 eval_interval_arith_hi n (fs.df m.variable p_stat.pp xx zz)
1331 eval_interval_arith_lo n (fs.df m.variable p_stat.pp xx zz)
1334 eval_m_taylor_partial_upper n p_stat.pp m.variable taylor_th
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
1349 fun domain_th certificate ->
1350 match certificate with
1351 | P_result_mono (p_stat, mono, r1) ->
1352 let _ = !info_print_level < 2 or
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
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
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)
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
1374 | P_result_glue (p_stat, i, convex_flag, r1, r2) ->
1375 let domain1_th, domain2_th =
1377 let d1, _ = restrict_domain n (i + 1) true domain_th in
1378 let d2, _ = restrict_domain n (i + 1) false domain_th in
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
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
1393 m_glue_cells n (i + 1) th1 th2
1396 let _ = !info_print_level < 2 or (report (sprintf "Ref: %d" i); true) in
1398 List.nth th_list (i - 1)
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
1404 rec_verify domain_th0 certificate;;
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) [];;
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
1418 let get_m_cell_domain n pp domain0 path =
1419 let rec get_rec domain_th path hash =
1423 let hash' = hash^s^(string_of_int j) in
1425 get_rec (find hash') ps hash'
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
1433 get_rec domain1_th ps hash'
1435 get_rec domain2_th ps hash'
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
1443 let domain_th0 = mk_m_center_domain n p_split xx zz in
1444 let size = length certificate_list in
1447 let total_size = end_itlist (+) (map (p_result_size o snd) certificate_list) in
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 [];;
1462 (*************************************)
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
1470 let kk = ref report_start in
1471 let last_report = ref (int_of_float (float_of_int !kk /. r_size2 *. 100.0)) in
1473 let rec rec_verify =
1474 let rec apply_trans sub_ths th0 acc =
1478 let th' = eval_subset_trans th th0 in
1479 apply_trans ths th' (th' :: acc) in
1481 let rec mk_domains mono th0 acc =
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
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 =
1496 TRUTH, fs.diff2_f xx zz
1498 let t_th = fs.taylor pp pp domain_th in
1499 let _, d_th, _, _ = dest_m_taylor_thms n t_th in
1502 let domain_ths = mk_domains mono domain_th [] in
1503 (* let domains = domain_th :: map fst (butlast domain_ths) in *)
1505 (* let gen_mono (m, domain_th) = *)
1509 eval_interval_arith_hi n (fs.df m.variable pp xx zz)
1511 eval_interval_arith_lo n (fs.df m.variable pp xx zz)
1514 eval_m_taylor_partial_upper n pp m.variable taylor_th
1516 eval_m_taylor_partial_lower n pp m.variable taylor_th in
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
1531 fun domain_th certificate ->
1532 match certificate with
1533 | Result_mono (mono, r1) ->
1534 failwith "Mono: not implemented"
1536 let _ = !info_print_level < 2 or
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
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
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)
1557 let taylor_th = fs.taylor pp pp domain_th in
1558 m_taylor_cell_list_pass n pp taylor_th
1560 | Result_glue (i, convex_flag, r1, r2) ->
1561 let domain1_th, domain2_th =
1563 let d1, _ = restrict_domain n (i + 1) true domain_th in
1564 let d2, _ = restrict_domain n (i + 1) false domain_th in
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
1571 failwith "convexity: not implemented"
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
1582 let th0 = m_glue_cells_list n (i + 1) th1 th2 in
1583 merge_m_cell_list_pass n th0
1585 | Result_pass_ref i ->
1586 let _ = !info_print_level < 2 or (report (sprintf "Ref: %d" i); true) in
1588 List.nth th_list (i - 1)
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
1594 | _ -> failwith "False result" in
1596 rec_verify domain_th0 certificate;;
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) [];;
1610 m_verify_list_raw0 2 pp [formal_f1; formal_f2] cert xx_float_tm zz_float_tm;;