From 87a63ffc6dd36be0ef2e757b46f3c81f67f96207 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 12 Jun 2017 11:34:53 +0200 Subject: Omega now aware of context variables with bodies (in type Z or nat) (fix bug 148) For compatibility, this extra feature of omega could be disabled via Unset Omega UseLocalDefs. Caveat : for now, real let-ins inside goals or hyps aren't handled, use some "cbv zeta" reduction if you want to get rid of them. And context definitions whose types aren't Z or nat are ignored, some manual "unfold" are still mandatory if expanding these definitions will help omega. --- plugins/omega/coq_omega.ml | 40 +++++++++++++++++++++++++++++++--------- 1 file changed, 31 insertions(+), 9 deletions(-) (limited to 'plugins/omega') diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ae1a563be..ff69ddefb 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -50,6 +50,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 ? *) @@ -100,6 +101,14 @@ let _ = 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), @@ -376,16 +385,15 @@ 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 (Lazy.force 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 (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 = mkApp (Lazy.force coq_eq, - [| Lazy.force coq_comparison; t1; t2 |]) +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 = @@ -1778,11 +1786,25 @@ let destructure_hyps = let type_of = Tacmach.New.pf_unsafe_type_of gl in let decidability = decidability gl in let pf_nf = pf_nf gl in - let rec loop = function - | [] -> (tclTHEN nat_inject coq_omega) - | decl::lit -> - let i = NamedDecl.get_id decl in - Proofview.tclEVARMAP >>= fun sigma -> + 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 sigma (pf_nf 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 -- cgit v1.2.3