Add Z.divideb and Bool.reflect for Z.divide (mit-plv#1473)

* Add `Z.divideb` and `Bool.reflect` for `Z.divide`

* Add Z.mod_div_mod_full and Z.mod_divide_full

* Add `Z.rewrite_mod_divide`

src/Util/Notations.v

@@ -196,3 +196,5 @@ Reserved Notation "### x" (at level 9, x at level 9, format "### x").
 Reserved Notation "#### x" (at level 9, x at level 9, format "#### x").
 Reserved Notation "##### x" (at level 9, x at level 9, format "##### x").
 Reserved Notation "\ x .. y , t" (at level 200, x binder, y binder, right associativity, format "\  x .. y , '//' t").
+(** If we use "( x |? y )", it conflicts with things like [destruct x as [?|?]; ...] *)
+Reserved Notation "( x | ? y )" (format "(  x  | ?  y  )").

src/Util/ZUtil.v

@@ -9,6 +9,7 @@ Require Crypto.Util.ZUtil.DistrIf.
 Require Crypto.Util.ZUtil.Div.
 Require Crypto.Util.ZUtil.Div.Bootstrap.
 Require Crypto.Util.ZUtil.Divide.
+Require Crypto.Util.ZUtil.Divide.Bool.
 Require Crypto.Util.ZUtil.EquivModulo.
 Require Crypto.Util.ZUtil.Ge.
 Require Crypto.Util.ZUtil.Hints.
@@ -57,6 +58,7 @@ Require Crypto.Util.ZUtil.Tactics.PullPush.
 Require Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
 Require Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Crypto.Util.ZUtil.Tactics.RewriteModDivide.
 Require Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe.
 Require Crypto.Util.ZUtil.Tactics.SplitMinMax.
 Require Crypto.Util.ZUtil.Tactics.ZeroBounds.

src/Util/ZUtil/Definitions.v

@@ -5,6 +5,11 @@ Require Import Crypto.Util.LetIn.
 Local Open Scope Z_scope.
 
 Module Z.
+  Definition divideb (x y : Z) : bool
+    := if x =? 0
+       then y =? 0
+       else y mod x =? 0.
+
   Definition pow2_mod n i := (n &' (Z.ones i)).
 
   Definition zselect (cond zero_case nonzero_case : Z) :=
@@ -119,7 +124,7 @@ Module Z.
 
   (** Special identity function for constant-time cmov *)
   Definition value_barrier (x : Z) := x.
-  
+
   (* arithmetic right shift *)
   Definition arithmetic_shiftr1 (m a : Z) :=
     (a &' 2^(m - 1)) |' (a >> 1).
@@ -138,7 +143,7 @@ Module Z.
           q |' (a >> k).
 
   (** Note that the following definition may be inconvenient to reason about,
-      and [(a + 2^(m-1)) mod 2^m - 2^(m-1)] may prove simpler to reason about arithmetically. 
+      and [(a + 2^(m-1)) mod 2^m - 2^(m-1)] may prove simpler to reason about arithmetically.
       See also https://github.com/mit-plv/coqutil/blob/c8006ceca816076b117c31d7feaefb5bbb850754/src/coqutil/Word/Naive.v#L15
       and https://github.com/mit-plv/coqutil/blob/c8006ceca816076b117c31d7feaefb5bbb850754/src/coqutil/Word/Properties.v#L190 *)
 
@@ -162,3 +167,7 @@ Module Z.
   Definition twos_complement_mul ma mb a b :=
     (sign_extend ma (ma + mb) a) * (sign_extend mb (ma + mb) b).
 End Z.
+
+Module Export Notations.
+  Notation "( x | ? y )" := (Z.divideb x y) : Z_scope.
+End Notations.

src/Util/ZUtil/Divide.v

@@ -4,6 +4,7 @@ Require Import Coq.micromega.Lia.
 Require Import Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.Div.
 Require Import Crypto.Util.ZUtil.Tactics.DivideExistsMul.
+Require Import Crypto.Util.Tactics.DestructHead.
 Local Open Scope Z_scope.
 
 Module Z.
@@ -40,4 +41,20 @@ Module Z.
     rewrite Z.pow_add_r by lia.
     apply Z.divide_factor_l.
   Qed.
+
+  Lemma mod_divide_full a b : (a mod b = 0) <-> (b | a).
+  Proof.
+    destruct (Z_zerop b); auto using Z.mod_divide; subst; [].
+    rewrite Zmod_0_r; cbv [Z.divide]; intuition (destruct_head'_ex; subst; try exists 0; lia).
+  Qed.
+
+  Lemma mod_div_mod_full a m n : (n | m) -> a mod n = (a mod m) mod n.
+  Proof.
+    intros (p,Hp); rewrite (Z_div_mod_eq_full a m) at 1.
+    rewrite Hp at 1.
+    destruct (Z_zerop n); subst; try now autorewrite with zsimplify_const.
+    rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add; auto.
+  Qed.
+  #[global]
+   Hint Rewrite <- mod_div_mod_full using assumption : zsimplify push_Zmod.
 End Z.

src/Util/ZUtil/Divide/Bool.v

@@ -0,0 +1,25 @@
+Require Import Coq.micromega.Lia.
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Bool.Reflect.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma divideb_divide x y : Z.divideb x y = true <-> Z.divide x y.
+  Proof.
+    cbv [Z.divideb].
+    pose proof (Z.mod_divide y x).
+    destruct (x =? 0) eqn:H'; intuition repeat (lia || reflect_hyps || subst || rewrite Z.eqb_eq || auto).
+    all: cbv [Z.divide] in *.
+    { exists 0; reflexivity. }
+    { destruct_head'_ex; lia. }
+  Qed.
+
+  #[global] Instance divideb_spec : reflect_rel Z.divide Z.divideb | 10.
+  Proof.
+    intros x y; pose proof (divideb_divide x y); destruct Z.divideb; constructor.
+    all: intuition congruence.
+  Qed.
+End Z.

src/Util/ZUtil/Tactics/RewriteModDivide.v

@@ -0,0 +1,21 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZUtil.Divide.
+Local Open Scope Z_scope.
+
+Module Z.
+  (** [rewrite_mod_divide] is a better version of [rewrite <- Z.mod_div_mod_full
+      by rewrite_mod_divide_solver]; it backtracks across occurences
+      that the solver fails to solve the side-conditions on. *)
+  Ltac rewrite_mod_divide_solver := assumption.
+  Ltac rewrite_mod_divide :=
+    repeat match goal with
+           | [ |- context[(?a mod ?m) mod ?n] ]
+             => rewrite <- (@Z.mod_div_mod_full a m n) by rewrite_mod_divide_solver
+           end.
+  Ltac rewrite_mod_divide_in_hyps :=
+    repeat match goal with
+           | [ H : context[(?a mod ?m) mod ?n] |- _ ]
+             => rewrite <- (@Z.mod_div_mod_full a m n) in H by rewrite_mod_divide_solver
+           end.
+  Ltac rewrite_mod_divide_in_all := repeat (rewrite_mod_divide || rewrite_mod_divide_in_hyps).
+End Z.