(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: nonlinear inequalities *) (* Author: Thomas Hales *) (* Date: 2013-01-28 *) (* ========================================================================== *) (* generate all theorems of terms in !Ineq.ineqs from a single assumption `prepared_nonlinear:bool`, defined as the conjunction of all inequalities in prep.hl Taking this a step further, we would get |- prepared_nonlinear ==> nonlinear *) flyspeck_needs "nonlinear/prep.hl";; module Mk_all_ineq = struct open Optimize;; let mk_nonlinear = let ineql = map (fun idv -> idv.ineq) !Ineq.ineqs in let ineq_conj = end_itlist (curry mk_conj) ineql in let _ = new_definition (mk_eq (`nonlinear:bool`,ineq_conj)) in ();; let get_nonlinear = let sl = map (fun ind -> ind.idv) !Ineq.ineqs in let ineql = map (fun idv -> idv.ineq) !Ineq.ineqs in let ineq_conj = end_itlist (curry mk_conj) ineql in let th = new_definition (mk_eq (`nonlinear:bool`,ineq_conj)) in let th1 = UNDISCH (MATCH_MP (TAUT `(a <=> b) ==> (a ==> b)`) th) in let co1 thm = if (is_conj (concl thm)) then CONJUNCT1 thm else thm in fun s -> let i = index s sl in let th2 = funpow i CONJUNCT2 th1 in co1 th2;; (* let prep_ineqs = ref ([]:ineq_datum list);; let add_inequality i = let _ = prep_ineqs:= i :: !prep_ineqs in ();; *) let prep_ineqs = Prep.prep_ineqs;; let mk_prepared_nonlinear = let ineql = map (fun idv -> idv.ineq) (!prep_ineqs) in let ineq_conj = end_itlist (curry mk_conj) ineql in let _ = new_definition (mk_eq (`prepared_nonlinear:bool`,ineq_conj)) in ();; let get_prep_nonlinear = let sl = map (fun ind -> ind.idv) !prep_ineqs in let ineql = map (fun ind -> ind.ineq) (!prep_ineqs) in let ineq_conj = end_itlist (curry mk_conj) ineql in let th = new_definition (mk_eq (`prepared_nonlinear:bool`,ineq_conj)) in let th1 = UNDISCH (MATCH_MP (TAUT `(a <=> b) ==> (a ==> b)`) th) in let co1 thm = if (is_conj (concl thm)) then CONJUNCT1 thm else thm in fun s -> let i = index s sl in let th2 = funpow i CONJUNCT2 th1 in co1 th2;; let hasprefix s sl = filter (fun t -> (String.length s <= String.length t) && (String.sub t 0 (String.length s) = s)) (sl);; let get_all_prep_nonlinear = let sl = map (fun ind -> ind.idv) !prep_ineqs in let ineql = map (fun ind -> ind.ineq) (!prep_ineqs) in let ineq_conj = end_itlist (curry mk_conj) ineql in let th = new_definition (mk_eq (`prepared_nonlinear:bool`,ineq_conj)) in let th1 = UNDISCH (MATCH_MP (TAUT `(a <=> b) ==> (a ==> b)`) th) in let co1 thm = if (is_conj (concl thm)) then CONJUNCT1 thm else thm in let c i thm = co1 (funpow i CONJUNCT2 thm) in let get s = c (index s sl) th1 in fun s -> try [get s] with Failure _ -> (let s' = s^" split(" in let ssl = hasprefix s' sl in map get ssl);; let example1 = get_all_prep_nonlinear "GLFVCVK4a 8328676778";; (* This follows the same sequence in the module Optimize that is used to generate the inequalities in prep.hl, finishing off the last step of the proof with a rewrite. *) let prove_ineq s = let DSPLIT_TAC i = DISCH_TAC THEN (Optimize.SPLIT_H0_TAC i) in let LET_ELIM_TAC = CONV_TAC (REDEPTH_CONV let_CONV) in let is_xconvert tags = mem Xconvert tags in let is_branch tags = mem Branching tags in let NONL = `prepared_nonlinear:bool` in let idq = hd(Ineq.getexact s) in let (s',tags,ineq) = idq_fields idq in let _ = (s = s') or failwith "prove_ineq: wrong ineq" in try (s,prove(mk_imp(NONL,ineq), LET_ELIM_TAC THEN EVERY (map DSPLIT_TAC (get_split_tags idq)) THEN EVERY [LET_ELIM_TAC; PRELIM_REWRITE_TAC; if (is_branch tags) then BRANCH_TAC else ALL_TAC; if (is_xconvert tags) then X_OF_Y_TAC else ALL_TAC; if (is_branch tags && not(is_xconvert tags)) then SERIES3Q1H_5D_TAC else ALL_TAC; STYLIZE_TAC; WRAPUP_TAC; REWRITE_TAC (get_all_prep_nonlinear s)])) with Failure m -> failwith (s^" "^m);; let example2 = map prove_ineq ["GLFVCVK4a 8328676778";"4750199435";"GLFVCVK4 2477216213 y4supercrit"];; Ineq.getexact "4528012043";; prove_ineq "4528012043";; let exec() = let sl = map (fun t -> t.idv) !Ineq.ineqs in map prove_ineq sl;; (* (* experimental, combine subgoals into a a single subgoal. *) let (merge1_goal:refinement) = fun (meta,sgs,just) -> if List.length sgs < 2 then (meta,sgs,just) else let s0::s1::s2 = sgs in let _ = fst(s0) = [] or failwith "merge1_goal asl nonempty" in let _ = fst(s1) = [] or failwith "merge1_goal asl nonempty" in let sgs' = ([],mk_conj (snd s0, snd s1)) ::s2 in let just' i ths = (just i ( (CONJUNCT1 (hd ths)) :: (CONJUNCT2 ( (hd ths))) :: tl ths)) in (meta,sgs',just');; let rec merge_all_goal (meta,sgs,just) = if (List.length sgs < 2) then (meta,sgs,just) else merge_all_goal (merge1_goal (meta,sgs,just));; let top_asl_thm() = let (_,sgs,f)::_ = !current_goalstack in let t = snd(hd sgs) in DISCH t (f null_inst [ASSUME t]);; *) end;;