{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}
module AFF2024.AlgebraicSets.DiscriminatingFunctions where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Powerset
open import Cubical.Algebra.CommRing
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation.Monad
open import Cubical.Data.Nat
open import Cubical.Data.List
open import Cubical.Relation.Nullary

open import AFF2024.Basics
open import AFF2024.Algebra.Basics
import AFF2024.AlgebraicSets.Basics

module _ {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) (is-field : IsField R…) where
  open AFF2024.AlgebraicSets.Basics R…
  open CommRingStr Rstr

  module _ {n : ℕ} (M : ℙ (𝔸 n)) (is-algebraic : IsAlgebraic M) where
    module _ (p : 𝔸 n) (p∉M : ¬ (p ∈ M)) where
      part-a : ∃[ f ∈ MultivariatePoly R… n ] ((f ∈ Idl M) × (evalT f p ≡ 1r))
      part-a = do
        (fs , eq) ← is-algebraic
        {!!}

      part-a' : (fs : List (MultivariatePoly R… n)) → ¬ (p ∈ V fs) → ∃[ f ∈ MultivariatePoly R… n ] ((f ∈ Idl {n = n} (V fs)) × (evalT f p ≡ 1r))
      part-a' fs q = do
        found ← is-field (map (λ f → evalT f p) fs) (λ rs → {!!})
        {!!}