feat: mark Nat power and divisibility theorems for grind (#11519)

This PR marks `Nat` power and divisibility theorems for `grind`. We use
the new `grind_pattern` constraints to control theorem instantiation.
Examples:

```lean
example {x m n : Nat} (h : x = 4 ^ (m + 1) * n) : x % 4 = 0 := by
  grind

example (a m n o p : Nat) : a ∣ n → a ∣ m * n * o * p := by
  grind

example {a b x m n : Nat}
    : n > 0 → x = b * 4^m * a → a = 9^n → m > 0 → x % 6 = 0 := by
  grind

example {a n : Nat}
    : m > 4 → a = 2^(m^n) → a % 2 = 0 := by
  grind
```

Closes #11515

Remark: We are adding support for installing extra theorems to `lia`
(aka `cutsat`). The example at #11515 can already be solved by `grind`
with this PR, but we still need to add the new theorems to the set for
`lia`.

cc @kim-em

Author: leodemoura

src/Init/Data/Nat/Dvd.lean

@@ -27,9 +27,15 @@ protected theorem dvd_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a
 protected theorem dvd_mul_left_of_dvd {a b : Nat} (h : a ∣ b) (c : Nat) : a ∣ c * b :=
   Nat.dvd_trans h (Nat.dvd_mul_left _ _)
 
+grind_pattern Nat.dvd_mul_left_of_dvd => a ∣ b, c * b where
+  guard a ∣ b
+
 protected theorem dvd_mul_right_of_dvd {a b : Nat} (h : a ∣ b) (c : Nat) : a ∣ b * c :=
   Nat.dvd_trans h (Nat.dvd_mul_right _ _)
 
+grind_pattern Nat.dvd_mul_right_of_dvd => a ∣ b, b * c where
+  guard a ∣ b
+
 protected theorem eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0 :=
   let ⟨c, H'⟩ := h; H'.trans c.zero_mul
 

src/Init/Data/Nat/Lemmas.lean

@@ -1086,6 +1086,17 @@ protected theorem pow_add (a m n : Nat) : a ^ (m + n) = a ^ m * a ^ n := by
   | zero => rw [Nat.add_zero, Nat.pow_zero, Nat.mul_one]
   | succ _ ih => rw [Nat.add_succ, Nat.pow_succ, Nat.pow_succ, ih, Nat.mul_assoc]
 
+theorem div_pow_of_pos (a n : Nat) : n > 0 → a ∣ a ^ n := by
+  cases n <;> simp [Nat.pow_add]
+  exact Nat.dvd_mul_left a (a ^ _)
+
+grind_pattern div_pow_of_pos => a ^ n where
+  is_value a
+  guard n > 0
+
+grind_pattern Nat.pow_pos => a ^ n where
+  guard a > 0
+
 protected theorem pow_add' (a m n : Nat) : a ^ (m + n) = a ^ n * a ^ m := by
   rw [← Nat.pow_add, Nat.add_comm]
 

tests/lean/run/grind_11515.lean

@@ -0,0 +1,66 @@
+example {x m n : Nat} (h : x = 4 ^ (m + 1) * n) : x % 4 = 0 := by
+  grind
+
+/--
+info: Try these:
+  [apply] grind only [usr Nat.div_pow_of_pos, usr Nat.dvd_mul_right_of_dvd]
+  [apply] grind =>
+    instantiate only [usr Nat.div_pow_of_pos]
+    instantiate only [usr Nat.dvd_mul_right_of_dvd]
+    lia
+-/
+#guard_msgs in
+example {x m n : Nat} (h : x = 4 ^ (m + 1) * n) : x % 4 = 0 := by
+  grind?
+
+example {x m n : Nat} (h : x = 4 ^ (m + 1) * n) : x % 4 = 0 := by
+  grind only [usr Nat.div_pow_of_pos, usr Nat.dvd_mul_right_of_dvd]
+
+example {x m n : Nat} (h : x = 4 ^ (m + 1) * n) : x % 4 = 0 := by
+  grind =>
+    instantiate only [usr Nat.div_pow_of_pos]
+    instantiate only [usr Nat.dvd_mul_right_of_dvd]
+    lia
+
+example {x m n : Nat} (h₁ : x = 4 ^ (m + 1) * n) : x % 4 = 0 := by
+  grind
+
+example {x m n : Nat} (h₁ : x = 4 ^ m * n) : m > 0 → x % 4 = 0 := by
+  grind
+
+example {x m n : Nat} (h₁ : x = n * 4 ^ (m + 1) * n) : x % 4 = 0 := by
+  grind
+
+example {a b x m n : Nat} (h₁ : x = b * a * 4 ^ (m + 1) * n) : x % 4 = 0 := by
+  grind
+
+example {a b x m n : Nat} (h₁ : x = b * 4 ^ m * a * 3 ^ n) : n > 0 → m > 0 → x % 12 = 0 := by
+  grind
+
+example {a b x m n : Nat} (h₁ : x = b * 4 ^ m * a * 3 ^ n) : n > 0 → m > 0 → x % 6 = 0 := by
+  grind
+
+example (m n : Nat) (h : 4 ∣ m) : 4 ∣ m * n := by
+  grind
+
+example (a m n : Nat) (h : a ∣ m) : a ∣ m * n := by
+  grind
+
+example (a m n o p : Nat) : a ∣ m → a ∣ m * n * o * p := by
+  grind
+
+example {a b x m n : Nat}
+    : x = b * 4 ^ m * a → a = 3^n → n > 0 → m > 0 → x % 12 = 0 := by
+  grind
+
+example {a b x m n : Nat}
+    : n > 0 → x = b * 4^m * a → a = 9^n → m > 0 → x % 6 = 0 := by
+  grind
+
+example {a n : Nat}
+    : a = 2^(3^n) → a % 2 = 0 := by
+  grind
+
+example {a n : Nat}
+    : m > 4 → a = 2^(m^n) → a % 2 = 0 := by
+  grind

tests/lean/run/grind_lint_bitvec.lean

@@ -7,11 +7,13 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 #guard_msgs in
 #grind_lint inspect (min := 30) BitVec.msb_replicate
 
+-- TODO: Reduce limit after we add support for `no_value` constraint
 -- `BitVec.msb_signExtend` is reasonable at 22.
 #guard_msgs in
-#grind_lint inspect (min := 25)  BitVec.msb_signExtend
+#grind_lint inspect (min := 26)  BitVec.msb_signExtend
 
 /-! Check BitVec namespace: -/
 
+-- TODO: Reduce limit after we add support for `no_value` constraint. It was `20`
 #guard_msgs in
-#grind_lint check (min := 20) in BitVec
+#grind_lint check (min := 23) in BitVec

tests/lean/run/grind_match_cond_issue.lean

@@ -1,13 +1,10 @@
 /--
 error: `grind` failed
-case grind.2.2.1.1
+case grind.1
 n m a : Nat
 ih : ∀ {a : Nat}, a ^ 2 = 4 ^ m * n → False
 h : a ^ 2 = 4 ^ (m + 1) * n
-h_1 : ¬4 * 4 ^ m = 4 ^ m
-h_2 : ¬4 * 4 ^ m = 4 ^ m
-h_3 : n = 4 ^ m
-h_4 : ↑a = 4
+h_1 : ↑a = 4
 ⊢ False
 -/
 #guard_msgs in