simplifying typeclass definitions

Stream: lean4

[Chris B]

What is the right way to simplify/rewrite using typeclass definitions? In Fin.val_zero, I want to simplify (@OfNat.ofNat (Fin (Nat.succ n)) 0 (@Fin.instOfNatFinHAdd n 0)) to the definition of Fin.instOfNatFinHAdd.ofNat, which is Fin.ofNat 0. If I go directly with simp only [OfNat.ofNat], I get a maximum recursion error.

The intermediate thing h0 is a workaround that makes the simplifier happy; the trace output is h0:1000, @OfNat.ofNat (Fin (Nat.succ n)) 0 (@Fin.instOfNatFinHAdd n 0) ==> @Fin.ofNat n 0.

import Mathlib.Data.Nat.Basic
import Mathlib.Algebra.Group.Defs

section Fin

variable {n : Nat}

instance : Zero (Fin n.succ) where
  zero := Fin.ofNat 0

lemma Fin.val_zero : (0 : Fin n.succ).val = (0 : Nat) := by
  have h0 : ∀ x, (OfNat.ofNat x : Fin n.succ) = Fin.ofNat x := by simp [OfNat.ofNat]
  simp only [h0, Fin.ofNat, Nat.zero_mod]

[Gabriel Ebner]

What is the right way to simplify/rewrite using typeclass definitions?

The usual way is to just state the desired rewrite as a lemma:

lemma ofNat_eq : (OfNat.ofNat x : Fin (n+1)) = Fin.ofNat x := rfl

In a similar vein, you can restate lemmas in terms of the canonical representation (i.e., OfNat.ofNat instead of Fin.ofNat):

lemma ofNat_val : (OfNat.ofNat x : Fin (n+1)).val = x % (n+1) := rfl

[Chris B]

@Gabriel Ebner Thanks, that makes sense. I got used to the convenience of being able to write simp [<def>] for definitions and thought classes might have similar behavior without writing explicit lemmas.

[Chris B]

In working with USize more today, the solution of extracting things into lemmas does not work well in some cases. For this: lemma val_zero : (0 : USize).val = (0 : Fin size), where the instance of Zero is defined as instance : Zero (Fin size) := (Nat.succ_pred_eq_of_pos size_positive) ▸ inferInstance, things are really obscured by the fact that size isn't reducible and isn't defined in terms of succ.

Without being able to just reduce what's already in the context of the theorem, it seems like I have set pp.all to true, then extract something about Zero (Fin size), which actually requires Zero (Fin size.pred.succ), and now I need another lemma to relate the two.

[Chris B]

Also where does the recursion depth error for simp only [OfNat.ofNat] come from?