polynomial eval dot notation

Stream: general

[Bolton Bailey]

This is a bit surprising,

import data.polynomial.eval

example (p : polynomial ℕ) : p.eval = (λ x, p.eval x) := sorry
-- p is expected to have type polynomial (polynomial (polynomial ℕ))

Is there any way to tell lean that the dot notation for polynomial.eval is always supposed to be for the second argument?

[Yaël Dillies]

Unfortunately not as far as I'm aware. The trick is to apply the function enough for Lean to figure out what you're dot notating on, and not use dot notation when that's impossible.

[Kevin Buzzard]

Ha ha exactly this happened to me in a live lean session yesterday and I just resorted to lambdas

[Yakov Pechersky]

One reason it's not this way is because "eval 0" is a pretty useful function to apply to the various polynomials as is. "eval r" is a ring_hom, for all r, for example.

[Eric Rodriguez]

i'm still sad that we can't make map a bundled morphism because of dot notation

[Chris Hughes]

Eric Rodriguez said:

i'm still sad that we can't make map a bundled morphism because of dot notation

I would much rather it be bundled and lose the notation.

[Eric Rodriguez]

there's something like 1K uses in the library, plus we'd want to migrate map_zero/one/mul/add... to use the fun_like ones. I'm happy to help with that, but I really don't want to start that and then be told "oh actually we don't like this"

[Bolton Bailey]

Reviving this thread to bring up a new MWE. It seems I can use dot notation to eval a Polynomial, but not a MvPolynomial. Why is this?

import Mathlib

open scoped BigOperators Classical

section Matrix

variable {F} [Field F] [Fintype F] {H : Subgroup Fˣ} [Fintype H]

lemma lincheck_to_sumcheck_matrix_completeness (z_hat_M z_hat : Polynomial F)
  (f_M : MvPolynomial (Fin 2) F) (r : MvPolynomial (Fin 2) F) :
    (fun x => Polynomial.eval x z_hat_M) =
      Matrix.mulVec
        (fun x y => MvPolynomial.eval ![x, y] f_M)
        (fun y => z_hat.eval y) := by
  sorry

lemma lincheck_to_sumcheck_matrix_completeness' (z_hat_M z_hat : Polynomial F)
  (f_M : MvPolynomial (Fin 2) F) (r : MvPolynomial (Fin 2) F) :
    (fun x => Polynomial.eval x z_hat_M) =
      Matrix.mulVec
        (fun x y => f_M.eval ![x, y]) -- invalid field notation, function 'MvPolynomial.eval' does not have argument with type (MvPolynomial ...) that can be used, it must be explicit or implicit with a unique name
        (fun y => z_hat.eval y) := by
  sorry


end Matrix

[Eric Wieser]

docs#MvPolynomial.eval is a RingHom which confuses dot notation, docs#Polynomial.eval is a regular function

[Antoine Chambert-Loir]

Doesn't this call for some homogeneization?

[David Ang]

I think eval should always be a regular function

[David Ang]

There’s also the question of map being a ring homomorphism or not

[Eric Wieser]

Once upon a time I think we had Polynomial = MvPolynomial Unit, which has the big advantage that the APIs are completely homogenous, but the big disadvantage that the APIs are completely homogenous.

[Bolton Bailey]

What do people think of having two functions, say eval and eval_at something else, with different argument orders/one is a hom and the other is a plain function?

[Yury G. Kudryashov]

Which one is the simp normal form?

[Eric Wieser]

We already have two functions for polynomial, docs#Polynomial.eval and docs#Polynomial.evalRingHom

[Bolton Bailey]

I don't really know what the criteria are for a good simp normal form. I think I would prefer eval (the polynomial first argument order) to be more widely used because this is how I think functions are usually designed.

[Bolton Bailey]

I guess what I'm suggesting then is that we redefine MvPolynomial.eval to have the polynomial argument first, rewrite everything we can to use the new eval argument order, and rewrite the things we can't to use evalRingHom.toFun.

[Bolton Bailey]

The overriding concern to me is that I am used to hearing "we evaluate a polynomial p at point x", and so this is the order of arguments I expect to see and use in the majority of cases where I am not taking advantage of the homomorphism structure of the particular point evaluation.

[Bolton Bailey]

Eric Wieser said:

docs#MvPolynomial.eval is a RingHom which confuses dot notation, docs#Polynomial.eval is a regular function

By the way, while I now understand this is why I was experiencing a bug, I think I don't get why this is the case. Even if the default argument order doesn't change, why is a different decision made for Polynomial versus MvPolynomial on the point of the point-first function being a hom?

[Eric Wieser]

Probably because different people made the decision without communicating

[Eric Wieser]

Or someone decided to change both, but only got around to changing one

[Eric Wieser]

Bolton Bailey said:

The overriding concern to me is that I am used to hearing "we evaluate a polynomial p at point x", and so this is the order of arguments I expect to see and use in the majority of cases where I am not taking advantage of the homomorphism structure of the particular point evaluation.

docs#Function.eval uses the same convention as docs#Polynomial.eval, both of which go against your intuition here.

[Bolton Bailey]

Wild. I see that docs#RatFunc.eval does as well, though the docstring does have the same form as the natural-language sentence I gave.

[Bolton Bailey]

Maybe the issue is that apply is the more natural word for the operation with my conception of the ordering, but that there is already a meaning for that?

[Bolton Bailey]

I am partially also thinking of functions like docs#List.nthLe or docs#Vector.get, which have the "function like structure" argument first.

[Damiano Testa]

It could be that the order is so that eval x is the function that happens to also be the homomorphism, as opposed to the (non-existing in Lean 3) (eval · x).

[Damiano Testa]

If I remember correctly, in Lean 3, certain things could/could not work depending on the order of the arguments.

[Damiano Testa]

(I also find the order eval polynomial point more natural, but the possibility of writing p.eval x anyway makes this rarely an issue for me.)

[Mario Carneiro]

This actually looks like a bug or at least an issue to be reported and decide whether we want this behavior. If T.foo : α -> T -> T then I expect (t:T).foo a to mean T.foo a t even if it is applied in the special case where α := T

[Mario Carneiro]

that is, the decision of which variable to treat as the main one should be done based on the constant's type before instantiation (possibly with the current behavior as fallback so that T.foo : α -> α -> α still works when applied with α := T)

[Mario Carneiro]

actually, this doesn't even work:

def Nat.foo {α} : α → α → α := fun _ y => y
#check (1:Nat).foo 2

invalid field notation, function 'Nat.foo' does not have argument with type (Nat ...) that can be used, it must be explicit or implicit with a unique name

so this seems more like a bug / inconsistent behavior

[Mario Carneiro]

Oh I was mislead, the initial issue is from lean 3, this does not replicate in lean 4

[Eric Wieser]

@Mario Carneiro, I'm confused by your comment; isn't the problem with dot notation for docs#MvPolynomial.eval due toT.foo : α -> SomeHom T U not knowing how to tell that SomeHom expects a T argument?

[Mario Carneiro]

yes, my comment was about the wrong issue

[Mario Carneiro]

because this issue was continued from a completely different one