import My.Algebra.Structure as MyAS
import Level as L
module My.Surd.CancellativeCommutativeMonoid {𝓁 𝓂 : L.Level}
(ccm : MyAS.CancellativeCommutativeMonoid 𝓁 𝓂) where
import Algebra as A
import Data.Product as DP
import Data.Sum as DS
import Function as F
import Relation.Binary as RB
import Relation.Binary.EqReasoning as RBER
import Relation.Nullary as RN
import Relation.Unary as RU
open DP using (_,_ ; _×_)
open DS using (_⊎_)
open F using (_$_ ; _∘_)
open L using (_⊔_)
import My.SetTheory.Induction as MySTI
import My.SetTheory.Sum as MySTS
private
module CCM = MyAS.CancellativeCommutativeMonoid ccm
import My.Surd.CommutativeMonoid CCM.commutativeMonoid as MySCM
open CCM using (_≈_ ; _∙_)
open MySCM using (_∣_)
private
module Squaring where
squareProd : {p x : CCM.Carrier} → MySCM.square (p ∙ x) ≈ p ∙ (p ∙ MySCM.square x)
squareProd {p} {x} =
begin
MySCM.square (p ∙ x) ≈⟨ CCM.assocˡ p x $ p ∙ x ⟩
p ∙ (x ∙ (p ∙ x)) ≈⟨ CCM.∙-congˡ $ CCM.assocʳ x p x ⟩
p ∙ ((x ∙ p) ∙ x) ≈⟨ CCM.∙-congˡ $ CCM.∙-congʳ $ CCM.comm x p ⟩
p ∙ ((p ∙ x) ∙ x) ≈⟨ CCM.∙-congˡ $ CCM.assocˡ p x x ⟩
p ∙ (p ∙ MySCM.square x) ∎
where
open RBER CCM.setoid
squarePres : MySCM.square RB.Preserves _≈_ ⟶ _≈_
squarePres {x} {y} p =
begin
MySCM.square x ≈⟨ CCM.∙-congˡ p ⟩
x ∙ y ≈⟨ CCM.∙-congʳ p ⟩
MySCM.square y ∎
where
open RBER CCM.setoid
private
module PrimeElement {p : CCM.Carrier} (primep : MySCM.Prime p) where
infix 4 _⊰_
_⊰_ : RB.Rel CCM.Carrier 𝓂
a ⊰ b = p ∙ a ≈ b
open Squaring
infix 4 _⊰⊰_
_⊰⊰_ : RB.Rel CCM.Carrier 𝓂
a ⊰⊰ b = p ∙ MySCM.square a ≈ MySCM.square b
Sq : RU.Pred CCM.Carrier (𝓁 ⊔ 𝓂)
Sq a = DP.Σ[ x ∈ CCM.Carrier ] x ⊰⊰ a
lem₁aux : {a b c : CCM.Carrier} → a ⊰⊰ b → c ⊰ b →
p ∙ (p ∙ MySCM.square c) ≈ p ∙ MySCM.square a
lem₁aux {a} {b} {c} a⊰⊰b c⊰b =
begin
p ∙ (p ∙ MySCM.square c) ≈⟨ CCM.sym $ squareProd ⟩
MySCM.square (p ∙ c) ≈⟨ squarePres c⊰b ⟩
MySCM.square b ≈⟨ CCM.sym a⊰⊰b ⟩
p ∙ MySCM.square a ∎
where
open RBER CCM.setoid
lem₁ : {a b c : CCM.Carrier} → a ⊰⊰ b → c ⊰ b → c ⊰⊰ a
lem₁ a⊰⊰b c⊰b = CCM.cancelˡ p $ lem₁aux a⊰⊰b c⊰b
p∣a²⇒p∣a : {a : CCM.Carrier} → p ∣ MySCM.square a → (p ∣ a)
p∣a²⇒p∣a = MySTS.sameSum ∘ (MySCM.Prime.prePrime primep)
lem₂ : {a x : CCM.Carrier} → x ⊰⊰ a → p ∣ a
lem₂ {x = x} x⊰⊰a = p∣a²⇒p∣a p∣a² where
p∣a² = record { quotient = MySCM.square x ; pf = x⊰⊰a }
φ : {a x : CCM.Carrier} → x ⊰⊰ a → CCM.Carrier
φ = MySCM._∣_.quotient ∘ lem₂
lem₃ : {a x : CCM.Carrier} → (x⊰⊰a : x ⊰⊰ a) → φ x⊰⊰a ⊰ a
lem₃ = MySCM._∣_.pf ∘ lem₂
lem₄ : {a x : CCM.Carrier} → (x⊰⊰a : x ⊰⊰ a) → φ x⊰⊰a ⊰⊰ x
lem₄ x⊰⊰a = lem₁ x⊰⊰a $ lem₃ x⊰⊰a
lem₅ : {a x : CCM.Carrier} → (x⊰⊰a : x ⊰⊰ a) → Sq x
lem₅ x⊰⊰a = (φ x⊰⊰a , lem₄ x⊰⊰a)
lem₆ : {a x : CCM.Carrier} → (x⊰⊰a : x ⊰⊰ a) → Sq $ φ x⊰⊰a
lem₆ = lem₅ ∘ lem₄
lem₇ : {a x : CCM.Carrier} → (x⊰⊰a : x ⊰⊰ a) → MySTI.notMinimal _⊰_ Sq a
lem₇ x⊰⊰a = record { elt = φ x⊰⊰a ; lessPf = lem₃ x⊰⊰a ; eltPf = lem₆ x⊰⊰a}
noMinimalElement : MySTI.NoMinimalElt _⊰_ Sq
noMinimalElement = lem₇ ∘ DP.proj₂
noInfiniteDescent⇒Surd : MySTI.NoInfiniteDescent _⊰_ (𝓁 ⊔ 𝓂) → MySCM.Surd p
noInfiniteDescent⇒Surd nid hasratsqrtp =
nid Sq noMinimalElement SQRT.num (SQRT.den , SQRT.pf)
where
module SQRT = MySCM.hasRatSqrt hasratsqrtp
thm : {p : CCM.Carrier} → (MySCM.Prime p) →
MySTI.NoInfiniteDescent (λ x y → p ∙ x ≈ y) (𝓁 ⊔ 𝓂) →
MySCM.Surd p
thm primep = M.noInfiniteDescent⇒Surd
where
module M = PrimeElement primep