Writing theorems about ofNat

Stream: lean4

[Eric Wieser]

Is there a way of writing this lemma such that it doesn't introduce superfluous ofNat wrappers?

def Int.factorial : Int → Int
| negSucc _ => 0
| (0 : Nat) => 1
| (n + 1 : Nat) => (n + 1) * factorial n
termination_by n => n.toNat

theorem Int.factorial_ofNat_succ (n : Nat) :
  Int.factorial (OfNat.ofNat <| n.succ) = OfNat.ofNat n.succ * Int.factorial (OfNat.ofNat n) := sorry

-- set_option pp.natLit true
-- set_option pp.explicit true
example : Int.factorial 3 = 6 := by
  rw [Int.factorial_ofNat_succ]
  -- want `3 * Int.factorial 2 = 6`, not
  guard_target =ₛ OfNat.ofNat (Nat.succ 2) * Int.factorial (OfNat.ofNat 2) = 6
  -- aka
  guard_target =ₛ OfNat.ofNat (Nat.succ (OfNat.ofNat <| nat_lit 2)) * Int.factorial (OfNat.ofNat (OfNat.ofNat <| nat_lit 2)) = 6
  sorry

example : 3 * Int.factorial 2 = 6 := by
  rw [← Int.factorial_ofNat_succ]
  -- want `Int.factorial 3 = 6`, not
  guard_target  =ₛ Int.factorial (OfNat.ofNat (Nat.succ 2)) = 6
  sorry

[Eric Wieser]

The context is docs#Real.Gamma_ofNat_eq_factorial, which seems to follow the antipattern of using ofNat on one side of the equation, and skipping it on the other. Despite this, the lemma actually half-works as intended!

import Mathlib

set_option pp.natLit true
example (x) (hx : Nat.factorial 36 = x) : Real.Gamma 37 = x := by
  rw [Real.Gamma_ofNat_eq_factorial] -- miraculously does the right thing
  guard_target =ₛ (Nat.factorial 36 : ℝ) = ↑x
  rw [← Real.Gamma_ofNat_eq_factorial] -- makes a mess
  -- goal is `Real.Gamma (OfNat.ofNat (36 + 1)) = x`

[Eric Wieser]

Without having a clear view of what is going on here, one possible fix might be to change ofNat to take a

structure NatLit where lit : Nat

and have Meta.isDefeq handle this specially to always assign {lit := nat_lit n} to such terms and never {lit := OfNat.ofNat _}