From 1b09c7b0802c85ea72931720a7cb4fbf9ab5e211 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 8 Jul 2017 11:19:13 +0200 Subject: Using is_conv rather than eq_constr to find `nat` or `Z` in omega. Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717. --- plugins/omega/coq_omega.ml | 54 +++++++++++++++++++++---------------------- test-suite/bugs/closed/4717.v | 35 ++++++++++++++++++++++++++++ test-suite/bugs/opened/4717.v | 19 --------------- 3 files changed, 62 insertions(+), 46 deletions(-) create mode 100644 test-suite/bugs/closed/4717.v delete mode 100644 test-suite/bugs/opened/4717.v 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.*) -- cgit v1.2.3 From 446b265f5d1f6e6828a7f653b1f648ebdf768321 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 13 Jul 2017 12:21:37 +0200 Subject: Recognizing Z in romega up to conversion. --- plugins/romega/const_omega.ml | 12 ++++-------- test-suite/bugs/closed/4717.v | 4 +++- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 5397b0065..7956be58b 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -198,6 +198,7 @@ let parse_logic_rel c = match destructurate c with (* Binary numbers *) +let coq_Z = lazy (bin_constant "Z") let coq_xH = lazy (bin_constant "xH") let coq_xO = lazy (bin_constant "xO") let coq_xI = lazy (bin_constant "xI") @@ -238,7 +239,7 @@ end module Z : Int = struct -let typ = lazy (bin_constant "Z") +let typ = coq_Z let plus = lazy (z_constant "Z.add") let mult = lazy (z_constant "Z.mul") let opp = lazy (z_constant "Z.opp") @@ -286,14 +287,9 @@ let parse_term t = (match recognize_Z t with Some t -> Tnum t | None -> Tother) | _ -> Tother -let pf_nf gl c = - EConstr.Unsafe.to_constr - (Tacmach.New.pf_apply Tacred.simpl gl (EConstr.of_constr c)) - let is_int_typ gl t = - match destructurate (pf_nf gl t) with - | Kapp("Z",[]) -> true - | _ -> false + Tacmach.New.pf_apply Reductionops.is_conv gl + (EConstr.of_constr t) (EConstr.of_constr (Lazy.force coq_Z)) let parse_rel gl t = match destructurate t with diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v index 4562ed1f1..1507fa4bf 100644 --- a/test-suite/bugs/closed/4717.v +++ b/test-suite/bugs/closed/4717.v @@ -19,7 +19,7 @@ Proof. omega. Qed. -Require Import ZArith. +Require Import ZArith ROmega. Open Scope Z_scope. @@ -32,4 +32,6 @@ Theorem Zle_not_eq_lt : forall n m, Proof. intros. omega. + Undo. + romega. Qed. -- cgit v1.2.3 From c5f9e3a03c1f089253622ec262adf931e6dc1ca2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 21 Nov 2017 15:00:38 +0100 Subject: Adding ad hoc overlay for sf/vfa. --- dev/ci/ci-sf.sh | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 272041205..217540cc1 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -14,6 +14,25 @@ tar xvfz vfa.tgz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v +# Delete useless calls to try omega; unfold +patch vfa/SearchTree.v < j) -> ~ (i < j) -> i=j. + Proof. + intros. +- try omega. (* Oops! [omega] cannot solve this one. +- The problem is that [i] and [j] have type [key] instead of type [nat]. +- The solution is easy enough: *) +- unfold key in *. + omega. + + (** So, if you get stuck on an [omega] that ought to work, +--- 674,679 ---- +EOF + ( cd lf && make clean && make ) ( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make ) -- cgit v1.2.3