norm_cast for algebras

Stream: metaprogramming / tactics

[Heather Macbeth]

I was looking at @Riccardo Brasca's code in #5052 and noticed that it was quite painful to verify facts about constant polynomials that hold because they are identities of the underlying field elements. One has to explicitly reverse-apply lemmas like C_eq_nat_cast and C_mul, in tasks like

import data.polynomial.monomial

variables {F : Type*} [field F]

open polynomial

example (n : ℕ) (a : F) (hn : (n:F) ≠ 0) (ha : a ≠ 0) :
  C (a⁻¹ * (↑n)⁻¹) * n = C a⁻¹ :=
begin
  rw [← C_eq_nat_cast, ← C_mul],
  field_simp [hn, ha]
end

example (a : F) (ha : a ≠ 0) :
  C a⁻¹ * C a = 1 :=
begin
  rw [← C_mul],
  field_simp [ha]
end

[Heather Macbeth]

@Rob Lewis Are these rewrites something that could be done by norm_cast? That is, could norm_cast apply to the not-a-coercion from a ring to the polynomials over it, or more generally from a ring into an algebra over that ring, by analogy with how it applies to the coercion from (eg) $\mathbb{Q}$ to $\mathbb{R}$?

[Riccardo Brasca]

That would be very useful!

[Rob Lewis]

norm_cast only looks at things that are explicitly coercion operators, under the logic of "you need to draw a line somewhere." In principle we could probably generalize things and let users tag arbitrary functions as coercions. But do you always want C to be treated as a coercion by norm_cast? My guess is no, there will be cases where this basically disrupts the expected behavior.

[Rob Lewis]

So you'd need syntax for locally enabling/disabling the "this is a coercion" tag.

[Rob Lewis]

And you'd have to train users to know when to apply this tag, and how to disable it, and how to recognize when to disable it.

[Rob Lewis]

And I bet that in the end rw [← C_mul] ends up looking less unpleasant in comparison.

[Heather Macbeth]

I see, thanks for thinking about it!