Bizarre bug with grind + norm_cast

Stream: general

[Peter Nelson]

import Mathlib.Data.ENat.Basic

variable {Foo : ℕ∞ → Prop} {Bar : Prop}

example (foo_imp_bar : ∀ x, Foo x → Bar) (h : Foo 2) : Bar := by
  grind -- succeeds

example (foo_imp_bar : ∀ x, Foo x → Bar) (h : Foo 2) : Bar := by
  norm_cast at h
  grind -- succeeds

example (foo_imp_bar : ∀ x, Foo x → Bar) (h : Foo 2) : Bar := by
  norm_cast at h
  norm_cast at h
  -- any larger number of norm_casts succeed but seem to do nothing
  grind -- fails

example (foo_imp_bar : ∀ x, Foo x → Bar) (h : Foo 1) : Bar := by
  norm_cast at h
  -- warning is given that norm_cast did nothing
  grind  -- succeeds

Perhaps this is not quite minimized (I don't know if ENat specifically is a problem), but I am very stumped.

With set_option pp.all true, none of the norm_casts appear to do anything, and so the proof states in all three cases before the grind are identical. Replacing 2 by anything larger gives the same problem.

[Damiano Testa]

The norm_cast calls appear to be adding nested mdata nodes to the expression. I wonder if grind is removing one layer of metadata, but not recursively removing all metadata.

[Notification Bot]

This topic was moved here from #ecosystem infrastructure > Bizarre bug with grind + norm_cast by Kim Morrison.

[Kim Morrison]

That sounds like bugs in both norm_cast (for adding the metadata) and in grind (for not removing it).

[Kim Morrison]

Given norm_cast is also in lean4, hopefully it would not be too hard to minimize. @Peter Nelson, any chance you'd have time to try to reduce this to something not importing Mathlib?

[Peter Nelson]

I think this is minimized as much as possible - mathlib is needed.

import Mathlib.Data.Nat.Cast.Defs

variable {R : Type} [NatCast R] {Foo : R → Prop} {Bar : Prop}

example (foo_imp_bar : ∀ x, Foo x → Bar) (h : Foo 2) : Bar := by
  norm_cast at h
  grind -- succeeds

example (foo_imp_bar : ∀ x, Foo x → Bar) (h : Foo 2) : Bar := by
  norm_cast at h
  norm_cast at h
  grind -- fails

The problem occurs with the tagging of Nat.cast_ofNat as norm_cast, which happens on line 57 of the imported file Mathlib.Data.Nat.Cast.Defs. The bug disappears if the example is placed before this tagging occurs, or if the tagging is removed.

[Peter Nelson]

What is the correct way to inspect the mdata nodes? I had always thought that set_option pp.all true was where the buck stops when it comes to deterministic behaviour.

[Damiano Testa]

I don't know if there is an built-in way for inspecting mdata. I used this custom tactic:

open Lean Elab Tactic in
elab "show_expr " id:ident : tactic => withMainContext do
  let ctx ← getLCtx
  let some var := ctx.findFromUserName? id.getId | throwError "No variable called {id}"
  dbg_trace var.type

example (foo_imp_bar : ∀ x, Foo x → Bar) (h : Foo 2) : Bar := by
  norm_cast at h
  norm_cast at h
  show_expr h
  grind -- fails

[Damiano Testa]

Thanks to your find, here is a minimization:

namespace Nat

class AtLeastTwo (n : Nat) : Prop where
  prop : 2 ≤ n

instance {R} {n : Nat} [NatCast R] [AtLeastTwo n] :
    OfNat R n where
  ofNat := n.cast

@[norm_cast] theorem cast_ofNat {R} {n : Nat} [NatCast R] [AtLeastTwo n] :
    (Nat.cast (no_index (OfNat.ofNat n)) : R) = no_index (OfNat.ofNat n) := rfl

instance : AtLeastTwo 2 where prop := Nat.le_refl _

variable {R : Type} [NatCast R] {Foo : R → Prop} {Bar : Prop}

example (foo_imp_bar : ∀ x, Foo x → Bar) (h : Foo 2) : Bar := by
  norm_cast at h
  grind -- succeeds

example (foo_imp_bar : ∀ x, Foo x → Bar) (h : Foo 2) : Bar := by
  norm_cast at h
  norm_cast at h
  grind -- fails

[Jovan Gerbscheid]

The #25500 by @Eric Wieser adds pretty printing for mdata

[Kim Morrison]

Oh, I forgot to say, this has been fixed now.