text_formalization/nonlinear/cleanDeriv_examples.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Nonlinear                                                  *)
   5 (* Author: Nicholas Volker                                                    *)
   6 (* Date: 2012-01-18                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (*
  11
  12 Module for automatic differentiation of functions in the flyspeck project.
  13 These functions resulted from Volker's 2011 undergraduate research project at Pitt.
  14
  15
  16 Key stuff:
  17   DIFF_TAC
  18   derived_goal (interactive goal-based differentiation)
  19   nonstack_goal (fully automated)
  20
  21 See cleanDeriv_examples.hl for examples of use.
  22
  23 *)
  24
  25 module Clean_deriv_examples = struct
  26 (* Examples of all the major methods in the cleanDeriv.hl file *)
  27
  28   open Clean_deriv;;
  29
  30
  31
  32
  33
  34 (* the original derived_goal and nonstack_goal methods are deprecated. You may use derived_goal2 and nonstack_goal2 to set the goal term as follows *)
  35
  36 derived_goal2 `\x1:real. ups_x x1 x2 x3`;;
  37
  38 (* This begins an interactive goalstack with the appropriate derived_form as the goal. *)
  39
  40 nonstack_goal2 `\x1:real. ups_x x1 x2 x3`;;
  41
  42 (* This is for use with prove_by_refinement *)
  43
  44 (* Produces the same thing as the previous method, but instead of returning it as a goal returns it as a term. *)
  45
  46 (* These methods attempt to rewrite the term by looking up an associated theorem in a list using the function name, e.g. ups_x or eta2_126. This is done automatically. If a theorem is not found, it does a normal set of rewrites on the term using a list of function definitions. *)
  47
  48 (* DIFF_TAC will reduce a derived_form goal to a set of equivalences with the results of differentiate. *)
  49
  50 derived_goal2 `\x1:real. ups_x x1 x2 x3`;;
  51 e (DIFF_TAC);;
  52 e (REAL_ARITH_TAC);;
  53
  54 let thm = prove_by_refinement ( nonstack_goal2 `\x1:real. ups_x x1 x2 x3`,
  55                                 [
  56                                   DIFF_TAC;
  57                                   REAL_ARITH_TAC;
  58                                 ]);;
  59
  60 (* This will only work for terms that do not require a theorem with extra assumptions to rewrite. For example, does not work for eta2_126. Use DIFF_TAC2. *)
  61
  62 (* 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`. *)
  63
  64 (*
  65 derived_goal2 `\x1:real. eta2_126 x1 x2 x3 x4 x5 x6`;;
  66
  67 e (DIFF_TAC2);;
  68 e (ASM_REWRITE_TAC[]);;
  69 e (MP_TAC (SPEC_ALL eta2_126_eta_x_open));;
  70 e (ASM_REWRITE_TAC[]);;
  71 e (STRIP_TAC);;
  72 e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN);;
  73 *)
  74
  75 (* This set of tactics should nearly complete the goal once those assumptions are added. See the proof of atn2 for an example to this process. Each such function will need a theorem proving its equivalence to something differentiate can handle, and an "openness" theorem. *)
  76
  77 (* mk_xy_derived_goal works as the first methods do, but you must pass it a variable as well as a term. The variable is what will be differentiated with respect to. *)
  78
  79 mk_xy_deriv_goal `x2:real` `\x1:real. eta2_126 x1 x2 x3 x4 x5 x6`;;
  80
  81 (* The final thing that needs to be done is a completion of the lists that these methods reference, and a full automation of creating the lambda abstracted terms. i.e. a method that will loop through all variables on a function and pass the terms to the *_goal2 methods etc. *)
  82
  83 end;;