Skip to content

Instantly share code, notes, and snippets.

@gergoerdi

gergoerdi/irreducible.agda

Last active Aug 29, 2015
Embed
What would you like to do?
Irreducibility vs. primality
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.