simproc for Fin

Stream: lean4

[Bhavik Mehta]

Do we have a simproc or simp lemma for

example : ((3 : Fin 4) : Nat) = 3 := by
  simp

or related explicit calculations? It seems to me like Fin.isValue is meant to do something like this, but currently (even in Mathlib) I can't see any automatic way of simplifying the lhs without already writing down the rhs.

[Eric Wieser]

rw [Fin.coe_ofNat_eq_mod] works here (docs#Fin.coe_ofNat_eq_mod)

[Eric Wieser]

rewrite [Fin.coe_ofNat_eq_mod] is a little less magic

[Eric Wieser]

Maybe this should be simp?

[Bhavik Mehta]

I just came across that lemma too, but it's marked simp. Why does simp not succeed using it?

[Bhavik Mehta]

Before finding that lemma I also tried making

@[simp] lemma coe_ofNat_of_lt {a b : ℕ} [NeZero b] (h : a < b) :
    ((OfNat.ofNat (no_index a) : Fin b) : ℕ) = a := Nat.mod_eq_of_lt h

which also doesn't work with simp in this example

[Eric Wieser]

I would guess this is all related to the no_index trouble around ofNat (edit: lean4#3684)

[Eric Wieser]

Oh, it's a typo, no_index OfNat.ofNat n should be no_index (OfNat.ofNat n)

@[simp]
theorem coe_ofNat_eq_mod (m n : ℕ) [NeZero m] :
    ((no_index (OfNat.ofNat n) : Fin m) : ℕ) = OfNat.ofNat n % m :=
  rfl

[Eric Wieser]

I always get the precedence of no_index wrong

[Eric Wieser]

#18872

[Bhavik Mehta]

There's two other instances of the pattern no_index OfNat.ofNat n in mathlib, do you want to change those in this PR too?

[Bhavik Mehta]

image.png
(for your convenience!)

[Yakov Pechersky]

We had a norm_fin tactic in mathlib3 that might be in scope for this. And, probably not what you wanted for your use site (you said you don't want to write the rhs), but rfl proves your original example.

[Bhavik Mehta]

Yeah, rfl working is good but I'd really like other simp and rw lemmas to apply afterwards, so rfl isn't really sufficient here unfortunately

[Eric Wieser]

Eric Wieser said:

#18872

I ended up removing @[simp] from this lemma because it's not very confluent. I think your version would be safer.