MvPolynomial index notation issue

Stream: mathlib4

[Shreyas Srinivas]

The following is an #mwe . I have found a fix, but I still want to understand what is happening. The issue is about variable indexing syntax for MvPolynomial inside a proof, one generated by apply?

Basically in the first example, I can't pass the Fin n index to X directly. The second example shows that the proof clearly works fine for objects in arbitrary rings. The error seems specifically w.r.t MvPolynomials. The third example shows the fixed version for completeness sake. I have just extracted the index into a let declaration. Maybe this is just a syntax priority issue or a limitation of refine syntax. But it is a rather strange error message: to complain that an inductive type is expected and that the constructor notation is invalid.

import Mathlib

open MvPolynomial

-- Why is there an error here?
example {α} (hn : n > 0) (d : ℕ) (hd : d > 0) [iCR: CommRing α]: @X α (Fin n) iCR.toCommSemiring ⟨0, by omega⟩ ^ (d - 1) * X ⟨0, by omega⟩ = (X ⟨0, by omega⟩) ^ d := by
  ring_nf
  -- apply? suggests the below
  refine mul_pow_sub_one ?_ (X ⟨0, hn⟩) -- why error?
  /-
  invalid constructor ⟨...⟩, expected type must be an inductive type
  ?m.6787
  -/

-- Note that nothing breaks below
example [CommRing α] (x : α) (d : ℕ) (hd : d > 0):
  x^(d - 1) * x = x^d := by
  ring_nf
  refine mul_pow_sub_one ?_ x
  omega

-- The fixed version
example {α} (hn : n > 0) (d : ℕ) (hd : d > 0) [iCR: CommRing α]: @X α (Fin n) iCR.toCommSemiring ⟨0, by omega⟩ ^ (d - 1) * X ⟨0, by omega⟩ = (X ⟨0, by omega⟩) ^ d := by
  ring_nf
  let i : Fin n := ⟨0, by omega⟩
  refine mul_pow_sub_one ?_ (X i)
  omega

[Kevin Buzzard]

Well judging by the error, unification must be proceeding in such a way that by the time it's got to figure out what ⟨0, hn⟩ means, the expected type is still a metavariable, so rotten luck. refine mul_pow_sub_one ?_ (X _) works. But in general you shouldn't be using ⟨0, hn⟩ in mathlib, the way to do this would be to use [NeZero n] rather than hn : n > 0 (i.e. put the hypothesis into typeclass inference) and then you can just use 0 : Fin n.

I guess I should add that I would strongly discourage using Fin n as a ring at all; we have ZMod n for that purpose, and 0 : ZMod n works fine even for n = 0 (because $\Z/0\Z\cong\Z$ as opposed to Fin 0 which really isn't a ring).

[Shreyas Srinivas]

As far as I can tell, Fin n is only being used as an index into a vector of variables

[Shreyas Srinivas]

I posted this question here since the question was about a mathlib provided interface. Basically the use case is arithmetic/algebraic circuit complexity, which is the computational complexity version of algebraic geometry according to its originators. It asks “what depth or size of a circuit composed of addition, multiplication, or negation gates can compute a given class of polynomials as a function of n, the number of variables”. One if its

[Shreyas Srinivas]

I am not sure we want to allow 0 variable polynomials to be interpreted as having one variable per integer, i.e., countably infinitely many variables. I am not sure what the concrete consequences are, but at first glance it seems wrong

[Shreyas Srinivas]

But I am not sure. Maybe, as you point out in your blog, that’s just going to be a default junk value situation like division by zero.

[Eric Wieser]

I think you could have stopped at your first message, aka "I am not using it as a ring"

[Shreyas Srinivas]

Yeah, but if Kevin’s suggestion is useful regardless and I have misunderstood, I would love to be corrected; maybe the context is helpful.

[Kevin Buzzard]

Oh no I'm a fool, sorry, you're using it as an index set. Ignore the ZMod stuff, but maybe you want to think about the NeZero stuff