1c1c534a03
This PR adds `solve_by_elim` as a fallback in the `try?` tactic's simple
tactics. When `rfl` and `assumption` both fail but `solve_by_elim`
succeeds (e.g., for goals requiring hypothesis chaining or
backtracking), `try?` will now suggest `solve_by_elim`.
The structure is `first | (attempt_all | rfl | assumption) |
solve_by_elim`, so `solve_by_elim` only runs when the faster tactics
fail.
This is a prerequisite for removing the "first pass" `solve_by_elim`
from `apply?`. Currently `apply?` calls `solve_by_elim` twice: once
before library search, and once after each lemma application. The first
pass can be removed once `try?` includes `solve_by_elim`.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
123 lines
3.6 KiB
Text
123 lines
3.6 KiB
Text
/-
|
|
Test that try? supports user-defined suggestion generators via @[try_suggestion]
|
|
-/
|
|
module
|
|
public import Lean
|
|
public meta import Lean.Elab.Tactic.Try
|
|
|
|
open Lean Meta Elab Tactic Try
|
|
|
|
-- Define an opaque predicate that built-in tactics (including solve_by_elim) won't solve
|
|
opaque CustomProp : Prop
|
|
axiom customPropHolds : CustomProp
|
|
|
|
section BasicTest
|
|
-- Define a generator that suggests the custom lemma
|
|
@[local try_suggestion]
|
|
meta def customPropSolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| exact customPropHolds)]
|
|
|
|
-- Test that try? picks up the user-defined suggestion
|
|
-- Built-in tactics won't solve this, so only user suggestion appears
|
|
/--
|
|
info: Try this:
|
|
[apply] exact customPropHolds✝
|
|
-/
|
|
#guard_msgs in
|
|
example : CustomProp := by
|
|
try?
|
|
end BasicTest
|
|
|
|
section PriorityTest
|
|
-- Test priority ordering with multiple generators
|
|
@[local try_suggestion 2000]
|
|
meta def highPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| apply customPropHolds)]
|
|
|
|
@[local try_suggestion 1000]
|
|
meta def midPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| exact customPropHolds)]
|
|
|
|
@[local try_suggestion 500]
|
|
meta def lowPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| constructor)]
|
|
|
|
-- All generators return successful tactics, ordered by priority (highest first)
|
|
-- Note: constructor doesn't work on opaque types, so lowPrioritySolver's suggestion is filtered out
|
|
/--
|
|
info: Try these:
|
|
[apply] apply customPropHolds✝
|
|
[apply] exact customPropHolds✝
|
|
-/
|
|
#guard_msgs in
|
|
example : CustomProp := by
|
|
try?
|
|
end PriorityTest
|
|
|
|
section BuiltInFallback
|
|
-- Test that user generators only run if built-ins fail
|
|
-- For True, built-ins succeed so user generators shouldn't run
|
|
@[local try_suggestion]
|
|
meta def shouldNotRunForTrue (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| exact True.intro)]
|
|
|
|
-- Built-ins succeed, so user suggestion doesn't appear
|
|
/--
|
|
info: Try these:
|
|
[apply] solve_by_elim
|
|
[apply] simp
|
|
[apply] simp only
|
|
[apply] grind
|
|
[apply] grind only
|
|
[apply] simp_all
|
|
-/
|
|
#guard_msgs in
|
|
example : True := by
|
|
try?
|
|
end BuiltInFallback
|
|
|
|
section DoubleSuggestion
|
|
-- Test double-suggestion: when a user tactic produces "Try this" messages,
|
|
-- both the original tactic and the suggestions should appear
|
|
-- Use CustomProp which built-ins can't solve
|
|
@[local try_suggestion]
|
|
meta def doubleSuggestionSolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| show_term apply customPropHolds)]
|
|
|
|
-- Double-suggestion: when show_term produces a "Try this" message,
|
|
-- both the original tactic and the extracted suggestion should appear
|
|
-- The message from show_term during extraction is suppressed
|
|
/--
|
|
info: Try these:
|
|
[apply] show_term apply customPropHolds✝
|
|
[apply] exact customPropHolds
|
|
-/
|
|
#guard_msgs in
|
|
example : CustomProp := by
|
|
try?
|
|
end DoubleSuggestion
|
|
|
|
section RegisterCommand
|
|
-- Test the register_try?_tactic convenience command
|
|
register_try?_tactic (priority := 500) exact customPropHolds
|
|
|
|
/--
|
|
info: Try this:
|
|
[apply] exact customPropHolds
|
|
-/
|
|
#guard_msgs in
|
|
example : CustomProp := by
|
|
try?
|
|
|
|
-- Test without explicit priority (should default to 1000, so appear before exact at 500)
|
|
register_try?_tactic apply customPropHolds
|
|
|
|
/--
|
|
info: Try these:
|
|
[apply] apply customPropHolds
|
|
[apply] exact customPropHolds
|
|
-/
|
|
#guard_msgs in
|
|
example : CustomProp := by
|
|
try?
|
|
end RegisterCommand
|