-- §──────────────────────────────────────────────────────────────────
-- Modules required for specifying the parameters of this module
-- §──────────────────────────────────────────────────────────────────

import My.Algebra.Structure as MyAS
import Level as L

-- §──────────────────────────────────────────────────────────────────
-- This module
-- §──────────────────────────────────────────────────────────────────

module My.Surd.CancellativeCommutativeMonoid {𝓁 𝓂 : L.Level}
  (ccm : MyAS.CancellativeCommutativeMonoid 𝓁 𝓂) where

-- §──────────────────────────────────────────────────────────────────
-- Other required modules
-- §──────────────────────────────────────────────────────────────────

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 (_∣_)

-- §──────────────────────────────────────────────────────────────────
-- Some properties of squaring
-- §──────────────────────────────────────────────────────────────────

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

-- §──────────────────────────────────────────────────────────────────
-- We now fix a prime element of ccm.
-- §──────────────────────────────────────────────────────────────────

private
  module PrimeElement {p : CCM.Carrier} (primep : MySCM.Prime p) where

    infix   _⊰_
    _⊰_ : RB.Rel CCM.Carrier 𝓂
    a ⊰ b = p ∙ a ≈ b

    open Squaring

    infix  _⊰⊰_
    _⊰⊰_ : 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

    -- §──────────────────────────────────────────────────────────────────
    -- Initial facts about a prime dividing a square
    -- §──────────────────────────────────────────────────────────────────

    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₂

    -- §──────────────────────────────────────────────────────────────────
    -- The predicate Sq has no minimal elements with respect to the
    -- relation _⊰_.  As a result, if the relation _⊰_ has no infinite
    -- descent, then we have ¬ Sq a for all a, hence p must be a surd.
    -- §──────────────────────────────────────────────────────────────────

    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