4fe0259354
This makes `exact?%` behave like `by exact?` rather than `by apply?`. If the underlying function `librarySearch` finds a suggestion which closes the goal, use it (and add a code action). Otherwise log an error and use `sorry`. The error is either ```text `exact?%` didn't find any relevant lemmas ``` or ```text `exact?%` could not close the goal. Try `by apply` to see partial suggestions. ``` --- [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Useful.20term.20elaborators/near/434863856) --------- Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
78 lines
3.1 KiB
Text
78 lines
3.1 KiB
Text
/-
|
|
Copyright (c) 2021-2024 Gabriel Ebner and Lean FRO. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Gabriel Ebner, Joe Hendrix, Scott Morrison
|
|
-/
|
|
prelude
|
|
import Lean.Meta.Tactic.LibrarySearch
|
|
import Lean.Meta.Tactic.TryThis
|
|
import Lean.Elab.Tactic.ElabTerm
|
|
|
|
namespace Lean.Elab.LibrarySearch
|
|
|
|
open Lean Meta LibrarySearch
|
|
open Elab Tactic Term TryThis
|
|
|
|
/--
|
|
Implementation of the `exact?` tactic.
|
|
|
|
* `ref` contains the input syntax and is used for locations in error reporting.
|
|
* `required` contains an optional list of terms that should be used in closing the goal.
|
|
* `requireClose` indicates if the goal must be closed.
|
|
It is `true` for `exact?` and `false` for `apply?`.
|
|
-/
|
|
def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
|
|
TacticM Unit := do
|
|
let mvar ← getMainGoal
|
|
let (_, goal) ← (← getMainGoal).intros
|
|
goal.withContext do
|
|
let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
|
|
let tactic := fun exfalso =>
|
|
solveByElim required (exfalso := exfalso) (maxDepth := 6)
|
|
let allowFailure := fun g => do
|
|
let g ← g.withContext (instantiateMVars (.mvar g))
|
|
return required.all fun e => e.occurs g
|
|
match ← librarySearch goal tactic allowFailure with
|
|
-- Found goal that closed problem
|
|
| none =>
|
|
addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta
|
|
-- Found suggestions
|
|
| some suggestions =>
|
|
if requireClose then throwError
|
|
"`exact?` could not close the goal. Try `apply?` to see partial suggestions."
|
|
reportOutOfHeartbeats `library_search ref
|
|
for (_, suggestionMCtx) in suggestions do
|
|
withMCtx suggestionMCtx do
|
|
addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)
|
|
if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas"
|
|
admitGoal goal
|
|
|
|
@[builtin_tactic Lean.Parser.Tactic.exact?]
|
|
def evalExact : Tactic := fun stx => do
|
|
let `(tactic| exact? $[using $[$required],*]?) := stx
|
|
| throwUnsupportedSyntax
|
|
exact? (← getRef) required true
|
|
|
|
|
|
@[builtin_tactic Lean.Parser.Tactic.apply?]
|
|
def evalApply : Tactic := fun stx => do
|
|
let `(tactic| apply? $[using $[$required],*]?) := stx
|
|
| throwUnsupportedSyntax
|
|
exact? (← getRef) required false
|
|
|
|
@[builtin_term_elab Lean.Parser.Syntax.exact?]
|
|
def elabExact?Term : TermElab := fun stx expectedType? => do
|
|
let `(exact?%) := stx | throwUnsupportedSyntax
|
|
withExpectedType expectedType? fun expectedType => do
|
|
let goal ← mkFreshExprMVar expectedType
|
|
let (_, introdGoal) ← goal.mvarId!.intros
|
|
introdGoal.withContext do
|
|
if let some suggestions ← librarySearch introdGoal then
|
|
if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas"
|
|
else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions."
|
|
mkSorry expectedType (synthetic := true)
|
|
else
|
|
addTermSuggestion stx (← instantiateMVars goal).headBeta
|
|
instantiateMVars goal
|
|
|
|
end Lean.Elab.LibrarySearch
|