has_coe_to_fun instance of mv_polynomial

Stream: general

[AHan]

Although finsupp has the instance has_coe_to_fun, I don't understand why lean cannot infer that mv_polynomial also has the instance.

For example, in the following code, Unlike lemma three, there is a type error in lemma one, which says that "expected a function at p...", and I have to write it as lemma two instead.

How can I fix this?

import linear_algebra.multivariate_polynomial

section
variables {α : Type*} {σ : Type*} [comm_semiring α]

lemma one {p : mv_polynomial σ α} : ∀ {a : σ →₀ ℕ}, p a = p a := sorry
lemma two {p : mv_polynomial σ α} : ∀ {a : σ →₀ ℕ}, p.to_fun a = p.to_fun a := sorry

end

section
variables {α : Type*} {β : Type*} [has_zero β]

lemma three {f : α →₀ β} : ∀ {x}, f x = f x := sorry

end

[Kenny Lau]

because mv_polynomial isn't @[reducible]

[Kenny Lau]

so the instances don't transfer

[Mario Carneiro]

by which kenny means not that you should add @[reducible], but you should copy the instances

[AHan]

Ahh... I added @[reducibility] instead...
@Mario Carneiro Adding the attribute @[reducible] did work, but why should I copy the instances instead of adding the attribute?

[Mario Carneiro]

because one of the purposes of type synonyms is to isolate different kinds of typeclasses on the same type. In fact this is one such example: the coe_fn instance on finsupp makes sense as applying the finitely supported function on an argument, but the coe_fn instance we would expect of mv_polynomial is treating the polynomial as a function on the base ring, i.e. eval. The actual coe_fn instance inherited from finsupp is the coeff function

[AHan]

Then if I don't add the attribute @[reducible ], some lemmas like finsupp.support_zero won't be simplified under the type of mv_polynomial
I have to copy the lemma and prove it again instead. How can I fix this kind of problem?

[Mario Carneiro]

that's a feature not a bug

[Mario Carneiro]

you don't need to reprove it, but you do need to restate it

[Mario Carneiro]

and this makes you think about how your new interpretation of the type affects the meaning of the theorems

[Mario Carneiro]

some of them are no longer applicable, some new theorems may appear

[AHan]

Sorry, I don't mean it's a bug, I'm just thinking of if there's anyway to avoid to restate those lemmas.

[AHan]

OK, I understand! Thanks a lot for explanations!

[Mario Carneiro]

You can also try using the original theorems in the new context but YMMV