module My.SetTheory.Nat.Prime where
import Algebra as A
import Data.Nat as DN
import Data.Nat.Coprimality as DNC
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 as RB
import Relation.Binary.PropositionalEquality as RBPE
open DN using (_*_ ; _≤_; _<_)
open DND using (_∣_)
open DP using (_×_ ; _,_)
open DS using (_⊎_)
open F using (_$_)
open RBPE using (_≡_ ; _≢_)
import My.SetTheory.Nat.Cancellation as MySTNC
import My.SetTheory.Nat.Divisibility as MySTND
import My.SetTheory.Nat.IdentityElement as MySTNIE
import My.SetTheory.Nat.Order as MySTNO
import My.SetTheory.Nat.TvD as MySTNTVD
import My.SetTheory.Sum.Misc as MySTSM
primeN⇒1≤n : {n : DN.ℕ} → DNPrime.Prime n → 1 ≤ n
primeN⇒1≤n {0} ()
primeN⇒1≤n {DN.suc n} p = DN.s≤s DN.z≤n
primeN⇒n≢0 : {n : DN.ℕ} → DNPrime.Prime n → n ≢ 0
primeN⇒n≢0 primen = MySTNO.1≤n⇒n≢0 $ primeN⇒1≤n primen
primeN⇒2≤n : {n : DN.ℕ} → DNPrime.Prime n → 2 ≤ n
primeN⇒2≤n {0} ()
primeN⇒2≤n {1} ()
primeN⇒2≤n {DN.suc (DN.suc n)} primen = DN.s≤s $ DN.s≤s DN.z≤n
primeN⇒n≡suc⌈predN⌉ : {n : DN.ℕ} → DNPrime.Prime n → n ≡ DN.suc (DN.pred n)
primeN⇒n≡suc⌈predN⌉ primen = MySTNTVD.n≢0⇒n≡s⌈predN⌉ (primeN⇒n≢0 primen)
primeN⇒m∣n⇒m≤n : {m n : DN.ℕ} → DNPrime.Prime n → m ∣ n → m ≤ n
primeN⇒m∣n⇒m≤n {m} {n} primen m∣n = s
where
q0 : n ≡ DN.suc (DN.pred n)
q0 = primeN⇒n≡suc⌈predN⌉ primen
q : m ∣ DN.suc (DN.pred n)
q = DIV.trans m∣n (DIV.reflexive q0)
where
module DIV = RB.Poset DND.poset
r : m ≤ DN.suc (DN.pred n)
r = DND.∣⇒≤ q
s : m ≤ n
s = MySTNO.≤-resp-≡ˡ (RBPE.sym q0) r
primeN⇒m∣n⇒m<n⊎m≡n : {m n : DN.ℕ} → DNPrime.Prime n → m ∣ n → m < n ⊎ m ≡ n
primeN⇒m∣n⇒m<n⊎m≡n primen m∣n =
MySTNTVD.m≤n⇒m<n⊎m≡n (primeN⇒m∣n⇒m≤n primen m∣n)
primeN⇒m∣n⇒m<n⇒m≡1 : {m n : DN.ℕ} → DNPrime.Prime n → m ∣ n → m < n → m ≡ 1
primeN⇒m∣n⇒m<n⇒m≡1 {m} {n} primen m∣n m<n = m≡1
where
0<m : 0 < m
0<m = MySTND.1≤n⇒m|n⇒0<m (primeN⇒1≤n primen) m∣n
cnm : DNC.Coprime n m
cnm = DNC.prime⇒coprime n primen m 0<m m<n
m∣m : m ∣ m
m∣m = DIV.reflexive RBPE.refl
where
module DIV = RB.Poset DND.poset
pair : m ∣ n × m ∣ m
pair = (m∣n , m∣m)
m≡1 : m ≡ 1
m≡1 = cnm pair
primeN⇒m∣n⇒m≡1⊎m≡n : {m n : DN.ℕ} → DNPrime.Prime n → m ∣ n → m ≡ 1 ⊎ m ≡ n
primeN⇒m∣n⇒m≡1⊎m≡n {m} {n} primen m∣n = m≡1⊎m≡n
where
m<n⊎m≣n : m < n ⊎ m ≡ n
m<n⊎m≣n = primeN⇒m∣n⇒m<n⊎m≡n primen m∣n
f : m < n → m ≡ 1
f = primeN⇒m∣n⇒m<n⇒m≡1 primen m∣n
g : m ≡ n → m ≡ n
g = F.id
h : m < n ⊎ m ≡ n → m ≡ 1 ⊎ m ≡ n
h = DS.map f g
m≡1⊎m≡n : m ≡ 1 ⊎ m ≡ n
m≡1⊎m≡n = h m<n⊎m≣n
primeN⇒n≡x*y⇒x≢1⇒y≡1 : {n x y : DN.ℕ} → DNPrime.Prime n → n ≡ x * y → x ≢ 1 →
y ≡ 1
primeN⇒n≡x*y⇒x≢1⇒y≡1 {n} {x} {y} primen n≡x*y x≢1 = y≡1
where
n≡y*x : n ≡ y * x
n≡y*x =
begin
n ≡⟨ n≡x*y ⟩
x * y ≡⟨ CSR.*-comm x y ⟩
y * x ∎
where
module CSR = A.CommutativeSemiring DNP.commutativeSemiring
open RBPE.≡-Reasoning
x∣n : x ∣ n
x∣n = DND.divides y n≡y*x
x≡1⊎x≡n : x ≡ 1 ⊎ x ≡ n
x≡1⊎x≡n = primeN⇒m∣n⇒m≡1⊎m≡n primen x∣n
x≡n : x ≡ n
x≡n = MySTSM.¬A⇒A⊎B⇒B x≢1 x≡1⊎x≡n
n*y≡n*1 : n * y ≡ n * 1
n*y≡n*1 =
begin
n * y ≡⟨ RBPE.cong (λ a → a * y) $ RBPE.sym x≡n ⟩
x * y ≡⟨ RBPE.sym n≡x*y ⟩
n ≡⟨ RBPE.sym $ MySTNIE.n*1≡n n ⟩
n * 1 ∎
where open RBPE.≡-Reasoning
m : DN.ℕ
m = DN.pred n
n≡sm : n ≡ DN.suc m
n≡sm = primeN⇒n≡suc⌈predN⌉ primen
sm*y≡sm*1 : DN.suc m * y ≡ DN.suc m * 1
sm*y≡sm*1 =
begin
DN.suc m * y ≡⟨ RBPE.cong (λ a → a * y) $ RBPE.sym n≡sm ⟩
n * y ≡⟨ n*y≡n*1 ⟩
n * 1 ≡⟨ RBPE.cong (λ a → a * 1) n≡sm ⟩
DN.suc m * 1 ∎
where open RBPE.≡-Reasoning
y≡1 : y ≡ 1
y≡1 = MySTNC.cancel-*-left m sm*y≡sm*1