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

module Data.Nat.Divisibility where

open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties
import Data.Fin as Fin
open Fin using (Fin; zero; suc)
import Data.Fin.Props as FP
open SemiringSolver
open import Algebra
private
  module CS = CommutativeSemiring commutativeSemiring
open import Data.Product
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Function

-- m Divides n is inhabited iff m is non-zero and divides n. (The
-- requirement that m should be non-zero follows MathWorld, which
-- follows Hardy and Wright's "An Introduction to the Theory of
-- Numbers".)

data _Divides_ :     Set where
  divides : {m n : } (q : ) (eq : n  q * suc m)  suc m Divides n

-- Extracts the quotient.

quotient :  {m n}  m Divides n  
quotient (divides q _) = q

-- d Divides m And n means that d is a common divisor of m and n.

_Divides_And_ : (d m n : )  Set
d Divides m And n = d Divides m × d Divides n

-- The divisibility relation is reflexive for positive integers.

divides-refl :  n  suc n Divides suc n
divides-refl n = divides 1 (sym $ proj₁ CS.*-identity (suc n))

-- 1 divides everything.

1-divides_ :  n  1 Divides n
1-divides n = divides n (sym $ proj₂ CS.*-identity n)

-- Every positive integer divides 0.

_+1-divides-0 :  n  suc n Divides 0
n +1-divides-0 = divides 0 refl

-- 0 divides nothing.

0-doesNotDivide :  {n}  ¬ 0 Divides n
0-doesNotDivide ()

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

divides-≤ :  {m n}  m Divides suc n  m  suc n
divides-≤             (divides 0       ())
divides-≤ {suc m} {n} (divides (suc q) eq) = begin
  suc m
    ≤⟨ m≤m+n (suc m) (q * suc m) 
  suc q * suc m
    ≡⟨ sym eq 
  suc n
    
  where open ≤-Reasoning

-- If m and n divide each other, then they are equal.

divides-≡ :  {m n}  m Divides n  n Divides m  m  n
divides-≡ (divides a₁ b₁) (divides a₂ b₂) =
  ≤≥⇒≡ (divides-≤ (divides a₁ b₁)) (divides-≤ (divides a₂ b₂))

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

divides-+ :  {i m n}  i Divides m  i Divides n  i Divides (m + n)
divides-+ (divides {m = i} q refl) (divides q' refl) =
  divides (q + q') (sym $ proj₂ CS.distrib (suc i) q q')

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

divides-∸ :  {i m n}  i Divides (m + n)  i Divides m  i Divides n
divides-∸ (divides {m = i} q' eq) (divides q refl) =
  divides (q'  q)
          (sym $ im≡jm+n⇒[i∸j]m≡n q' q (suc i) _ $ sym eq)

-- If i divides i + n then i divides n.

divides-Δ :  {i n}  i Divides (i + n)  i Divides n
divides-Δ {suc i} d  = divides-∸ d (divides-refl i)
divides-Δ {zero}  ()

-- 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) Divides (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 ≡-Reasoning
nonZeroDivisor-lemma m zero r r≢zero (divides (suc q) eq) =
  ¬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 (divides-Δ d')
  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) Divides x) lem d

-- Divisibility is decidable.

divisible? : Decidable _Divides_
divisible? zero    n                            = no 0-doesNotDivide
divisible? (suc m) n                            with n divMod suc m
divisible? (suc m) .(q * suc m)                 | result q zero    =
  yes $ divides q refl
divisible? (suc m) .(1 + Fin.toℕ r + q * suc m) | result q (suc r) =
  no $ nonZeroDivisor-lemma m q (suc r) (λ())