strict grind only

Stream: lean4

[Patrick Massot]

Now that cc has been moved away from Mathlib, it becomes more urgent to understand how grind could fully replace it. Is there any way to have a strictgrind only that do not use local assumptions that it was not told to use?

[Yury G. Kudryashov]

Is grind fast enough to close all the relevant goals without this restriction?

[Patrick Massot]

This has nothing to do with speed. It's about control.

[Patrick Massot]

I secretly use cc in Verbose Lean where I need to control that students provide the relevant justifications.

[Yury G. Kudryashov]

Can you clear all other assumptions before calling grind only in your wrapper tactic?

[Patrick Massot]

Sure, I could do that, and I even thought about it. But it’s really super inconvenient.

[Kim Morrison]

What is the inconvenience? Just having to implement it, or is there a particular difficulty anticipated?

How about we write verbose_grind_wrapper [X, Y, Z] which:

• checks which of X, Y, Z are names of local hypotheses
• clears all local hypotheses except those (and hypotheses these depend on)
• passes everything that was not a local hypothesis to grind only [...]

Is that the behaviour you want?

[Kim Morrison :bot:]

I've implemented a draft at https://github.com/kim-em/verbose-lean4/blob/grind_strict/Verbose/Tactics/Grind.lean

grind_strict [h1, h2, some_theorem]

Let me know if this matches what you need, or if you'd like adjustments.

[Kim Morrison]

@Patrick Massot, just checking if this satisfies your needs or not.

[Patrick Massot]

Sorry I haven’t found time to investigate yet. I must confess the bot thing is very off-putting too.

[Andrés Goens]

you could also just depend on https://github.com/Komyyy/legacy-cc in Verbose Lean?

[Miyahara Kō]

As for me, it's fine temporarily, but if you can avoid the dependency, I can archive the repository and spend the maintenance time on other things.