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

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Nat.Divisibility where

open import Data.Nat.Base
open import Data.Nat.DivMod
  using (m≡m%n+[m/n]*n; m%n≡m∸m/n*n; m*n/n≡m; m*n%n≡0; *-/-assoc)
open import Data.Nat.Properties
open import Function.Base using (_∘′_; _$_; flip)
open import Function.Bundles using (_⇔_; mk⇔)
open import Level using (0ℓ)
open import Relation.Nullary.Decidable as Dec using (yes; no)
open import Relation.Nullary.Negation.Core using (contradiction)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.Bundles using (Preorder; Poset)
open import Relation.Binary.Structures
  using (IsPreorder; IsPartialOrder)
open import Relation.Binary.Definitions
  using (Reflexive; Transitive; Antisymmetric; Decidable)
import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; _≢_; refl; sym; cong; subst)
open import Relation.Binary.Reasoning.Syntax
open import Relation.Binary.PropositionalEquality.Properties
  using (isEquivalence; module ≡-Reasoning)

private
  variable d m n o p : 


------------------------------------------------------------------------
-- Definition and derived properties

open import Data.Nat.Divisibility.Core public hiding (*-pres-∣)

quotient≢0 : (m∣n : m  n)  .{{NonZero n}}  NonZero (quotient m∣n)
quotient≢0 m∣n rewrite _∣_.equality m∣n = m*n≢0⇒m≢0 (quotient m∣n)

m∣n⇒n≡quotient*m : (m∣n : m  n)  n  (quotient m∣n) * m
m∣n⇒n≡quotient*m m∣n = _∣_.equality m∣n

m∣n⇒n≡m*quotient : (m∣n : m  n)  n  m * (quotient m∣n)
m∣n⇒n≡m*quotient {m = m} m∣n rewrite _∣_.equality m∣n = *-comm (quotient m∣n) m

quotient-∣ : (m∣n : m  n)  (quotient m∣n)  n
quotient-∣ {m = m} m∣n = divides m (m∣n⇒n≡m*quotient m∣n)

quotient>1 : (m∣n : m  n)  m < n  1 < quotient m∣n
quotient>1 {m} {n} m∣n m<n = *-cancelˡ-< m 1 (quotient m∣n) $ begin-strict
    m * 1        ≡⟨ *-identityʳ m 
    m            <⟨ m<n 
    n            ≡⟨ m∣n⇒n≡m*quotient m∣n 
    m * quotient m∣n 
  where open ≤-Reasoning

quotient-< : (m∣n : m  n)  .{{NonTrivial m}}  .{{NonZero n}}  quotient m∣n < n
quotient-< {m} {n} m∣n = begin-strict
  quotient m∣n     <⟨ m<m*n (quotient m∣n) m (nonTrivial⇒n>1 m) 
  quotient m∣n * m ≡⟨ _∣_.equality m∣n 
  n                
  where open ≤-Reasoning; instance _ = quotient≢0 m∣n

------------------------------------------------------------------------
-- Relating _/_ and quotient

n/m≡quotient : (m∣n : m  n) .{{_ : NonZero m}}  n / m  quotient m∣n
n/m≡quotient {m = m} (divides-refl q) = m*n/n≡m q m

------------------------------------------------------------------------
-- Relationship with _%_

m%n≡0⇒n∣m :  m n .{{_ : NonZero n}}  m % n  0  n  m
m%n≡0⇒n∣m m n eq = divides (m / n) $ begin
  m                ≡⟨ m≡m%n+[m/n]*n m n 
  m % n + [m/n]*n  ≡⟨ cong (_+ [m/n]*n) eq 
  [m/n]*n          
  where open ≡-Reasoning; [m/n]*n = m / n * n

n∣m⇒m%n≡0 :  m n .{{_ : NonZero n}}  n  m  m % n  0
n∣m⇒m%n≡0 .(q * n) n (divides-refl q) = m*n%n≡0 q n

m%n≡0⇔n∣m :  m n .{{_ : NonZero n}}  m % n  0  n  m
m%n≡0⇔n∣m m n = mk⇔ (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n)

------------------------------------------------------------------------
-- Properties of _∣_ and _≤_

∣⇒≤ : .{{_ : NonZero n}}  m  n  m  n
∣⇒≤ {n@.(q * m)} {m} (divides-refl q@(suc p)) = m≤m+n m (p * m)

>⇒∤ : .{{_ : NonZero n}}  m > n  m  n
>⇒∤ {n@(suc _)} n<m@(s<s _) m∣n = contradiction (∣⇒≤ m∣n) (<⇒≱ n<m)

------------------------------------------------------------------------
-- _∣_ is a partial order

-- these could/should inherit from Algebra.Properties.Monoid.Divisibility

∣-reflexive : _≡_  _∣_
∣-reflexive {n} refl = divides 1 (sym (*-identityˡ n))

∣-refl : Reflexive _∣_
∣-refl = ∣-reflexive refl

∣-trans : Transitive _∣_
∣-trans (divides-refl p) (divides-refl q) =
  divides (q * p) (sym (*-assoc q p _))

∣-antisym : Antisymmetric _≡_ _∣_
∣-antisym {m}     {zero}   _  q∣p = m∣n⇒n≡m*quotient q∣p
∣-antisym {zero}  {n}     p∣q  _  = sym (m∣n⇒n≡m*quotient p∣q)
∣-antisym {suc m} {suc n} p∣q q∣p = ≤-antisym (∣⇒≤ p∣q) (∣⇒≤ q∣p)

infix 4 _∣?_

_∣?_ : Decidable _∣_
zero  ∣? zero   = yes (divides-refl 0)
zero  ∣? suc m  = no ((λ()) ∘′ ∣-antisym (divides-refl 0))
n@(suc _) ∣? m  = Dec.map (m%n≡0⇔n∣m m n) (m % n  0)

∣-isPreorder : IsPreorder _≡_ _∣_
∣-isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = ∣-reflexive
  ; trans         = ∣-trans
  }

∣-isPartialOrder : IsPartialOrder _≡_ _∣_
∣-isPartialOrder = record
  { isPreorder = ∣-isPreorder
  ; antisym    = ∣-antisym
  }

∣-preorder : Preorder 0ℓ 0ℓ 0ℓ
∣-preorder = record
  { isPreorder = ∣-isPreorder
  }

∣-poset : Poset 0ℓ 0ℓ 0ℓ
∣-poset = record
  { isPartialOrder = ∣-isPartialOrder
  }

------------------------------------------------------------------------
-- A reasoning module for the _∣_ relation

module ∣-Reasoning where
  private module Base = ≲-Reasoning ∣-preorder

  open Base public
    hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-∼; step-≲)
    renaming (≲-go to ∣-go)

  open ∣-syntax _IsRelatedTo_ _IsRelatedTo_ ∣-go public


------------------------------------------------------------------------
-- Simple properties of _∣_

infix 10 _∣0 1∣_

_∣0 :  n  n  0
n ∣0 = divides-refl 0

0∣⇒≡0 : 0  n  n  0
0∣⇒≡0 {n} 0∣n = ∣-antisym (n ∣0) 0∣n

1∣_ :  n  1  n
1∣ n = divides n (sym (*-identityʳ n))

∣1⇒≡1 : n  1  n  1
∣1⇒≡1 {n} n∣1 = ∣-antisym n∣1 (1∣ n)

n∣n : n  n
n∣n = ∣-refl

------------------------------------------------------------------------
-- Properties of _∣_ and _+_

∣m∣n⇒∣m+n : d  m  d  n  d  m + n
∣m∣n⇒∣m+n (divides-refl p) (divides-refl q) =
  divides (p + q) (sym (*-distribʳ-+ _ p q))

∣m+n∣m⇒∣n : d  m + n  d  m  d  n
∣m+n∣m⇒∣n {d} {m} {n} (divides p m+n≡p*d) (divides-refl q) =
  divides (p  q) $ begin-equality
    n             ≡⟨ m+n∸n≡m n m 
    n + m  m     ≡⟨ cong (_∸ m) (+-comm n m) 
    m + n  m     ≡⟨ cong (_∸ m) m+n≡p*d 
    p * d  q * d ≡⟨ *-distribʳ-∸ d p q 
    (p  q) * d   
    where open ∣-Reasoning

------------------------------------------------------------------------
-- Properties of _∣_ and _*_

n∣m*n :  m {n}  n  m * n
n∣m*n m = divides m refl

m∣m*n :  {m} n  m  m * n
m∣m*n n = divides n (*-comm _ n)

n∣m*n*o :  m {n} o  n  m * n * o
n∣m*n*o m o = ∣-trans (n∣m*n m) (m∣m*n o)

∣m⇒∣m*n :  n  d  m  d  m * n
∣m⇒∣m*n n (divides-refl q) = ∣-trans (n∣m*n q) (m∣m*n n)

∣n⇒∣m*n :  m {n}  d  n  d  m * n
∣n⇒∣m*n m {n} rewrite *-comm m n = ∣m⇒∣m*n m

m*n∣⇒m∣ :  m n  m * n  d  m  d
m*n∣⇒m∣ m n (divides-refl q) = ∣n⇒∣m*n q (m∣m*n n)

m*n∣⇒n∣ :  m n  m * n  d  n  d
m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m

*-pres-∣ : o  m  p  n  o * p  m * n
*-pres-∣ {o} {m@.(q * o)} {p} {n@.(r * p)} (divides-refl q) (divides-refl r) =
  divides (q * r) ([m*n]*[o*p]≡[m*o]*[n*p] q o r p)

*-monoʳ-∣ :  o  m  n  o * m  o * n
*-monoʳ-∣ o = *-pres-∣ (∣-refl {o})

*-monoˡ-∣ :  o  m  n  m * o  n * o
*-monoˡ-∣ o = flip *-pres-∣ (∣-refl {o})

*-cancelˡ-∣ :  o .{{_ : NonZero o}}  o * m  o * n  m  n
*-cancelˡ-∣ {m} {n} o o*m∣o*n = divides q $ *-cancelˡ-≡ n (q * m) o $ begin-equality
  o * n       ≡⟨ m∣n⇒n≡m*quotient o*m∣o*n 
  o * m * q   ≡⟨ *-assoc o m q 
  o * (m * q) ≡⟨ cong (o *_) (*-comm q m) 
  o * (q * m) 
  where
  open ∣-Reasoning
  q = quotient o*m∣o*n

*-cancelʳ-∣ :  o .{{_ : NonZero o}}  m * o  n * o  m  n
*-cancelʳ-∣ {m} {n} o rewrite *-comm m o | *-comm n o = *-cancelˡ-∣ o

------------------------------------------------------------------------
-- Properties of _∣_ and _∸_

∣m∸n∣n⇒∣m :  d  n  m  d  m  n  d  n  d  m
∣m∸n∣n⇒∣m {n} {m} d n≤m (divides p m∸n≡p*d) (divides-refl q) =
  divides (p + q) $ begin-equality
    m             ≡⟨ m+[n∸m]≡n n≤m 
    n + (m  n)   ≡⟨ +-comm n (m  n) 
    m  n + n     ≡⟨ cong (_+ n) m∸n≡p*d 
    p * d + q * d ≡⟨ *-distribʳ-+ d p q 
    (p + q) * d   
  where open ∣-Reasoning

------------------------------------------------------------------------
-- Properties of _∣_ and _/_

m/n∣m : .{{_ : NonZero n}}  n  m  m / n  m
m/n∣m {n} {m} n∣m = begin
  m / n        ≡⟨ n/m≡quotient n∣m 
  quotient n∣m ∣⟨ quotient-∣ n∣m 
  m            
  where open ∣-Reasoning

m*n∣o⇒m∣o/n :  m n .{{_ : NonZero n}}  m * n  o  m  o / n
m*n∣o⇒m∣o/n m n (divides-refl p) = divides p $ begin-equality
  p * (m * n) / n   ≡⟨ *-/-assoc p (n∣m*n m) 
  p * ((m * n) / n) ≡⟨ cong (p *_) (m*n/n≡m m n) 
  p * m 
  where open ∣-Reasoning

m*n∣o⇒n∣o/m :  m n .{{_ : NonZero m}}  m * n  o  n  (o / m)
m*n∣o⇒n∣o/m m n rewrite *-comm m n = m*n∣o⇒m∣o/n n m

m∣n/o⇒m*o∣n : .{{_ : NonZero o}}  o  n  m  n / o  m * o  n
m∣n/o⇒m*o∣n {o} {n@.(p * o)} {m} (divides-refl p) m∣p*o/o = begin
  m * o ∣⟨ *-monoˡ-∣ o (subst (m ∣_) (m*n/n≡m p o) m∣p*o/o) 
  p * o 
  where open ∣-Reasoning

m∣n/o⇒o*m∣n : .{{_ : NonZero o}}  o  n  m  n / o  o * m  n
m∣n/o⇒o*m∣n {o} {_} {m} rewrite *-comm o m = m∣n/o⇒m*o∣n

m/n∣o⇒m∣o*n : .{{_ : NonZero n}}  n  m  m / n  o  m  o * n
m/n∣o⇒m∣o*n {n} {m@.(p * n)} {o} (divides-refl p) p*n/n∣o = begin
  p * n ∣⟨ *-monoˡ-∣ n (subst (_∣ o) (m*n/n≡m p n) p*n/n∣o) 
  o * n 
  where open ∣-Reasoning

m∣n*o⇒m/n∣o : .{{_ : NonZero n}}  n  m  m  o * n  m / n  o
m∣n*o⇒m/n∣o {n} {m@.(p * n)} {o} (divides-refl p) pn∣on = begin
  m / n     ≡⟨⟩
  p * n / n ≡⟨ m*n/n≡m p n 
  p         ∣⟨ *-cancelʳ-∣ n pn∣on 
  o         
  where open ∣-Reasoning

------------------------------------------------------------------------
-- Properties of _∣_ and _%_

∣n∣m%n⇒∣m : .{{_ : NonZero n}}  d  n  d  m % n  d  m
∣n∣m%n⇒∣m {n@.(p * d)} {d} {m} (divides-refl p) (divides q m%n≡qd) =
  divides (q + (m / n) * p) $ begin-equality
    m                         ≡⟨ m≡m%n+[m/n]*n m n 
    m % n + (m / n) * n       ≡⟨ cong (_+ (m / n) * n) m%n≡qd 
    q * d + (m / n) * n       ≡⟨⟩
    q * d + (m / n) * (p * d) ≡⟨ cong (q * d +_) (*-assoc (m / n) p d) 
    q * d + ((m / n) * p) * d ≡⟨ *-distribʳ-+ d q _ 
    (q + (m / n) * p) * d     
  where open ∣-Reasoning

%-presˡ-∣ : .{{_ : NonZero n}}  d  m  d  n  d  m % n
%-presˡ-∣ {n} {d} {m@.(p * d)} (divides-refl p) (divides q 1+n≡qd) =
  divides (p  m / n * q) $ begin-equality
    m % n                   ≡⟨ m%n≡m∸m/n*n m n 
    m  m / n * n           ≡⟨ cong  v  m  m / n * v) 1+n≡qd 
    m  m / n * (q * d)     ≡⟨ cong (m ∸_) (*-assoc (m / n) q d) 
    m   (m / n * q) * d    ≡⟨⟩
    p * d  (m / n * q) * d ≡⟨ *-distribʳ-∸ d p (m / n * q) 
    (p  m / n * q) * d     
  where open ∣-Reasoning

------------------------------------------------------------------------
-- Properties of _∣_ and !_

m≤n⇒m!∣n! : m  n  m !  n !
m≤n⇒m!∣n! m≤n = help (≤⇒≤′ m≤n)
  where
  help : m ≤′ n  m !  n !
  help         ≤′-refl       = ∣-refl
  help {n = n} (≤′-step m≤n) = ∣n⇒∣m*n n (help m≤n)

------------------------------------------------------------------------
-- Properties of _HasNonTrivialDivisorLessThan_

-- Smart constructor

hasNonTrivialDivisor-≢ : .{{NonTrivial d}}  .{{NonZero n}} 
                         d  n  d  n  n HasNonTrivialDivisorLessThan n
hasNonTrivialDivisor-≢ d≢n d∣n
  = hasNonTrivialDivisor (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n

-- Monotonicity wrt ∣

hasNonTrivialDivisor-∣ : m HasNonTrivialDivisorLessThan n  m  o 
                         o HasNonTrivialDivisorLessThan n
hasNonTrivialDivisor-∣ (hasNonTrivialDivisor d<n d∣m) m∣o
  = hasNonTrivialDivisor d<n (∣-trans d∣m m∣o)

-- Monotonicity wrt ≤

hasNonTrivialDivisor-≤ : m HasNonTrivialDivisorLessThan n  n  o 
                         m HasNonTrivialDivisorLessThan o
hasNonTrivialDivisor-≤ (hasNonTrivialDivisor d<n d∣m) n≤o
  = hasNonTrivialDivisor (<-≤-trans d<n n≤o) d∣m