## 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