My.SetTheory.Nat.Irreducible

module My.SetTheory.Nat.Irreducible where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Algebra as A
import Data.Empty as DE
import Data.Fin as DF
import Data.Nat as DN
import Data.Nat.Divisibility as DND
import Data.Nat.Primality as DNPrime
import Data.Nat.Properties as DNP
import Data.Product as DP
import Data.Sum as DS
import Function as F
import Relation.Binary.PropositionalEquality as RBPE

open DN using (_*_ ; _+_ ; _≤_)
open DND using (_∣_)
open DS using (_⊎_)
open F using (_$_)
open RBPE using (_≡_ ; _≢_)

import My.SetTheory.Fin.Misc as MySTFM
import My.SetTheory.Nat.Divisibility as MySTND
import My.SetTheory.Nat.IdentityElement as MySTNIE
import My.SetTheory.Nat.Misc as MySTNM
import My.SetTheory.Nat.Order as MySTNO
import My.SetTheory.Nat.Prime as MySTNP
import My.SetTheory.Nat.TvD as MySTNTVD

-- §──────────────────────────────────────────────────────────────────
-- Definition
-- §──────────────────────────────────────────────────────────────────

Irreducible : DN.ℕ → Set
Irreducible 0 = DE.⊥
Irreducible 1 = DE.⊥
Irreducible (DN.suc (DN.suc n′)) = (x y : DN.ℕ) → n ≡ x * y → x ≡ 1 ⊎ y ≡ 1
  where
    n = DN.suc (DN.suc n′)

-- §──────────────────────────────────────────────────────────────────
-- Irreducibile ⇒ Prime in the sense of Data.Nat.Primality
-- §──────────────────────────────────────────────────────────────────

IrreducibleN⇒PrimeN : {n : DN.ℕ} → Irreducible n → DNPrime.Prime n
IrreducibleN⇒PrimeN {0} ()
IrreducibleN⇒PrimeN {1} ()
IrreducibleN⇒PrimeN {DN.suc (DN.suc n′)} irredn i m∣n = s
  where
    ni : DN.ℕ
    ni = DF.toℕ i
    m : DN.ℕ
    m = 2 + ni
    n : DN.ℕ
    n = 2 + n′
    q : DN.ℕ
    q = DND.quotient m∣n
    n≡q*m : n ≡ q * m
    n≡q*m = MySTND.quotientEqn m∣n
    q≡1⊎m≡1 : q ≡ 1 ⊎ m ≡ 1
    q≡1⊎m≡1 = irredn q m n≡q*m
    f : q ≡ 1 → DE.⊥
    f q≡1 = r where
      n≡m : n ≡ m
      n≡m =
        begin
          n ≡⟨ n≡q*m ⟩
          q * m ≡⟨ RBPE.cong (λ a → a * m) q≡1 ⟩
          1 * m ≡⟨ MySTNIE.1*n≡n m ⟩
          m ∎
        where
          open RBPE.≡-Reasoning
      n′≡ni : n′ ≡ ni
      n′≡ni = DNP.cancel-+-left 2 n≡m
      r : DE.⊥
      r = MySTFM.iFinN⇒N≢toℕi i n′≡ni
    g : m ≡ 1 → DE.⊥
    g m≡1 = MySTNM.2+n≢1 ni m≡1
    h : q ≡ 1 ⊎ m ≡ 1 → DE.⊥
    h = DS.[ f , g ]
    s : DE.⊥
    s = h q≡1⊎m≡1

-- §──────────────────────────────────────────────────────────────────
-- Prime in the sense of Data.Nat.Primality ⇒ Irreducible
-- §──────────────────────────────────────────────────────────────────

PrimeN⇒IrreducibleN : {n : DN.ℕ} → DNPrime.Prime n → Irreducible n
PrimeN⇒IrreducibleN {0} ()
PrimeN⇒IrreducibleN {DN.suc 0} ()
PrimeN⇒IrreducibleN {DN.suc (DN.suc n′)} primen = f
  where
    n : DN.ℕ
    n = DN.suc (DN.suc n′)
    2≤n : 2 ≤ n
    2≤n = MySTNP.primeN⇒2≤n primen
    n≢1 : n ≢ 1
    n≢1 = MySTNO.2≤n⇏n≢1 2≤n
    f : (x y : DN.ℕ) → n ≡ x * y → x ≡ 1 ⊎ y ≡ 1
    f x y n≡x*y = x≡1⊎y≡1
      where
        x≡1⊎x≢1 : x ≡ 1 ⊎ x ≢ 1
        x≡1⊎x≢1 = MySTNTVD.m≡n⊎m≢n x 1
        g : x ≢ 1 → y ≡ 1
        g = MySTNP.primeN⇒n≡x*y⇒x≢1⇒y≡1 primen n≡x*y
        x≡1⊎y≡1 : x ≡ 1 ⊎ y ≡ 1
        x≡1⊎y≡1 = DS.map F.id g x≡1⊎x≢1