226a90f1eb
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 <noreply@anthropic.com>
|
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||