Making a computable version of MvPolynomial.monomial

Stream: Is there code for X?

[Hyunsang Hwang]

I am trying to simulate Buchberger's algorithm on Lean4 but MvPolynomial.monomial seems to be declared in a noncomputable way so I am trying to declare it locally and I would like to receive some help:

import Mathlib.Data.MvPolynomial.Basic

universe u
variable {R : Type u}[CommSemiring R]{p : MvPolynomial σ R}(t : Finsupp.support p)


def monomial (p : MvPolynomial σ R)(t : Finsupp.support p)[nonzero : NeZero p]:
  (MvPolynomial σ R) :=
    {support := Set.toFinset (Set.singleton t),
      toFun := (Set.singleton t →
        Set.singleton ((Finsupp.toFun p) t)),
      mem_support_toFun:= _
      : Finsupp _ _}
/-
type mismatch
  type mismatch
  { support := Set.toFinset (Set.singleton t), toFun := ?m.126323, mem_support_toFun := ?m.126837 }
has type
  { x // x ∈ p.support } →₀ ?m.78690 : Type (max ?u.77308 ?u.78687)
but is expected to have type
  MvPolynomial σ R : Type (max ?u.77308 u)
-/

Also apart from having a difficulty on defining my own version of MvPolynomial.monomial, would I run into more trouble for using preexisting MvPolynomial and Finsupp which are again defined as noncomputable?

[Eric Wieser]

You'll quickly find that you can reuse almost none of MvPolynomial or Finsupp if you want computability

[Eric Wieser]

Im still hoping that we can change that, but we certainly can't do so until the port is over

[Eric Wieser]

In the meantime, you could build your polynomials from DFinsupp which is computable

[Eric Wieser]

Though algorithmically it's not very efficient

[Kevin Buzzard]

What would be an efficient way to do multivariable polynomials?

[Yaël Dillies]

A list (monomial times coefficients) quotiented out by the obvious thing?

[Eric Wieser]

That's dfinsupp

[Eric Wieser]

Arguably mv_poly V R = finsupp (finsupp V ℕ) R as we have it today is fine, the problem is that dfinsupp is inefficient for this use and finsupp is infinitely inefficient as it doesn't compute at all!

[Kyle Miller]

Yaël Dillies said:

A list (monomial times coefficients) quotiented out by the obvious thing?

It you have a monomial order, then rather than a quotient you can use the subtype of lists than are in strict monomial order with nonzero coefficients. Polynomial addition then for example is a merging of the two lists (like merge sort) where when there are duplicates you add coefficients.

[Hyunsang Hwang]

I'm currently trying Dfinsupp as suggested. But I am not sure whether I am using it right.

If I want to declare x as a Dfinsupp from σ to ℕ would it be correct to write (x : (Π₀ (i : σ), ℕ))?

Also, I am having trouble understanding the meaning of the [inst : (i : ι) → Zero (β i)] part in definition of Dfinsupp. Does this mean that initially β is a zero function?

[Eric Wieser]

The zero thing just means that every type in your codomain defines a zero

[Eric Wieser]

You can write it more succinctly as (x : Π₀ i : σ, ℕ), no need for the other two pairs of parens

[Hyunsang Hwang]

Thank you

[Hyunsang Hwang]

Also, I find that β does not quite act like I expect it would. For instance, I tried to build a way of representing the multiplication of (monic) monomials as the following way but it doesn't seem to work:

import Mathlib

def TermMul (x y : Π₀ i : σ, ℕ)[DecidableEq σ]:=
  Dfinsupp.mk (x.support.toList ++ y.support.toList).toFinset
   ((i : (x.support.toList ++ y.support.toList).toFinset) → (x.toFun + y.toFun ) i)
/-
type expected, got
  ((x.toFun + y.toFun) ↑i : ℕ)
-/

Is there a way that I can explicitly define the shape of the underlying function when using Dfinsupp.mk?

[Eric Wieser]

I'd recommend avoiding Dfinsupp.mk and just using the constructor directly via where syntax

[Eric Wieser]

Though I feel like what you actually want is just def TermMul (x y : Π₀ i : σ, ℕ) := x + y?

[Hyunsang Hwang]

Then is there a way to input an arbitrary function in Dfinsupp.toFun? I am trying some experiments but I seem to be misunderstanding the format:

import Mathlib

universe u v
variable (σ : Type u)
def square : Fin 5 → ℕ :=
  fun x => x * x
def DfinsuppBuilder (a : σ → Type v)[(i : σ) → Zero (a i)]:=
  { toFun := (i : σ) → a i, support' := _ : Dfinsupp _ }
/-
type mismatch
  (i : Type u) → a i
has type
  Type (max (u + 1) v) : Type (max (u + 2) (v + 1))
but is expected to have type
  (i : ?m.112963 a) → ?m.112964 a i : Type (max ?u.1227 ?u.1228)
-/
#check { toFun := (i : Fin 5) → square i, support' := _ : Dfinsupp _ }
/-
type expected, got
  (square i : ℕ)
-/

[Kevin Buzzard]

First error: (i : σ) → a i is not a function, it's the type of all functions. toFun wants one function.

[Kevin Buzzard]

Second error is the same. You make functions with the fun constructor.

[Kevin Buzzard]

#check { toFun := fun (i : Fin 5) ↦ square i, support' := _ : Dfinsupp _ }

[Hyunsang Hwang]

Thank you

[Hyunsang Hwang]

I am trying to implement the support' part of Dfinsupp but I am having an issue. The only way I know how to match the shape of { s // ∀ (i : ι), i ∈ s ∨ toFun i = 0 } is by using Classical.indefiniteDescription which does not seem to be the intention of the authors of Dfinsupp since Classical.indefiniteDescription is noncomputable. Is there a way to solve this?

import Mathlib

def square : Fin 5 → ℕ :=
  fun x => x * x

def p2 (s : Multiset (Fin 5)) := ∀ i, i ∈ s ∨ square i = 0

theorem t :(∃ x, p2 x):= sorry

def p3 :=
  { toFun := fun (i : Fin 5) ↦ square i,
    support' := Trunc.mk (Classical.indefiniteDescription p2 t)
    : Dfinsupp _ }
/-
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.indefiniteDescription', and it does not have executable code
-/

[Eric Wieser]

I think you want Trunk.mk ⟨{1, 2, 3, 4}, sorry⟩

[Hyunsang Hwang]

Thank you