Merge PR coq#17927: add Z.divide support for Z.to_euclidean_division_…

…equations

Reviewed-by: JasonGross
Reviewed-by: jfehrle
Co-authored-by: JasonGross <[email protected]>

doc/changelog/04-tactics/17927-divide_to_euclidean_division_equations.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  When using :g:`Z.to_euclidean_division_equations`, you can now pose
+  equations of the form ``x = y * q`` using :g:`Z.divide`
+  (`#17927 <https://github.com/coq/coq/pull/17927>`_,
+  by Evgenii Kosogorov).

doc/sphinx/addendum/micromega.rst

@@ -366,10 +366,12 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    :tacn:`zify` can also be extended by rebinding the tactics `Zify.zify_pre_hook` and `Zify.zify_post_hook` that are
    respectively run in the first and the last steps of :tacn:`zify`.
 
+   + To support :g:`Z.divide`: ``Ltac Zify.zify_post_hook ::= Z.divide_to_equations``.
    + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``.
    + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``.
-   + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot` and :g:`Z.rem`: either ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations`` or ``Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true)``.
+   + To support :g:`Z.divide`, :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot` and :g:`Z.rem`: either ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations`` or ``Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true)``.
      The :g:`Z.to_euclidean_division_equations` tactic consists of the following passes:
+     - :g:`Z.divide_to_equations'`, posing characteristic equations using factors from :g:`Z.divide`
      - :g:`Z.div_mod_to_equations'`, posing characteristic equations for and generalizing over :g:`Z.div` and :g:`Z.modulo`
      - :g:`Z.quot_rem_to_equations'`, posing characteristic equations for and generalizing over :g:`Z.quot` and :g:`Z.rem`
      - :g:`Z.euclidean_division_equations_cleanup`, removing impossible hypotheses introduced by the above passes, such as those presupposing :g:`x <> x`

test-suite/success/Nia.v

@@ -409,6 +409,7 @@ Example Zdiv_unique: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> q = a /
 Example Z_div_unique_pos: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed.
 Example Z_div_small_iff: forall a b : Z, b <> 0 -> a / b = 0 <-> 0 <= a < b \/ b < a <= 0. Proof. intros; nia. Qed.
 Example Z_div_unique: forall a b q r : Z, 0 <= r < b \/ b < r <= 0 -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed.
+Example Z_divide_mod : forall a b : Z, (b | a) -> a mod b = 0. Proof. intros. nia. Qed.
 Example Z_mod_divide: forall a b : Z, b <> 0 -> a mod b = 0 <-> (b | a). Proof. split; intros. Fail all: nia. Abort.
 Example Zmod_divides: forall a b : Z, b <> 0 -> a mod b = 0 <-> (exists c : Z, a = b * c). Proof. split; intros. Fail all: nia. Abort.
 

theories/omega/PreOmega.v

@@ -48,6 +48,10 @@ Module Z.
   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.
 
+  (* Make the direction of [Z.divide] line up with the rest of the Euclidean equation facts *)
+  Local Lemma divide_alt x y : Z.divide x y -> exists z, y = x * z.
+  Proof. intros [z H]; exists z; subst; apply Z.mul_comm. Qed.
+
   Ltac div_mod_to_equations_generalize x y :=
     pose proof (Z.div_mod x y);
     pose proof (Z.mod_pos_bound x y);
@@ -87,8 +91,11 @@ Module Z.
     | [ 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 divide_to_equations_step :=
+    match goal with | [ H : Z.divide _ _ |- _ ] => apply divide_alt in H; destruct H end.
   Ltac div_mod_to_equations' := repeat div_mod_to_equations_step.
   Ltac quot_rem_to_equations' := repeat quot_rem_to_equations_step.
+  Ltac divide_to_equations' := repeat divide_to_equations_step.
   Ltac euclidean_division_equations_cleanup :=
     repeat match goal with
            | [ H : ?x = ?x -> ?Q |- _ ] => specialize (H eq_refl)
@@ -158,6 +165,7 @@ Module Z.
     repeat euclidean_division_equations_find_duplicate_quotients_step.
   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 divide_to_equations := divide_to_equations'; euclidean_division_equations_cleanup.
   Module euclidean_division_equations_flags.
     #[local] Set Primitive Projections.
     Record t :=
@@ -208,7 +216,7 @@ Module Z.
   End euclidean_division_equations_flags.
   Import euclidean_division_equations_flags (find_duplicate_quotients).
   Ltac to_euclidean_division_equations_with flags :=
-    div_mod_to_equations'; quot_rem_to_equations';
+    divide_to_equations'; div_mod_to_equations'; quot_rem_to_equations';
     euclidean_division_equations_cleanup;
     euclidean_division_equations_flags.guard_with find_duplicate_quotients flags euclidean_division_equations_find_duplicate_quotients.
   Ltac to_euclidean_division_equations :=