grind no error, but not using lemma

Stream: general

[Moritz R]

When writing a manual grind pattern, grind doesn't complain, but also doesn't use it.
When trying to tag the lemma with @[grind ->] one gets invalid grind forward theorem, theorem mytheorem does not have propositional hypotheses
When trying to tag the lemma with@[grind?] one gets invalid grind theorem, failed to find an usable pattern using different modifiers

class Interpretation (F M : Type u) where
  nonempty : Nonempty M
  data_arg : M → M

@[grind →]-- invalid `grind` forward theorem, theorem `mylemma` does not have propositional hypotheses
theorem mytheorem {F M : Type u} [Interpretation F M] :
    Nonempty M := Interpretation.nonempty F

grind_pattern mytheorem => Interpretation F M -- succeeds but is not used?

theorem mytheorem2 {F M : Type u} [Interpretation F M] :
    Nonempty M := by grind -- `grind` failed

1. in `mytheorem` does not have propositional hypotheses is it meant does not have any prop hyps or does not have only prop. hyps.?
2. Are prop. hyps the elements that have type Prop or the elements of elements that have type Prop (i.,e. proofs)?
3. Is Interpretation.nonempty not a propositional hypothesis because it needs to take F and M?
4. An error on my grind_pattern would be nice. Also a very short doc-string on grind_pattern to remember which way the names and Terms go would be nice.
5. Can i use grind effectively for this any other way?

[Jakub Nowak]

Moritz R said:

Also a very short doc-string on grind_pattern to remember which way the names and Terms go would be nice.

You can hover over grind_pattern in an editor to see its doc-string.

[Jakub Nowak]

grind can only work with equalities, so I'm not sure if you can use grind for this. Nvm, grind treats Nonempty M as just Nonempty M = True so it can work with it too.

You can use aesop instead:

import Mathlib

class Interpretation (F M : Type u) where
  nonempty : Nonempty M
  data_arg : M → M

@[aesop unsafe]
def mytheorem {F M : Type u} (h : Interpretation F M) : Nonempty M :=
  Interpretation.nonempty F

theorem mytheorem2 {F M : Type u} [Interpretation F M] :
    Nonempty M := by aesop

But I would also be interested in an answer of someone more experienced with grind whether it's possible with grind.

[Jakub Nowak]

Hm, but this works. :thinking:

import Mathlib

@[grind]
class Interpretation (F M : Type u) where
  nonempty : Nonempty M
  data_arg : M → M

theorem mytheorem2 {F M : Type u} [Interpretation F M] :
    Nonempty M := by grind

[Jakub Nowak]

So it looks like grind is able to insert Nonempty M intro e-matching tree if I mark class Interpretation (F M : Type u) with @[grind]. But I have no idea how to instruct grind to do so from the definition like theorem mytheorem {F M : Type u} (h : Interpretation F M) : Nonempty M. Does someone know how to do that?

[Moritz R]

Jakub Nowak schrieb:

Hm, but this works. :thinking:

import Mathlib

@[grind]
class Interpretation (F M : Type u) where
  nonempty : Nonempty M
  data_arg : M → M

theorem mytheorem2 {F M : Type u} [Interpretation F M] :
    Nonempty M := by grind

oh this is so bleeding edge, that it fails on mathlib stable but succeeds on latest mathlib.
Same for the grind_pattern docstring not showing up for me.