diff options
-rw-r--r-- | CHANGES | 3 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 40 | ||||
-rw-r--r-- | test-suite/bugs/closed/148.v | 26 |
3 files changed, 60 insertions, 9 deletions
@@ -12,6 +12,9 @@ Tactics utility. The command "Set NativeCompute Profiling" enables profiling, and "Set NativeCompute Profile Filename" customizes the profile filename. +- The tactic "omega" is now aware of the bodies of context variables + such as "x := 5 : Z" (see bug #148). This could be disabled via + Unset Omega UseLocalDefs. Changes from 8.7+beta1 to 8.7.0 =============================== 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 diff --git a/test-suite/bugs/closed/148.v b/test-suite/bugs/closed/148.v new file mode 100644 index 000000000..6cafb9f0c --- /dev/null +++ b/test-suite/bugs/closed/148.v @@ -0,0 +1,26 @@ +(** Omega is now aware of the bodies of context variables + (of type Z or nat). *) + +Require Import ZArith Omega. +Open Scope Z. + +Goal let x := 3 in x = 3. +intros. +omega. +Qed. + +Open Scope nat. + +Goal let x := 2 in x = 2. +intros. +omega. +Qed. + +(** NB: this could be disabled for compatibility reasons *) + +Unset Omega UseLocalDefs. + +Goal let x := 4 in x = 4. +intros. +Fail omega. +Abort. |