On the uniqueness of solutions to congruential equations

Stream: maths

[Move fast]

image.png

import Mathlib
open ZMod
/--6. Solve the simultaneous congruences
$$
\begin{aligned}

x & \equiv 1(\bmod 2) \\

x & \equiv 6(\bmod 7) \\

x & \equiv 2(\bmod 27) \\

x & \equiv 6(\bmod 11)

\end{aligned}
$$-/
-- Step 1 Function to compute the modular inverse of `a` modulo `m`
def modInverse (a m : Nat) : Option Nat :=
  let g := Nat.gcd a m
  if g = 1 then
    -- Use extended Euclidean algorithm to find the inverse
    let (x, _) := Nat.xgcd a m
    -- Ensure the result is a natural number in [0, m-1]
    some (Nat.mod (Int.toNat (x % m + m)) m)
  else
    none

-- Step 2 Function to solve the system of congruences using CRT
def solveCRT (moduli residues : List Nat) : Option Nat :=
  let M := moduli.prod
  -- Compute the solution using CRT
  let result := residues.zip moduli |>.foldlM (fun acc (r, m) =>
    let Mi := M / m
    match modInverse Mi m with
    | some yi =>
      -- Compute the term and ensure it remains a natural number
      let term := r * Mi * yi
      pure (acc + term)
    | none => none -- Modular inverse doesn't exist
  ) 0
  match result with
  | some x => some (x % M)
  | none => none

-- Step 3 Define the moduli and residues
def moduli : List Nat := [2, 7, 27, 11]
def residues : List Nat := [1, 6, 2, 6]

-- Step 4 Solve the system of congruences
def solution : Option Nat :=
  solveCRT moduli residues

-- Step 5 Print the special solution
#eval solution

-- Step 6 Check the condition of the CRT theorem
#eval (2 : Nat).Coprime 7
#eval (2 : Nat).Coprime 27
#eval (2 : Nat).Coprime 11
#eval (7 : Nat).Coprime 27
#eval (7 : Nat).Coprime 1
#eval (27 : Nat).Coprime 11
#eval 2*7*27*11
-- Thus by the CRT theorem, the unique soulution is $x \equiv 83 (\bmod M)$, where $M=2 × 7 × 27 × 11 = 4158$.

I hope to be able to show that (83: ZMod 4158) is the only solution of the above congruent equation in the congruent sense, and I do not know how to give a formal proof. Can someone help me?

[Michael Rothgang]

It seems you want to use the Chinese Remainder Theorem. Can you state that? (Or, if you're willing to use the mathlib version: what does it say?) Have you tried using that theorem?

[Michael Rothgang]

Or is your question rather "how do I prove a theorem" (as opposed to making a definition)?

[Michael Rothgang]

Perhaps, the first step: can you state the result you want to prove in Lean? You won't be able to prove it in Lean otherwise :-)

[Move fast]

I want to show that (83: ZMod 4158) is the only solution of the above congruent equation in the congruent sense, but I don't know how to use the Chinese Remainder Theorem in Mathlib.

[Move fast]

If you can give me a Lean's proof to solve the following question, maybe I will know how to prove the more complex situation.

\begin{aligned}

x & \equiv 1(\bmod 2) \\

x & \equiv 6(\bmod 7) \\

\end{aligned}

[Aaron Liu]

You still haven't stated the result yet :)

[Aaron Liu]

There are many ways to say this in Lean.

[Move fast]

The result is (83: ZMod 4158), that is to say $x \equiv 83 (\bmod 4158)$. I want to show that is the unique solution by the Chinese Remainder Theorem.

[Michał Mrugała]

I think Aaron is asking for a statement in Lean

[Move fast]

Maybe like (83: ZMod 4158), if we can get the result like this

[Aaron Liu]

Here are three ways to state this in Lean

import Mathlib

example (n : ZMod 4158) :
    ZMod.castHom (by decide : 2 ∣ 4158) (ZMod 2) n = 1 ∧
    ZMod.castHom (by decide : 7 ∣ 4158) (ZMod 7) n = 6 ∧
    ZMod.castHom (by decide : 27 ∣ 4158) (ZMod 27) n = 2 ∧
    ZMod.castHom (by decide : 11 ∣ 4158) (ZMod 11) n = 6 ↔
    n = 83 := by
  sorry

example (n : ℕ) :
    n ≡ 1 [MOD 2] ∧
    n ≡ 6 [MOD 7] ∧
    n ≡ 2 [MOD 27] ∧
    n ≡ 6 [MOD 11] ↔
    n ≡ 83 [MOD 4158] := by
  sorry

example (n : ℤ) :
    n ≡ 1 [ZMOD 2] ∧
    n ≡ 6 [ZMOD 7] ∧
    n ≡ 2 [ZMOD 27] ∧
    n ≡ 6 [ZMOD 11] ↔
    n ≡ 83 [ZMOD 4158] := by
  sorry

[Move fast]

The Third statement is that i want to show.

[Move fast]

The third is that i want to show.

[Edward van de Meent]

joy:

import Mathlib

example (n : ℕ) :
    n ≡ 1 [MOD 2] ∧
    n ≡ 6 [MOD 7] ∧
    n ≡ 2 [MOD 27] ∧
    n ≡ 6 [MOD 11] ↔
    n ≡ 83 [MOD 4158] := by
  simp_rw [Nat.ModEq]
  omega


example (n : ℤ) :
    n ≡ 1 [ZMOD 2] ∧
    n ≡ 6 [ZMOD 7] ∧
    n ≡ 2 [ZMOD 27] ∧
    n ≡ 6 [ZMOD 11] ↔
    n ≡ 83 [ZMOD 4158] := by
  simp_rw [Int.ModEq]
  omega

[Move fast]

ok, thank you very much!