feat: exact? +grind and exact? +try? discharger options
#11469
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This PR adds a `+try?` option to `exact?` and `apply?` tactics, similar to the existing `+grind` option. When `+try?` is enabled, `try?` is used as a fallback discharger for subgoals that `solve_by_elim` cannot close. The proof is wrapped in `Try.Marker` so suggestions display `(by try?)` instead of the complex proof term. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
algebraic-dev
pushed a commit
that referenced
this pull request
Dec 8, 2025
This PR adds `+grind` and `+try?` options to `exact?` and `apply?` tactics. ## `+grind` option When `+grind` is enabled, `grind` is used as a fallback discharger for subgoals that `solve_by_elim` cannot close. The proof is wrapped in `Grind.Marker` so suggestions display `(by grind)` instead of the complex grind proof term. Example: ```lean axiom foo (x : Nat) : x < 37 → 5 < x → x.log2 < 6 /-- info: Try this: [apply] exact foo x (by grind) (by grind) -/ #guard_msgs in example (x : Nat) (h₁ : x < 30) (h₂ : 8 < x) : x.log2 < 6 := by exact? +grind ``` ## `+try?` option When `+try?` is enabled, `try?` is used as a fallback discharger for subgoals. This is useful when subgoals require induction or other strategies that `try?` can find but `solve_by_elim` and `grind` cannot. Example: ```lean inductive MyList (α : Type _) where | nil : MyList α | cons : α → MyList α → MyList α axiom MyListProp : MyList α → Prop @[grind .] axiom mylist_nil : MyListProp (MyList.nil : MyList α) @[grind .] axiom mylist_cons : ∀ (x : α) (xs : MyList α), MyListProp xs → MyListProp (MyList.cons x xs) axiom qux (xs : MyList α) (p : MyListProp xs) : MyListProp2 xs /-- info: Try this: [apply] exact qux xs (by try?) -/ example (xs : MyList α) : MyListProp2 xs := by exact? +try? ``` 🤖 Prepared with Claude Code --------- Co-authored-by: Claude <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds
+grindand+try?options toexact?andapply?tactics.+grindoptionWhen
+grindis enabled,grindis used as a fallback discharger for subgoals thatsolve_by_elimcannot close. The proof is wrapped inGrind.Markerso suggestions display(by grind)instead of the complex grind proof term.Example:
+try?optionWhen
+try?is enabled,try?is used as a fallback discharger for subgoals. This is useful when subgoals require induction or other strategies thattry?can find butsolve_by_elimandgrindcannot.Example:
🤖 Prepared with Claude Code