Note: the rules in this file are not a homomorphism. Nat and Int are not homomorphism source types (they are not registered in getHomoSourceTypes): grind has builtin support for both in its cutsat solver, including the Nat to Int cast bridge, so there is no injection out of Nat or Int and none should be added. The rules here support the source types (BitVec, Fin, the fixed-width integer types), applied to the Nat and Int images their injections produce: shifts are normalized to arithmetic, testBit decomposes bitwise operations, and the %/bmod-cleanup rules remove the redundant modular wrappers introduced by the injections.

theorem Lean.Grind.Int.emod_mul_emod (m n k : Int) : m % n * k % n = m * k % n

theorem Lean.Grind.Int.mul_emod_emod (m n k : Int) : m * (n % k) % k = m * n % k

Support theorems for the builtin [grind hom] simproc that rewrites &&& with a literal mask of the form 1…10…0 over Nat. The simproc instantiates n and k from the mask, and the hypotheses are discharged by rfl (the kernel evaluates the powers). The results use %, /, and * by literals, which cutsat supports.

theorem Lean.Grind.Nat.and_eq_mod (x c m n : Nat) (h₁ : c = 2 ^ n - 1) (h₂ : m = 2 ^ n) : x &&& c = x % m

theorem Lean.Grind.Nat.ones_and_eq_mod (x c m n : Nat) (h₁ : c = 2 ^ n - 1) (h₂ : m = 2 ^ n) : c &&& x = x % m

theorem Lean.Grind.Nat.and_eq_div_mod_mul (x c p q k n : Nat) (h₁ : c = (2 ^ n - 1) * 2 ^ k) (h₂ : p = 2 ^ k) (h₃ : q = 2 ^ n) : x &&& c = x / p % q * p

theorem Lean.Grind.Nat.ones_zeros_and_eq_div_mod_mul (x c p q k n : Nat) (h₁ : c = (2 ^ n - 1) * 2 ^ k) (h₂ : p = 2 ^ k) (h₃ : q = 2 ^ n) : c &&& x = x / p % q * p

Support theorem for the builtin [grind hom] simproc that rewrites c * x % m with literals c, m, m / 2 < c < m into (m - c' * x % m) % m with c' = m - c, so that -k * a and -(k * a) over UIntN/BitVec get the same image. cutsat splits on the coefficient of a variable when it has to eliminate it exactly, so a coefficient close to the modulus is replaced by its small complement. The hypothesis is a ground equality between literals, discharged by rfl.

theorem Lean.Grind.Nat.mul_mod_eq_sub_mul_mod (x c c' m : Nat) (h : c + c' = m) : c * x % m = (m - c' * x % m) % m

theorem Lean.Grind.Nat.mul_mod_eq_sub_mul_mod' (x c c' m : Nat) (h : c + c' = m) : x * c % m = (m - c' * x % m) % m