aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/omega/coq_omega.ml54
-rw-r--r--test-suite/bugs/closed/4717.v35
-rw-r--r--test-suite/bugs/opened/4717.v19
3 files changed, 62 insertions, 46 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ff69ddefb..869284246 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -466,12 +466,14 @@ let destructurate_prop sigma t =
| Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal")
| _ -> Kufo
-let destructurate_type sigma t =
- let eq_constr c1 c2 = eq_constr sigma c1 c2 in
- let c, args = decompose_app sigma t in
+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 eq_constr c (Lazy.force coq_Z) -> Kapp (Z,args)
- | _, [] when eq_constr c (Lazy.force coq_nat) -> Kapp (Nat,args)
+ | _, [] 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 sigma t =
@@ -1459,17 +1461,13 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
else
(tactic,defs)
-let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c
-
-let destructure_omega gl tac_def (id,c) =
- let open Tacmach.New in
- let sigma = project gl in
+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 sigma c with
| Kapp(Eq,[typ;t1;t2])
- when begin match destructurate_type sigma (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 sigma
id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
@@ -1507,7 +1505,7 @@ let coq_omega =
Proofview.Goal.enter begin fun gl ->
clear_constr_tables ();
let hyps_types = Tacmach.New.pf_hyps_types gl in
- let destructure_omega = 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 =
@@ -1727,27 +1725,26 @@ let not_binop = function
exception Undecidable
-let rec decidability gl t =
- let open Tacmach.New in
- match destructurate_prop (project gl) 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 (project gl) (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
@@ -1784,15 +1781,16 @@ let onClearedName2 id tac =
let destructure_hyps =
Proofview.Goal.enter begin fun gl ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
- let decidability = decidability gl in
- let pf_nf = pf_nf 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 = 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
+ 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
@@ -1895,7 +1893,7 @@ let destructure_hyps =
with Not_found -> loop lit)
| Kapp(Eq,[typ;t1;t2]) ->
if !old_style_flag then begin
- match destructurate_type sigma (pf_nf typ) with
+ match destructurate_type env sigma typ with
| Kapp(Nat,_) ->
tclTHENLIST [
(simplest_elim
@@ -1912,7 +1910,7 @@ let destructure_hyps =
]
| _ -> loop lit
end else begin
- match destructurate_type sigma (pf_nf typ) with
+ match destructurate_type env sigma typ with
| Kapp(Nat,_) ->
(tclTHEN
(convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
@@ -1940,7 +1938,9 @@ let destructure_hyps =
let destructure_goal =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
- let decidability = 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 =
Proofview.tclEVARMAP >>= fun sigma ->
let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in
diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v
new file mode 100644
index 000000000..4562ed1f1
--- /dev/null
+++ b/test-suite/bugs/closed/4717.v
@@ -0,0 +1,35 @@
+(* Omega being smarter on recognizing nat and Z *)
+
+Require Import Omega.
+
+Definition nat' := nat.
+
+Theorem le_not_eq_lt : forall (n m:nat),
+ n <= m ->
+ n <> m :> nat' ->
+ n < m.
+Proof.
+ intros.
+ omega.
+Qed.
+
+Goal forall (x n : nat'), x = x + n - n.
+Proof.
+ intros.
+ omega.
+Qed.
+
+Require Import ZArith.
+
+Open Scope Z_scope.
+
+Definition Z' := Z.
+
+Theorem Zle_not_eq_lt : forall n m,
+ n <= m ->
+ n <> m :> Z' ->
+ n < m.
+Proof.
+ intros.
+ omega.
+Qed.
diff --git a/test-suite/bugs/opened/4717.v b/test-suite/bugs/opened/4717.v
deleted file mode 100644
index 9ad474672..000000000
--- a/test-suite/bugs/opened/4717.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(*See below. They sometimes work, and sometimes do not. Is this a bug?*)
-
-Require Import Omega Psatz.
-
-Definition foo := nat.
-
-Goal forall (n : foo), 0 = n - n.
-Proof. intros. omega. (* works *) Qed.
-
-Goal forall (x n : foo), x = x + n - n.
-Proof.
- intros.
- Fail omega. (* Omega can't solve this system *)
- Fail lia. (* Cannot find witness. *)
- unfold foo in *.
- omega. (* works *)
-Qed.
-
-(* Guillaume Melquiond: What matters is the equality. In the first case, it is @eq nat. In the second case, it is @eq foo. The same issue exists for ring and field. So it is not a bug, but it is worth fixing.*)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 11:02:03 +0000