-- §──────────────────────────────────────────────────────────────────
-- 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 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

    -- §──────────────────────────────────────────────────────────────────
    -- 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