Smart unfolding markers

[abentkamp]

Lean4's smart unfolding relies on the markers markSmartUnfoldigMatch and markSmartUnfoldigMatchAlt. Since they are not present in mathbin definitions, definitional equality checks sometimes loop:

import Mathbin.Data.Int.Basic

example (n : ℕ) (x y : ℤ) : npowRec n x = npowRec n y := rfl
-- maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

[gebner]

What's happening here is that the smart unfolding lemma from Lean 3 is indeed successfully applied, but without reducing to any of the cases. For reference, this is the binported smart unfolding lemma:

def npowRec._sunfold.{u} : {M : Type u} → [_inst_1 : One M] → [_inst_2 : Mul M] → ℕ → M → M :=
fun {M} [One M] [Mul M] ᾰ ᾰ_1 => Nat.casesOn ᾰ (idRhs M One.one) fun ᾰ_1_1 => idRhs M (ᾰ_1 * npowRec ᾰ_1_1 ᾰ_1)

I don't think it will be easy to translate Lean 3 smart unfolding lemmas to Lean 4. Lean 4 now has two smart unfolding markers instead of just one. The second kind, sunfoldMatchAlt, corresponds to the old idRhs. However the first kind, sunfoldMatch, is new. Lean 4 no longer produces Nat.casesOn applications directly, but instead creates matcher definitions. The sunfoldMatch annotation is applied to the matcher application. We might get away with applying sunfoldMatch to Nat.casesOn and register Nat.casesOn as a matcher.