Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_division_equations

4 files changed, 127 insertions, 22 deletions

diff --git a/CHANGES.md b/CHANGES.md
index cacf0e09e4..54acb610bb 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -75,10 +75,13 @@ Tactics
   foo : database`). When the database name is omitted, the hint is added to the
   core database (as previously), but a deprecation warning is emitted.
 
-- There is now a tactic in `PreOmega.v` called `Z.div_mod_to_quot_rem`
-  which allows `lia`, `nia`, `romega`, etc to support `Z.div` and
-  `Z.modulo`, by posing the specifying equation for `Z.div` and
-  `Z.modulo` before replacing them with atoms.
+- There are now tactics in `PreOmega.v` called
+  `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and
+  `Z.to_euclidean_division_equations` (which combines the `div_mod`
+  and `quot_rem` variants) which allow `lia`, `nia`, `romega`, etc to
+  support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively),
+  by posing the specifying equation for `Z.div` and `Z.modulo` before
+  replacing them with atoms.
 
 Vernacular commands
 
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 2ace8a59e1..b076aac1ed 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -250,8 +250,16 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 
 .. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with
   the ``zify`` tactic.
-.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by pre-processing the goal with
-  the ``Z.div_mod_to_quot_rem`` tactic after manually running ``zify``.
+.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by
+  pre-processing the goal with the ``Z.div_mod_to_equations`` tactic (you may
+  need to manually run ``zify`` first).
+.. [#] Support for :g:`Z.quot` and :g:`Z.rem` may be obtained by pre-processing
+  the goal with the ``Z.quot_rem_to_equations`` tactic (you may need to manually
+  run ``zify`` first).
+.. [#] Note that support for :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and
+  :g:`Z.rem` may be simultaneously obtained by pre-processing the goal with the
+  ``Z.to_euclidean_division_equations`` tactic (you may need to manually run
+  ``zify`` first).
 .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#] Variants deal with equalities and strict inequalities.
 .. [#] In practice, the oracle might fail to produce such a refutation.
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 7ebc2fb04f..695f000cb1 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -12,12 +12,15 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat.
 
 Local Open Scope Z_scope.
 
-(** * [Z.div_mod_to_quot_rem]: the tactic for preprocessing [Z.div] and [Z.modulo] *)
+(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *)
 
-(** This tactic uses the complete specification of [Z.div] and
-    [Z.modulo] to remove these functions from the goal without losing
-    information.  The [Z.div_mod_to_quot_rem_cleanup] tactic removes
-    needless hypotheses, which makes tactics like [nia] run faster. *)
+(** These tactic use the complete specification of [Z.div] and
+    [Z.modulo] ([Z.quot] and [Z.rem], respectively) to remove these
+    functions from the goal without losing information.  The
+    [Z.euclidean_division_equations_cleanup] tactic removes needless
+    hypotheses, which makes tactics like [nia] run faster.  The tactic
+    [Z.to_euclidean_division_equations] combines the handling of both variants
+    of division/quotient and modulo/remainder. *)
 
 Module Z.
   Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0.
@@ -25,7 +28,21 @@ Module Z.
   Lemma div_0_r_ext x y : y = 0 -> x / y = 0.
   Proof. intro; subst; destruct x; reflexivity. Qed.
 
-  Ltac div_mod_to_quot_rem_generalize x y :=
+  Lemma rem_0_r_ext x y : y = 0 -> Z.rem x y = x.
+  Proof. intro; subst; destruct x; reflexivity. Qed.
+  Lemma quot_0_r_ext x y : y = 0 -> Z.quot x y = 0.
+  Proof. intro; subst; destruct x; reflexivity. Qed.
+
+  Lemma rem_bound_pos_pos x y : 0 < y -> 0 <= x -> 0 <= Z.rem x y < y.
+  Proof. intros; apply Z.rem_bound_pos; assumption. Qed.
+  Lemma rem_bound_neg_pos x y : y < 0 -> 0 <= x -> 0 <= Z.rem x y < -y.
+  Proof. rewrite <- Z.rem_opp_r'; intros; apply Z.rem_bound_pos; rewrite ?Z.opp_pos_neg; assumption. Qed.
+  Lemma rem_bound_pos_neg x y : 0 < y -> x <= 0 -> -y < Z.rem x y <= 0.
+  Proof. rewrite <- (Z.opp_involutive x), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg; apply rem_bound_pos_pos. Qed.
+  Lemma rem_bound_neg_neg x y : y < 0 -> x <= 0 -> y < Z.rem x y <= 0.
+  Proof. rewrite <- (Z.opp_involutive x), <- (Z.opp_involutive y), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg, Z.opp_involutive; apply rem_bound_neg_pos. Qed.
+
+  Ltac div_mod_to_equations_generalize x y :=
     pose proof (Z.div_mod x y);
     pose proof (Z.mod_pos_bound x y);
     pose proof (Z.mod_neg_bound x y);
@@ -36,23 +53,78 @@ Module Z.
     set (q := x / y) in *;
     set (r := x mod y) in *;
     clearbody q r.
-  Ltac div_mod_to_quot_rem_step :=
+  Ltac quot_rem_to_equations_generalize x y :=
+    pose proof (Z.quot_rem' x y);
+    pose proof (rem_bound_pos_pos x y);
+    pose proof (rem_bound_pos_neg x y);
+    pose proof (rem_bound_neg_pos x y);
+    pose proof (rem_bound_neg_neg x y);
+    pose proof (quot_0_r_ext x y);
+    pose proof (rem_0_r_ext x y);
+    let q := fresh "q" in
+    let r := fresh "r" in
+    set (q := Z.quot x y) in *;
+    set (r := Z.rem x y) in *;
+    clearbody q r.
+
+  Ltac div_mod_to_equations_step :=
     match goal with
-    | [ |- context[?x / ?y] ] => div_mod_to_quot_rem_generalize x y
-    | [ |- context[?x mod ?y] ] => div_mod_to_quot_rem_generalize x y
-    | [ H : context[?x / ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
-    | [ H : context[?x mod ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
+    | [ |- context[?x / ?y] ] => div_mod_to_equations_generalize x y
+    | [ |- context[?x mod ?y] ] => div_mod_to_equations_generalize x y
+    | [ H : context[?x / ?y] |- _ ] => div_mod_to_equations_generalize x y
+    | [ H : context[?x mod ?y] |- _ ] => div_mod_to_equations_generalize x y
     end.
-  Ltac div_mod_to_quot_rem' := repeat div_mod_to_quot_rem_step.
-  Ltac div_mod_to_quot_rem_cleanup :=
+  Ltac quot_rem_to_equations_step :=
+    match goal with
+    | [ |- context[Z.quot ?x ?y] ] => quot_rem_to_equations_generalize x y
+    | [ |- context[Z.rem ?x ?y] ] => quot_rem_to_equations_generalize x y
+    | [ H : context[Z.quot ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y
+    | [ H : context[Z.rem ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y
+    end.
+  Ltac div_mod_to_equations' := repeat div_mod_to_equations_step.
+  Ltac quot_rem_to_equations' := repeat quot_rem_to_equations_step.
+  Ltac euclidean_division_equations_cleanup :=
     repeat match goal with
+           | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
+           | [ H : ?x <> ?x -> _ |- _ ] => clear H
+           | [ H : ?x < ?x -> _ |- _ ] => clear H
            | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
            | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
            | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
+           | [ H : ?A -> ?x = ?x -> _ |- _ ] => specialize (fun a => H a eq_refl)
+           | [ H : ?A -> ?x <> ?x -> _ |- _ ] => clear H
+           | [ H : ?A -> ?x < ?x -> _ |- _ ] => clear H
+           | [ H : ?A -> ?B -> _, H' : ?B |- _ ] => specialize (fun a => H a H')
+           | [ H : ?A -> ?B -> _, H' : ~?B |- _ ] => clear H
+           | [ H : ?A -> ~?B -> _, H' : ?B |- _ ] => clear H
            | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
            | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
+           | [ H : ?A -> 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
+           | [ H : ?A -> ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
+           | [ H : 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
+           | [ H : ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
+           | [ H : ?A -> 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
+           | [ H : ?A -> ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
+           | [ H : 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
+           | [ H : ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
+           | [ H : ?A -> 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
+           | [ H : ?A -> ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
+           | [ H : 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x (eq_sym pf)))
+           | [ H : ?A -> 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl 0 x (eq_sym pf)))
+           | [ H : ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x pf))
+           | [ H : ?A -> ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl x 0 pf))
+           | [ H : ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
+           | [ H : ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
+           | [ H : ?A -> ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
+           | [ H : ?A -> ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
+           | [ H : ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
+           | [ H : ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
+           | [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
+           | [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
            end.
-  Ltac div_mod_to_quot_rem := div_mod_to_quot_rem'; div_mod_to_quot_rem_cleanup.
+  Ltac div_mod_to_equations := div_mod_to_equations'; euclidean_division_equations_cleanup.
+  Ltac quot_rem_to_equations := quot_rem_to_equations'; euclidean_division_equations_cleanup.
+  Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup.
 End Z.
 
 (** * zify: the Z-ification tactic *)
@@ -453,6 +525,24 @@ Ltac zify_N_op :=
   | |- context [ Z.of_N  (N.mul ?a ?b) ] =>
         pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in *
 
+  (* N.div -> Z.div and a positivity hypothesis *)
+  | H : context [ Z.of_N (N.div ?a ?b) ] |- _ =>
+        pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in *
+  | |- context [ Z.of_N  (N.div ?a ?b) ] =>
+        pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in *
+
+  (* N.modulo -> Z.rem / Z.modulo and a positivity hypothesis (N.modulo agrees with Z.modulo on everything except 0; so we pose both the non-zero proof for this agreement, but also replace things with [Z.rem]) *)
+  | H : context [ Z.of_N (N.modulo ?a ?b) ] |- _ =>
+    pose proof (N2Z.is_nonneg (N.modulo a b));
+    pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+    pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+    rewrite (N2Z.inj_rem a b) in *
+  | |- context [ Z.of_N  (N.div ?a ?b) ] =>
+    pose proof (N2Z.is_nonneg (N.modulo a b));
+    pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+    pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+    rewrite (N2Z.inj_rem a b) in *
+
   (* atoms of type N : we add a positivity condition (if not already there) *)
   | _ : 0 <= Z.of_N ?a |- _ => hide_Z_of_N a
   | _ : context [ Z.of_N ?a ] |- _ => pose proof (N2Z.is_nonneg a); hide_Z_of_N a
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index 6cb645d9eb..15028a4c00 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -2,9 +2,9 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 Open Scope Z_scope.
 
-(** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this
+(** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this
     file. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.to_euclidean_division_equations.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
@@ -22,6 +22,10 @@ Ltac saturate_mod_div :=
          | [ H : context[?x mod ?y] |- _ ] => unique_pose_proof (Z_zerop_or (x / y))
          | [ |- context[?x / ?y] ] => unique_pose_proof (Z_zerop_or y)
          | [ H : context[?x / ?y] |- _ ] => unique_pose_proof (Z_zerop_or y)
+         | [ |- context[Z.rem ?x ?y] ] => unique_pose_proof (Z_zerop_or (Z.quot x y))
+         | [ H : context[Z.rem ?x ?y] |- _ ] => unique_pose_proof (Z_zerop_or (Z.quot x y))
+         | [ |- context[Z.quot ?x ?y] ] => unique_pose_proof (Z_zerop_or y)
+         | [ H : context[Z.quot ?x ?y] |- _ ] => unique_pose_proof (Z_zerop_or y)
          end.
 
 Ltac t := intros; saturate_mod_div; try nia.