diff options
Diffstat (limited to 'plugins/omega/coq_omega.ml')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 670 |
1 files changed, 392 insertions, 278 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d625e307..51cd665f 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**************************************************************************) (* *) @@ -18,8 +20,9 @@ open Util open Names open Nameops open Term -open Tacticals -open Tacmach +open EConstr +open Tacticals.New +open Tacmach.New open Tactics open Logic open Libnames @@ -27,19 +30,21 @@ open Globnames open Nametab open Contradiction open Misctypes -open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver (* Added by JCF, 09/03/98 *) let elim_id id = - Proofview.Goal.nf_enter { enter = begin fun gl -> - simplest_elim (Tacmach.New.pf_global id gl) - end } -let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl + Proofview.Goal.enter begin fun gl -> + simplest_elim (mkVar id) + end +let resolve_id id = Proofview.Goal.enter begin fun gl -> + apply (mkVar id) +end let timing timer_name f arg = f arg @@ -47,6 +52,7 @@ let display_time_flag = ref false let display_system_flag = ref false let display_action_flag = ref false let old_style_flag = ref false +let letin_flag = ref true (* Should we reset all variable labels between two runs of omega ? *) @@ -67,8 +73,7 @@ open Goptions let _ = declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Omega system time displaying flag"; optkey = ["Omega";"System"]; optread = read display_system_flag; @@ -76,8 +81,7 @@ let _ = let _ = declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Omega action display flag"; optkey = ["Omega";"Action"]; optread = read display_action_flag; @@ -85,8 +89,7 @@ let _ = let _ = declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Omega old style flag"; optkey = ["Omega";"OldStyle"]; optread = read old_style_flag; @@ -94,13 +97,20 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = true; + { optdepr = true; optname = "Omega automatic reset of generated names"; optkey = ["Stable";"Omega"]; optread = read reset_flag; optwrite = write reset_flag } +let _ = + declare_bool_option + { optdepr = false; + optname = "Omega takes advantage of context variables with body"; + optkey = ["Omega";"UseLocalDefs"]; + optread = read letin_flag; + optwrite = write letin_flag } + let intref, reset_all_references = let refs = ref [] in (fun n -> let r = ref n in refs := (r,n) :: !refs; r), @@ -144,14 +154,14 @@ let intern_id,unintern_id,reset_intern_tables = Hashtbl.add table v idx; Hashtbl.add co_table idx v; v), (fun () -> cpt := 0; Hashtbl.clear table) -let mk_then = tclTHENLIST +let mk_then tacs = tclTHENLIST tacs let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) let generalize_tac t = generalize t let elim t = simplest_elim t -let exact t = Tacmach.refine t let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] +let pf_nf gl c = pf_apply Tacred.simpl gl c let rev_assoc k = let rec loop = function @@ -171,8 +181,8 @@ let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags = let hide_constr,find_constr,clear_constr_tables,dump_tables = let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in (fun h id eg b -> l := (h,(id,eg,b)):: !l), - (fun h -> - try List.assoc_f eq_constr_nounivs h !l with Not_found -> failwith "find_contr"), + (fun sigma h -> + try List.assoc_f (eq_constr_nounivs sigma) h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), (fun () -> !l) @@ -196,6 +206,7 @@ let coq_modules = init_modules @arith_modules @ [logic_dir] @ zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] +let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s) let init_constant = gen_constant_in_modules "Omega" init_modules let constant = gen_constant_in_modules "Omega" coq_modules @@ -347,14 +358,21 @@ let coq_not_iff = lazy (constant "not_iff") let coq_not_not = lazy (constant "not_not") let coq_imp_simp = lazy (constant "imp_simp") let coq_iff = lazy (constant "iff") +let coq_not = lazy (init_constant "not") +let coq_and = lazy (init_constant "and") +let coq_or = lazy (init_constant "or") +let coq_eq = lazy (init_constant "eq") +let coq_ex = lazy (init_constant "ex") +let coq_False = lazy (init_constant "False") +let coq_True = lazy (init_constant "True") (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) (* For unfold *) -let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with +let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> EvalConstRef kn - | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant")) + | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant.")) let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc) let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) @@ -363,22 +381,21 @@ let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle) let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt) let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge) let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt) -let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ()))) +let sp_not = lazy (evaluable_ref_of_constr "not" coq_not) let mk_var v = mkVar (Id.of_string v) let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |]) let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |]) let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |]) -let mk_eq t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()), - [| Lazy.force coq_Z; t1; t2 |]) +let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |]) +let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2 let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |]) let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |]) let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |]) -let mk_and t1 t2 = mkApp (build_coq_and (), [| t1; t2 |]) -let mk_or t1 t2 = mkApp (build_coq_or (), [| t1; t2 |]) -let mk_not t = mkApp (build_coq_not (), [| t |]) -let mk_eq_rel t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()), - [| Lazy.force coq_comparison; t1; t2 |]) +let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |]) +let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |]) +let mk_not t = mkApp (Lazy.force coq_not, [| t |]) +let mk_eq_rel t1 t2 = mk_gen_eq (Lazy.force coq_comparison) t1 t2 let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) let mk_integer n = @@ -419,22 +436,23 @@ type result = the term parts that we manipulate, but rather Var's. Said otherwise: all constr manipulated here are closed *) -let destructurate_prop t = - let c, args = decompose_app t in - match kind_of_term c, args with - | _, [_;_;_] when is_global (build_coq_eq ()) c -> Kapp (Eq,args) +let destructurate_prop sigma t = + let eq_constr c1 c2 = eq_constr sigma c1 c2 in + let c, args = decompose_app sigma t in + match EConstr.kind sigma c, args with + | _, [_;_;_] when eq_constr (Lazy.force coq_eq) c -> Kapp (Eq,args) | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zlt) -> Kapp (Zlt,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zge) -> Kapp (Zge,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zgt) -> Kapp (Zgt,args) - | _, [_;_] when eq_constr c (build_coq_and ()) -> Kapp (And,args) - | _, [_;_] when eq_constr c (build_coq_or ()) -> Kapp (Or,args) + | _, [_;_] when eq_constr c (Lazy.force coq_and) -> Kapp (And,args) + | _, [_;_] when eq_constr c (Lazy.force coq_or) -> Kapp (Or,args) | _, [_;_] when eq_constr c (Lazy.force coq_iff) -> Kapp (Iff, args) - | _, [_] when eq_constr c (build_coq_not ()) -> Kapp (Not,args) - | _, [] when eq_constr c (build_coq_False ()) -> Kapp (False,args) - | _, [] when eq_constr c (build_coq_True ()) -> Kapp (True,args) + | _, [_] when eq_constr c (Lazy.force coq_not) -> Kapp (Not,args) + | _, [] when eq_constr c (Lazy.force coq_False) -> Kapp (False,args) + | _, [] when eq_constr c (Lazy.force coq_True) -> Kapp (True,args) | _, [_;_] when eq_constr c (Lazy.force coq_le) -> Kapp (Le,args) | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args) | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args) @@ -447,19 +465,23 @@ let destructurate_prop t = Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) | Var id,[] -> Kvar id | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) - | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal" + | Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") | _ -> Kufo -let destructurate_type t = - let c, args = decompose_app t in - match kind_of_term c, args with - | _, [] when eq_constr c (Lazy.force coq_Z) -> Kapp (Z,args) - | _, [] when eq_constr c (Lazy.force coq_nat) -> Kapp (Nat,args) +let nf = Tacred.simpl + +let destructurate_type env sigma t = + let is_conv = Reductionops.is_conv env sigma in + let c, args = decompose_app sigma (nf env sigma t) in + match EConstr.kind sigma c, args with + | _, [] when is_conv c (Lazy.force coq_Z) -> Kapp (Z,args) + | _, [] when is_conv c (Lazy.force coq_nat) -> Kapp (Nat,args) | _ -> Kufo -let destructurate_term t = - let c, args = decompose_app t in - match kind_of_term c, args with +let destructurate_term sigma t = + let eq_constr c1 c2 = eq_constr sigma c1 c2 in + let c, args = decompose_app sigma t in + match EConstr.kind sigma c, args with | _, [_;_] when eq_constr c (Lazy.force coq_Zplus) -> Kapp (Zplus,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zmult) -> Kapp (Zmult,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zminus) -> Kapp (Zminus,args) @@ -479,15 +501,16 @@ let destructurate_term t = | Var id,[] -> Kvar id | _ -> Kufo -let recognize_number t = +let recognize_number sigma t = + let eq_constr c1 c2 = eq_constr sigma c1 c2 in let rec loop t = - match decompose_app t with + match decompose_app sigma t with | f, [t] when eq_constr f (Lazy.force coq_xI) -> one + two * loop t | f, [t] when eq_constr f (Lazy.force coq_xO) -> two * loop t | f, [] when eq_constr f (Lazy.force coq_xH) -> one | _ -> failwith "not a number" in - match decompose_app t with + match decompose_app sigma t with | f, [t] when eq_constr f (Lazy.force coq_Zpos) -> loop t | f, [t] when eq_constr f (Lazy.force coq_Zneg) -> neg (loop t) | f, [] when eq_constr f (Lazy.force coq_Z0) -> zero @@ -503,9 +526,9 @@ type constr_path = | P_ARITY | P_ARG -let context operation path (t : constr) = +let context sigma operation path (t : constr) = let rec loop i p0 t = - match (p0,kind_of_term t) with + match (p0,EConstr.kind sigma t) with | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t) | ([], _) -> operation i t | ((P_APP n :: p), App (f,v)) -> @@ -516,7 +539,7 @@ let context operation path (t : constr) = let v' = Array.copy v in v'.(n) <- loop i p v'.(n); (mkCase (ci,q,c,v')) | ((P_ARITY :: p), App (f,l)) -> - appvect (loop i p f,l) + mkApp (loop i p f,l) | ((P_ARG :: p), App (f,v)) -> let v' = Array.copy v in v'.(0) <- loop i p v'.(0); mkApp (f,v') @@ -541,8 +564,8 @@ let context operation path (t : constr) = in loop 1 path t -let occurrence path (t : constr) = - let rec loop p0 t = match (p0,kind_of_term t) with +let occurrence sigma path (t : constr) = + let rec loop p0 t = match (p0,EConstr.kind sigma t) with | (p, Cast (c,_,_)) -> loop p c | ([], _) -> t | ((P_APP n :: p), App (f,v)) -> loop p v.(pred n) @@ -561,14 +584,17 @@ let occurrence path (t : constr) = in loop path t -let abstract_path typ path t = +let abstract_path sigma typ path t = let term_occur = ref (mkRel 0) in - let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in + let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur -let focused_simpl path gl = - let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in - Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl +let focused_simpl path = + let open Tacmach.New in + Proofview.Goal.nf_enter begin fun gl -> + let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in + convert_concl_no_check newc DEFAULTcast + end let focused_simpl path = focused_simpl path @@ -615,7 +641,7 @@ let compile name kind = let id = new_id () in tag_hypothesis name id; {kind = kind; body = List.rev accu; constant = n; id = id} - | _ -> anomaly (Pp.str "compile_equation") + | _ -> anomaly (Pp.str "compile_equation.") in loop [] @@ -626,11 +652,18 @@ let decompile af = in loop af.body -let mkNewMeta () = mkMeta (Evarutil.new_meta()) +(** Backward compat to emulate the old Refine: normalize the goal conclusion *) +let new_hole env sigma c = + let c = Reductionops.nf_betaiota env sigma c in + Evarutil.new_evar env sigma c -let clever_rewrite_base_poly typ p result theorem gl = +let clever_rewrite_base_poly typ p result theorem = + let open Tacmach.New in + Proofview.Goal.nf_enter begin fun gl -> let full = pf_concl gl in - let (abstracted,occ) = abstract_path typ (List.rev p) full in + let env = pf_env gl in + let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in + Refine.refine ~typecheck:false begin fun sigma -> let t = applist (mkLambda @@ -643,13 +676,17 @@ let clever_rewrite_base_poly typ p result theorem gl = [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), [abstracted]) in - exact (applist(t,[mkNewMeta()])) gl + let argt = mkApp (abstracted, [|result|]) in + let (sigma, hole) = new_hole env sigma argt in + (sigma, applist (t, [hole])) + end + end -let clever_rewrite_base p result theorem gl = - clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl +let clever_rewrite_base p result theorem = + clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem -let clever_rewrite_base_nat p result theorem gl = - clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem gl +let clever_rewrite_base_nat p result theorem = + clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem let clever_rewrite_gen p result (t,args) = let theorem = applist(t, args) in @@ -659,12 +696,61 @@ let clever_rewrite_gen_nat p result (t,args) = let theorem = applist(t, args) in clever_rewrite_base_nat p result theorem -let clever_rewrite p vpath t gl = +(** Solve using the term the term [t _] *) +let refine_app gl t = + let open Tacmach.New in + Refine.refine ~typecheck:false begin fun sigma -> + let env = pf_env gl in + let ht = match EConstr.kind sigma (pf_get_type_of gl t) with + | Prod (_, t, _) -> t + | _ -> assert false + in + let (sigma, hole) = new_hole env sigma ht in + (sigma, applist (t, [hole])) + end + +let clever_rewrite p vpath t = + let open Tacmach.New in + Proofview.Goal.nf_enter begin fun gl -> let full = pf_concl gl in - let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in - let vargs = List.map (fun p -> occurrence p occ) vpath in + let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in + let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in let t' = applist(t, (vargs @ [abstracted])) in - exact (applist(t',[mkNewMeta()])) gl + refine_app gl t' + end + +(** simpl_coeffs : + The subterm at location [path_init] in the current goal should + look like [(v1*c1 + (v2*c2 + ... (vn*cn + k)))], and we reduce + via "simpl" each [ci] and the final constant [k]. + The path [path_k] gives the location of constant [k]. + Earlier, the whole was a mere call to [focused_simpl], + leading to reduction inside the atoms [vi], which is bad, + for instance when the atom is an evaluable definition + (see #4132). *) + +let simpl_coeffs path_init path_k = + Proofview.Goal.enter begin fun gl -> + let sigma = project gl in + let rec loop n t = + if Int.equal n 0 then pf_nf gl t + else + (* t should be of the form ((v * c) + ...) *) + match EConstr.kind sigma t with + | App(f,[|t1;t2|]) -> + (match EConstr.kind sigma t1 with + | App (g,[|v;c|]) -> + let c' = pf_nf gl c in + let t2' = loop (pred n) t2 in + mkApp (f,[|mkApp (g,[|v;c'|]);t2'|]) + | _ -> assert false) + | _ -> assert false + in + let n = Pervasives.(-) (List.length path_k) (List.length path_init) in + let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) + in + convert_concl_no_check newc DEFAULTcast + end let rec shuffle p (t1,t2) = match t1,t2 with @@ -728,7 +814,7 @@ let shuffle_mult p_init k1 e1 k2 e2 = let tac' = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: + tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: loop p (l1,l2) else tac :: loop (P_APP 2 :: p) (l1,l2) else if v1 > v2 then @@ -763,7 +849,7 @@ let shuffle_mult p_init k1 e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) ([],l2) - | [],[] -> [focused_simpl p_init] + | [],[] -> [simpl_coeffs p_init p] in loop p_init (e1,e2) @@ -786,7 +872,7 @@ let shuffle_mult_right p_init e1 k2 e2 = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: + tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: loop p (l1,l2) else tac :: loop (P_APP 2 :: p) (l1,l2) else if v1 > v2 then @@ -813,7 +899,7 @@ let shuffle_mult_right p_init e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) ([],l2) - | [],[] -> [focused_simpl p_init] + | [],[] -> [simpl_coeffs p_init p] in loop p_init (e1,e2) @@ -847,14 +933,14 @@ let rec scalar p n = function (Lazy.force coq_fast_Zmult_assoc_reverse); focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (n*x)) - | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products" + | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") | (Oatom _ as t) -> [], Otimes(t,Oz n) | Oz i -> [focused_simpl p],Oz(n*i) | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |])) let scalar_norm p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | (_::l) -> clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2]; @@ -865,7 +951,7 @@ let scalar_norm p_init = let norm_add p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | _:: l -> clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zplus_assoc_reverse) :: @@ -875,7 +961,7 @@ let norm_add p_init = let scalar_norm_add p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | _ :: l -> clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; @@ -899,17 +985,17 @@ let rec negate p = function [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] (Lazy.force coq_fast_Zopp_mult_distr_r); focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x)) - | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products" + | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") | (Oatom _ as t) -> let r = Otimes(t,Oz(negone)) in [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r | Oz i -> [focused_simpl p],Oz(neg i) | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |])) -let rec transform p t = +let rec transform sigma p t = let default isnat t' = try - let v,th,_ = find_constr t' in + let v,th,_ = find_constr sigma t' in [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v with e when CErrors.noncritical e -> let v = new_identifier_var () @@ -917,29 +1003,29 @@ let rec transform p t = hide_constr t' v th isnat; [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v in - try match destructurate_term t with + try match destructurate_term sigma t with | Kapp(Zplus,[t1;t2]) -> - let tac1,t1' = transform (P_APP 1 :: p) t1 - and tac2,t2' = transform (P_APP 2 :: p) t2 in + let tac1,t1' = transform sigma (P_APP 1 :: p) t1 + and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in let tac,t' = shuffle p (t1',t2') in tac1 @ tac2 @ tac, t' | Kapp(Zminus,[t1;t2]) -> let tac,t = - transform p + transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in - Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t + unfold sp_Zminus :: tac,t | Kapp(Zsucc,[t1]) -> - let tac,t = transform p (mkApp (Lazy.force coq_Zplus, + let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer one |])) in - Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t + unfold sp_Zsucc :: tac,t | Kapp(Zpred,[t1]) -> - let tac,t = transform p (mkApp (Lazy.force coq_Zplus, + let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer negone |])) in - Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t + unfold sp_Zpred :: tac,t | Kapp(Zmult,[t1;t2]) -> - let tac1,t1' = transform (P_APP 1 :: p) t1 - and tac2,t2' = transform (P_APP 2 :: p) t2 in + let tac1,t1' = transform sigma (P_APP 1 :: p) t1 + and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in begin match t1',t2' with | (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t' | (Oz n,_) -> @@ -950,11 +1036,11 @@ let rec transform p t = | _ -> default false t end | Kapp((Zpos|Zneg|Z0),_) -> - (try ([],Oz(recognize_number t)) + (try ([],Oz(recognize_number sigma t)) with e when CErrors.noncritical e -> default false t) | Kvar s -> [],Oatom s | Kapp(Zopp,[t]) -> - let tac,t' = transform (P_APP 1 :: p) t in + let tac,t' = transform sigma (P_APP 1 :: p) t in let tac',t'' = negate p t' in tac @ tac', t'' | Kapp(Z_of_nat,[t']) -> default true t' @@ -982,7 +1068,7 @@ let shrink_pair p f1 f2 = | t1,t2 -> begin oprint t1; print_newline (); oprint t2; print_newline (); - flush Pervasives.stdout; error "shrink.1" + flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1") end let reduce_factor p = function @@ -994,10 +1080,10 @@ let reduce_factor p = function let rec compute = function | Oz n -> n | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2) - | _ -> error "condense.1" + | _ -> CErrors.user_err Pp.(str "condense.1") in [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c)) - | t -> oprint t; error "reduce_factor.1" + | t -> oprint t; CErrors.user_err Pp.(str "reduce_factor.1") let rec condense p = function | Oplus(f1,(Oplus(f2,r) as t)) -> @@ -1054,7 +1140,7 @@ let replay_history tactic_normalisation = | HYP e :: l -> begin try - Tacticals.New.tclTHEN + tclTHEN (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation) (loop l) with Not_found -> loop l end @@ -1066,16 +1152,16 @@ let replay_history tactic_normalisation = let k = if b then negone else one in let p_initial = [P_APP 1;P_TYPE] in let tac= shuffle_mult_right p_initial e1.body k e2.body in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ generalize_tac [mkApp (Lazy.force coq_OMEGA17, [| val_of eq1; val_of eq2; mk_integer k; mkVar id1; mkVar id2 |])]; - Proofview.V82.tactic (mk_then tac); + mk_then tac; (intros_using [aux]); - Proofview.V82.tactic (resolve_id aux); + resolve_id aux; reflexivity ] | CONTRADICTION (e1,e2) :: l -> @@ -1084,14 +1170,14 @@ let replay_history tactic_normalisation = let p_initial = [P_APP 2;P_TYPE] in let tac = shuffle_cancel p_initial e1.body in let solve_le = - let not_sup_sup = mkApp (Universes.constr_of_global (build_coq_eq ()), + let not_sup_sup = mkApp (Lazy.force coq_eq, [| Lazy.force coq_comparison; Lazy.force coq_Gt; Lazy.force coq_Gt |]) in - Tacticals.New.tclTHENS - (Tacticals.New.tclTHENLIST [ + tclTHENS + (tclTHENLIST [ unfold sp_Zle; simpl_in_concl; intro; @@ -1104,7 +1190,7 @@ let replay_history tactic_normalisation = mkVar (hyp_of_tag e1.id); mkVar (hyp_of_tag e2.id) |]) in - Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (generalize_tac [theorem])) (mk_then tac))) (solve_le) + Proofview.tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) solve_le | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> let id = hyp_of_tag e1.id in let eq1 = val_of(decompile e1) @@ -1114,10 +1200,10 @@ let replay_history tactic_normalisation = let rhs = mk_plus (mk_times eq2 kk) dd in let state_eg = mk_eq eq1 rhs in let tac = scalar_norm_add [P_APP 3] e2.body in - Tacticals.New.tclTHENS + tclTHENS (cut state_eg) - [ Tacticals.New.tclTHENS - (Tacticals.New.tclTHENLIST [ + [ tclTHENS + (tclTHENLIST [ (intros_using [aux]); (generalize_tac [mkApp (Lazy.force coq_OMEGA1, @@ -1125,9 +1211,9 @@ let replay_history tactic_normalisation = (clear [aux;id]); (intros_using [id]); (cut (mk_gt kk dd)) ]) - [ Tacticals.New.tclTHENS + [ tclTHENS (cut (mk_gt kk izero)) - [ Tacticals.New.tclTHENLIST [ + [ tclTHENLIST [ (intros_using [aux1; aux2]); (generalize_tac [mkApp (Lazy.force coq_Zmult_le_approx, @@ -1135,13 +1221,13 @@ let replay_history tactic_normalisation = (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] + tclTHEN (mk_then tac) reflexivity ] | NOT_EXACT_DIVIDE (e1,k) :: l -> let c = floor_div e1.constant k in @@ -1152,10 +1238,10 @@ let replay_history tactic_normalisation = let kk = mk_integer k and dd = mk_integer d in let tac = scalar_norm_add [P_APP 2] e2.body in - Tacticals.New.tclTHENS + tclTHENS (cut (mk_gt dd izero)) - [ Tacticals.New.tclTHENS (cut (mk_gt kk dd)) - [Tacticals.New.tclTHENLIST [ + [ tclTHENS (cut (mk_gt kk dd)) + [tclTHENLIST [ (intros_using [aux2;aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA4, @@ -1163,14 +1249,14 @@ let replay_history tactic_normalisation = (clear [aux1;aux2]); unfold sp_not; (intros_using [aux]); - Proofview.V82.tactic (resolve_id aux); - Proofview.V82.tactic (mk_then tac); + resolve_id aux; + mk_then tac; assumption ] ; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ] @@ -1183,9 +1269,9 @@ let replay_history tactic_normalisation = let state_eq = mk_eq eq1 (mk_times eq2 kk) in if e1.kind == DISE then let tac = scalar_norm [P_APP 3] e2.body in - Tacticals.New.tclTHENS + tclTHENS (cut state_eq) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA18, @@ -1193,14 +1279,14 @@ let replay_history tactic_normalisation = (clear [aux1;id]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] + tclTHEN (mk_then tac) reflexivity ] else let tac = scalar_norm [P_APP 3] e2.body in - Tacticals.New.tclTHENS (cut state_eq) + tclTHENS (cut state_eq) [ - Tacticals.New.tclTHENS + tclTHENS (cut (mk_gt kk izero)) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux2;aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA3, @@ -1208,11 +1294,11 @@ let replay_history tactic_normalisation = (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] + tclTHEN (mk_then tac) reflexivity ] | (MERGE_EQ(e3,e1,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1225,16 +1311,16 @@ let replay_history tactic_normalisation = (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: scalar_norm [P_APP 3] e1.body in - Tacticals.New.tclTHENS + tclTHENS (cut (mk_eq eq1 (mk_inv eq2))) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux]); (generalize_tac [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); (clear [id1;id2;aux]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity] + tclTHEN (mk_then tac) reflexivity] | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l -> let id = new_identifier () @@ -1244,7 +1330,7 @@ let replay_history tactic_normalisation = and eq2 = val_of(decompile orig) in let vid = unintern_id v in let theorem = - mkApp (build_coq_ex (), [| + mkApp (Lazy.force coq_ex, [| Lazy.force coq_Z; mkLambda (Name vid, @@ -1258,9 +1344,9 @@ let replay_history tactic_normalisation = [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: shuffle_mult_right p_initial orig.body m ({c= negone;v= v}::def.body) in - Tacticals.New.tclTHENS + tclTHENS (cut theorem) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux]); (elim_id aux); (clear [aux]); @@ -1268,11 +1354,11 @@ let replay_history tactic_normalisation = (generalize_tac [mkApp (Lazy.force coq_OMEGA9, [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); - Proofview.V82.tactic (mk_then tac); + mk_then tac; (clear [aux]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ] + tclTHEN (exists_tac eq1) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in @@ -1281,10 +1367,10 @@ let replay_history tactic_normalisation = let tac1 = norm_add [P_APP 2;P_TYPE] e.body in let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in let eq = val_of(decompile e) in - Tacticals.New.tclTHENS + tclTHENS (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) - [Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac1); (intros_using [id1]); (loop act1) ]; - Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac2); (intros_using [id2]); (loop act2) ]] + [tclTHENLIST [ mk_then tac1; (intros_using [id1]); (loop act1) ]; + tclTHENLIST [ mk_then tac2; (intros_using [id2]); (loop act2) ]] | SUM(e3,(k1,e1),(k2,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1303,10 +1389,10 @@ let replay_history tactic_normalisation = let p_initial = if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in let tac = shuffle_mult_right p_initial e1.body k2 e2.body in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); - Proofview.V82.tactic (mk_then tac); + mk_then tac; (intros_using [id]); (loop l) ] @@ -1315,10 +1401,10 @@ let replay_history tactic_normalisation = and kk2 = mk_integer k2 in let p_initial = [P_APP 2;P_TYPE] in let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in - Tacticals.New.tclTHENS (cut (mk_gt kk1 izero)) - [Tacticals.New.tclTHENS + tclTHENS (cut (mk_gt kk1 izero)) + [tclTHENS (cut (mk_gt kk2 izero)) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux2;aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA7, [| @@ -1326,102 +1412,102 @@ let replay_history tactic_normalisation = mkVar aux1;mkVar aux2; mkVar id1;mkVar id2 |])]); (clear [aux1;aux2]); - Proofview.V82.tactic (mk_then tac); + mk_then tac; (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ] | CONSTANT_NOT_NUL(e,k) :: l -> - Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl + tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl | CONSTANT_NUL(e) :: l -> - Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity + tclTHEN (resolve_id (hyp_of_tag e)) reflexivity | CONSTANT_NEG(e,k) :: l -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkVar (hyp_of_tag e)]); unfold sp_Zle; simpl_in_concl; unfold sp_not; (intros_using [aux]); - Proofview.V82.tactic (resolve_id aux); + resolve_id aux; reflexivity ] | _ -> Proofview.tclUNIT () in loop -let normalize p_initial t = - let (tac,t') = transform p_initial t in +let normalize sigma p_initial t = + let (tac,t') = transform sigma p_initial t in let (tac',t'') = condense p_initial t' in let (tac'',t''') = clear_zero p_initial t'' in tac @ tac' @ tac'' , t''' -let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) = +let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = let p_initial = [P_APP pos ;P_TYPE] in - let (tac,t') = normalize p_initial t in + let (tac,t') = normalize sigma p_initial t in let shift_left = tclTHEN - (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])) - (tclTRY (Proofview.V82.of_tactic (clear [id]))) + (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]) + (tclTRY (clear [id])) in if not (List.is_empty tac) then let id' = new_identifier () in - ((id',(Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (shift_left); Proofview.V82.tactic (mk_then tac); (intros_using [id']) ])) + ((id',(tclTHENLIST [ shift_left; mk_then tac; (intros_using [id']) ])) :: tactic, compile id' flag t' :: defs) else (tactic,defs) -let destructure_omega gl tac_def (id,c) = +let destructure_omega env sigma tac_def (id,c) = if String.equal (atompart_of_id id) "State" then tac_def else - try match destructurate_prop c with + try match destructurate_prop sigma c with | Kapp(Eq,[typ;t1;t2]) - when begin match destructurate_type (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end -> + when begin match destructurate_type env sigma typ with Kapp(Z,[]) -> true | _ -> false end -> let t = mk_plus t1 (mk_inv t2) in - normalize_equation + normalize_equation sigma id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def | Kapp(Zne,[t1;t2]) -> let t = mk_plus t1 (mk_inv t2) in - normalize_equation + normalize_equation sigma id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def | Kapp(Zle,[t1;t2]) -> let t = mk_plus t2 (mk_inv t1) in - normalize_equation + normalize_equation sigma id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def | Kapp(Zlt,[t1;t2]) -> let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in - normalize_equation + normalize_equation sigma id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def | Kapp(Zge,[t1;t2]) -> let t = mk_plus t1 (mk_inv t2) in - normalize_equation + normalize_equation sigma id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def | Kapp(Zgt,[t1;t2]) -> let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in - normalize_equation + normalize_equation sigma id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def | _ -> tac_def with e when catchable_exception e -> tac_def let reintroduce id = (* [id] cannot be cleared if dependent: protect it by a try *) - Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) (intro_using id) + tclTHEN (tclTRY (clear [id])) (intro_using id) open Proofview.Notations let coq_omega = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> clear_constr_tables (); let hyps_types = Tacmach.New.pf_hyps_types gl in - let destructure_omega = Tacmach.New.of_old destructure_omega gl in + let destructure_omega = Tacmach.New.pf_apply destructure_omega gl in let tactic_normalisation, system = List.fold_left destructure_omega ([],[]) hyps_types in let prelude,sys = @@ -1431,7 +1517,7 @@ let coq_omega = let id = new_identifier () in let i = new_id () in tag_hypothesis id i; - (Tacticals.New.tclTHENLIST [ + (tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); (intros_using [v; id]); (elim_id id); @@ -1442,7 +1528,7 @@ let coq_omega = body = [{v=intern_id v; c=one}]; constant = zero; id = i} :: sys else - (Tacticals.New.tclTHENLIST [ + (tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_new_var, [t]))); (intros_using [v;th]); tac ]), @@ -1458,94 +1544,96 @@ let coq_omega = with UNSOLVABLE -> let _,path = depend [] [] (history ()) in if !display_action_flag then display_action display_var path; - (Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)) + (tclTHEN prelude (replay_history tactic_normalisation path)) end else begin try let path = simplify_strong (new_id,new_var_num,display_var) system in if !display_action_flag then display_action display_var path; - Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system") + tclTHEN prelude (replay_history tactic_normalisation path) + with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system") + end end - end } let coq_omega = coq_omega let nat_inject = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in let rec explore p t : unit Proofview.tactic = - try match destructurate_term t with + Proofview.tclEVARMAP >>= fun sigma -> + try match destructurate_term sigma t with | Kapp(Plus,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) + tclTHENLIST [ + (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_plus),[t1;t2])); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ] | Kapp(Mult,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) + tclTHENLIST [ + (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_mult),[t1;t2])); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ] | Kapp(Minus,[t1;t2]) -> let id = new_identifier () in - Tacticals.New.tclTHENS - (Tacticals.New.tclTHEN + tclTHENS + (tclTHEN (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) (intros_using [id])) [ - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (clever_rewrite_gen p + tclTHENLIST [ + (clever_rewrite_gen p (mk_minus (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id])); (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ]; - (Tacticals.New.tclTHEN - (Proofview.V82.tactic (clever_rewrite_gen p (mk_integer zero) - ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))) + (tclTHEN + (clever_rewrite_gen p (mk_integer zero) + ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])) (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])])) ] | Kapp(S,[t']) -> let rec is_number t = - try match destructurate_term t with + try match destructurate_term sigma t with Kapp(S,[t]) -> is_number t | Kapp(O,[]) -> true | _ -> false with e when catchable_exception e -> false in let rec loop p t : unit Proofview.tactic = - try match destructurate_term t with + try match destructurate_term sigma t with Kapp(S,[t]) -> - (Tacticals.New.tclTHEN - (Proofview.V82.tactic (clever_rewrite_gen p + (tclTHEN + (clever_rewrite_gen p (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |])) - ((Lazy.force coq_inj_S),[t]))) + ((Lazy.force coq_inj_S),[t])) (loop (P_APP 1 :: p) t)) | _ -> explore p t with e when catchable_exception e -> explore p t in - if is_number t' then Proofview.V82.tactic (focused_simpl p) else loop p t + if is_number t' then focused_simpl p else loop p t | Kapp(Pred,[t]) -> let t_minus_one = mkApp (Lazy.force coq_minus, [| t; mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in - Tacticals.New.tclTHEN - (Proofview.V82.tactic (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one - ((Lazy.force coq_pred_of_minus),[t]))) + tclTHEN + (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one + ((Lazy.force coq_pred_of_minus),[t])) (explore p t_minus_one) - | Kapp(O,[]) -> Proofview.V82.tactic (focused_simpl p) + | Kapp(O,[]) -> focused_simpl p | _ -> Proofview.tclUNIT () with e when catchable_exception e -> Proofview.tclUNIT () and loop = function | [] -> Proofview.tclUNIT () | (i,t)::lit -> - begin try match destructurate_prop t with + Proofview.tclEVARMAP >>= fun sigma -> + begin try match destructurate_prop sigma t with Kapp(Le,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1554,7 +1642,7 @@ let nat_inject = (loop lit) ] | Kapp(Lt,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1563,7 +1651,7 @@ let nat_inject = (loop lit) ] | Kapp(Ge,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1572,7 +1660,7 @@ let nat_inject = (loop lit) ] | Kapp(Gt,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1581,7 +1669,7 @@ let nat_inject = (loop lit) ] | Kapp(Neq,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1591,7 +1679,7 @@ let nat_inject = ] | Kapp(Eq,[typ;t1;t2]) -> if is_conv typ (Lazy.force coq_nat) then - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 2; P_TYPE] t1); @@ -1605,7 +1693,7 @@ let nat_inject = in let hyps_types = Tacmach.New.pf_hyps_types gl in loop (List.rev hyps_types) - end } + end let dec_binop = function | Zne -> coq_dec_Zne @@ -1639,26 +1727,26 @@ let not_binop = function exception Undecidable -let rec decidability gl t = - match destructurate_prop t with +let rec decidability env sigma t = + match destructurate_prop sigma t with | Kapp(Or,[t1;t2]) -> mkApp (Lazy.force coq_dec_or, [| t1; t2; - decidability gl t1; decidability gl t2 |]) + decidability env sigma t1; decidability env sigma t2 |]) | Kapp(And,[t1;t2]) -> mkApp (Lazy.force coq_dec_and, [| t1; t2; - decidability gl t1; decidability gl t2 |]) + decidability env sigma t1; decidability env sigma t2 |]) | Kapp(Iff,[t1;t2]) -> mkApp (Lazy.force coq_dec_iff, [| t1; t2; - decidability gl t1; decidability gl t2 |]) + decidability env sigma t1; decidability env sigma t2 |]) | Kimp(t1,t2) -> (* This is the only situation where it's not obvious that [t] is in Prop. The recursive call on [t2] will ensure that. *) mkApp (Lazy.force coq_dec_imp, - [| t1; t2; decidability gl t1; decidability gl t2 |]) + [| t1; t2; decidability env sigma t1; decidability env sigma t2 |]) | Kapp(Not,[t1]) -> - mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |]) + mkApp (Lazy.force coq_dec_not, [| t1; decidability env sigma t1 |]) | Kapp(Eq,[typ;t1;t2]) -> - begin match destructurate_type (pf_nf gl typ) with + begin match destructurate_type env sigma typ with | Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |]) | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |]) | _ -> raise Undecidable @@ -1670,59 +1758,78 @@ let rec decidability gl t = | Kapp(True,[]) -> Lazy.force coq_dec_True | _ -> raise Undecidable +let fresh_id avoid id gl = + fresh_id_in_env avoid id (Proofview.Goal.env gl) + let onClearedName id tac = (* We cannot ensure that hyps can be cleared (because of dependencies), *) (* so renaming may be necessary *) - Tacticals.New.tclTHEN - (Tacticals.New.tclTRY (clear [id])) - (Proofview.Goal.nf_enter { enter = begin fun gl -> - let id = Tacmach.New.of_old (fresh_id [] id) gl in - Tacticals.New.tclTHEN (introduction id) (tac id) - end }) + tclTHEN + (tclTRY (clear [id])) + (Proofview.Goal.nf_enter begin fun gl -> + let id = fresh_id Id.Set.empty id gl in + tclTHEN (introduction id) (tac id) + end) let onClearedName2 id tac = - Tacticals.New.tclTHEN - (Tacticals.New.tclTRY (clear [id])) - (Proofview.Goal.nf_enter { enter = begin fun gl -> - let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in - let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in - Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] - end }) + tclTHEN + (tclTRY (clear [id])) + (Proofview.Goal.nf_enter begin fun gl -> + let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in + let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in + tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] + end) let destructure_hyps = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - let decidability = Tacmach.New.of_old decidability gl in - let pf_nf = Tacmach.New.of_old pf_nf gl in - let rec loop = function - | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) - | decl::lit -> - let (i,_,t) = to_tuple decl in - begin try match destructurate_prop t with + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let decidability = decidability env sigma in + let rec loop = function + | [] -> (tclTHEN nat_inject coq_omega) + | LocalDef (i,body,typ) :: lit when !letin_flag -> + Proofview.tclEVARMAP >>= fun sigma -> + begin + try + match destructurate_type env sigma typ with + | Kapp(Nat,_) | Kapp(Z,_) -> + let hid = fresh_id Id.Set.empty (add_suffix i "_eqn") gl in + let hty = mk_gen_eq typ (mkVar i) body in + tclTHEN + (assert_by (Name hid) hty reflexivity) + (loop (LocalAssum (hid, hty) :: lit)) + | _ -> loop lit + with e when catchable_exception e -> loop lit + end + | decl :: lit -> (* variable without body (or !letin_flag isn't set) *) + let i = NamedDecl.get_id decl in + Proofview.tclEVARMAP >>= fun sigma -> + begin try match destructurate_prop sigma (NamedDecl.get_type decl) with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> - (Tacticals.New.tclTHENS + (tclTHENS (elim_id i) [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit))); onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ]) | Kapp(And,[t1;t2]) -> - Tacticals.New.tclTHEN + tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit))) | Kapp(Iff,[t1;t2]) -> - Tacticals.New.tclTHEN + tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit))) | Kimp(t1,t2) -> (* t1 and t2 might be in Type rather than Prop. For t1, the decidability check will ensure being Prop. *) - if is_Prop (type_of t2) + if Termops.is_Prop sigma (type_of t2) then let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> @@ -1731,9 +1838,9 @@ let destructure_hyps = else loop lit | Kapp(Not,[t]) -> - begin match destructurate_prop t with + begin match destructurate_prop sigma t with Kapp(Or,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); (onClearedName i (fun i -> @@ -1741,7 +1848,7 @@ let destructure_hyps = ] | Kapp(And,[t1;t2]) -> let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_and, [| t1; t2; d1; mkVar i |])]); @@ -1751,7 +1858,7 @@ let destructure_hyps = | Kapp(Iff,[t1;t2]) -> let d1 = decidability t1 in let d2 = decidability t2 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_iff, [| t1; t2; d1; d2; mkVar i |])]); @@ -1763,7 +1870,7 @@ let destructure_hyps = (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok. For t1, being decidable implies being Prop. *) let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_imp, [| t1; t2; d1; mkVar i |])]); @@ -1772,7 +1879,7 @@ let destructure_hyps = ] | Kapp(Not,[t]) -> let d = decidability t in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit)))) @@ -1780,7 +1887,7 @@ let destructure_hyps = | Kapp(op,[t1;t2]) -> (try let thm = not_binop op in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); (onClearedName i (fun _ -> loop lit)) @@ -1788,16 +1895,16 @@ let destructure_hyps = with Not_found -> loop lit) | Kapp(Eq,[typ;t1;t2]) -> if !old_style_flag then begin - match destructurate_type (pf_nf typ) with + match destructurate_type env sigma typ with | Kapp(Nat,_) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (simplest_elim (mkApp (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); (onClearedName i (fun _ -> loop lit)) ] | Kapp(Z,_) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (simplest_elim (mkApp (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); @@ -1805,16 +1912,16 @@ let destructure_hyps = ] | _ -> loop lit end else begin - match destructurate_type (pf_nf typ) with + match destructurate_type env sigma typ with | Kapp(Nat,_) -> - (Tacticals.New.tclTHEN - (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) - decl)) + (tclTHEN + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + decl)) (loop lit)) | Kapp(Z,_) -> - (Tacticals.New.tclTHEN - (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) - decl)) + (tclTHEN + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + decl)) (loop lit)) | _ -> loop lit end @@ -1828,34 +1935,41 @@ let destructure_hyps = in let hyps = Proofview.Goal.hyps gl in loop hyps - end } + end let destructure_goal = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let decidability = Tacmach.New.of_old decidability gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let decidability = decidability env sigma in let rec loop t = - match destructurate_prop t with + Proofview.tclEVARMAP >>= fun sigma -> + let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in + Proofview.V82.wrap_exceptions prop >>= fun prop -> + match prop with | Kapp(Not,[t]) -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (unfold sp_not) intro) + (tclTHEN + (tclTHEN (unfold sp_not) intro) destructure_hyps) - | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b)) + | Kimp(a,b) -> (tclTHEN intro (loop b)) | Kapp(False,[]) -> destructure_hyps | _ -> let goal_tac = try let dec = decidability t in - Tacticals.New.tclTHEN - (Proofview.V82.tactic (Tacmach.refine - (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))) + tclTHEN + (Proofview.Goal.nf_enter begin fun gl -> + refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |])) + end) intro - with Undecidable -> Tactics.elim_type (build_coq_False ()) + with Undecidable -> Tactics.elim_type (Lazy.force coq_False) + | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in - Tacticals.New.tclTHEN goal_tac destructure_hyps + tclTHEN goal_tac destructure_hyps in (loop concl) - end } + end let destructure_goal = destructure_goal |