Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion

5 files changed, 87 insertions, 54 deletions

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 <<EOF
+*** SearchTree.v.bak	2017-09-06 19:12:59.000000000 +0200
+--- SearchTree.v	2017-11-21 16:34:41.000000000 +0100
+***************
+*** 674,683 ****
+     forall i j : key, ~ (i > 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 )
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/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 32a1c07b2..337510ef1 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -197,6 +197,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")
@@ -237,7 +238,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")
@@ -285,14 +286,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
new file mode 100644
index 000000000..1507fa4bf
--- /dev/null
+++ b/test-suite/bugs/closed/4717.v
@@ -0,0 +1,37 @@
+(* 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 ROmega.
+
+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.
+  Undo.
+  romega.
+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.*)