Trichotomy of `int.sign`

Stream: Is there code for X?

[Michael Stoll]

Is there a better way of doing the following? Should it be in mathlib?

lemma int.sign_trichotomy (a : ℤ) : a.sign = 0 ∨ a.sign = 1 ∨ a.sign = -1 :=
int.cases_on a (λ (n : ℕ), nat.cases_on n (or.inl rfl) (λ _, or.inr (or.inl rfl)))
  (λ _, or.inr (or.inr rfl))

[Yaël Dillies]

Yes: Use docs#sign_type, not docs#int.sign.

[Michael Stoll]

But a.sign does not live in sign_type. What I have is an integer, whose sign I'm conisdering, and a.sign is an integer.

[Riccardo Brasca]

I think Yaël is suggesting to use docs#sign instead of docs#int.sign

[Michael Stoll]

But I also need that a is its sign multiplied by a.nat_abs. I don't think I can get this easily via sign.

[Riccardo Brasca]

Note that we have docs#int.sign_eq_sign

[Michael Stoll]

Right now, I'm doing

rcases int.sign_trichotomy a with h₀ | hpos | hneg,

and deal with the three cases (which involve showing that some expression involving a.sign equals 1). How would I do this using signinstead?

[Michael Stoll]

OK, I guess it's something like

  rw int.sign_eq_sign a,
  set s := sign a,
  fin_cases s; rw this,

Still, having int.sign_trichotomy seems to make for a shorter proof...
(For example, to rewrite, I need to coerce explicitly back to an integer.)

[Eric Rodriguez]

the whole idea of sign_type is that it spends most of its life coerced and the API should work pretty smoothly with that

[Eric Rodriguez]

sign_trichotomy should just be something like cases (sign a)

[Eric Rodriguez]

I forgot how but there's some explicit syntax for doing cases on non-trivial terms, induction h : sign z works but seems weird to someone not used to Lean

[Eric Rodriguez]

(also, this pretty prints as below - how can we make it preferrably use numerals instead of constructors?)

image.png

[Eric Wieser]

how can we make it preferrably use numerals instead of constructors

By defining a custom recursor instead of using the builtin one, but then you can't use cases

[Yaël Dillies]

Yeah, I wanted to remove int.sign entirely but it's used in core.

[Joseph Myers]

Used in C++ code in core, or used in lemmas in core that could themselves move to mathlib? I think we should remove both int.sign and real.sign after adding versions of their lemmas that apply to the generic sign and sign_type. (But I don't know what the std4 maintainers think - that's where int.sign is now for Lean 4.) real.sign should be easy to remove since the only import of data.real.sign is linear_algebra.quadratic_form.real, which is a leaf file.