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

open import Cubical.Foundations.Prelude
open import Cubical.HITs.PropositionalTruncation
open import Cubical.HITs.PropositionalTruncation.Monad
open import Cubical.Data.Sigma
open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.Vec hiding (length)
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Polynomials.UnivariateList.Base
open import Data.List
open import Data.List.Relation.Unary.All
open import Data.List.Relation.Unary.AllPairs

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

module _ {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) where
  open CommRingStr Rstr
  open Degree R…
  open Apartness R…
  open PolyMod R… hiding (0r)

  lemma : {n : ℕ} (f : Poly R…) → HasDegree≤ f n → (xs : List R) → length xs ≡ n → All (λ x → eval f x ≡ 0r) xs → AllPairs _##_ xs → f ≡ 0P
  lemma = {!!}

  module _ (inf : Infinite R _##_) where
    lemma' : (f : Poly R…) → ((x : R) → eval f x ≡ 0r) → f ≡ 0P
    lemma' f p =
      elim (λ _ → isSetPoly _ _) (λ e → e) do
        (n , deg≤n)    ← degreeBound f
        (xs , len , q) ← takeFrom∞ inf n
        return (lemma f deg≤n xs len (allP p xs) q)

    corollary : (n : ℕ) (f : MultivariatePoly R… n) → ((xs : Vec R n) → evalT f xs ≡ 0r) → f ≡ const n 0r
    corollary n f p = {!!}