Add Subtype.property to grind?

Stream: lean4

[Jakub Nowak]

def Fin2 := { n : Nat // n < 2 }

/--
error: `grind` failed
case grind
n : Fin2
h : 2 ≤ n.val
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] 2 ≤ n.val
  [eqc] True propositions
    [prop] 2 ≤ n.val
  [cutsat] Assignment satisfying linear constraints
    [assign] n.val := 2
-/
#guard_msgs in
example (n : Fin2) : n.val < 2 := by
  grind

example (n : Fin2) : n.val < 2 := by
  grind [Subtype.property]

Should we add [grind .] attribute to Subtype.property so it can solve goals like this?

[Robin Arnez]

I mean this would work with actual subtypes and e.g. if you marked Fin2 an abbrev. In this case, you used Subtype.val on a Fin2 though which, to grind, is not a subtype. So here the better option would be to avoid the defeq abuse and define the necessary functions and lemmas yourself:

def Fin2 := { n : Nat // n < 2 }
def Fin2.val (x : Fin2) : Nat := x.1

@[grind! .]
theorem Fin2.lt (x : Fin2) : x.val < 2 := x.2

example (n : Fin2) : n.val < 2 := by
  grind

[Wrenna Robson]

Note that Fin2 already has a meaning in Mathlib (though I think in practice it's somewhat deprecated?)... also is there a reason you aren't using Fin 2?

[Jakub Nowak]

Wrenna Robson said:

is there a reason you aren't using Fin 2?

It's example for #mwe.

[Wrenna Robson]

Aha.

[Wrenna Robson]

Yeah I assume the issue is that grind can't see through the def.

[Jakub Nowak]

But I agree with @Robin Arnez. grind probably shouldn't even see past the definition in the first place. The fact that adding Subtype.property to grind set helped me solve the goal is a bit of a defeq abuse as Robin called it.

[Kim Morrison]

Surely we have grind_pattern Subtype.property => self.val somewhere!?! I'm sure I added that way back, but I can't find it. :-(

[Jakub Nowak]

Kim Morrison said:

Surely we have grind_pattern Subtype.property => self.val somewhere!?! I'm sure I added that way back, but I can't find it. :-(

Can't find it either. But is it needed? This works fine:

abbrev Fin2 := { n : Nat // n < 2 }

example (n : Fin2) : n.val < 2 := by
  grind only