grind with theorems used

Stream: Is there code for X?

[Snir Broshi]

Kim recently added grind +premises (lean#10920), which I think calls grind with the suggestions from apply?, and then added a linter to try grind +premises at every step of an existing proof (#30808).

Instead of suggestions, for a finished proof is there a way to ask grind to use everything that follows it in the proof?
For example, let's say I want to attempt to replace the last line of this proof with grind:

import Mathlib
lemma Finset.powersetCard_eq_empty' {α : Type*} {n : ℕ} {s : Finset α} : powersetCard n s = ∅ ↔ s.card < n := by
  refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩
  contrapose!
  exact fun h ↦ nonempty_iff_ne_empty.1 <| (exists_subset_card_eq h).imp <| by simp

Then it'll call grind [nonempty_iff_ne_empty, exists_subset_card_eq, Exists.imp, mem_powersetCard, imp_self, implies_true] since the first 3 are used in the last line and the simp uses the rest.
(it also needs to remove parameters that cause "failed to find an usable pattern" or "this parameter is redundant")

Does this exist / is planned to exist?

[Floris van Doorn]

lean4#10920 (also permises -> premises)

[Snir Broshi]

If this does not exist, is it possible to build?
I'm not sure how difficult it is to start developing tactics, but I'm willing to try if this is not already in the works

[Kim Morrison]

grind +premises does not call apply?, but instead uses a configurable premise selector.

Currently lean doesn't ship with a useful built in premise selector (it ships with a naive implementation of MePo, accessible via set_premise_selector Lean.PremiseSelection.mepoSelector (useRarity := false), which gives terrible suggestions!) We're working on this, but if others want to write more premise selectors that is wonderful!

There is a quite good neural premise selector, which supports this API, from the PKU group (@Yutong Wang), which we're hoping to make easily accessible to Mathlib users soon/

[Kim Morrison]

I also like your idea of pulling out all constants from the remaining proof. I wonder how to best implement it... We could write grindify which eats a tacticSeq, replays that tactic, extracts constants, and then tries running grind with those as parameters.

@Snir Broshi, does that sound like something you could experiment with? I can put it (low down) on my TODO list as well.

[Snir Broshi]

I've never done metaprogramming so far, but I'll give it a shot. Do you happen to have an existing tactic that does a similar thing that I can use as a reference? The closest one I have in mind is suffices but just because it takes in a tacticSeq

[Kenny Lau]

how do you propose the syntax to be? as in, in the finished products, what steps exactly would you take to transform that final line exact ... into the desired grind [...?

[Snir Broshi]

I was thinking of adding a line with grind by (or grindify as Kim suggested) and indenting the rest of the proof by one level, and then it would call grind with extra lemmas.
And possibly having something similar to simp? which let's you click in the info view to replace the entire thing with the equivalent grind call.

[Snir Broshi]

lemma Finset.powersetCard_eq_empty' {α : Type*} {n : ℕ} {s : Finset α} : powersetCard n s = ∅ ↔ s.card < n := by
  refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩
  contrapose!
  grindify by
    exact fun h ↦ nonempty_iff_ne_empty.1 <| (exists_subset_card_eq h).imp <| by simp

---

Try this:
  [apply] grind [nonempty_iff_ne_empty, exists_subset_card_eq, Exists.imp, mem_powersetCard, imp_self, implies_true]

[Kenny Lau]

@Snir Broshi i can write a skeleton for you:

import Mathlib

open Lean Meta Elab Tactic

elab "grindify?" colGt t:tacticSeq : tactic => withMainContext do
  logInfo t

lemma Finset.powersetCard_eq_empty' {α : Type*} {n : ℕ} {s : Finset α} : powersetCard n s = ∅ ↔ s.card < n := by
  refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩
  contrapose!
  grindify?
    exact fun h ↦ nonempty_iff_ne_empty.1 <| (exists_subset_card_eq h).imp <| by simp
    exact fun h ↦ nonempty_iff_ne_empty.1 <| (exists_subset_card_eq h).imp <| by simp
    exact fun h ↦ nonempty_iff_ne_empty.1 <| (exists_subset_card_eq h).imp <| by simp

[Aaron Liu]

Don't forget to with main context

[Kim Morrison]

You will probably need the brand new grind +lax which I just wrote, that means that when you write grind +lax [X, Y, Z], any bad parameters (don't exist, can't find good grind patterns, etc) get silently ignored.

[Kenny Lau]

(edited with aaron's suggestion)

[Kim Morrison]

(Although this is probably only available on nightly toolchains, it didn't make it into v4.25.0-rc2)

[Yutong Wang]

One can always test the premise selector from reap by set_premise_selector (You need to require reap or on correct mathlib branch)

import Mathlib
import Reap
set_premise_selector reapSelector
open Finset Set

/-- If two finite sets are subsets of each other,
then they have the same cardinality -/
example (s t : Finset ℕ) (h : s ⊆ t)
  (h' : t ⊆ s) : #s = #t := by
  suggest_premises
  -- Premise suggestions: [Finset, Finset.card, And, Eq.symm, Iff.mpr, Finset.empty]
  sorry

But I didn't try how these premises work for grind. Maybe need to checkout grind_premise branch to test it?

[Yutong Wang]

btw, we are planning to develop an automatic pipeline to update premise selection database to at least match every mathlib release. So maybe we indeed need a standard benchmark for downstream usage like grind to see the actual benefits.