grind_calc

Stream: lean4

[Frédéric Dupuis]

I recently found myself writing the following calc block:

calc _ = z i * x i + (z i + c) * M := by grind only
  _ = z i * x i + z i * M + c * M := by grind only
  _ ≤ z i * x i + z i * M + c * x i := by have := hM i hi; gcongr
  _ = (z i + c) * x i + z i * M := by grind only
  _ = x i + z i * M := by grind only

This struck me as rather inefficient: almost all the steps are just grind only which, unless there's a caching mechanism I'm not aware of, basically restarts grind everytime on more or less the same proof state. To avoid this, we could take advantage of grind's new interactive mode:

grind =>
  have : z i * x i + M = z i * x i + (z i + c) * M
  have : z i * x i + (z i + c) * M = z i * x i + z i * M + c * M
  have : z i * x i + z i * M + c * M ≤ z i * x i + z i * M + c * x i := by
    have := hM i hi; gcongr
  have : z i * x i + z i * M + c * x i = (z i + c) * x i + z i * M

This is basically the same thing, but "inside" a single grind call, and it did feel faster though I didn't run any benchmarks. I think this kind of pattern is very useful, to the point that it might make sense to have syntax for it to avoid having to write the LHS of every line, something like:

grind_calc =>
  _ = z i * x i + (z i + c) * M
  _ = z i * x i + z i * M + c * M
  _ ≤ z i * x i + z i * M + c * x i := by have := hM i hi; gcongr
  _ = (z i + c) * x i + z i * M

Also it would be nice to retain the ability to use the other commands available in interactive mode, like instantiate and so on, in between the lines.

Any thoughts?

[Ruben Van de Velde]

Would it be possible to have a tactic that does all_goals => grind but faster?

[Yury G. Kudryashov]

Why not merge the fist two steps and the last 2 steps into 1 by grind only?

[Frédéric Dupuis]

Sure, I'm not claiming that this example is particularly optimised; indeed the last line was already deleted in the grind => version and the first have can also be removed.

[Floris van Doorn]

This sounds nice. Is there a reason to not just write this as a calc-tactic in grind-mode, so using the syntax below instead of adding a new grind_calc mode?

grind =>
  calc
    a = b
    _ = c
    _ ≤ d := by gcongr
    _ = e

[Andrés Goens]

FWIW, this seems inefficient but it is efficient in a different way: a lot of the information that you might need to get from the first version to the second gets in the way when going from the second to the third (that was kind of the idea of our "guided equality saturation paper" https://dl.acm.org/doi/10.1145/3632900 ).In your example the steps are small so for grind it's easier, but for more complex examples there's definitely value in restarting grind. So in lean egg we had syntactic sugar for precisely that pattern for that reason (lean-egg has the same underlying approach and data structure as grind).

[Frédéric Dupuis]

Floris van Doorn said:

This sounds nice. Is there a reason to not just write this as a calc-tactic in grind-mode, so using the syntax below instead of adding a new grind_calc mode?

Yes, that would be a great option as well!

[Frédéric Dupuis]

Andrés Goens said:

FWIW, this seems inefficient but it is efficient in a different way: a lot of the information that you might need to get from the first version to the second gets in the way when going from the second to the third (that was kind of the idea of our "guided equality saturation paper" https://dl.acm.org/doi/10.1145/3632900 ).In your example the steps are small so for grind it's easier, but for more complex examples there's definitely value in restarting grind. So in lean egg we had syntactic sugar for precisely that pattern for that reason (lean-egg has the same underlying approach and data structure as grind).

Yes, I'm certainly not suggesting this as a replacement for calc mode as it currently exists!