------------------------------------------------------------------------
-- Divisibility
------------------------------------------------------------------------

module Data.Nat.Divisibility where

open import Data.Nat as Nat hiding (poset)
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 Data.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
      ; ∼-resp-≈      = PropEq.resp₂ _∣_
      }
    ; antisym = antisym
    }
  }
  where
  module P = Poset Nat.poset
  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₂) =
    P.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) (λ())