-- The two-modulus Chinese remainder theorem over quotient integers
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.NumberTheory.ChineseRemainder
import Coprime

theorem IntegerDivides.coprime_product (m n z : Integer)
  requires coprime : IntegerCoprime(m, n)
  requires left : IntegerDivides(m, z)
  requires right : IntegerDivides(n, z)
  shows IntegerDivides(m * n, z)
proof
  obtain ⟨q, qInteger, equation⟩ := left
  have symmetric := IntegerCoprime.symmetric with *
  rw ← equation at right
  have quotient := IntegerCoprime.cancel with *
  obtain ⟨k, kInteger, factor⟩ := quotient
  witness k
  rw [← equation, ← factor]
  ring

-- If u*m+v*n=1, then a*v*n+b*u*m has the prescribed residues.
def chineseCombination (m n a b u v : Integer) : Integer := a * v * n + b * u * m

theorem chineseCombination.correct (m n a b u v : Integer)
  requires identity : u * m + v * n = integerOne
  shows IntegerCongruent(m, chineseCombination(m, n, a, b, u, v), a) ∧
    IntegerCongruent(n, chineseCombination(m, n, a, b, u, v), b)
proof
  constructor
    witness u * (b - a)
    unfold chineseCombination
    linear_combination -a * identity
    witness v * (a - b)
    unfold chineseCombination
    linear_combination -b * identity

theorem ChineseRemainder.exists (m n a b : Integer)
  requires coprime : IntegerCoprime(m, n)
  shows ∃ x, Integer(x) ∧ IntegerCongruent(m, x, a) ∧ IntegerCongruent(n, x, b)
proof
  obtain ⟨u, uInteger, v, vInteger, identity⟩ := IntegerCoprime.bezout at m, n with *
  have integer := chineseCombination.type at m, n, a, b, u, v with *
  have residues := chineseCombination.correct at m, n, a, b, u, v with *
  witness chineseCombination(m, n, a, b, u, v)
  exact residues

theorem ChineseRemainder.unique (m n a b x y : Integer)
  requires coprime : IntegerCoprime(m, n)
  requires xm : IntegerCongruent(m, x, a)
  requires xn : IntegerCongruent(n, x, b)
  requires ym : IntegerCongruent(m, y, a)
  requires yn : IntegerCongruent(n, y, b)
  shows IntegerCongruent(m * n, x, y)
proof
  have reverseM := IntegerCongruent.symmetric at m, y, a with *
  have reverseN := IntegerCongruent.symmetric at n, y, b with *
  have sameM := IntegerCongruent.transitive at m, x, a, y with *
  have sameN := IntegerCongruent.transitive at n, x, b, y with *
  unfold IntegerCongruent at sameM
  unfold IntegerCongruent at sameN
  unfold IntegerCongruent
  exact IntegerDivides.coprime_product with *