grind with Fin literals

Stream: lean4

[Frédéric Dupuis]

I'm currently having a very hard time getting grind to deal with Fin, i.e. things like proving that Finset.Iic (b - 1) = Finset.Iio b under appropriate conditions. I think I've boiled down the issue to the fact that grind does not play well with literals of type Fin n. For instance:

example {n : Nat} [NeZero n] (hn : 2 ≤ n) : (1 : Fin n).val = 1 := by
  grind

doesn't work, and there doesn't seem like there's an easy way to tag lemmas to make this work. Is there a quick way to fix this?

[Robin Arnez]

grind needs to know docs#Fin.coe_ofNat_eq_mod and docs#Nat.mod_eq_of_lt for this:

theorem Fin.coe_ofNat_eq_mod (m n : Nat) [NeZero m] : (no_index (OfNat.ofNat n : Fin m)).val = (no_index (OfNat.ofNat n : Nat)) % m := rfl

grind_pattern Fin.coe_ofNat_eq_mod => (OfNat.ofNat n : Fin m).val

grind_pattern Nat.mod_eq_of_lt => a % b where
  not_value a
  guard a < b

grind_pattern Nat.mod_eq_of_lt => a % b where
  not_value b
  is_value a -- prevents overlaps with the above `grind_pattern`
  guard a < b

example {n : Nat} [NeZero n] (hn : 2 ≤ n) : (1 : Fin n).val = 1 := by
  grind

See also lean4#11584

[Frédéric Dupuis]

Nice, thanks!