feat: new Int operations in grind (#11656)

This PR adds support for `Int.sign`, `Int.fdiv`, `Int.tdiv`, `Int.fmod`,
`Int.tmod`, and `Int.bmod` to `grind`. These operations are just
preprocessed away. We assume that they are not very common in practice.
Examples:
```lean
example {x y : Int} : y = 0 → (x.fdiv y) = 0 := by grind
example {x y : Int} : y = 0 → (x.tdiv y) = 0 := by grind
example {x y : Int} : y = 0 → (x.fmod y) = x := by grind
example {x y : Int} : y = 1 → (x.fdiv (2 - y)) = x := by grind
example {x : Int} : x > 0 → x.sign = 1 := by grind
example {x : Int} : x < 0 → x.sign = -1 := by grind
example {x y : Int} : x.sign = 0 → x*y = 0 := by grind
```

See #11622

src/Init/Grind/Norm.lean

@@ -152,6 +152,12 @@ theorem smul_int_eq_mul {α} [Ring α] (i : Int) (a : α) : i • a = Int.cast i
 theorem Int.subNatNat_eq (a b : Nat) : Int.subNatNat a b = NatCast.natCast a - NatCast.natCast b := by
   apply Int.subNatNat_eq_coe
 
+theorem Int.sign_eq (x : Int) : x.sign = if x > 0 then 1 else if x < 0 then -1 else 0 := by
+  split; simp [*]
+  split; simp [*]
+  have : x = 0 := by omega
+  simp [*]
+
 -- Remark: for additional `grind` simprocs, check `Lean/Meta/Tactic/Grind`
 init_grind_norm
   /- Pre theorems -/
@@ -197,6 +203,11 @@ init_grind_norm
   Int.Linear.sub_fold Int.Linear.neg_fold
   -- Int divides
   Int.one_dvd Int.zero_dvd
+  -- Int alternative div and mod. We just expand them
+  Int.fdiv_eq_ediv Int.tdiv_eq_ediv
+  Int.fmod_eq_emod Int.tmod_eq_emod Int.bmod_eq_emod
+  -- Int sign. We just expand it
+  Int.sign_eq
   -- Function composition
   Function.const_apply Function.comp_apply Function.const_comp
   Function.comp_const Function.true_comp Function.false_comp

tests/lean/run/grind_11622.lean

@@ -0,0 +1,7 @@
+example {x y : Int} : y = 0 → (x.fdiv y) = 0 := by grind
+example {x y : Int} : y = 0 → (x.tdiv y) = 0 := by grind
+example {x y : Int} : y = 0 → (x.fmod y) = x := by grind
+example {x y : Int} : y = 1 → (x.fdiv (2 - y)) = x := by grind
+example {x : Int} : x > 0 → x.sign = 1 := by grind
+example {x : Int} : x < 0 → x.sign = -1 := by grind
+example {x y : Int} : x.sign = 0 → x*y = 0 := by grind

tests/lean/run/grind_bitvec2.lean

@@ -291,7 +291,13 @@ theorem sub_sub_toNat_cancel {x : BitVec w} :
 theorem sub_add_bmod_cancel {x y : BitVec w} :
     ((((2 ^ w : Nat) - y.toNat) : Int) + x.toNat).bmod (2 ^ w) =
       ((x.toNat : Int) - y.toNat).bmod (2 ^ w) := by
-  grind [=_ Int.add_bmod_right] -- TODO: teach `grind` about Int.bmod
+  /-
+  **Note**: This is a goal containing nonlinear integer arithmetic.
+  This is not in `grind`s scope. The following command used to work
+  before we expanded `Int.bmod` into `Int.emod`.
+  -/
+  -- grind [=_ Int.add_bmod_right]
+  sorry
 
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_right (by trivial : 0 < 2) le)