SignType API

Stream: mathlib4

[Michael Stoll]

What is the recommended way of showing

example (n : ℤ) : ((SignType.sign n : ℤ) : ℂ) = SignType.sign (n : ℝ) := by sorry

? (This came up in #12779 @David Loeffler.) @Yaël Dillies

My best effort is

example (n : ℤ) : ((SignType.sign n : ℤ) : ℂ) = SignType.sign (n : ℝ) := by
  simp only [sign_apply]
  norm_cast
  split_ifs <;> simp

(squeezing the simps makes it a bit faster; the version above takes > 3000 heartbeats, which strikes me as slow for such an elementary fact), but I was hoping there would be sufficient API available to not have to split cases in the proof.

[Yaël Dillies]

docs#map_sign ?

[Yaël Dillies]

Missing :frown:

[Michael Stoll]

David's proof is

example (n : ℤ) : ((SignType.sign n : ℤ) : ℂ) = SignType.sign (n : ℝ) := by
  rw [← SignType.map_cast (f := Int.castRingHom ℂ), Int.coe_castRingHom, Int.cast_inj,
      ← eq_intCast (Int.castRingHom ℝ) n, StrictMono.sign_comp]
  simp_rw [strictMono_iff_map_pos, Int.coe_castRingHom, Int.cast_pos, imp_self, forall_const]

which is fairly involved (and slower)...

[Joseph Myers]

I think there are two missing lemmas here.

import Mathlib

@[simp]
lemma sign_cast_int {α : Type*} [OrderedRing α] [Nontrivial α]
    [DecidableRel ((· < ·) : α → α → Prop)] (n : ℤ) :
    SignType.sign (n : α) = SignType.sign n := by
  simp [sign_apply]

@[simp, norm_cast]
lemma sign_int_cast {α : Type*} [AddGroupWithOne α] (s : SignType) : ((s : ℤ) : α) = s :=
  SignType.map_cast' _ (mod_cast rfl) (mod_cast rfl) (mod_cast rfl) s

example (n : ℤ) : ((SignType.sign n : ℤ) : ℂ) = SignType.sign (n : ℝ) := by
  simp

Names may not be optimal and I haven't thought about where they should go in mathlib. Also, neither lemma properly is anything to do with ℤ; the first should be for any order-preserving cast, the second should be for any cast preserving 0, 1 and negation. But maybe using type classes to assert that casts have those properties is hard given how Lean 4 elaborates casts (see the reverted !3#17048).

[David Loeffler]

Joseph Myers said:

I think there are two missing lemmas here. […] Also, neither lemma properly is anything to do with ℤ; the first should be for any order-preserving cast, the second should be for any cast preserving 0, 1 and negation. But maybe using type classes to assert that casts have those properties is hard given how Lean 4 elaborates casts (see the reverted !3#17048).

That’s exactly the issue. More general versions of both lemmas already exist - for an arbitrary homomorphism of ordered types satisfying the necessary type class assumptions. The problem is that mathlib has two different versions of the canonical map from Z to an arbitrary ring - one which is a homomorphism type (Int.castRingHom) and one that’s just a bare function - and the one that’s used by default as a coercion is the bare-function version. So you have to rewrite (using “eq_intCast”) to substitute the homomorphism version, before the SignType lemmas will work; and that’s exactly the proof of mine that Michael posted earlier in this thread and was criticising as overcomplicated.

[David Loeffler]

It’s a pity that there is no information at all in the PR !3#17048, or the later PR !3#17733 that reverts it, explaining why the decision was take to remove it again.

[Yaël Dillies]

Joseph Myers said:

I think there are two missing lemmas here.

Names should be SignType.sign_intCast and SignType.intCast_cast (or Int.cast_signTypeCast) respectively

[David Loeffler]

I have added @Joseph Myers 's two missing lemmas (using the names suggested by Yaël) to Data.Sign as part of #12779. Thanks!