Solving linear congruences

DefinitionModular linear equation solver#✓fully proved

Given natural numbers \(a > 0\) and \(n > 0\) and an integer \(b\), the solver solves \(a x \equiv b \pmod{n}\) following CLRS. Let \(d = \gcd(a, n)\) and let \(y\) be the coefficient of \(a\) in the Bézout identity \(d = n u + a y\) computed by the extended Euclidean algorithm on \((n, a)\). If \(d \mid b\), it returns the array \([x_0, x_1, \dots, x_{d-1}]\), where \(x_i = \bigl((y \cdot (b / d)) \bmod n + i \cdot (n / d)\bigr) \bmod n\) and \(r \bmod n\) denotes the least nonnegative residue of \(r\); otherwise it returns the empty array.

Its cost is \(6s + 1 + 4 + 3d\) when \(d \mid b\) and \(6s + 1\) otherwise, where \(s\) is the number of times the Euclidean algorithm, started from \((r, r') = (n, a)\), replaces \((r, r')\) by \((r' \bmod r, r)\) before \(r\) becomes \(0\): six arithmetic operations per such step, one divisibility test, four setup operations and three operations per returned residue.

@[no_expose]
def modularLinearEquationSolver
    (a : Nat) (b : Int) (n : Nat) (_ha : 0 < a) (_hn : 0 < n) :
    TimeM Nat (Array Nat) :=
  let extended := countedXgcdAux n 1 0 a 0 1
  let d := extended.ret.1
  if (d : Int) ∣ b then
    let seed := (extended.ret.2.2 * (b / (d : Int))) % (n : Int)
    let stride := n / d
    let values := (List.range d).map (fun (i : Nat) =>
      ((seed + (i : Int) * (stride : Int)) % (n : Int)).toNat)
    ⟨values.toArray, extended.time + 1 + 4 + 3 * d⟩
  else
    ⟨#[], extended.time + 1⟩

Used by 6

Used byThe solver returns nothing exactly when \(\gcd(a, n) \nmid b\) · Number of residues returned by the solver · The solver returns exactly the solutions below \(n\) · The solver returns no repeated residues · Output of the modular linear equation solver · Cost bounds for the modular linear equation solver

TheoremOutput of the modular linear equation solver#✓fully proved

Let \(a > 0\) and \(n > 0\) be natural numbers, \(b\) an integer, \(d = \gcd(a, n)\), and \(y\) the coefficient of \(a\) in the Bézout identity \(d = n u + a y\) computed by the extended Euclidean algorithm on \((n, a)\). If \(d \mid b\), the list returned by the modular linear equation solver on \(a\), \(b\), \(n\) is \([x_0, x_1, \dots, x_{d-1}]\) with \(x_i = \bigl((y \cdot (b / d)) \bmod n + i \cdot (n / d)\bigr) \bmod n\), where \(r \bmod n\) denotes the least nonnegative residue of \(r\); otherwise it is the empty list.

theorem modularLinearEquationSolver_ret
    (a : Nat) (b : Int) (n : Nat) (ha : 0 < a) (hn : 0 < n) :
    (modularLinearEquationSolver a b n ha hn).ret.toList =
      if (Nat.gcd a n : Int) ∣ b then
        (List.range (Nat.gcd a n)).map (fun (i : Nat) =>
          (((Nat.gcdB n a * (b / (Nat.gcd a n : Int))) % (n : Int) +
            (i : Int) * ((n / Nat.gcd a n : Nat) : Int)) % (n : Int)).toNat)
      else []

Uses 1 · Used by 4

Statement usesModular linear equation solver

Used byThe solver returns nothing exactly when \(\gcd(a, n) \nmid b\) · Number of residues returned by the solver · The solver returns exactly the solutions below \(n\) · The solver returns no repeated residues

TheoremThe solver returns exactly the solutions below \(n\)#✓fully proved

Let \(a > 0\) and \(n > 0\) be natural numbers and \(b\) an integer. A natural number \(x\) occurs in the output of the modular linear equation solver on \(a\), \(b\), \(n\) if and only if \(x < n\) and \(a x \equiv b \pmod{n}\).

theorem modularLinearEquationSolver_mem_iff
    (a : Nat) (b : Int) (n : Nat) (ha : 0 < a) (hn : 0 < n) (x : Nat) :
    x ∈ (modularLinearEquationSolver a b n ha hn).ret.toList ↔
      x < n ∧ Int.ModEq (n : Int) ((a : Int) * (x : Int)) b

Uses 2

Statement usesModular linear equation solver

Proof usesOutput of the modular linear equation solver

TheoremThe solver returns no repeated residues#✓fully proved

For natural numbers \(a > 0\) and \(n > 0\) and an integer \(b\), the entries of the output of the modular linear equation solver on \(a\), \(b\), \(n\) are pairwise distinct.

theorem modularLinearEquationSolver_nodup
    (a : Nat) (b : Int) (n : Nat) (ha : 0 < a) (hn : 0 < n) :
    (modularLinearEquationSolver a b n ha hn).ret.toList.Nodup

Uses 2

Statement usesModular linear equation solver

Proof usesOutput of the modular linear equation solver

TheoremNumber of residues returned by the solver#✓fully proved

For natural numbers \(a > 0\) and \(n > 0\) and an integer \(b\), the output of the modular linear equation solver on \(a\), \(b\), \(n\) has \(\gcd(a, n)\) entries if \(\gcd(a, n)\) divides \(b\), and no entries otherwise.

theorem modularLinearEquationSolver_length
    (a : Nat) (b : Int) (n : Nat) (ha : 0 < a) (hn : 0 < n) :
    (modularLinearEquationSolver a b n ha hn).ret.size =
      if (Nat.gcd a n : Int) ∣ b then Nat.gcd a n else 0

Uses 2 · Used by 1

Statement usesModular linear equation solver

Proof usesOutput of the modular linear equation solver

Used byThe solver returns nothing exactly when \(\gcd(a, n) \nmid b\)

TheoremThe solver returns nothing exactly when \(\gcd(a, n) \nmid b\)#✓fully proved

For natural numbers \(a > 0\) and \(n > 0\) and an integer \(b\), the modular linear equation solver on \(a\), \(b\), \(n\) returns the empty array if and only if \(\gcd(a, n)\) does not divide \(b\).

theorem modularLinearEquationSolver_empty_iff
    (a : Nat) (b : Int) (n : Nat) (ha : 0 < a) (hn : 0 < n) :
    (modularLinearEquationSolver a b n ha hn).ret = #[] ↔
      ¬ ((Nat.gcd a n : Int) ∣ b)

Uses 3

Statement usesModular linear equation solver

Proof usesNumber of residues returned by the solver · Output of the modular linear equation solver

TheoremCost bounds for the modular linear equation solver#✓fully proved

Let \(a > 0\) and \(n > 0\) be natural numbers, \(b\) an integer and \(d = \gcd(a, n)\), and put \(c = 4 + 3d\) if \(d \mid b\) and \(c = 0\) otherwise. The cost \(T\) of the modular linear equation solver on \(a\), \(b\), \(n\) satisfies \(1 + c \le T \le 6(2 \lfloor \log_2 n \rfloor + 2) + 1 + c\).

The cost counts arithmetic events, so this is the \(O(\log n + \gcd(a, n))\) bound of the source.

theorem modularLinearEquationSolver_time_bounds
    (a : Nat) (b : Int) (n : Nat) (ha : 0 < a) (hn : 0 < n) :
    1 + (if (Nat.gcd a n : Int) ∣ b then 4 + 3 * Nat.gcd a n else 0)
      ≤ (modularLinearEquationSolver a b n ha hn).time ∧
    (modularLinearEquationSolver a b n ha hn).time
      ≤ 6 * (2 * Nat.log2 n + 2) + 1 +
        (if (Nat.gcd a n : Int) ∣ b then 4 + 3 * Nat.gcd a n else 0)

Uses 1

Statement usesModular linear equation solver

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.