SignType woes

Stream: mathlib4

[Michael Stoll]

One of my students just now stumbled over something like the following.

import Mathlib

example (x y : SignType) : ((x * y : SignType) : ℤ) = (x : ℤ) * y := by
  -- simp -- simp made no progress
  -- norm_cast -- no change
  -- push_cast -- no change
  -- rw [map_mul] -- tactic 'rewrite' failed
  simp_rw [← SignType.castHom_apply, map_mul] -- works, but is not really obvious

It looks like there are some simp/norm_cast lemmas missing here (also for pow [the actual problem was something like ((-1 : SignType) ^ k : ℤ) = (-1 : ℤ) ^ k] and zpow).
@Yaël Dillies ?

[Michael Stoll]

Strangely enough,

example {k : ℕ} : ((-1 : SignType)^k : ℤ) = (-1 : ℤ)^k := by simp

does work. (simp? says simp only [SignType.coe_neg_one, Nat.odd_iff_not_even].)

[Michael Stoll]

But the actual problem really was

example {k : ℕ} : ((-1)^k : SignType) = (-1 : ℤ)^k := sorry

where simp does not work...

[Yaël Dillies]

What if you add @[simp, norm_cast] lemma SignType.cast_pow (a : SignType) (k : Nat) : a ^ k = (a ^ k : alpha) for appropriate alpha?

[Michael Stoll]

I guess somebody should do that (including _mul and _zpow). Who implemented SignType?

[Yaël Dillies]

@Eric Rodriguez

[Eric Rodriguez]

This all seems reasonable to do, yes

[Michael Stoll]

OK, I can do it. Is [MonoidWithZero α] [HasDistribNeg α] the appropriate set of assumptions here?

[Eric Rodriguez]

MulZeroOneClass I think?

[Michael Stoll]

That does not want to give me powers. failed to synthesize instance HPow α ℕ ?m.16075 without local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y), and with it, I get norm_cast: badly shaped lemma, rhs can't start with coe ↑(a ^ k).

@[simp, norm_cast] lemma SignType.cast_pow {α} [MulZeroOneClass α] [HasDistribNeg α] (a : SignType) (k : Nat) :
    ((a ^ k : SignType) : α) = (a ^ k : α) := by sorry

[Michael Stoll]

So I'll go ahead with MonoidWithZero, and people are welcome to try to weaken that...

[Eric Rodriguez]

Ah, that makes sense; yes, powers you'll need the monoids, just multiplication is okay with MulZeroOneClass

[Ruben Van de Velde]

Nerd-sniped - assumptions probably not minimal

import Mathlib

@[simp, norm_cast]
lemma SignType.cast_pow
    {α : Type*} [Ring α]
    (a : SignType) (k : Nat) : (a ^ k : SignType) = (a : α) ^ k := by
  rw [← SignType.castHom_apply]
  simp

@[simp, norm_cast]
lemma SignType.cast_mul
    {α : Type*} [Ring α]
    (a b : SignType) : (a * b : SignType) = (a * b : α) := by
  rw [← SignType.castHom_apply]
  simp

@[simp, norm_cast]
lemma SignType.cast_one
    {α : Type*} [Ring α] : (1 : SignType) = (1 : α) := by
  rw [← SignType.castHom_apply]
  simp

@[simp, norm_cast]
lemma SignType.cast_neg
    {α : Type*} [Ring α]
    (a : SignType) : (-a : SignType) = - (a : α) := by
  calc ((-a : SignType) : α)
    _ = castHom (-a) := by simp
    _ = (castHom (-1 * a) : α) := by simp
    _ = castHom (-1) * (castHom a : α) := by rw [map_mul]
    _ = -1 * (castHom a : α) := by simp
    _ = - (a : α) := by simp

example {k : ℕ} : ((-1)^k : SignType) = (-1 : ℤ)^k := by
  simp -- works
  -- norm_cast doesn't work
  push_cast; rfl

example (x y : SignType) : ((x * y : SignType) : ℤ) = (x : ℤ) * y := by
  simp -- works
  norm_cast -- works
  push_cast; rfl -- works

[Michael Stoll]

Then @Ruben Van de Velde , I'll let you do the PR :smile:

[Kyle Miller]

@Michael Stoll Could you make a mwe for "badly shaped lemma"? It might be useful to improve error messages in the elaborator.

[Ruben Van de Velde]

Ha. Not right now :)

[Michael Stoll]

SignType.coe_{one|zero|neg_one} do exist, BTW.

[Michael Stoll]

@Kyle Miller :

import Mathlib.Data.Sign

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)

@[norm_cast] lemma SignType.cast_pow {α} [MulZeroOneClass α] [HasDistribNeg α] (a : SignType) (k : Nat) :
    ((a ^ k : SignType) : α) = (a ^ k : α) := by sorry
-- norm_cast: badly shaped lemma, rhs can't start with coe
--  ↑(a ^ k)

[Michael Stoll]

The error message goes away when writing (a : α) ^ k on the rhs.

[Kyle Miller]

Thanks for the mwe. I see, it's entirely caused by local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y), and without it you get a reasonable error message*. (PSA: this macro_rules trick should no longer be needed for anything. It was for an elaborator issue where you'd get the wrong ^, not for failing to find an instance.)

(*) It's "reasonable", but it could be probably be more helpful than "failed to synthesize instance HPow α ℕ ?m.2519". I wonder if one day there might be documentation attached to classes that could give hints about how to get certain instances when there's an instance synthesis failure?

[Michael Stoll]

#9074

[Michael Stoll]

@Kyle Miller Apparently the mcaro_rules lead to the coercion being outside instead of inside.

[Ruben Van de Velde]

Wait, why do you still have the macro_rules? The lean bug was fixed

[Ruben Van de Velde]

I guess Kyle said that

[Michael Stoll]

I tried that because without it, I got the error "failed to synthesize instance HPow α ℕ ?m.2519" mentioned above.

[Kevin Buzzard]

If people are fiddling with Data.Sign then on line 394 there's attribute [local instance] LinearOrderedRing.decidableLT with a comment "I'm not sure why this is necessary", but as far as I can see it is indeed not necessary.

[Michael Stoll]

I can try to remove it and see what happens.

[Eric Rodriguez]

It was necessary in lean3 to work around some issue

[Eric Rodriguez]

It was only local to the file so if it builds then we are all good :)