-- Divisibility of natural numbers
-- 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.Divisibility
import Nat

predicate Divides (a b : Nat) := ∃ k, Nat(k) ∧ mul(a, k) = b
notation infix 50 "∣" => Divides

theorem divides.definition (a b : Nat)
  shows a ∣ b ↔ ∃ k, Nat(k) ∧ mul(a, k) = b
proof
  simp [Divides]

theorem divides.reflexive (a : Nat)
  shows a ∣ a
proof
  witness 1
  simp [mul.right_unit]

theorem one.divides (a : Nat)
  shows 1 ∣ a
proof
  witness a
  simp [mul.left_unit]

theorem divides.zero (a : Nat)
  shows a ∣ 0
proof
  witness 0
  simp [mul.right_zero]

theorem zero.divides_only_zero (a : Nat)
  requires h : 0 ∣ a
  shows a = 0
proof
  obtain ⟨k, hkNat, hkEq⟩ := h
  rw ← hkEq
  simp [mul.left_zero]

theorem divides.one_only (a : Set)
  requires haNat : Nat(a)
  requires h : a ∣ 1
  shows a = 1
proof
  obtain ⟨k, hkNat, hProduct⟩ := h
  apply mul.left_factor_one at k, a
  . exact hProduct

theorem divides.transitive (a b c : Nat)
  requires hab : a ∣ b
  requires hbc : b ∣ c
  shows a ∣ c
proof
  obtain ⟨k, hkNat, hkEq⟩ := hab
  obtain ⟨l, hlNat, hlEq⟩ := hbc
  witness mul(k, l)
  simp [mul.associative_reverse]

theorem divides.multiply_right (a b c : Nat)
  requires hab : a ∣ b
  shows a ∣ mul(b, c)
proof
  obtain ⟨k, hkNat, hkEq⟩ := hab
  witness mul(k, c)
  simp [mul.associative_reverse]

theorem divides.multiply_left (a b c : Set)
  requires haNat : Nat(a)
  requires hbNat : Nat(b)
  requires hcNat : Nat(c)
  requires hab : a ∣ b
  shows a ∣ mul(c, b)
proof
  have right := divides.multiply_right with haNat, hbNat, hcNat, hab
  have commute := mul.commutative with hcNat, hbNat
  rwa commute at right

theorem divides.add (a b c : Nat)
  requires hab : a ∣ b
  requires hac : a ∣ c
  shows a ∣ add(b, c)
proof
  obtain ⟨k, hkNat, hkEq⟩ := hab
  obtain ⟨l, hlNat, hlEq⟩ := hac
  witness add(k, l)
  simp [mul.distributes_left]

lemma divides.successor_product_one (p : Set, k : Nat)
  requires hpNat : Nat(p)
  shows p ∣ succ(mul(p, k)) → p = 1
proof
  induction k
  | zero =>
    intro h
    have zero := mul.right_zero with hpNat
    rw zero at h
    apply divides.one_only
    . exact hpNat
    . exact h
  | succ(j) using ih =>
    intro h
    obtain ⟨l, hlNat, hEquation⟩ := h
    have lShape := natural.zero_or_successor with hlNat
    cases lShape with hlZero | hlSuccessor
    . exfalso
      rw hlZero at hEquation
      have productZero := mul.right_zero with hpNat
      rw productZero at hEquation
      have impossible := Naturals.disjoint.zero.succ at mul(p, succ(j))
      apply impossible
      exact hEquation
    . obtain ⟨q, hq⟩ := hlSuccessor
      rcases hq with ⟨hqNat, hlSucc⟩
      rw hlSucc at hEquation
      have leftStep := mul.succ_right with hqNat, hpNat
      rw leftStep at hEquation
      have innerStep := mul.succ_right with h_j, hpNat
      rw innerStep at hEquation
      have rightStep := add.succ_right at mul(p, j), p with hpNat
      rw ← rightStep at hEquation
      have cancel := add.left_cancel with hpNat, hEquation
      apply ih
      refine ⟨q, hqNat, cancel⟩

-- This is the arithmetic fact Euclid's proof needs.  Its statement contains
-- no representation-level membership: common divisors of n and n+1 are one.
theorem divides.consecutive_one (p n : Set)
  requires hpNat : Nat(p)
  requires hnNat : Nat(n)
  requires hn : p ∣ n
  requires hNext : p ∣ succ(n)
  shows p = 1
proof
  obtain ⟨k, hkNat, hProduct⟩ := hn
  rw ← hProduct at hNext
  apply divides.successor_product_one at p, k
  . exact hNext

theorem factorial.successor_divides (n : Nat)
  shows succ(n) ∣ succ(n)!
proof
  witness n!
  simp [factorial]

-- Every positive natural at most n occurs among the factors of n!.
theorem factorial.divisible_through (p : Set, n : Nat)
  requires hpNat : Nat(p)
  shows 0 ∈ p → p ∈ succ(n) → p ∣ n!
proof
  induction n
  | zero =>
    intros hpPositive hpBound
    exfalso
    have membership := membership.one.forward at p with hpBound
    rw membership at hpPositive
    simp [nat.zero, set.empty]
  | succ(k) using ih =>
    intros hpPositive hpBound
    have bound := membership.successor_forward{n := succ(k)} at p
    cases bound with hpEarlier | hpNewest
    . have dividesPrevious := ih with hpPositive, hpEarlier
      settle with divides.multiply_left, factorial, factorial.closed,
        Naturals.constructor.succ
    . rw hpNewest
      simp [factorial.successor_divides]

-- A nonzero multiple is at least its divisor.
theorem divides.le (a b : Nat)
  requires divides : a ∣ b
  requires nonzero : b ≠ 0
  shows a ≤ b
proof
  obtain ⟨k, kNat, product⟩ := divides
  have shape := natural.zero_or_successor at k with *
  cases shape with zero | successor
  . exfalso
    rw zero at product
    have value := mul.right_zero at a with *
    rw value at product
    apply nonzero
    symm
    exact product
  . obtain ⟨j, jNat, step⟩ := successor
    rw step at product
    witness a * j
    have expand := mul.succ_right at j, a with *
    rwa expand at product

theorem divides.antisymmetric (a b : Nat)
  requires forward : a ∣ b
  requires backward : b ∣ a
  shows a = b
proof
  have splitA : a = 0 ∨ a ≠ 0
  . tauto
  cases splitA with az | az
  . rw az at forward
    have bz := zero.divides_only_zero with *
    simp
  . have splitB : b = 0 ∨ b ≠ 0
    . tauto
    cases splitB with bz | bz
    . rw bz at backward
      have aZero := zero.divides_only_zero with *
      simp
    . have ab := divides.le at a, b with *
      have ba := divides.le at b, a with *
      exact LessEqual.antisymmetric with *

-- Cancel a known divisible summand without introducing signed naturals.
theorem divides.add_cancel_left (d a b : Nat)
  requires dividesLeft : d ∣ a
  requires dividesSum : d ∣ a + b
  shows d ∣ b
proof
  have splitD : d = 0 ∨ d ≠ 0
  . tauto
  cases splitD with dz | dz
  . rw dz at dividesSum
    have sumZero := zero.divides_only_zero with *
    have bZero := add.eq_zero_right with *, sumZero
    rw bZero
    exact divides.zero with *
  . obtain ⟨k, kNat, left⟩ := dividesLeft
    obtain ⟨l, lNat, sum⟩ := dividesSum
    have notLess : ¬l < k
    . intro less
      have strict := Less.mul_left with *
      rw [sum, left] at strict
      have bound : a ≤ a + b
        witness b
        rfl
      have cycle := Less.transitive_LessEqual with *
      exact Less.irreflexive with *, cycle
    have order := LessEqual.of_not_Less with *
    obtain ⟨r, rNat, gap⟩ := order
    have expanded : d * k + d * r = d * l
    . rw ← gap
      ring
    rw [left, sum] at expanded
    have remainder := add.left_cancel with *, expanded
    unfold Divides
    refine ⟨r, rNat, remainder⟩

theorem divides.add_cancel_right (d a b : Nat)
  requires dividesRight : d ∣ b
  requires dividesSum : d ∣ a + b
  shows d ∣ a
proof
  have commute := add.commutative at a, b with *
  rw ← commute at dividesSum
  exact divides.add_cancel_left with *

-- Common divisors are unchanged by a Euclidean remainder equation.
theorem divides.remainder_iff (d a b q r : Nat)
  requires equation : a = b * q + r
  requires dividesB : d ∣ b
  shows d ∣ a ↔ d ∣ r
proof
  have multiple := divides.multiply_right at d, b, q with *
  constructor
  . intro dividesA
    rw equation at dividesA
    exact divides.add_cancel_left with *
  . intro dividesR
    rw equation
    exact divides.add with *

lemma divides.sample
  shows 7 ∣ 42
proof
  witness 6
  compute