{-# OPTIONS --cubical --no-import-sorts -WnoUnsupportedIndexedMatch --allow-unsolved-metas #-}
module AFF2024.Algebra.Basics where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Powerset
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Data.Sigma
open import Cubical.Data.Nat hiding (_+_; _·_)
open import Cubical.Data.Vec hiding (map)
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.Polynomials.UnivariateList.Base
open import Cubical.Algebra.CommAlgebra.UnivariatePolyList
open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyList
open import Cubical.Relation.Nullary.Base
open import Data.List hiding (map)
open import Data.List.Relation.Unary.All hiding (map)
open import Data.List.Relation.Unary.Any hiding (map)
open import Data.Fin hiding (_+_; _-_)

open import AFF2024.Basics

module _ {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) where
  open CommRingStr Rstr

  CommRing→CommAlgebra : CommAlgebra R… ℓ
  CommRing→CommAlgebra = commAlgebraFromCommRing R… _·_ (λ x y z → sym (·Assoc x y z)) ·DistR+ ·DistL+ ·IdL λ x y z → sym (·Assoc x y z)

module _ {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) where
  open CommRingStr Rstr

  MultivariatePoly… : ℕ → CommRing ℓ
  MultivariatePoly… = nUnivariatePolyList R…

  MultivariatePoly : ℕ → Type ℓ
  MultivariatePoly n = fst (MultivariatePoly… n)

  data MonicPolynomial : Type ℓ where
    1p    : MonicPolynomial
    _+X*_ : R → MonicPolynomial → MonicPolynomial

  --X : MonicPolynomial
  --X = 0r +X* 1p

  evalM : MonicPolynomial → R → R
  evalM 1p        x = x
  evalM (a +X* f) x = a + x · evalM f x

  data HasPositiveDegree : MonicPolynomial → Type ℓ where
    triv : {f : MonicPolynomial} {a : R} → HasPositiveDegree (a +X* f)

  IsAlgebraicallyClosed : Type ℓ
  IsAlgebraicallyClosed = (f : MonicPolynomial) → HasPositiveDegree f → ∃[ x ∈ R ] evalM f x ≡ 0r

module _ {ℓ : Level} {R…@(R , Rstr) : CommRing ℓ} where
  open CommRingStr Rstr

  eval : Poly R… → R → R
  eval f x = inducedMap R… (CommAlgebra→Algebra (CommRing→CommAlgebra R…)) x f

module _ {ℓ : Level} {R…@(R , Rstr) : CommRing ℓ} where
  open CommRingStr Rstr

  const : (n : ℕ) → R → MultivariatePoly R… n
  const zero    x = x
  const (suc n) x = const n x ∷ []

  var : {n : ℕ} → Fin n → MultivariatePoly R… n
  var {suc n} zero = const n 1r ∷ const n 0r ∷ []
  var (suc n) = var n ∷ []

  evalT : {n : ℕ} → MultivariatePoly R… n → Vec R n → R
  evalT {zero}  f xs       = f
  evalT {suc n} f (x ∷ xs) = evalT (eval f (const n x)) xs

  evalT' : {n : ℕ} → MultivariatePoly R… (suc n) → Vec R n → Poly R…
  evalT' {zero}  f xs       = f
  evalT' {suc n} f (x ∷ xs) = evalT' (eval f (const n x ∷ [])) xs

module Apartness {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) where
  open CommRingStr Rstr
  open Units R…

  _#_ : R → R → Type ℓ
  x # y = (x - y) ∈ Rˣ

  IsRegular : R → Type ℓ
  IsRegular x = (y : R) → x · y ≡ 0r → y ≡ 0r

  _##_ : R → R → Type ℓ
  x ## y = IsRegular (x - y)

module _ {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) where
  open CommRingStr Rstr
  open Units R…

  IsField : Type ℓ
  IsField = (xs : List R) → ¬ (All (_≡ 0r) xs) → ∥ Any (_∈ Rˣ) xs ∥₁

  ≢→inv : IsField → (x : R) → x ≢ 0r → x ∈ Rˣ
  ≢→inv p x e = {!!}
  -- with p (x ∷ []) (λ { (q ∷ qs) → e q })
  -- ... | here px = px

module Degree {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) where
  open CommRingStr Rstr

  0P : Poly R…
  0P = []

  data HasDegree≤ : Poly R… → ℕ → Type ℓ where
    base : {n : ℕ} → HasDegree≤ 0P n
    step : {a : R} {f : Poly R…} {n : ℕ} → HasDegree≤ f n → HasDegree≤ (a ∷ f) (suc n)

  degreeBound : (f : Poly R…) → ∃[ n ∈ ℕ ] HasDegree≤ f n
  degreeBound []        = ∣ zero , base ∣₁
  degreeBound (a ∷ f)   = map (λ (n , p) → suc n , step p) (degreeBound f)
  degreeBound (drop0 i) = {!!}