Tactic to get rid of `Nat.cast`to `Fin m`

Stream: mathlib4

[Robin Carlier]

When working on #21745 and #21746, I ran into the annoying situation where I would end ups with casts of a : Nat to Fin m while having a context "easily" proving that a < m , and had to manually rewrite it to ⟨a, h⟩ using something like

lemma fin_natCast_of_lt (m a : ℕ) (ha : a < m) (hm : NeZero m) : (↑a : Fin m) = ⟨a, ha⟩ := by
  ext
  rw [Fin.val_natCast, Nat.mod_eq_of_lt ha]

This is probably a design issue on my end that I ended up with such casts in the first place, but it made me feel like some kind of tactic could automate getting rid of those, and I ended up writing the following. It’s basically a wrapper around rwand omegathat looks for occurences of casts from a : Nat to Fin m (for a in a list of Nat-valued terms provided as argument to the tactic), tries to find a proof that a < m using omega, and replace the cast by a better term using that proof.

I am rather new to metaprogramming so I would greatly appreciate overall comments on the code/ the way this kind of things are done normally.

Arguably, this is a very specific tactic for a very specific application in a situation people should avoid ending up in the first place, so is it worth cleaning this up and try to PR it or would that be unneeded?

[Aaron Liu]

I broke it... Looks like it can't handle forall expressions. Maybe if you test it a bit more.

-- PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:366:22: loose bvar in expression
-- backtrace:
example (a : ℕ) (m : ℕ) [NeZero m] (ha : a < m) :
    ∀ (v : Vector Nat (a : Fin (m + 1))), v = v := by
  fin_natcast [a]
  intro v
  rfl

[Robin Carlier]

Well, that says a lot about my meta skills :sweat_smile:, guess I indeed need to test more...

[Robin Carlier]

matching on e rather than on whnfR e at line 13 seems to fix this particular case, but I can’t say I understand why...

[Aaron Liu]

The problem seems to be in partial def collectTargets calling whnfR on expressions that may contain loose bvars. You can check if an expression has loose bvars with docs#Lean.Expr.hasLooseBVars, and skip the ones that do (this is what docs#Lean.Meta.kabstract, the machinery behind rw, does).

[Robin Carlier]

Yup, trying around it looks like overall I need to do better on the parsing. It performs badly on stuff like

example (a : ℕ) (m : ℕ) [NeZero m] (ha : a < m) :
    ∀ x : ℕ, ∀ h : a < x, ∀ (v : Vector Nat (a : Fin (x + 1))), v = v := by
  fin_natcast [a]
  intros; rfl

So this is very much not ready yet