norm_cast regression?

Stream: mathlib4

[Kevin Buzzard]

I don't remember this happening before:

import Mathlib.Tactic

example (x : ℤ) : x = -1 := by
  norm_cast
  -- ⊢ x = Int.negSucc 0
  sorry

I don't like seeing my least favourite constructor in the game, it's a mathematical abomination. More to the point, I don't know any lemmas about it :-)

[Kim Morrison]

show_term casts suspicion on Mathlib.Data.Int.Cast.Basic._auxLemma.3, but I've yet again forgotten how to inspect declarations with numbers in their names.

[Kim Morrison]

Ah, https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/norm_cast.20leaks.20Int.2EsubSubNat/near/375827016

[Kim Morrison]

open Lean in
elab "#printNum " n:ident i:num : command => do
  let name := Name.num n.getId i.getNat
  let some decl := (← getEnv).find? name | throwError "no such declaration {name}"
  logInfo m!"{name} : {decl.type} :=\n{decl.value?.getD (.bvar 0)}"

#printNum Mathlib.Data.Int.Cast.Basic._auxLemma 3

says

Mathlib.Data.Int.Cast.Basic._auxLemma.3 : ∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℕ),
  -↑(n + 1) = ↑(Int.negSucc n) :=
fun {R} [AddGroupWithOne R] n => Eq.symm (Int.cast_negSucc n)

[Kim Morrison]

It seems simply that norm_cast is (unwisely) willing to apply Int.cast_negSucc backwards.

[Michael Stoll]

I had noticed this some time ago, and it was fixed, but apparently later reverted. I think there is an issue about this. I'll try to dig it up, but right now I'm on a train with slow internet...

[Michael Stoll]

Here on Zulip.

[Michael Stoll]

The issue.

[Ruben Van de Velde]

I was gonna say - didn't I file an issue about this?

[Yaël Dillies]

#11573 ?

[Ruben Van de Velde]

Yeah, Michael linked it as well

[Yaël Dillies]

Sorry, I am shortsighted, colorblind and asleep!