Grind sets? (equivalent of simp sets for `grind`)

Stream: lean4

[Théophile]

Hello! I have a bunch of theorems I would like to use with grind's e-matching feature, but only in some specific scenarios, therefore I would like grind to refrain from instantiating them unless I configure it to do so. Does this feature exists? I found the function registerGrindAttr which shares a similar name with registerSimpAttr, but it is private and does not seem to do something similar.

I the meantime I have a workaround using a trick I also employ in other SMT-based verifiers, it emulates having grind sets although it is a bit hacky (see on Lean 4 Web)

def f_lemmas_enabled (_: Unit): Prop := True
theorem enable_f_lemmas: f_lemmas_enabled () := by simp [f_lemmas_enabled]

axiom f: Nat -> Nat
axiom f_is_id (n: Nat) (dummy: Unit): f n = n

grind_pattern f_is_id => f n, f_lemmas_enabled dummy

example (n: Nat): f (f n) = n := by
  fail_if_success grind -- f_is_id is not instantiated
  have := enable_f_lemmas
  grind

[Kim Morrison]

You can used scoped.

[Théophile]

Thanks, I was not familiar with this attribute. I looked through the documentation, however it seems that we can't use scoped grind patterns outside the namespace they are scoped in (this is somewhat expected from scoped I guess)? How can we use the scoped grind pattern outside the corresponding namespace? See example below.

My usecase is that I have grind patterns associated to some theorems that would in general be instantiated a lot, but in practice they are useful only in some specific proofs, so I want to enable them only in that case. I relied the trick I've shown above in other SMT-based program verifiers with success in the past, but wondered if there was a cleaner option in Lean (otherwise if there is no cleaner option, the trick is good enough for me).

axiom f: Nat -> Nat

namespace Test

@[scoped grind]
axiom f_is_id (n: Nat): f n = n

-- `grind` works here
example (n: Nat): f (f n) = n := by
  grind

end Test

example (n: Nat): f (f n) = n := by
  -- how to make `grind` work here?
  fail_if_success grind
  sorry

-- we need to reopen the namespace to prove our theorem
namespace Test

-- `grind` works here again
example (n: Nat): f (f n) = n := by
  grind

end Test

-- also works
theorem Test.toto (n: Nat): f (f n) = n := by
  grind

[Alex Meiburg]

You can use open scoped Test in any other section, and then they'll be available there. You can also run open scoped Test in theorem foo :...to have it open just for that one theorem!

[Théophile]

Ah, but then all grinds in the proof will instantiate the theorem. I hoped to be able to do something such as annotating lemmas with e.g. @[grind f_lemma] and use such theorems only when using e.g. grind [f_lemmas] (which I can do with the trick in the first post).

Anyway, thank you for your answers, I now have a better picture of the different ways to achieve my goal!

[Kim Morrison]

You can break your proof into lemmas (always a good idea, as soon as the proof is more than 10 lines! :-) and use open scoped ... in ... only for those lemmas that need the additional grind annotations.

[Kyle Miller]

If I'm not mistaken, using open scoped ... in grind at the tactic level should work too.

[Théophile]

Thanks, indeed! (MWE at the end for posterity)
This is more convincing and doesn't have drawbacks compared to the initial hack I've shown.

For my own curiosity, I am wondering: if this is the official way to implement grind sets, it should also work to implement simp sets, so why does simp has built-in support for simp sets and not grind?

axiom f: Nat -> Nat

@[scoped grind]
axiom Test.f_is_id (n: Nat): f n = n

example (n: Nat): f (f n) = n := by
  fail_if_success grind
  open Test in
  grind

[Kyle Miller]

Some speculation on simp sets:

• Simp sets are a fairly old feature (I remember them in Lean 3). Possibly in Lean 4 they were implemented even before open scoped.
• Simp sets seem to be more efficient than open scoped (though I didn't measure) since simp doesn't merge simp sets into a single simp set during its operation; each simp set is queried one at a time to see if they apply.
• There are no grind sets because they are not implemented, and open scoped works. I don't know if there's a reason they weren't implemented beyond the fact it would take more engineering time.

[Théophile]

Ok, thanks! I realize I have one last question about this: in my usecase I call grind from a custom tactic (i.e. code in TacticM) I am writing, how do I implement the open trick in the TacticM world? I don't know what to do because open ... in seems to be primarily for elaboration and doesn't change the proof term.

    -- how to do add `open Test in` here for auxGoal?
    let _ ← grind auxGoal {} false #[] (pure ())

(with the hack I've shown in the first post, it's just a matter of doing auxGoal.assert on enable_f_lemmas)
Note: I use grind to solve automatically auxiliary goals generated by my tactic, probably not recommended, but for a first proof-of-concept it's good enough, and much easier than writing a full-blown tactic for these specific auxiliary goals (and they all should be straightforward for grind)

[Kyle Miller]

If you "go to definition" on open ... in it will bring you to the elaborator, and I suppose you could copy how it does it.

Alternatively, rather than use the meta interface, you could evalTactic some syntax. There's also Lean.Elab.Term.runTactic, which is more straightforward. For both of these you create a metavariable whose type is auxGoal.

[Kyle Miller]

Are you wanting grind sets because you want it to be user-extensible?

Lean.Elab.Tactic.grind lets you pass in grind parameters directly if not.

[Robin Arnez]

try
  pushScope
  activateScoped `myNamespace
finally
  popScope

should do the trick

[Théophile]

@Robin Arnez yes that works, thanks!
@Kyle Miller indeed I want it to be user-extensible, this is why I want grind sets

[Kim Morrison]

I've also recently wanted to run open ... in tac in TacticM. Having an out of the box solution for this would be nice.

[Théophile]

In case it is useful to anyone, I wrote the following utility function in my project

/--
  Opens a namespace (similarly to `open ... in` in tactics).
  Useful to enable scoped lemmas (e.g. for `grind` or `simp`).
-/
def withOpenIn
  [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] [MonadFinally m]
  (namespaceName : Name) (k : m α): m α
  := do
    try
      pushScope
      activateScoped namespaceName
      k
    finally
      popScope

[Théophile]

And to conclude if someone has the same problem as me and reads this thread in the future, when working in a namespace: I first found it annoying to have to close it in order to add my lemma in the correct namespace, but discovered that we can simply use _root_ like this:

namespace Test

-- ...

axiom f: Nat -> Nat

@[scoped grind]
axiom _root_.Bla.GrindNamespace.f_is_id (n: Nat): f n = n

-- ...

end Test

instead of

namespace Test

-- ...

axiom f: Nat -> Nat

end Test -- ugh

@[scoped grind]
axiom Bla.GrindNamespace.f_is_id (n: Nat): Test.f n = n

namespace Test -- ugh

-- ...

end Test