Irreducibility vs. primality

irreducible.agda

open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Data.Nat

data Irreducible (n : ℕ) : Set where
  irreducible : n ≢ 1 → (∀ x y → n ≡ x * y → x ≡ 1 ⊎ y ≡ 1) → Irreducible n

open import Data.Nat.Primality
open import Data.Nat.Divisibility
open import Data.Fin using (Fin; zero; suc; toℕ; fromℕ≤)
open import Relation.Nullary
open import Function using (_$_; _∘_)

suc-inj : {n m : ℕ} → suc n ≡ suc m → n ≡ m
suc-inj = cong Data.Nat.pred

toℕ-max : ∀ n → (i : Fin n) → n ≢ toℕ i
toℕ-max zero () _
toℕ-max (suc n) zero ()
toℕ-max (suc n) (suc i) eq = toℕ-max n i $ suc-inj eq

Irreducible⇒Prime : ∀ {n} → Irreducible n → Prime n
Irreducible⇒Prime {zero} (irreducible _ prf) with prf zero zero refl
... | inj₁ ()
... | inj₂ ()
Irreducible⇒Prime {suc zero} (irreducible n≢1 prf) = n≢1 refl
Irreducible⇒Prime {suc (suc n)} (irreducible _ prf) = lem
  where
    lem : (i : Fin n) → ¬ suc (suc (toℕ i)) ∣ suc (suc n)
    lem i (divides q eq) with prf q (suc (suc (toℕ i))) eq
    lem i (divides q eq) | inj₂ ()
    lem i (divides .1 eq) | inj₁ refl = toℕ-max n i $ suc-inj $ suc-inj $ begin
        2 + n ≡⟨ eq ⟩
        1 * (2 + toℕ i) ≡⟨ proj₁ CS.*-identity _ ⟩
        2 + toℕ i ∎
      where
        open Relation.Binary.PropositionalEquality.≡-Reasoning
        import Data.Nat.Properties
        open import Algebra
        module CS = CommutativeSemiring Data.Nat.Properties.commutativeSemiring

Prime⇒Irreducible : ∀ {n} → Prime n → Irreducible n
Prime⇒Irreducible {zero} ()
Prime⇒Irreducible {suc zero} ()
Prime⇒Irreducible {suc (suc n)} p = irreducible (λ ()) lem
  where
    open import Data.Empty

    -- It should be possible to simplify this, I would hope...
    factor-< : ∀ {n} x y → 2 + n ≡ (2 + x) * (2 + y) → y < n
    factor-< {zero} x zero ()
    factor-< {zero} x (suc y) ()
    factor-< {suc n} x y eq = lem eq′
      where
        open import Data.Nat.Properties
        open import Relation.Binary

        eq′ : 1 + n ≡ 2 + (y + (y + x * (2 + y)))
        eq′ = cong (pred ∘ pred) $ begin
          3 + n ≡⟨ eq ⟩
          2 + (y + (2 + (y + x * (2 + y)))) ≡⟨ solve 2 (λ x y → con 2 :+ (y :+ (con 2 :+ (y :+ x :* (con 2 :+ y)))) := (con 4 :+ y) :+ (y :+ x :* (con 2 :+ y))) refl x y ⟩
          (4 + y) + (y + x * (2 + y)) ∎
          where
            open Data.Nat.Properties.SemiringSolver
            open Relation.Binary.PropositionalEquality.≡-Reasoning

        lem : ∀ {x y z} → x ≡ 2 + y + z → y < x
        lem {x} {y} {z} eq = begin
          1 + y ≤⟨ ≤-step STO.refl ⟩
          2 + y ≤⟨ m≤m+n _ _ ⟩
          2 + y + z ≤⟨ STO.reflexive (sym eq) ⟩
          x ∎
          where
            module STO = DecTotalOrder decTotalOrder
            open import Relation.Binary.PartialOrderReasoning STO.poset

        ≡⇒≤ : ∀ {x y} → x ≡ y → x ≤ y
        ≡⇒≤ {zero} refl = z≤n
        ≡⇒≤ {suc x} refl = s≤s (≡⇒≤ refl)

    lem : ∀ x y → suc (suc n) ≡ x * y → x ≡ 1 ⊎ y ≡ 1
    lem zero y ()
    lem (suc zero) y eq = inj₁ refl
    lem (suc (suc x)) zero eq = ⊥-elim (*0 x eq)
      where
        *0 : ∀ x → 2 + n ≢ x * zero
        *0 zero ()
        *0 (suc x) eq = *0 x eq

    lem (suc (suc x)) (suc zero) eq = inj₂ refl
    lem (suc (suc x)) (suc (suc y)) eq = ⊥-elim $ p y′ $ divides (2 + x) $ begin
      2 + n ≡⟨ eq ⟩
      (2 + x) * (2 + y) ≡⟨ cong (λ z → (2 + x) * (2 + z)) $ sym (toℕ-fromℕ≤ y<n) ⟩
      (2 + x) * (2 + toℕ y′) ∎
      where
        open Relation.Binary.PropositionalEquality.≡-Reasoning
        open import Data.Fin.Properties

        y<n : y < n
        y<n = factor-< x y eq

        y′ : Fin n
        y′ = fromℕ≤ y<n