-- Further divisibility laws for the natural numbers: truncated subtraction,
-- powers, cancellation of a common factor, remainders, minimum and maximum,
-- parity, the distance between naturals, and factorials
-- 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.DivisibilityMore
import Modular
import Nat.Distance

theorem divides.intro (a b k : Nat)
  requires product : a * k = b
  shows a ∣ b
proof
  witness k
  exact product

theorem divides.of_eq (a b : Nat)
  requires same : a = b
  shows a ∣ b
proof
  rw same
  exact divides.reflexive at b

theorem divides.mul_left_self (a b : Nat)
  shows a ∣ a * b
proof
  witness b
  rfl

theorem divides.mul_right_self (a b : Nat)
  shows a ∣ b * a
proof
  witness b
  ring

theorem divides.mul_self (a b : Nat)
  requires hab : a ∣ b
  shows a ∣ b * b
proof
  exact divides.multiply_right with hab

theorem divides.of_mul_left (a b c : Nat)
  requires product : a * b ∣ c
  shows a ∣ c
proof
  have factor := divides.mul_left_self at a, b
  exact divides.transitive at a, a * b, c with factor, product

theorem divides.of_mul_right (a b c : Nat)
  requires product : a * b ∣ c
  shows b ∣ c
proof
  have factor := divides.mul_right_self at b, a
  exact divides.transitive at b, a * b, c with factor, product

theorem divides.mul_mono (a b c d : Nat)
  requires left : a ∣ b
  requires right : c ∣ d
  shows a * c ∣ b * d
proof
  obtain ⟨k, kNat, kEquation⟩ := left
  obtain ⟨l, lNat, lEquation⟩ := right
  witness k * l
  rw [← kEquation, ← lEquation]
  ring

theorem divides.mul_cancel_left (a b c : Nat)
  requires nonzero : a ≠ 0
  shows a * b ∣ a * c ↔ b ∣ c
proof
  constructor
  . intro scaled
    obtain ⟨k, kNat, equation⟩ := scaled
    have rearranged : a * (b * k) = a * c
    . rw ← equation
      ring
    have cancelled := mul.left_cancel_positive with nonzero, rearranged
    witness k
    exact cancelled
  . intro plain
    obtain ⟨k, kNat, equation⟩ := plain
    witness k
    rw ← equation
    ring

theorem divides.mul_cancel_right (a b c : Nat)
  requires nonzero : a ≠ 0
  shows b * a ∣ c * a ↔ b ∣ c
proof
  have left : b * a = a * b by ring
  have right : c * a = a * c by ring
  rw [left, right]
  exact divides.mul_cancel_left with nonzero

theorem divides.zero_iff (a : Nat)
  shows 0 ∣ a ↔ a = 0
proof
  constructor
  . intro h
    exact zero.divides_only_zero with h
  . intro zero
    rw zero
    exact divides.reflexive at 0

theorem divides.one_iff (a : Nat)
  shows a ∣ 1 ↔ a = 1
proof
  constructor
  . intro h
    exact divides.one_only at a with *
  . intro one
    rw one
    exact divides.reflexive at 1

theorem divides.antisymmetric_iff (a b : Nat)
  shows a ∣ b ∧ b ∣ a ↔ a = b
proof
  constructor
  . intro both
    rcases both with ⟨forward, backward⟩
    exact divides.antisymmetric with forward, backward
  . intro same
    rw same
    have reflexive := divides.reflexive at b
    exact ⟨reflexive, reflexive⟩

theorem divides.nonzero (a b : Nat)
  requires hab : a ∣ b
  requires nonzero : b ≠ 0
  shows a ≠ 0
proof
  intro zero
  rw zero at hab
  have bZero := zero.divides_only_zero with hab
  exact nonzero with bZero

theorem divides.lt_of_ne (a b : Nat)
  requires hab : a ∣ b
  requires nonzero : b ≠ 0
  requires distinct : a ≠ b
  shows a < b
proof
  have below := divides.le at a, b with hab, nonzero
  exact Less.of_LessEqual_ne with below, distinct

theorem divides.factor_le (a b k : Nat)
  requires product : a * k = b
  requires nonzero : b ≠ 0
  shows k ≤ b
proof
  have factor : k ∣ b
    witness a
    rw ← product
    ring
  exact divides.le at k, b with factor, nonzero

theorem divides.sub (a b c : Nat)
  requires left : a ∣ b
  requires right : a ∣ c
  shows a ∣ b - c
proof
  have total := LessEqual.total at c, b
  cases total with below | above
  . have split := sub.add_cancel_left at b, c with below
    rw ← split at left
    exact divides.add_cancel_left at a, c, b - c with right, left
  . have zero := sub.eq_zero_of_le at b, c with above
    rw zero
    exact divides.zero at a

theorem divides.of_sub (a b c : Nat)
  requires below : c ≤ b
  requires right : a ∣ c
  requires difference : a ∣ b - c
  shows a ∣ b
proof
  have split := sub.add_cancel_left at b, c with below
  rw ← split
  exact divides.add at a, c, b - c with right, difference

theorem divides.natDist (a b c : Nat)
  requires left : a ∣ b
  requires right : a ∣ c
  shows a ∣ natDist(b, c)
proof
  have first := divides.sub at a, b, c with left, right
  have second := divides.sub at a, c, b with right, left
  have value := natDist.value at b, c
  rw value
  exact divides.add at a, b - c, c - b with first, second

theorem divides.pow (a b n : Nat)
  requires hab : a ∣ b
  shows a ∣ b ^ (n + 1)
proof
  have expand := pow.add_one at b, n
  rw expand
  exact divides.multiply_right with hab

theorem divides.self_pow (a n : Nat)
  shows a ∣ a ^ (n + 1)
proof
  have reflexive := divides.reflexive at a
  exact divides.pow with reflexive

theorem divides.pow_of_le (a m n : Nat)
  requires below : m ≤ n
  shows a ^ m ∣ a ^ n
proof
  obtain ⟨k, kNat, split⟩ := LessEqual.exists_add with below
  rw split
  have expand := pow.add at a, k, m
  rw expand
  exact divides.mul_left_self at a ^ m, a ^ k

theorem divides.pow_mono (a b n : Nat)
  requires hab : a ∣ b
  shows a ^ n ∣ b ^ n
proof
  obtain ⟨k, kNat, equation⟩ := hab
  witness k ^ n
  rw ← equation
  symm
  exact pow.mul_base at a, k, n

theorem divides.two_iff_even (n : Nat)
  shows 2 ∣ n ↔ Even(n)
proof
  have characterization := Even.iff_two_mul at n
  constructor
  . intro h
    obtain ⟨k, kNat, equation⟩ := h
    apply characterization.backward
    refine ⟨k, kNat, _⟩
    symm
    exact equation
  . intro h
    obtain ⟨k, kNat, equation⟩ := characterization.forward with h
    witness k
    symm
    exact equation

theorem divides.not_two_iff_odd (n : Nat)
  shows ¬(2 ∣ n) ↔ Odd(n)
proof
  have even := divides.two_iff_even at n
  have odd := Odd.iff_not_even at n
  constructor
  . intro notDivides
    apply odd.backward
    intro isEven
    exact notDivides with (even.backward with isEven)
  . intro isOdd
    intro h
    have isEven := even.forward with h
    exact odd.forward with isOdd, isEven

theorem divides.iff_mod_zero (d n : Nat)
  shows d ∣ n ↔ n % d = 0
proof
  have split : d = 0 ∨ d ≠ 0 by tauto
  cases split with zero | nonzero
  . rw zero
    have value := mod.zero_right at n
    rw value
    exact divides.zero_iff at n
  . have characterization := mod.zero_iff at d, n with nonzero
    constructor
    . intro h
      exact characterization.backward with h
    . intro h
      exact characterization.forward with h

theorem divides.mod (d n m : Nat)
  requires left : d ∣ n
  requires right : d ∣ m
  shows d ∣ n % m
proof
  have split : m = 0 ∨ m ≠ 0 by tauto
  cases split with zero | nonzero
  . rw zero
    have value := mod.zero_right at n
    rw value
    exact left
  . obtain ⟨q, qNat, equation⟩ := mod.equation at n, m with nonzero
    have multiple := divides.multiply_right at d, m, q with right
    rw equation at left
    exact divides.add_cancel_left at d, m * q, n % m with multiple, left

theorem divides.mod_iff (d n m : Nat)
  requires right : d ∣ m
  shows d ∣ n ↔ d ∣ n % m
proof
  have split : m = 0 ∨ m ≠ 0 by tauto
  cases split with zero | nonzero
  . rw zero
    have value := mod.zero_right at n
    rw value
    tauto
  . obtain ⟨q, qNat, equation⟩ := mod.equation at n, m with nonzero
    exact divides.remainder_iff at d, n, m, q, n % m with equation, right

theorem divides.add_right_iff (a b c : Nat)
  requires hab : a ∣ b
  shows a ∣ b + c ↔ a ∣ c
proof
  constructor
  . intro sum
    exact divides.add_cancel_left at a, b, c with hab, sum
  . intro hac
    exact divides.add at a, b, c with hab, hac

theorem divides.add_left_iff (a b c : Nat)
  requires hac : a ∣ c
  shows a ∣ b + c ↔ a ∣ b
proof
  have commute : b + c = c + b by ring
  rw commute
  exact divides.add_right_iff at a, c, b with hac

theorem divides.add_mul_iff (a b k : Nat)
  shows a ∣ b + a * k ↔ a ∣ b
proof
  have multiple := divides.mul_left_self at a, k
  exact divides.add_left_iff at a, b, a * k with multiple

theorem divides.natMin (a b c : Nat)
  requires left : a ∣ b
  requires right : a ∣ c
  shows a ∣ natMin(b, c)
proof
  have alternatives := natMin.cases at b, c
  cases alternatives with first | second
  . rw first
    exact left
  . rw second
    exact right

theorem divides.natMax (a b c : Nat)
  requires left : a ∣ b
  requires right : a ∣ c
  shows a ∣ natMax(b, c)
proof
  have alternatives := natMax.cases at b, c
  cases alternatives with first | second
  . rw first
    exact left
  . rw second
    exact right

theorem divides.quotient_equation (a b : Nat)
  requires nonzero : a ≠ 0
  requires hab : a ∣ b
  shows b = a * quotientNat(b, a)
proof
  have equation := quotientNat.equation at a, b
  have remainder := divides.iff_mod_zero at a, b
  have zero := remainder.forward with hab
  rw zero at equation
  have shape : a * quotientNat(b, a) + 0 = a * quotientNat(b, a) by ring
  rw shape at equation
  exact equation

theorem divides.quotient (a b : Nat)
  requires nonzero : a ≠ 0
  requires hab : a ∣ b
  shows quotientNat(b, a) ∣ b
proof
  have equation := divides.quotient_equation with nonzero, hab
  witness a
  have shape : quotientNat(b, a) * a = a * quotientNat(b, a) by ring
  rw shape
  symm
  exact equation

theorem divides.factorial_of_le (p n : Nat)
  requires positive : 0 < p
  requires below : p ≤ n
  shows p ∣ n!
proof
  have zeroMember := membership.of_Less at 0, p with *, positive
  have bound : p < succ(n) by arith
  have member := membership.of_Less at p, succ(n) with *, bound
  exact factorial.divisible_through at p, n with *, zeroMember, member