Feasibility of an `exact?` tactic exploring two lemmas deep?

Stream: new members

[Isak Colboubrani]

The exact? tactic is useful when there is a single lemma that can immediately solve the current goal. Is there a comparable mechanism for situations where exactly two lemmas, used together, suffice to close the goal?

I suspect a naïve approach—exploring all possible pairs of lemmas, i.e. $n^2$ combinations—would be prohibitively slow. In absolute terms, roughly how slow would this be? Are there any clever heuristics or pruning strategies that would reduce the search space enough to handle simpler “two-lemma” scenarios in a reasonable time?

Two simple examples:

import Mathlib
example (p : ℕ) (h : Fact p.Prime) : Prime p := by exact_2? -- would suggest `exact Nat.prime_iff.mp (fact_iff.mp h)`
example (p : ℕ) (h : Prime p) : Fact p.Prime := by exact_2? -- would suggest `exact fact_iff.mpr h.nat_prime`

The question is twofold: does a mechanism of this kind already exist, and if not, could one be built without incurring prohibitive performance costs?

[Etienne Marion]

Does apply? followed by exact? work here?

[Aaron Liu]

That would only search the first result of apply?

[Etienne Marion]

I meant once apply? found something you can use exact? to close the goal (of course this requires that you picked the right suggestion from apply? in the first place)

[Isak Colboubrani]

@Etienne Marion Using the mechanical strategy "try all apply? suggestions two lemmas deep" does succeed in one of the two example cases:

import Mathlib
example (p : ℕ) (h : Prime p) : Fact p.Prime := by
  -- "apply?" gives two suggestions. One of them is "fact_iff.mpr".
  apply fact_iff.mpr
  -- "apply?" now gives one suggestion: "Prime.nat_prime".
  apply Prime.nat_prime
  assumption

However, for the second test case -- example (p : ℕ) (h : Prime p) : Fact p.Prime := by sorry which can be solved by exact fact_iff.mpr h.nat_prime-- this mechanical approach does not seem to work.

[Etienne Marion]

I guess you mean for the 1st test case. I think that's because the search made by apply? does not take hypotheses into accounts, it only uses the hypotheses when it found a candidate lemma. So when looking for a lemma to prove Prime _ apply will only look at lemmas whose conclusion has the form Prime _, which is not the case of fact_iff.mp.

[Isak Colboubrani]

@Etienne Marion Yes, I mixed them up! Could we come up with a search heuristic that would find the other case too?

[Isak Colboubrani]

Also, does anyone want to weigh in on this more generally?

I suspect a naïve approach—exploring all possible pairs of lemmas, i.e. $n^2$ combinations—would be prohibitively slow. In absolute terms, roughly how slow would this be? Are there any clever heuristics or pruning strategies that would reduce the search space enough to handle simpler “two-lemma” scenarios in a reasonable time?