Grind manual arguments patterns

Stream: general

[Moritz R]

I have had the situation that a proof using grind [mylemma] succeeded, but tagging the lemma with @[grind] (and calling grind) didn't.
So I am wondering which patterns are chosen for manual arguments to grind and if they can be viewed.

[Moritz R]

I didn't find this info in the docs, maybe it can be added if i really didn't just miss it

[Kim Morrison]

Usually this should work as you expected, so I would be interested in seeing a #mwe if it's possible to construct one.

In this case, usually set_option trace.grind.ematch.pattern true is helpful, as it will tell you which pattern was selected.

[Kim Morrison]

There's still a small manual step to write a grind_pattern command to reproduces a pattern you see from that trace option.

Are you using an old version of Lean, btw? If you tag a lemma with plain @[grind] you should always get a message about the different sigils you could use to select a particular pattern. (At least for theorems, for definitions @[grind] is expected.)

[Moritz R]

import Mathlib.Tactic

inductive Tree23 (α : Type u)
| nil
| node2 (l : Tree23 α) (a : α) (r : Tree23 α)
| node3 (l : Tree23 α) (a : α) (m : Tree23 α) (b : α) (r : Tree23 α)

namespace Tree23

universe u
variable {α : Type u}

def height : Tree23 α  → ℕ
| nil => 0
| node2 l _ r => max (height l) (height r) + 1
| node3 l _ m _ r => max (height l) (max (height m) (height r)) + 1

lemma heightNil : height (nil : Tree23 α) = 0 := by simp [height]

def complete : Tree23 α  → Bool
| nil => true
| node2 l _ r => height l = height r ∧ complete l ∧ complete r
| node3 l _ m _ r =>
  height l = height m ∧ height m = height r ∧ complete l ∧ complete m ∧ complete r

@[grind]
lemma not_nil_height_pos (t : Tree23 α) : t ≠ nil → height t > 0 :=
  by induction t <;> simp [height]

set_option trace.grind.ematch.pattern true
/- Can't remove `not_nil_height_pos` from the grind call, altough it is annotated with `grind`.
   Annotating with `grind .` also doesn't work. Annotating with `grind! .` does work.
   How does grind decide what patterns are used in a manual call? -/
lemma failhere {l r : Tree23 α} (h : (l.node2 a r).complete = true) (hl : ¬l = nil) :
  r ≠ nil := by grind [complete, heightNil, not_nil_height_pos]

end Tree23

Here is a smaller example of what i saw.

[Moritz R]

It looks to me, as if in a manual grind call, it just adds the generated patterns for all modifiers?
If this is true, i just want it to be added to the grind docs and then this is expected behavior

[Moritz R]

until now i would have thought, that probably grind [lemma] does the same as @[grind] or as @[grind .]

[Kim Morrison]

As you see, that's incorrect.

I think you must be using an old version, as I asked above?

On

@[grind]
lemma not_nil_height_pos (t : Tree23 α) : t ≠ nil → height t > 0 :=
  by induction t <;> simp [height]

I see the message

Try these:
  [apply] [grind .] for pattern: [@LE.le `[ℕ] `[instLENat] `[1] (@height #2 #1)]
  [apply] [grind =>] for pattern: [@nil #2, @LE.le `[ℕ] `[instLENat] `[1] (@height _ #1)]
  [apply] [grind! .] for pattern: [@height #2 #1]
  [apply] [grind! =>] for pattern: [@nil #2, @height _ #1]

which is asking you to choose which pattern you want.

As an argument to grind, it picks the "more aggressive" grind! . pattern.

[Moritz R]

I used Lean 4 Web, on the most recent version availible

[Moritz R]

image.png
This is the message from the set_option trace.grind.ematch.pattern true and it prints exactly the same as the Try these suggestions (with duplicates)

[Moritz R]

How should i have seen this as incorrect? I thought maybe the duplicates belong to additional modifiers that aren't shown in the Try these, since they would be duplicated else

[Moritz R]

Kim Morrison schrieb:

As an argument to grind, it picks the "more aggressive" grind! . pattern.

That's the answer i was looking for. Thank you :) Can you also put this into the docs, please?

[Moritz R]

i listed "@[grind] does nothing" out of confusion, since e.g. that also does something, but yes it shouldn't here

[Moritz R]

Moritz R schrieb:

image.png
This is the message from the set_option trace.grind.ematch.pattern true and it prints exactly the same as the Try these suggestions (with duplicates)

What does this output tell me? Because there are 4 different patterns listed, but you say it should only use 1.

[Moritz R]

Sorry if im being a bit dense rn

[Kim Morrison]

Do you see the message on the @[grind] annotation? It is telling you that you should replace @[grind] with one of the four options it suggests, by clicking on one of the "Try this:" suggestions.

[Moritz R]

Yes, that one i understand. The other message which stems from the (traced) grind call with the manual arguments (see my screenshot above) is unclear to me. Why is there 6 patterns (4 when deduplicated) printed from that call?