Question on `grind` multi-pattern matching with `a < b`

Stream: general

[Ayhon]

All code

I had a question about grind and multipatterns. I would like to teach grind to work with compare, in particular by recognizing that if a < b is in the context, then compare a b = .lt. At first, I thought it would be enough to define a multipattern where both a < b and compare a b must match. However, although this pattern is accepted, it doesn't appear to do what I would expect.

theorem foo(a b: Int): a < b → compare a b = .lt := by grind [Int.compare_eq_lt]

local grind_pattern foo => a < b, compare a b

example(n: Int): n < 0 → compare n 0 = .lt := by
  grind -- Failure

If I remove a < b from my statement, the proof goes on fine. But why is grind getting hung up with the added a < b?

[Robin Arnez]

Look at the goal state in the failure of grind:

error: `grind` failed
case grind
n : Int
h : n + 1 ≤ 0
h_1 : ¬compare n 0 = Ordering.lt
⊢ False

grind normalized n < 0 to n + 1 ≤ 0 so it doesn't find an <. In general, it's best not to pattern on arithmetic stuff, in particular on Nat and Int (including <, ≤, +, *) because grind may decide to do whatever kind of normalization to those.

[Ayhon]

But even putting the goal as a + 1 ≤ b doesn't fix the issue

[Ayhon]

I understand how, even if grind closed my goal when adding the parameter a + 1 ≤ b, this would not be still not be ideal. But I'm surprised that this doesn't seem to be the solution either. So there's something happening here which I don't understand

[Ayhon]

Some exhaustive checking I've tried: here

grind_pattern ex_lt =>      a + 1 ≤ b,          compare a b
grind_pattern ex_lt =>          a < b,          compare a b
grind_pattern ex_lt =>          b > a,          compare a b
grind_pattern ex_lt =>          b ≥  a + 1,     compare a b
grind_pattern ex_lt =>   -1*a - 1 ≥  -1*b,      compare a b
grind_pattern ex_lt =>       -1*a > -1*b,       compare a b
grind_pattern ex_lt =>       -1*b < -1*a,       compare a b
grind_pattern ex_lt =>       -1*b ≤ -1*a - 1,   compare a b

[Jakub Nowak]

This works

theorem foo(a: Int): a + 1 ≤ 0 → compare a 0 = .lt := by grind [Int.compare_eq_lt]

local grind_pattern foo => a + 1 ≤ 0, compare a 0

example(n: Int): n < 0 → compare n 0 = .lt := by
  grind -- Failure

[Ayhon]

I'm confused. What do you mean by "it works"?

[Jakub Nowak]

I forgot to remove Failure comment, but now grind does prove the goal.

[Ayhon]

Ah, I see

[Jakub Nowak]

It looks to me like grind's normalization is actually hindering us, instead of helping, but maybe it's because we're using grind wrong?

[Ayhon]

A friend suggested that I'd probably want to use gring_pattern constraints, probably guard.
https://github.com/leanprover/lean4/blob/38c401cf3bd02d1ebf7dcf134f941aee08fbc2db/src/Lean/Meta/Tactic/Grind/Parser.lean#L108

[Jakub Nowak]

Hmm, that could work.

[Ayhon]

Not available in 4.26 though :/

[Jakub Nowak]

You can test Lean nightly at https://live.lean-lang.org/#project=lean-nightly&codez=C4Cwpg9gTmC2AEAzCEAUBDeAjAXPAkgHbACUemAPNvIEmE8AxhLAA7ozyZbwC88AdABtg8HLywBPeAHMoAS0IATeAG0iwPoxZswAfTABHHUIC6AKFMBnMMB0RmwWRELxgUdPTB8Z8hXzjpgehA+eQtgdEIPFygAVzBzAQh6dAFpOUUdVmBgMChnZAgeAD4GJlZ2TngAd3AYU3hpGLYlSmxzMAAPdBYBMFRCPDUyeGcqAAZaUq12ZwneQWFRbHF6tJ94AFoN+AAxdFkBGLqgA by switching to nightly in the upper-right corner.

[Jakub Nowak]

Notice, how this fails:

theorem foo(a b: Int): a < b ↔ compare a b = .lt := by grind [Int.compare_eq_lt]

set_option trace.grind.ematch.instance true

local grind_pattern foo => compare a b where
  guard a < b

example(n: Int): compare n 1 = .lt → compare n 2 = .lt := by
  grind -- Failure

While this doesn't:

theorem foo(a b: Int): a < b ↔ compare a b = .lt := by grind [Int.compare_eq_lt]

set_option trace.grind.ematch.instance true

local grind_pattern foo => compare a b

example(n: Int): compare n 1 = .lt → compare n 2 = .lt := by
  grind

[Ayhon]

Hmm, :/

[Jakub Nowak]

I think that's good and what you expected? In the first case grind didn't finish the proof, because it never tried to use foo. The guard a < b prevented it from using it.

[Ayhon]

Oh, my bad! I hadn't noticed how you changed the examples (tbh, I was checking your messages while playing factorio, I have stopped now and I could look at it with more pause)

[Ayhon]

Yeah, that's a bit what I was expecting my multi-patterns to achieve

[Jakub Nowak]

Ah, sorry, I forgot to also mention, that it works with your original example:

theorem foo(a b: Int): a < b ↔ compare a b = .lt := by grind [Int.compare_eq_lt]

set_option trace.grind.ematch.instance true

local grind_pattern foo => compare a b where
  guard a < b

example(n: Int): n < 3 → compare n 3 = .lt := by
  grind

[Ayhon]

So I guess then that what the guard enables you to do is handle the problem of grind normalizing expressions a bit more gracefully.

[Jakub Nowak]

It can't prove this though:

theorem foo(a b: Int): a < b → compare a b = .lt := by grind [Int.compare_eq_lt]

set_option trace.grind.ematch.instance true

local grind_pattern foo => compare a b where
  guard a < b

example(n: Int): n < 4 → compare n 3 = .lt := by
  grind -- Failure

So I'm guessing that grind doesn't make any special effort to try and prove the guard expression?

[Ayhon]

Hmm, interesting

[Jakub Nowak]

Ah, wait, no, it's me being dumb, that example was just false. This works:

theorem foo(a b: Int): a < b → compare a b = .lt := by grind [Int.compare_eq_lt]

set_option trace.grind.ematch.instance true

local grind_pattern foo => compare a b where
  guard a < b

example(n: Int): n < 2 → compare n 3 = .lt := by
  grind

[Ruben Van de Velde]

A theorem being false is a common cause for it being hard to prove

[Ayhon]

I would even argue "the most common"