From b26b781992f11fa77b3be9345f6d77cfb190b76e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 13 Feb 2025 21:43:38 -0800
Subject: [PATCH] feat: simprocs for `Int` and `Nat` divides predicates (#7078)

This PR implements simprocs for `Int` and `Nat` divides predicates.
---
 src/Init/Data/Int/DivModLemmas.lean               | 11 +++++++++++
 src/Init/Data/Nat/Dvd.lean                        |  9 +++++++++
 .../Meta/Tactic/Simp/BuiltinSimprocs/Int.lean     | 10 ++++++++++
 .../Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean     | 10 ++++++++++
 tests/lean/run/dvd_simproc.lean                   | 15 +++++++++++++++
 5 files changed, 55 insertions(+)
 create mode 100644 tests/lean/run/dvd_simproc.lean

diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index 64102471c7..6c880e6ec8 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -1347,3 +1347,14 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
 theorem bmod_neg_bmod : bmod (-(bmod x n)) n = bmod (-x) n := by
   apply (bmod_add_cancel_right x).mp
   rw [Int.add_left_neg, ← add_bmod_bmod, Int.add_left_neg]
+
+/-! Helper theorems for `dvd` simproc -/
+
+protected theorem dvd_eq_true_of_mod_eq_zero {a b : Int} (h : b % a == 0) : (a ∣ b) = True := by
+  simp [Int.dvd_of_emod_eq_zero, eq_of_beq h]
+
+protected theorem dvd_eq_false_of_mod_ne_zero {a b : Int} (h : b % a != 0) : (a ∣ b) = False := by
+  simp [eq_of_beq] at h
+  simp [Int.dvd_iff_emod_eq_zero, h]
+
+end Int
diff --git a/src/Init/Data/Nat/Dvd.lean b/src/Init/Data/Nat/Dvd.lean
index 3a58c1b544..c29559b589 100644
--- a/src/Init/Data/Nat/Dvd.lean
+++ b/src/Init/Data/Nat/Dvd.lean
@@ -129,4 +129,13 @@ protected theorem mul_div_assoc (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k
     have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
     rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]
 
+/-! Helper theorems for `dvd` simproc -/
+
+protected theorem dvd_eq_true_of_mod_eq_zero {m n : Nat} (h : n % m == 0) : (m ∣ n) = True := by
+  simp [Nat.dvd_of_mod_eq_zero, eq_of_beq h]
+
+protected theorem dvd_eq_false_of_mod_ne_zero {m n : Nat} (h : n % m != 0) : (m ∣ n) = False := by
+  simp [eq_of_beq] at h
+  simp [dvd_iff_mod_eq_zero, h]
+
 end Nat
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
index 33ee83ecba..7f11a06301 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
@@ -108,4 +108,14 @@ builtin_dsimproc [simp, seval] reduceOfNat (Int.ofNat _) := fun e => do
   let some a ← getNatValue? a | return .continue
   return .done <| toExpr (Int.ofNat a)
 
+builtin_simproc [simp, seval] reduceDvd ((_ : Int) ∣ _) := fun e => do
+  let_expr Dvd.dvd _ i a b ← e | return .continue
+  unless ← matchesInstance i (mkConst ``instDvd) do return .continue
+  let some va ← fromExpr? a | return .continue
+  let some vb ← fromExpr? b | return .continue
+  if vb % va == 0 then
+    return .done { expr := mkConst ``True, proof? := mkApp3 (mkConst ``Int.dvd_eq_true_of_mod_eq_zero) a b reflBoolTrue}
+  else
+    return .done { expr := mkConst ``False, proof? := mkApp3 (mkConst ``Int.dvd_eq_false_of_mod_ne_zero) a b reflBoolTrue}
+
 end Int
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
index 47651cd617..0e3ee00756 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
@@ -345,4 +345,14 @@ builtin_simproc [simp, seval] reduceSubDiff ((_ - _ : Nat)) := fun e => do
       let geProof ← mkOfDecideEqTrue (mkGENat po no)
       applySimprocConst finExpr ``Nat.Simproc.add_sub_add_ge #[pb, nb, po, no, geProof]
 
+builtin_simproc [simp, seval] reduceDvd ((_ : Nat) ∣ _) := fun e => do
+  let_expr Dvd.dvd _ i a b ← e | return .continue
+  unless ← matchesInstance i (mkConst ``instDvd) do return .continue
+  let some va ← fromExpr? a | return .continue
+  let some vb ← fromExpr? b | return .continue
+  if vb % va == 0 then
+    return .done { expr := mkConst ``True, proof? := mkApp3 (mkConst ``Nat.dvd_eq_true_of_mod_eq_zero) a b reflBoolTrue}
+  else
+    return .done { expr := mkConst ``False, proof? := mkApp3 (mkConst ``Nat.dvd_eq_false_of_mod_ne_zero) a b reflBoolTrue}
+
 end Nat
diff --git a/tests/lean/run/dvd_simproc.lean b/tests/lean/run/dvd_simproc.lean
new file mode 100644
index 0000000000..cc37557bdf
--- /dev/null
+++ b/tests/lean/run/dvd_simproc.lean
@@ -0,0 +1,15 @@
+example : 2 ∣ 6 := by simp
+example : 2 ∣ 0 := by simp
+example : 3 ∣ 6 := by simp
+example : ¬ 5 ∣ 6 := by simp
+example : ¬ 6 ∣ 11 := by simp
+example : ¬ 0 ∣ 6 := by simp
+example : 1 ∣ 6 := by simp
+
+example : (2:Int) ∣ 0 := by simp
+example : (2:Int) ∣ 6 := by simp
+example : (3:Int) ∣ 6 := by simp
+example : ¬ (5:Int) ∣ 6 := by simp
+example : ¬ (6:Int) ∣ 11 := by simp
+example : ¬ (0:Int) ∣ 6 := by simp
+example : (1:Int) ∣ 6 := by simp