```------------------------------------------------------------------------
-- The Agda standard library
--
-- Divisibility
------------------------------------------------------------------------

module Data.Nat.Divisibility where

open import Data.Nat as Nat
open import Data.Nat.DivMod
import Data.Nat.Properties as NatProp
open import Data.Fin as Fin using (Fin; zero; suc)
import Data.Fin.Props as FP
open NatProp.SemiringSolver
open import Algebra
private
module CS = CommutativeSemiring NatProp.commutativeSemiring
open import Data.Product
open import Relation.Nullary
open import Relation.Binary
import Relation.Binary.PartialOrderReasoning as PartialOrderReasoning
open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_; _≢_; refl; sym; cong; subst)
open import Function

-- m ∣ n is inhabited iff m divides n. Some sources, like Hardy and
-- Wright's "An Introduction to the Theory of Numbers", require m to
-- be non-zero. However, some things become a bit nicer if m is
-- allowed to be zero. For instance, _∣_ becomes a partial order, and
-- the gcd of 0 and 0 becomes defined.

infix 4 _∣_

data _∣_ : ℕ → ℕ → Set where
divides : {m n : ℕ} (q : ℕ) (eq : n ≡ q * m) → m ∣ n

-- Extracts the quotient.

quotient : ∀ {m n} → m ∣ n → ℕ
quotient (divides q _) = q

-- If m divides n, and n is positive, then m ≤ n.

∣⇒≤ : ∀ {m n} → m ∣ suc n → m ≤ suc n
∣⇒≤         (divides zero    ())
∣⇒≤ {m} {n} (divides (suc q) eq) = begin
m          ≤⟨ NatProp.m≤m+n m (q * m) ⟩
suc q * m  ≡⟨ sym eq ⟩
suc n      ∎
where open ≤-Reasoning

-- _∣_ is a partial order.

poset : Poset _ _ _
poset = record
{ Carrier        = ℕ
; _≈_            = _≡_
; _≤_            = _∣_
; isPartialOrder = record
{ isPreorder = record
{ isEquivalence = PropEq.isEquivalence
; reflexive     = reflexive
; trans         = trans
}
; antisym = antisym
}
}
where
module DTO = DecTotalOrder Nat.decTotalOrder
open PropEq.≡-Reasoning

reflexive : _≡_ ⇒ _∣_
reflexive {n} refl = divides 1 (sym \$ proj₁ CS.*-identity n)

antisym : Antisymmetric _≡_ _∣_
antisym (divides {n = zero} q₁ eq₁) (divides {n = n₂} q₂ eq₂) = begin
n₂      ≡⟨ eq₂ ⟩
q₂ * 0  ≡⟨ CS.*-comm q₂ 0 ⟩
0       ∎
antisym (divides {n = n₁} q₁ eq₁) (divides {n = zero} q₂ eq₂) = begin
0       ≡⟨ CS.*-comm 0 q₁ ⟩
q₁ * 0  ≡⟨ sym eq₁ ⟩
n₁      ∎
antisym (divides {n = suc n₁} q₁ eq₁) (divides {n = suc n₂} q₂ eq₂) =
DTO.antisym (∣⇒≤ (divides q₁ eq₁)) (∣⇒≤ (divides q₂ eq₂))

trans : Transitive _∣_
trans (divides q₁ refl) (divides q₂ refl) =
divides (q₂ * q₁) (sym (CS.*-assoc q₂ q₁ _))

module ∣-Reasoning = PartialOrderReasoning poset
renaming (_≤⟨_⟩_ to _∣⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_)

private module P = Poset poset

-- 1 divides everything.

1∣_ : ∀ n → 1 ∣ n
1∣ n = divides n (sym \$ proj₂ CS.*-identity n)

-- Everything divides 0.

_∣0 : ∀ n → n ∣ 0
n ∣0 = divides 0 refl

-- 0 only divides 0.

0∣⇒≡0 : ∀ {n} → 0 ∣ n → n ≡ 0
0∣⇒≡0 {n} 0∣n = P.antisym (n ∣0) 0∣n

-- Only 1 divides 1.

∣1⇒≡1 : ∀ {n} → n ∣ 1 → n ≡ 1
∣1⇒≡1 {n} n∣1 = P.antisym n∣1 (1∣ n)

-- If i divides m and n, then i divides their sum.

∣-+ : ∀ {i m n} → i ∣ m → i ∣ n → i ∣ m + n
∣-+ (divides {m = i} q refl) (divides q' refl) =
divides (q + q') (sym \$ proj₂ CS.distrib i q q')

-- If i divides m and n, then i divides their difference.

∣-∸ : ∀ {i m n} → i ∣ m + n → i ∣ m → i ∣ n
∣-∸ (divides {m = i} q' eq) (divides q refl) =
divides (q' ∸ q)
(sym \$ NatProp.im≡jm+n⇒[i∸j]m≡n q' q i _ \$ sym eq)

-- A simple lemma: n divides kn.

∣-* : ∀ k {n} → n ∣ k * n
∣-* k = divides k refl

-- If i divides j, then ki divides kj.

*-cong : ∀ {i j} k → i ∣ j → k * i ∣ k * j
*-cong {i} {j} k (divides q eq) = divides q lemma
where
open PropEq.≡-Reasoning
lemma = begin
k * j        ≡⟨ cong (_*_ k) eq ⟩
k * (q * i)  ≡⟨ solve 3 (λ k q i → k :* (q :* i)
:=  q :* (k :* i))
refl k q i ⟩
q * (k * i)  ∎

-- If ki divides kj, and k is positive, then i divides j.

/-cong : ∀ {i j} k → suc k * i ∣ suc k * j → i ∣ j
/-cong {i} {j} k (divides q eq) = divides q lemma
where
open PropEq.≡-Reasoning
k′    = suc k
lemma = NatProp.cancel-*-right j (q * i) (begin
j * k′        ≡⟨ CS.*-comm j k′ ⟩
k′ * j        ≡⟨ eq ⟩
q * (k′ * i)  ≡⟨ solve 3 (λ q k i → q :* (k :* i)
:=  q :* i :* k)
refl q k′ i ⟩
q * i * k′    ∎)

-- If the remainder after division is non-zero, then the divisor does
-- not divide the dividend.

nonZeroDivisor-lemma
: ∀ m q (r : Fin (1 + m)) → Fin.toℕ r ≢ 0 →
¬ (1 + m) ∣ (Fin.toℕ r + q * (1 + m))
nonZeroDivisor-lemma m zero r r≢zero (divides zero eq) = r≢zero \$ begin
Fin.toℕ r
≡⟨ sym \$ proj₁ CS.*-identity (Fin.toℕ r) ⟩
1 * Fin.toℕ r
≡⟨ eq ⟩
0
∎
where open PropEq.≡-Reasoning
nonZeroDivisor-lemma m zero r r≢zero (divides (suc q) eq) =
NatProp.¬i+1+j≤i m \$ begin
m + suc (q * suc m)
≡⟨ solve 2 (λ m q → m :+ (con 1 :+ q)  :=  con 1 :+ m :+ q)
refl m (q * suc m) ⟩
suc (m + q * suc m)
≡⟨ sym eq ⟩
1 * Fin.toℕ r
≡⟨ proj₁ CS.*-identity (Fin.toℕ r) ⟩
Fin.toℕ r
≤⟨ ≤-pred \$ FP.bounded r ⟩
m
∎
where open ≤-Reasoning
nonZeroDivisor-lemma m (suc q) r r≢zero d =
nonZeroDivisor-lemma m q r r≢zero (∣-∸ d' P.refl)
where
lem = solve 3 (λ m r q → r :+ (m :+ q)  :=  m :+ (r :+ q))
refl (suc m) (Fin.toℕ r) (q * suc m)
d' = subst (λ x → (1 + m) ∣ x) lem d

-- Divisibility is decidable.

_∣?_ : Decidable _∣_
zero  ∣? zero                         = yes (0 ∣0)
zero  ∣? suc n                        = no ((λ ()) ∘′ 0∣⇒≡0)
suc m ∣? n                            with n divMod suc m
suc m ∣? .(q * suc m)                 | result q zero    =
yes \$ divides q refl
suc m ∣? .(1 + Fin.toℕ r + q * suc m) | result q (suc r) =
no \$ nonZeroDivisor-lemma m q (suc r) (λ())
```