1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Nonlinear *)
5 (* Author: Nicholas Volker *)
7 (* ========================================================================== *)
12 Module for automatic differentiation of functions in the flyspeck project.
13 These functions resulted from Volker's 2011 undergraduate research project at Pitt.
18 derived_goal (interactive goal-based differentiation)
19 nonstack_goal (fully automated)
21 See cleanDeriv_examples.hl for examples of use.
25 module Clean_deriv = struct
30 open Calc_derivative;;
32 let goal_concl = Hales_tactic.goal_concl;;
34 (* Begin various useful identities about derived_form *)
36 let derived_form_equivalence = prove_by_refinement(`!t1 t2 f1 f2 f1' f2' x s. (t1 = t2) /\ (f1' = f2') /\ (f1 = f2) ==> (derived_form t1 f1 f1' x s ==> derived_form t2 f2 f2' x s)`,
41 let extra_assum_derived_form = prove_by_refinement(`!t1 t2 f1 f2 f1' f2' x s.(f1' = f2') /\ (f2 = f1) ==> (derived_form t1 f1 f1' x s ==> derived_form (t1 /\ t2) f2 f2' x s)`,
43 REWRITE_TAC[derived_form];
47 let retrieve_assum = prove_by_refinement(`!p q f f' x s. (q ==> derived_form (p /\ q) f f' x s) ==> derived_form (p /\ q) f f' x s`,
50 REWRITE_TAC[derived_form];
54 (* End derived_form identities *)
56 (* Begin theorems in order to rewrite function definitions. Currently working on eta2_126. Will probably need to rework these in order to use HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN. *)
58 let zero_lemma = prove_by_refinement(`!x:real. &0 <= x ==> &0 pow 2 <= x`,
63 let sqrt_squared = prove_by_refinement(`!x:real. &0 < x ==> x = sqrt x * sqrt x`,
66 SUBGOAL_THEN `&0 < x ==> &0 <= x` MP_TAC;
69 ASM_MESON_TAC[(SPECL[`x:real`] zero_lemma); (SPECL[`&0`;`x:real`] Nonlinear_lemma.sq_pow2)];
72 let eta2_assum = prove_by_refinement (`!x1 x2 x3 x4 x5 x6. (&0 < x1) /\ (&0 < x2) /\ (&0 < x6) ==> eta2_126 x1 x2 x3 x4 x5 x6 = eta_x x1 x2 x6 pow 2`,
75 MP_TAC (SPEC_ALL eta2_126);
78 ASM_MESON_TAC[(SPECL[`x1:real`] sqrt_squared);(SPECL[`x2:real`] sqrt_squared);(SPECL[`x6:real`] sqrt_squared)];
81 let x_greater_lemma = prove_by_refinement (`!x:real (s:real->bool). &0 < x ==> (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> &0 < x'))`,
90 let eta2_126_eta_x_open = prove_by_refinement (`!x1:real x2:real x3:real x4:real x5:real x6:real (s:real->bool). &0 < x1 /\ &0 < x2 /\ &0 < x6 ==>
91 (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x1) < d ==>
92 ((\x'. eta_x x' x2 x6 pow 2) x') = ((\x'. eta2_126 x' x2 x3 x4 x5 x6) x')))`,
95 MP_TAC (SPECL [`x1:real`;`s:real->bool`] x_greater_lemma);
101 SUBGOAL_THEN `&0 < x'` MP_TAC;
103 MP_TAC (SPECL [`x':real`;`x2:real`;`x3:real`;`x4:real`;`x5:real`;`x6:real`] eta2_assum);
108 (* End theorems needed to rewrite function defns. *)
112 (* A list of the function names and their associated rewrite theorems. If a function requires assumptions in order to rewrite it into a form differentiate understands, it goes here. *)
114 let thms_rew = [(`eta2_126`, eta2_assum)];;
116 (* A list of functions that require no assumptions in order to rewrite. *)
118 let fn_defs_matching = [(`dih_x`, dih_x); (`ups_x`, ups_x); (`delta_x`, delta_x); (`delta_x4`, delta_x4); (`eta_x`, eta_x)];;
120 let fn_defs = [dih_x;ups_x;delta_x;delta_x4;eta_x;chi_x;rho_x];;
122 (* Basic rewrite methods. *)
124 let fn_rewrite (f:term) = rhs (concl (REWRITE_CONV fn_defs f));;
125 let full_rewrite (f:term) = rhs (concl (REPEATC let_CONV (rhs (concl (REWRITE_CONV fn_defs f)))));;
127 (* From here until the notes section I wrote for myself, the first attempt at writing the automatic differentiation and cleanup methods, for first derivatives. Works fine for polynomials and functions that require no assumptions to rewrite for differentiate. *)
129 (* Reduces the goal set by the next 2 methods to a series of three statements of equivalence, that of the assumptions, function and derivative each of which can then be solved using ARITH methods and other identities needed for simplifying the output of differentiate. *)
132 let (_,[t;f;f';x;s]) = strip_comb (goal_concl gl) in
133 let fr = full_rewrite f in
134 (MATCH_MP_TAC retrieve_assum THEN
135 REPEAT STRIP_TAC THEN
136 MP_TAC (Calc_derivative.differentiate fr x s) THEN
137 MATCH_MP_TAC derived_form_equivalence THEN
138 REWRITE_TAC fn_defs) gl;;
140 (* Produces a goal for the interactive goal stack *)
142 let derived_goal (f,var,final_deriv) =
143 let expanded = full_rewrite f in
144 let lambda = mk_abs(var, expanded) in
145 let (_,[p;f;f';x;s]) = strip_comb (concl (Calc_derivative.differentiate lambda var `(:real)`)) in
146 let goal_term = list_mk_comb(`derived_form`, [p;lambda;final_deriv;var;`(:real)`]) in
147 (set_goal([], goal_term));;
149 (* Produces a term for use with prove_by_refinement *)
151 let nonstack_goal (f,var,final_deriv) =
152 let expanded = full_rewrite f in
153 let lambda = mk_abs(var, expanded) in
154 let (_,[p;f;f';x;s]) = strip_comb (concl (Calc_derivative.differentiate lambda var `(:real)`)) in
155 list_mk_comb(`derived_form`, [p;lambda;final_deriv;var;`(:real)`]);;
157 (* Encapsulates the above for Polynomial functions, since the simplification of the derivative is just collection of terms, so REAL_ARITH can handle it. *)
159 let clean_differentiate (f,var,final_deriv) =
160 prove_by_refinement(nonstack_goal (f,var,final_deriv),
163 (* REPEAT try MATCH_MP_TAC fn_identities *)
167 (* <<<<<<<<<<<<<<<<<<<NOTES>>>>>>>>>>>>>>>>>> *)
168 (* Do rewrites in order to differentiate. Collect assumptions from differentiate and the rewrites and apply to the goal of derived_form (pdiff /\ prew) fun simpderiv var universe. Throw extra assumptions into returned value from differentiate to get matching assumption lists. The rewrite assumptions allow you to get fun = f where f is pattern matched from differentiate. Then use all assumptions to apply identities to get derivatives to match. *)
170 (* A list where the desired first derivatives will be put, if there are any. *)
172 let deriv_list = [(`\x1:real. ups_x`,`-- &2 * x1 + &2 * x3 + &2 * x2`)];;
174 (* A method to lookup the theorem needed to rewrite a function name. What I wanted to use to prove equivalence of lambda-abstracted functions. *)
177 let (var,f) = dest_abs tm in
178 let (name,_) = strip_comb f in
179 try REWRITE_TAC[(assoc name thms_rew)]
180 with DNE -> REWRITE_TAC[(assoc name fn_defs_matching)];;
182 (* Methods to grab the assumptions needed to do a rewrite on the original function. These assumptions will be added to those from the differentiate method and put in as the full assumption list in the final goal that we set. *)
185 let (var,f) = dest_abs tm in
186 let (name,_) = strip_comb f in
187 let rw = assoc name thms_rew in
188 let (_,[assum;concl]) = strip_comb (concl (SPEC_ALL rw)) in
189 (assum, mk_abs (var, (full_rewrite (rhs concl))));;
194 let (var,fn) = dest_abs(tm) in
195 (`T`, mk_abs (var, full_rewrite(fn)));;
197 (* Method to search the list of set first derivatives and find a matching one for the function and variable we are differentiating over. If one does not exist, it simply returns what the differentiate method would give you. *)
200 let (var,fn) = dest_abs tm in
201 let (name,_) = strip_comb fn in
202 let searchtm = mk_abs (var, name) in
203 try assoc searchtm deriv_list
205 let (var,_) = dest_abs (tm) in
206 let (assum, lambda) = case_handle tm in
207 let (_,[p;f;f';x;s]) = strip_comb (concl (Calc_derivative.differentiate lambda var `(:real)`)) in
210 (* Methods to set the final goal. derived_goal2 gives a goalstack, nonstack_goal2 returns a term which can be used in a prove_by_refinement. Each take a starting lambda-abstracted term, see if the term needs assumptions in order to be rewritten into a form that differentiate will understand and searches the first derivative list to see if there's a particular form we want. It then applies differentiate to the rewritten function, adds the gathered assumptions together, and sets the final derived_form goal. *)
212 let derived_goal2 tm =
213 let (assum,lambda) = case_handle tm in
214 let final_deriv = find_deriv tm in
215 let (var,_) = dest_abs (lambda) in
216 let (_,[p;f;f';x;s]) = strip_comb (concl (Calc_derivative.differentiate lambda var `(:real)`)) in
217 let all_assum = list_mk_comb(`/\`, [p;assum]) in
218 let goal_term = list_mk_comb(`derived_form`, [all_assum;tm;final_deriv;var;`(:real)`]) in
219 (set_goal([], goal_term));;
221 let nonstack_goal2 tm =
222 let (assum,lambda) = case_handle tm in
223 let final_deriv = find_deriv tm in
224 let (var,_) = dest_abs (lambda) in
225 let (_,[p;f;f';x;s]) = strip_comb (concl (Calc_derivative.differentiate lambda var `(:real)`)) in
226 let all_assum = list_mk_comb(`/\`, [p;assum]) in
227 list_mk_comb(`derived_form`, [all_assum;tm;final_deriv;var;`(:real)`]);;
229 (* A tactic to reduce the above goals to a set of equivalence statements about the assumptions, f and f'. Has been reworked to use HAS_REAL_DERIVATIVE_TRANFORM_WITHIN. A method still needs to be written that will produce the assumption "xi IN s" for each i and add it to the assumption list in order to apply that sequence of reasoning. See the proof of atn2 for more detail. Each method will need an "openness lemma" as well.*)
232 let (_,[t;f;f';x;s]) = strip_comb (goal_concl gl) in
233 let (_,rw) = case_handle f in
234 (REWRITE_TAC[derived_form] THEN
235 REPEAT STRIP_TAC THEN
236 MP_TAC (Calc_derivative.differentiate rw x s) THEN
237 REWRITE_TAC[derived_form]) gl;;
239 (* The below sequence will not work yet because the assumptions "xi IN s" are not in the assumption list. list_mk_comb did not work when applied to IN, but is_comb returns true on the term `x IN s`. *)
242 derived_goal2 `\x1:real. eta2_126 x1 x2 x3 x4 x5 x6`;;
245 e (ASM_REWRITE_TAC[]);;
246 e (MP_TAC (SPEC_ALL eta2_126_eta_x_open));;
247 e (ASM_REWRITE_TAC[]);;
249 e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN);;
252 (* Begin cheating in order to test. Calls mk_fthm. *)
255 let f = `\x1:real. eta2_126 x1 x2 x3 x4 x5 x6`;;
257 let x1_eta2 = mk_fthm([],`derived_form
260 (--x1 * x1 - x2 * x2 - x6 * x6 +
264 ~(--x1 * x1 - x2 * x2 - x6 * x6 +
272 (\x1. eta2_126 x1 x2 x3 x4 x5 x6)
276 (--x1 * x1 - x2 * x2 - x6 * x6 +
282 (--x1 * x1 - x2 * x2 - x6 * x6 +
286 (x1 * x2 * x6) * ((--x1 + -- &1 * x1) + &2 * x6 + &2 * x2)) /
287 (--x1 * x1 - x2 * x2 - x6 * x6 +
296 (--x1 * x1 - x2 * x2 - x6 * x6 +
303 let first_derivs = [(`\x1:real. eta2_126`, x1_eta2)];;
306 (* End cheating. Cheated in in order to test second derivative stuff. This list will be where all the first derivatives will be put *)
308 (* Translated from C code, what the final 2nd derivative should be. Is this correct? *)
310 let x1x2_eta2_126 = `(x6 * (x1 pow 4 + &2 * x1 pow 3 * x2 - &6 * x1 pow 2 * x2 pow 2 + &2 * x1 * x2 pow 3 + x2 pow 4 - &2 * x1 pow 3 * x6 + &6 * x1 pow 2 * x2 * x6 + &6 * x1 * x2 pow 2 * x6 - &2 * x2 pow 3 * x6 - &10 * x1 * x2 * x6 pow 2 + &2 * x1 * x6 pow 3 + &2 * x2 * x6 pow 3 - x6 pow 4))/((ups_x x1 x2 x6) pow 3)`;;
312 let goal_2deriv = full_rewrite x1x2_eta2_126;;
314 let final_second_deriv = [(`\x2:real. \x1:real. eta2_126`, x1x2_eta2_126)];;
316 (* A method to find the first derivative we are looking for. *)
318 let find_deriv_thm tm =
319 let (var,fn) = dest_abs tm in
320 let (name,_) = strip_comb fn in
321 let searchtm = mk_abs (var, name) in
322 assoc searchtm first_derivs;;
324 (* A method to find the desired second derivative. *)
326 let find_wanted_second_deriv y tm =
327 let (var,fn) = dest_abs tm in
328 let (name,_) = strip_comb fn in
329 let firstabs = mk_abs (var, name) in
330 let secondabs = mk_abs (y, firstabs) in
331 assoc secondabs final_second_deriv;;
333 (* Similar to the first derivative case, makes a goal using the f' from the first derivative and carries with it all the assumptions. *)
335 let mk_xy_deriv_goal y tm =
336 let (_,[p;f;f';x;s]) = strip_comb (concl (find_deriv_thm tm)) in
337 let (x,_) = dest_abs(f) in
338 let deriv_abs = mk_abs(y,f') in
339 let (_,[q;g;g';y;s]) = strip_comb (concl (differentiate deriv_abs y `(:real)`)) in
340 let all_assum = list_mk_comb(`/\`,[q;p]) in
341 let goal_deriv = find_wanted_second_deriv y tm in
342 set_goal([], list_mk_comb(`derived_form`,[all_assum;deriv_abs;goal_deriv;y;s]));;
344 (* A similar reduction tactic. Should work better in the second derivative case, since the equivalence of the lambda-abstracted function is immediate. Since has_real_derivative handles nth derivatives in a curried fashion, we don't need to worry about directly associating any function name (such as eta2_126) directly with its second derivative, as long as its first derivative is associated with its second derivative. *)
346 let SECOND_DIFF_TAC gl =
347 let (_,[t;f;f';x;s]) = strip_comb (goal_concl gl) in
348 (MATCH_MP_TAC retrieve_assum THEN
349 REPEAT STRIP_TAC THEN
350 MP_TAC (Calc_derivative.differentiate f x s) THEN
351 MATCH_MP_TAC extra_assum_derived_form THEN
352 ASM_REWRITE_TAC[]) gl;;