Efficient certificate generation

Stream: general

[Daniel Weber]

Suppose we want to prove a theorem of the form ∃x, p x, where DecidablePred p. A proof could be by use solution; decide, where solution is some earlier def. However, this requires the kernel to evaluate solution, which could be really slow in some cases, while the kernel only has to care about its value, not the definition.
Is there some way to have solution evaluated in native code, and then only give its value to the kernel? I don't want to just hardcode it.

[Yury G. Kudryashov]

Do you have an example? What's slow: the evaluation of the solution in the kernel, or the decision procedure?

[Yury G. Kudryashov]

I'm the former case, try %eval

[Yury G. Kudryashov]

Never used it myself

[Daniel Weber]

Yury G. Kudryashov said:

I'm the former case, try %eval

How do you use it? I can't find anything about it

[Daniel Weber]

An example is a generation of Pratt primality certificates. https://github.com/leanprover-community/mathlib4/blob/6439ce3f194a2acd309af6831d753e560c46bcf6/Mathlib/NumberTheory/LucasPrimality.lean#L567 uses a special tactic to do this, but I wonder if there's a more general method

[Yury G. Kudryashov]

import Mathlib.Tactic.Eval

example : True := by
  let n := eval% 2 + 3
  -- now you have `n : Nat := 5`