-- Euler's theorem and Fermat's little theorem: a coprime to n satisfies
-- a^φ(n) ≡ 1 (mod n), because multiplication by a permutes the units mod n
-- and so leaves their product unchanged; for a prime p, φ(p) = p − 1
-- 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.Euler
import ResidueLists
import Nat.Subtraction

theorem units.coprime_product (n : Nat)
  requires nonzero : n ≠ 0
  shows gcd(∏ units(n), n) = 1
proof
  have unitsList := units.list at n
  have all := listProduct.coprime at n, units(n) with nonzero, *
  apply all
  intros x xNat positive
  have member := units.member with positive
  exact member.right

-- An inverse of a unit is a unit.
theorem units.inverse_coprime (a b n : Nat)
  requires nonzero : n ≠ 0
  requires inverse : (a * b) % n = 1
  shows gcd(b, n) = 1
proof
  have gNat := gcd.natural at b, n
  have dividesB := gcd.divides_left at b, n
  have dividesN := gcd.divides_right at b, n
  obtain ⟨q, qNat, equation⟩ := mod.equation at a * b, n with nonzero
  rw inverse at equation
  have bDividesProduct : b ∣ a * b
    witness a
    ring
  have dividesProduct := divides.transitive with dividesB, bDividesProduct
  have dividesMultiple := divides.multiply_right at gcd(b, n), n, q with dividesN
  rw equation at dividesProduct
  have dividesOne := divides.add_cancel_left with dividesMultiple, dividesProduct
  exact divides.one_only with gNat, dividesOne

-- Scaling by a unit permutes the units.
theorem units.scaled_multiplicity (a n v : Nat)
  requires aboveOne : 1 < n
  requires coprime : gcd(a, n) = 1
  shows multiplicity(v, scaledList(a, n, units(n))) = multiplicity(v, units(n))
proof
  have nonzero : n ≠ 0
    intro zero
    rw zero at aboveOne
    have impossible : ¬(1:N) < 0 by arith
    exact impossible with aboveOne
  have unitsList := units.list at n
  obtain ⟨b, bNat, bBelow, inverse⟩ := coprime.inverse with aboveOne, coprime
  have bCoprime := units.inverse_coprime with nonzero, inverse
  have alternatives : v < n ∨ ¬v < n by tauto
  cases alternatives with vBelow | vNotBelow
  . have residues : ∀ x, Nat(x) → 0 < multiplicity(x, units(n)) → x < n
      intros x xNat positive
      have member := units.member with positive
      exact member.left
    have key := scaledList.multiplicity at a, b, n, v, units(n) with nonzero, inverse, vBelow, *
    have reduced := key with residues
    rw reduced
    have scaledBelow := mod.less at b * v, n with nonzero
    have coprimeAlternatives : gcd(v, n) = 1 ∨ gcd(v, n) ≠ 1 by tauto
    cases coprimeAlternatives with vCoprime | vNotCoprime
    . have scaledCoprime := coprime.mul_mod with nonzero, bCoprime, vCoprime
      have left := units.multiplicity with scaledBelow, scaledCoprime
      have right := units.multiplicity with vBelow, vCoprime
      rw [left, right]
      rfl
    . have scaledNotCoprime : gcd((b * v) % n, n) ≠ 1
        intro scaledCoprime
        apply vNotCoprime
        have recover : (a * ((b * v) % n)) % n = v
          have step1 := mod.mul_right at n, a, b * v with nonzero
          have rearrange : a * (b * v) = (a * b) * v by ring
          have step2 := mod.mul_left at n, a * b, v with nonzero
          have one : 1 * v = v by ring
          have self := mod.of_less with vBelow
          rw [step1, rearrange, ← step2, inverse, one, self]
          rfl
        have product := coprime.mul_mod with nonzero, coprime, scaledCoprime
        rwa recover at product
      have leftNot : ¬((b * v) % n < n ∧ gcd((b * v) % n, n) = 1)
        intro both
        exact scaledNotCoprime with both.right
      have rightNot : ¬(v < n ∧ gcd(v, n) = 1)
        intro both
        exact vNotCoprime with both.right
      have left := units.multiplicity_other with leftNot
      have right := units.multiplicity_other with rightNot
      rw [left, right]
      rfl
  . have rightNot : ¬(v < n ∧ gcd(v, n) = 1)
      intro both
      exact vNotBelow with both.left
    have right := units.multiplicity_other with rightNot
    rw right
    have scaledList2 := scaledList.list at a, n, units(n) with *
    have members := scaledList.member at a, n, units(n) with nonzero, *
    have trichotomy := Less.trichotomy at 0, multiplicity(v, scaledList(a, n, units(n)))
    rcases trichotomy with positive | zero | negative
    . exfalso
      have vNat : Nat(v) by typecheck
      have below := members with v, positive
      exact vNotBelow with below
    . symm at zero
      exact zero
    . exfalso
      have impossible : ¬multiplicity(v, scaledList(a, n, units(n))) < 0 by arith
      exact impossible with negative

-- Euler's theorem.
theorem euler.theorem (a n : Nat)
  requires aboveOne : 1 < n
  requires coprime : gcd(a, n) = 1
  shows (a ^ totient(n)) % n = 1
proof
  have nonzero : n ≠ 0
    intro zero
    rw zero at aboveOne
    have impossible : ¬(1:N) < 0 by arith
    exact impossible with aboveOne
  have unitsList := units.list at n
  have scaledUnits := scaledList.list at a, n, units(n) with *
  have sameMultiplicity : ∀ q, Nat(q) → multiplicity(q, scaledList(a, n, units(n))) = multiplicity(q, units(n))
    intros q qNat
    exact units.scaled_multiplicity with aboveOne, coprime
  have sameProducts := listProduct.of_multiplicities at scaledList(a, n, units(n)) with *
  have sameProduct := sameProducts with units(n), unitsList, sameMultiplicity
  have productMod := scaledList.product at a, n, units(n) with nonzero, *
  rw sameProduct at productMod
  have lengthDef := totient.definition at n
  rw ← lengthDef at productMod
  have productCoprime := units.coprime_product with nonzero
  have arranged : (∏ units(n) * 1) % n = (∏ units(n) * a ^ totient(n)) % n
    have one : ∏ units(n) * 1 = ∏ units(n) by ring
    have commute : ∏ units(n) * a ^ totient(n) = a ^ totient(n) * ∏ units(n) by ring
    rwa [one, commute]
  have cancelled := coprime.mul_cancel_mod with nonzero, productCoprime, arranged
  have oneSelf := mod.of_less with aboveOne
  rw oneSelf at cancelled
  symm at cancelled
  exact cancelled

-- Below a prime, every positive residue is a unit.
theorem prime.coprime_below (p k : Nat)
  requires prime : Prime(p)
  requires positive : 0 < k
  requires below : k < p
  shows gcd(k, p) = 1
proof
  have kNonzero : k ≠ 0
    intro zero
    rw zero at positive
    exact Less.irreflexive with *, positive
  have notDivides : ¬(p ∣ k)
    intro divides
    have le := divides.le with divides, kNonzero
    have impossible : ¬p ≤ k by arith
    exact impossible with le
  have certificate := Prime.coprime_of_not_divides with prime, notDivides
  have same := gcd.unique with certificate
  have commute := gcd.commutative at k, p
  rwa commute

theorem unitsBelow.prime_length (p j : Nat)
  requires prime : Prime(p)
  shows j < p → length{ℕ}(unitsBelow(p, succ(j))) = j
proof
  induction j
  | zero =>
    intro below
    have aboveOne := Prime.greater_than_one at p with prime
    have zeroGcd := gcd.zero_left at p
    have notCoprime : gcd(0, p) ≠ 1
      intro one
      rw zeroGcd at one
      rw one at aboveOne
      exact Less.irreflexive at 1 with *, aboveOne
    have step := unitsBelow.succ_other at p, 0 with notCoprime
    rw [step, unitsBelow.zero]
    exact length.nil at ℕ
  | succ(i) using ih =>
    intro below
    have smaller : i < p by arith
    have previous := ih with smaller
    have positive : 0 < succ(i) by arith
    have coprime := prime.coprime_below at p, succ(i) with prime, positive, below
    have step := unitsBelow.succ_unit at p, succ(i) with coprime
    have restList := unitsBelow.list at p, succ(i)
    have expand := length.cons at ℕ, succ(i), unitsBelow(p, succ(i)) with *
    rw [step, expand, previous]
    rfl

theorem totient.prime (p : Nat)
  requires prime : Prime(p)
  shows totient(p) = p - 1
proof
  have nonzero := Prime.nonzero with prime
  have shape := natural.zero_or_successor at p
  cases shape with zero | successor
  . exfalso
    exact nonzero with zero
  . obtain ⟨q, qNat, form⟩ := successor
    have below : q < p
      rw form
      arith
    have lengths := unitsBelow.prime_length with prime
    have value := lengths with below
    have same : totient(p) = length{ℕ}(unitsBelow(p, p))
      unfold totient
      rfl
    have inner : unitsBelow(p, p) = unitsBelow(p, succ(q))
      rw ← form
      rfl
    rw [same, inner, value, form]
    simp [sub, predecessor]

theorem fermat.little (a p : Nat)
  requires prime : Prime(p)
  requires notDivides : ¬(p ∣ a)
  shows a ^ (p - 1) % p = 1
proof
  have aboveOne := Prime.greater_than_one with prime
  have certificate := Prime.coprime_of_not_divides with prime, notDivides
  have same := gcd.unique with certificate
  have commute := gcd.commutative at a, p
  have coprime : gcd(a, p) = 1
    rwa commute
  have totientValue := totient.prime with prime
  rw ← totientValue
  exact euler.theorem with aboveOne, coprime