Problems with MvPolynomial evaluation

Stream: new members

[Sarah Azevedo Pereira]

Hi everyone! I’m working with multivariable polynomials in Lean, using the MvPolynomial type, and I created a function that takes a string and converts it into a polynomial. However, when I try to evaluate the result, it doesn’t simplify as expected.
Here is an example:

import Mathlib

open MvPolynomial

noncomputable def str_poly (s : String) : MvPolynomial (Fin 2) ℤ :=
  let vars := s.splitOn "+"
  if vars.length == 2 then
    X 0 + X 1
  else
    C 0

#reduce str_poly "a+b"  -- Expected to see something like `X 0 + X 1`
#reduce str_poly "a+b+c" -- Expected to see `C 0`

When I run #reduce, Lean returns a more complex output with support and other internal details of the polynomial structure... Here's a sample of the output I get:

{
  support :=
    Decidable.rec
      (fun h ↦
        {
          val :=
            Quot.mk List.Perm
              [{ support := { val := Quot.mk List.Perm [], nodup := ⋯ }, toFun := fun x ↦ Nat.zero,
                  mem_support_toFun := ⋯ }],
          nodup := ⋯ })
      (fun h ↦ { val := Quot.mk List.Perm [], nodup := ⋯ }) ...

Does anyone know how to make Lean simplify the expression so that #reduce only shows the simplified polynomial (X 0 + X 1 or C 0) instead of this full internal structure? I feel like I might be missing a configuration needed to get the reduced form.

[Daniel Weber]

The problem is that #reduce also reduces X and C, as well as addition

[Sarah Azevedo Pereira]

Well, I thought that comparing the output using #reduce ((str_poly "a+b") == X 0 + X 1) would work out and return true. However, the output is something like Decidable.rec (...)
An alternative way would be: example : Eq (str_poly "a+b") (X 0 + X 1) := by decide, but it gave the following error:

tactic 'decide' failed for proposition
  str_poly "a+b" = X 0 + X 1
since its 'Decidable' instance
  (str_poly "a+b").decidableEqMvPolynomial (X 0 + X 1)
did not reduce to 'isTrue' or 'isFalse'.

After unfolding the instances 'decidable_of_decidable_of_iff', 'decidable_of_iff', 'instDecidableAnd', 'instDecidableEqBool', 'instDecidableEqList', 'instDecidableEqNat', 'instDecidableEqString', 'Bool.decEq', 'Finset.decidableEq', 'Finsupp.instDecidableEq', 'List.hasDecEq', 'Multiset.decidableEq', 'decidableEqMvPolynomial', 'Nat.decEq' and 'String.decEq', reduction got stuck at the 'Decidable' instance
  ⋯ ▸
    (Quot.lift
        (Quot.indep fun a =>
          (fun a =>
              Quot.recOnSubsingleton (X 0 + X 1).support.val fun a_1 =>
                (fun x x_1 => decidable_of_iff' (x ≈ x_1) ⋯) a a_1)
            a)
        ⋯ (str_poly "a+b").support.val).snd

Hint: Reduction got stuck on '▸' (Eq.rec), which suggests that one of the 'Decidable' instances is defined using tactics such as 'rw' or 'simp'. To avoid tactics, make use of functions such as 'inferInstanceAs' or 'decidable_of_decidable_of_iff' to alter a proposition.

The error message suggests trying alternatives like inferInstanceAs or decidable_of_decidable_of_iff, but I’m not sure how to apply these here.

Has anyone had this kind of issue with polynomials or have ideas on how to test the function? I'd appreciate any insights

[Kevin Buzzard]

The issue is that much of Lean (and in particular, polynomials) is (intentionally) noncomputable (to make proving easier). I think the philosophy in mathlib is that you're supposed to test your definitions by proving theorems about them, rather than checking examples! You might be better off writing a decidable version of polynomials which is optimised to your needs.

[Kevin Buzzard]

The issue seems to be with String.splitOn rather than polynomials:

example : str_poly "a+b" = X 0 + X 1 := by
  have foo : ("a+b".splitOn "+").length = 2 := by
    -- I need a computer scientist to do this because I don't
    -- know the API for `String.splitOn`
    sorry
  simp_all [str_poly]

[Tomaz Mascarenhas]

shouldn't it be possible to prove foo just by reducing both sides?

[Tomaz Mascarenhas]

or is splitOn noncomputable too? :face_with_monocle:

[Sarah Azevedo Pereira]

Kevin Buzzard said:

The issue seems to be with String.splitOn rather than polynomials:

example : str_poly "a+b" = X 0 + X 1 := by
  have foo : ("a+b".splitOn "+").length = 2 := by
    -- I need a computer scientist to do this because I don't
    -- know the API for `String.splitOn`
    sorry
  simp_all [str_poly]

Well, that's weird, because when I do this: #reduce ("a+b".splitOn "+").length == 2 it returns true

[Kevin Buzzard]

It's not noncomputable, it's just CS gobble-de-gook and I can't find any API for it.

[Kevin Buzzard]

Sarah Azevedo Pereira said:

Well, that's weird, because when I do this: #reduce ("a+b".splitOn "+").length == 2 it returns true

That's surprising because rfl doesn't close the goal. But all this is way beyond my comfort zone, I have no idea what #reduce does.

[Tomaz Mascarenhas]

Kevin Buzzard said:

The issue is that much of Lean (and in particular, polynomials) is (intentionally) noncomputable (to make proving easier). I think the philosophy in mathlib is that you're supposed to test your definitions by proving theorems about them, rather than checking examples! You might be better off writing a decidable version of polynomials which is optimised to your needs.

Also, I am a bit confused about how can we have DecidableEq for polynomials if they are noncomputable

[Kevin Buzzard]

I should shut up and we should wait until someone who knows what they're talking about comes along.

[Eric Wieser]

Also, I am a bit confused about how can we have DecidableEq for polynomials if they are noncomputable

DecidableEq and noncomputable are somewhat independent

[Kevin Buzzard]

Oh that didn't take long

[Eric Wieser]

But you can computably decide whether the polynomial 0 is equal to itself

[Eric Wieser]

DecidableEq just says "I have a function that tells you if x = y given x and y". If x or y are noncomputable (as all polynomials except 0 are for stupid reasons), then calling f x y is going to be noncomputable even if f is computable.

[Eric Wieser]

#reduce is something different again, and is not what is meant in lean when people talk about computability.

[Sarah Azevedo Pereira]

Kevin Buzzard said:

The issue is that much of Lean (and in particular, polynomials) is (intentionally) noncomputable (to make proving easier). I think the philosophy in mathlib is that you're supposed to test your definitions by proving theorems about them, rather than checking examples! You might be better off writing a decidable version of polynomials which is optimised to your needs.

Well, at first i tried to do that, but for this project I’ll need mathlib to help prove certain theorems about the polynomials as well, so I guess defining them another way wouldn't be the best solution

[Tomaz Mascarenhas]

Eric Wieser said:

DecidableEq just says "I have a function that tells you if x = y given x and y". If x or y are noncomputable (as all polynomials except 0 are for stupid reasons), then calling f x y is going to be noncomputable even if f is computable.

So there is no hope to test the function str_poly?

[Daniel Weber]

Kevin Buzzard said:

The issue seems to be with String.splitOn rather than polynomials:

example : str_poly "a+b" = X 0 + X 1 := by
  have foo : ("a+b".splitOn "+").length = 2 := by
    -- I need a computer scientist to do this because I don't
    -- know the API for `String.splitOn`
    sorry
  simp_all [str_poly]

with_unfolding_all rfl works here, as String.splitOn is irreducible

[Kevin Buzzard]

Oh nice!