Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: norm_cast for algebras


view this post on Zulip 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

view this post on Zulip 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) Q\mathbb{Q} to R\mathbb{R}?

view this post on Zulip Riccardo Brasca (Nov 25 2020 at 14:36):

That would be very useful!

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Nov 25 2020 at 15:18):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Nov 25 2020 at 15:28):

I see, thanks for thinking about it!


Last updated: May 09 2021 at 21:10 UTC