text_formalization/nonlinear/mk_all_ineq.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: nonlinear inequalities                                            *)
   5 (* Author:  Thomas Hales     *)
   6 (* Date: 2013-01-28                                                           *)
   7 (* ========================================================================== *)
   8
   9 (* generate all theorems of terms in !Ineq.ineqs from a single assumption `prepared_nonlinear:bool`,
  10    defined as the conjunction of all inequalities in prep.hl
  11
  12    Taking this a step further, we would get |- prepared_nonlinear ==> nonlinear
  13
  14  *)
  15
  16 flyspeck_needs "nonlinear/prep.hl";;
  17
  18 module Mk_all_ineq = struct
  19
  20   open Optimize;;
  21
  22 let mk_nonlinear =
  23   let ineql = map (fun idv -> idv.ineq) !Ineq.ineqs in
  24   let ineq_conj = end_itlist (curry mk_conj) ineql in
  25   let _ = new_definition (mk_eq (`nonlinear:bool`,ineq_conj)) in
  26     ();;
  27
  28 let get_nonlinear =
  29   let sl = map (fun ind -> ind.idv) !Ineq.ineqs in
  30   let ineql = map (fun idv -> idv.ineq) !Ineq.ineqs in
  31   let ineq_conj = end_itlist (curry mk_conj) ineql in
  32   let th = new_definition (mk_eq (`nonlinear:bool`,ineq_conj)) in
  33   let th1 = UNDISCH (MATCH_MP (TAUT `(a <=> b) ==> (a ==> b)`) th) in
  34   let co1 thm = if (is_conj (concl thm)) then CONJUNCT1 thm else thm in
  35     fun s ->
  36       let i = index s sl in
  37       let th2 = funpow i CONJUNCT2 th1 in
  38         co1 th2;;
  39
  40 (*
  41 let prep_ineqs = ref ([]:ineq_datum list);;
  42
  43 let add_inequality i  =
  44   let _ = prep_ineqs:= i :: !prep_ineqs in
  45     ();;
  46 *)
  47
  48 let prep_ineqs = Prep.prep_ineqs;;
  49
  50 let mk_prepared_nonlinear =
  51   let ineql = map (fun idv -> idv.ineq) (!prep_ineqs) in
  52   let ineq_conj = end_itlist (curry mk_conj) ineql in
  53   let _ = new_definition (mk_eq (`prepared_nonlinear:bool`,ineq_conj)) in
  54     ();;
  55
  56 let get_prep_nonlinear =
  57   let sl = map (fun ind -> ind.idv) !prep_ineqs in
  58   let ineql = map (fun ind -> ind.ineq) (!prep_ineqs) in
  59   let ineq_conj = end_itlist (curry mk_conj) ineql in
  60   let th = new_definition (mk_eq (`prepared_nonlinear:bool`,ineq_conj)) in
  61   let th1 = UNDISCH (MATCH_MP (TAUT `(a <=> b) ==> (a ==> b)`) th) in
  62   let co1 thm = if (is_conj (concl thm)) then CONJUNCT1 thm else thm in
  63     fun s ->
  64       let i = index s sl in
  65       let th2 = funpow i CONJUNCT2 th1 in
  66         co1 th2;;
  67
  68 let hasprefix s sl = filter (fun t -> (String.length s <= String.length t) &&
  69                              (String.sub t 0 (String.length s) = s)) (sl);;
  70
  71 let get_all_prep_nonlinear =
  72   let sl = map (fun ind -> ind.idv) !prep_ineqs in
  73   let ineql = map (fun ind -> ind.ineq) (!prep_ineqs) in
  74   let ineq_conj = end_itlist (curry mk_conj) ineql in
  75   let th = new_definition (mk_eq (`prepared_nonlinear:bool`,ineq_conj)) in
  76   let th1 = UNDISCH (MATCH_MP (TAUT `(a <=> b) ==> (a ==> b)`) th) in
  77   let co1 thm = if (is_conj (concl thm)) then CONJUNCT1 thm else thm in
  78   let c i thm = co1 (funpow i CONJUNCT2 thm) in
  79   let get s = c (index s sl) th1 in
  80     fun s ->
  81       try [get s] with
  82           Failure _ ->
  83             (let s' = s^" split(" in
  84              let ssl = hasprefix s' sl in
  85                map get ssl);;
  86
  87 let example1 = get_all_prep_nonlinear  "GLFVCVK4a 8328676778";;
  88
  89 (* This follows the same sequence in the module Optimize that is used to generate the inequalities
  90    in prep.hl, finishing off the last step of the proof with a rewrite. *)
  91
  92 let prove_ineq s =
  93   let DSPLIT_TAC i = DISCH_TAC THEN (Optimize.SPLIT_H0_TAC i) in
  94   let LET_ELIM_TAC = CONV_TAC (REDEPTH_CONV let_CONV) in
  95   let is_xconvert tags = mem Xconvert tags in
  96   let is_branch tags = mem Branching tags in
  97   let NONL = `prepared_nonlinear:bool` in
  98   let idq = hd(Ineq.getexact s) in
  99   let (s',tags,ineq) = idq_fields idq in
 100   let _ = (s = s') or failwith "prove_ineq: wrong ineq" in
 101     try (s,prove(mk_imp(NONL,ineq),
 102           LET_ELIM_TAC THEN
 103             EVERY (map DSPLIT_TAC (get_split_tags idq)) THEN
 104             EVERY
 105             [LET_ELIM_TAC;
 106              PRELIM_REWRITE_TAC;
 107              if (is_branch tags) then BRANCH_TAC else ALL_TAC;
 108              if (is_xconvert tags) then X_OF_Y_TAC else ALL_TAC;
 109              if (is_branch tags && not(is_xconvert tags)) then SERIES3Q1H_5D_TAC else ALL_TAC;
 110              STYLIZE_TAC;
 111              WRAPUP_TAC;
 112              REWRITE_TAC (get_all_prep_nonlinear s)]))
 113     with Failure m -> failwith (s^" "^m);;
 114
 115 let example2 = map prove_ineq  ["GLFVCVK4a 8328676778";"4750199435";"GLFVCVK4 2477216213 y4supercrit"];;
 116
 117 Ineq.getexact "4528012043";;
 118 prove_ineq "4528012043";;
 119
 120 let exec() =
 121   let sl = map (fun t -> t.idv) !Ineq.ineqs in
 122     map prove_ineq sl;;
 123
 124 (* (* experimental, combine subgoals into a a single subgoal. *)
 125 let (merge1_goal:refinement) =
 126   fun (meta,sgs,just) ->
 127   if List.length sgs < 2 then (meta,sgs,just)
 128   else
 129     let s0::s1::s2 = sgs in
 130     let _ = fst(s0) = [] or failwith "merge1_goal asl nonempty" in
 131     let _ = fst(s1) = [] or failwith "merge1_goal asl nonempty" in
 132     let sgs' = ([],mk_conj (snd s0, snd s1)) ::s2 in
 133     let just' i ths =
 134       (just i ( (CONJUNCT1 (hd ths)) :: (CONJUNCT2 ( (hd ths))) :: tl ths)) in
 135       (meta,sgs',just');;
 136
 137 let rec merge_all_goal (meta,sgs,just) =
 138   if (List.length sgs < 2) then (meta,sgs,just)
 139   else merge_all_goal (merge1_goal (meta,sgs,just));;
 140
 141 let top_asl_thm() =
 142   let (_,sgs,f)::_ = !current_goalstack in
 143   let t = snd(hd sgs) in
 144     DISCH t (f null_inst [ASSUME t]);;
 145 *)
 146
 147
 148
 149  end;;