Stream: metaprogramming / tactics

Topic: norm_cast for algebras

Heather Macbeth (Nov 25 2020 at 14:31):

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 (Nov 25 2020 at 14:31):

@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 (Nov 25 2020 at 14:36):

That would be very useful!

Rob Lewis (Nov 25 2020 at 15:17):

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 (Nov 25 2020 at 15:18):

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

Rob Lewis (Nov 25 2020 at 15:18):

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 (Nov 25 2020 at 15:19):

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

Heather Macbeth (Nov 25 2020 at 15:28):

I see, thanks for thinking about it!

Last updated: May 09 2021 at 21:10 UTC