doc-next-gen

Init.Data.Nat.Mod

Module docstring

{"# Further results about mod.

This file proves some results about mod that are useful for bitblasting, in particular Nat.mod_mul : x % (a * b) = x % a + a * (x / a % b) and its corollary Nat.mod_pow_succ : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b).

It contains the necessary preliminary results relating order and * and /, which should probably be moved to their own file. "}

Nat.mul_lt_mul_left theorem
(a0 : 0 < a) : a * b < a * c ↔ b < c
Full source 
@[simp] protected theorem mul_lt_mul_left (a0 : 0 < a) : a * b < a * c ↔ b < c := by
  induction a with
  | zero => simp_all
  | succ a ih =>
    cases a
    · simp
    · simp_all [succ_eq_add_one, Nat.right_distrib]
      omega
Left Multiplication Preserves Strict Inequality in Natural Numbers
Informal description
For any natural numbers $a$, $b$, and $c$ with $0 < a$, the inequality $a \cdot b < a \cdot c$ holds if and only if $b < c$.
Nat.lt_of_mul_lt_mul_left theorem
{a b c : Nat} (h : a * b < a * c) : b < c
Full source 
protected theorem lt_of_mul_lt_mul_left {a b c : Nat} (h : a * b < a * c) : b < c := by
  cases a <;> simp_all
Left Multiplication Preserves Strict Inequality in Natural Numbers
Informal description
For any natural numbers $a$, $b$, and $c$, if $a \cdot b < a \cdot c$, then $b < c$.
Nat.lt_of_mul_lt_mul_right theorem
{a b c : Nat} (h : b * a < c * a) : b < c
Full source 
protected theorem lt_of_mul_lt_mul_right {a b c : Nat} (h : b * a < c * a) : b < c := by
  rw [Nat.mul_comm b a, Nat.mul_comm c a] at h
  exact Nat.lt_of_mul_lt_mul_left h
Right Multiplication Preserves Strict Inequality in Natural Numbers
Informal description
For any natural numbers $a$, $b$, and $c$, if $b \cdot a < c \cdot a$, then $b < c$.
Nat.div_lt_of_lt_mul theorem
{m n k : Nat} (h : m < n * k) : m / n < k
Full source 
protected theorem div_lt_of_lt_mul {m n k : Nat} (h : m < n * k) : m / n < k :=
  Nat.lt_of_mul_lt_mul_left <|
    calc
      n * (m / n) ≤ m % n + n * (m / n) := Nat.le_add_left _ _
      _ = m := mod_add_div _ _
      _ < n * k := h
Floor Division Bounded by Strict Inequality: $m / n < k$ when $m < n \cdot k$
Informal description
For any natural numbers $m, n, k$ such that $m < n \cdot k$, it holds that the floor division $m / n$ is strictly less than $k$.
Nat.mod_mul_right_div_self theorem
(m n k : Nat) : m % (n * k) / n = m / n % k
Full source 
theorem mod_mul_right_div_self (m n k : Nat) : m % (n * k) / n = m / n % k := by
  rcases Nat.eq_zero_or_pos n with (rfl | hn); simp [mod_zero]
  rcases Nat.eq_zero_or_pos k with (rfl | hk); simp [mod_zero]
  conv => rhs; rw [← mod_add_div m (n * k)]
  rw [Nat.mul_assoc, add_mul_div_left _ _ hn, add_mul_mod_self_left,
    mod_eq_of_lt (Nat.div_lt_of_lt_mul (mod_lt _ (Nat.mul_pos hn hk)))]
Modulo-Multiplication-Division Identity: $\frac{m \% (n \cdot k)}{n} = \left(\frac{m}{n}\right) \% k$
Informal description
For any natural numbers $m$, $n$, and $k$, the floor division of the remainder $m \% (n \cdot k)$ by $n$ equals the remainder of the floor division $m / n$ by $k$, i.e., \[ \frac{m \% (n \cdot k)}{n} = \left(\frac{m}{n}\right) \% k. \]
Nat.mod_mul_left_div_self theorem
(m n k : Nat) : m % (k * n) / n = m / n % k
Full source 
theorem mod_mul_left_div_self (m n k : Nat) : m % (k * n) / n = m / n % k := by
  rw [Nat.mul_comm k n, mod_mul_right_div_self]
Modulo-Multiplication-Division Identity: $\frac{m \% (k \cdot n)}{n} = \left(\frac{m}{n}\right) \% k$
Informal description
For any natural numbers $m$, $n$, and $k$, the floor division of the remainder $m \% (k \cdot n)$ by $n$ equals the remainder of the floor division $m / n$ by $k$, i.e., \[ \frac{m \% (k \cdot n)}{n} = \left(\frac{m}{n}\right) \% k. \]
Nat.mod_mul_right_mod theorem
(a b c : Nat) : a % (b * c) % b = a % b
Full source 
@[simp]
theorem mod_mul_right_mod (a b c : Nat) : a % (b * c) % b = a % b :=
  Nat.mod_mod_of_dvd a (Nat.dvd_mul_right b c)
Nested Modulo Identity: $(a \bmod (b \cdot c)) \bmod b = a \bmod b$
Informal description
For any natural numbers $a$, $b$, and $c$, the remainder of $a$ modulo $b \cdot c$ modulo $b$ equals the remainder of $a$ modulo $b$, i.e., $(a \bmod (b \cdot c)) \bmod b = a \bmod b$.
Nat.mod_mul_left_mod theorem
(a b c : Nat) : a % (b * c) % c = a % c
Full source 
@[simp]
theorem mod_mul_left_mod (a b c : Nat) : a % (b * c) % c = a % c :=
  Nat.mod_mod_of_dvd a (Nat.mul_comm _ _ ▸ Nat.dvd_mul_left c b)
Nested Modulo Identity: $(a \bmod (b \cdot c)) \bmod c = a \bmod c$
Informal description
For any natural numbers $a$, $b$, and $c$, the remainder of $a$ modulo $b \times c$ modulo $c$ equals the remainder of $a$ modulo $c$, i.e., $(a \bmod (b \cdot c)) \bmod c = a \bmod c$.
Nat.mod_mul theorem
{a b x : Nat} : x % (a * b) = x % a + a * (x / a % b)
Full source 
theorem mod_mul {a b x : Nat} : x % (a * b) = x % a + a * (x / a % b) := by
  rw [Nat.add_comm, ← Nat.div_add_mod (x % (a*b)) a, Nat.mod_mul_right_mod,
    Nat.mod_mul_right_div_self]
Modulo-Multiplication Decomposition: $x \% (a \cdot b) = x \% a + a \cdot \left( (x / a) \% b \right)$
Informal description
For any natural numbers $a$, $b$, and $x$, the remainder of $x$ modulo $a \cdot b$ can be expressed as: \[ x \% (a \cdot b) = x \% a + a \cdot \left( (x / a) \% b \right). \]
Nat.mod_pow_succ theorem
{x b k : Nat} : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b)
Full source 
theorem mod_pow_succ {x b k : Nat} :
    x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b) := by
  rw [Nat.pow_succ, Nat.mod_mul]
Modulo-Power Decomposition: $x \% b^{k+1} = x \% b^k + b^k \cdot \left( (x / b^k) \% b \right)$
Informal description
For any natural numbers $x$, $b$, and $k$, the remainder of $x$ modulo $b^{k+1}$ can be expressed as: \[ x \% b^{k+1} = x \% b^k + b^k \cdot \left( (x / b^k) \% b \right). \]
Nat.two_pow_mod_two_eq_zero theorem
{n : Nat} : 2 ^ n % 2 = 0 ↔ 0 < n
Full source 
@[simp] theorem two_pow_mod_two_eq_zero {n : Nat} : 2 ^ n % 2 = 0 ↔ 0 < n := by
  cases n <;> simp [Nat.pow_succ]
Power of Two Modulo Two Equals Zero if and only if Exponent is Positive
Informal description
For any natural number $n$, the remainder when $2^n$ is divided by $2$ is zero if and only if $n$ is positive, i.e., $2^n \mod 2 = 0 \leftrightarrow n > 0$.
Nat.two_pow_mod_two_eq_one theorem
{n : Nat} : 2 ^ n % 2 = 1 ↔ n = 0
Full source 
@[simp] theorem two_pow_mod_two_eq_one {n : Nat} : 2 ^ n % 2 = 1 ↔ n = 0 := by
  cases n <;> simp [Nat.pow_succ]
Power of Two Modulo Two Equals One if and only if Exponent is Zero
Informal description
For any natural number $n$, the remainder when $2^n$ is divided by $2$ is $1$ if and only if $n = 0$, i.e., $2^n \mod 2 = 1 \leftrightarrow n = 0$.