This PR improves the `grind` tactic generated by the `instantiate`
action in tracing mode. It also updates the syntax for the `instantiate`
tactic, making it similar to `simp`. For example:
* `instantiate only [thm1, thm2]` instantiates only theorems `thm1` and
`thm2`.
* `instantiate [thm1, thm2]` instantiates theorems marked with the
`@[grind]` attribute **and** theorems `thm1` and `thm2`.
The action produces `instantiate only [...]` tactics. Example:
```lean
/--
info: Try this:
[apply] ⏎
instantiate only [= Array.getElem_set]
instantiate only [= Array.getElem_set]
-/
#guard_msgs in
example (as bs cs : Array α) (v₁ v₂ : α)
(i₁ i₂ j : Nat)
(h₁ : i₁ < as.size)
(h₂ : bs = as.set i₁ v₁)
(h₃ : i₂ < bs.size)
(h₄ : cs = bs.set i₂ v₂)
(h₅ : i₁ ≠ j ∧ i₂ ≠ j)
(h₆ : j < cs.size)
(h₇ : j < as.size) :
cs[j] = as[j] := by
grind => finish?
```
Recall that `finish?` replays generated tactics before suggesting them.
The `instantiate` action inspects the generated proof term to decide
which theorems to include as parameters in the `instantiate only [...]`
tactic. However, in some cases, a theorem contributes only by adding a
term to the state. In such cases, the generated tactic cannot be fully
replayed, and the action uses
`instantiate approx [<thms instantiated>]` to indicate which parts of
the tactic script are approximate. The `approx` is just a hint for
users.
This PR implements the `finish?` tactic for the `grind` interactive
mode. When it successfully closes the goal, it produces a code action
that allows the user to close the goal using explicit grind tactic
steps, i.e., without any search. It also makes explicit which solvers
have been used.
This is just the first version, we will add many "bells and whistles"
later. For example, `instantiate` steps will clearly show which theorems
have been instantiated.
Example:
```lean
/--
info: Try this:
[apply] ⏎
cases #b0f4
next => cases #50fc
next => cases #50fc <;> lia
-/
#guard_msgs in
example (p : Nat → Prop) (x y z w : Int) :
(x = 1 ∨ x = 2) →
(w = 1 ∨ w = 4) →
(y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
(z = 1 ∨ z = 0) → x + y ≤ 6 := by
grind => finish?
```
The anchors in the generated script are based on stable hash codes.
Moreover, users can hover over them to see the exact term used in the
case split. `grind?` will also be implemented using the new framework.
This PR implements support for `Action` in the `grind` solver extensions
(`SolverExtension`). It also provides the `Solvers.mkAction` function
that constructs an `Action` using all registered solvers. The generated
action is "fair," that is, a solver cannot prevent other solvers from
making progress.
This PR implements infrastructure for evaluating `grind` tactics in the
`GrindM` monad. We are going to use it to check whether auto-generated
tactics can effectively close the original goal.
This PR moves many operations involving `String.Pos.Raw` to a the
`String.Pos.Raw` namespace with the eventual aim of freeing up the
`String` namespace to contain operations using `String.ValidPos` (to be
renamed to `String.Pos`) instead.
This PR adds the `String.ValidPos.set` and `String.ValidPos.modify`
functions.
After this PR, `String.pos_lt_eq` is no longer a `simp` lemma. Add
`String.Pos.Raw.lt_iff` as a `simp` lemma if your proofs break.
This PR renames `String.split` to `String.splitToList`, because soon the
name `String.split` will be used by a new implementation which is
superior because it is polymorphic over the pattern kind and it returns
an iterator of slices instead of a list of strings.
This PR implements a compact notation for inspecting the `grind` state
in interactive mode. Within a `grind` tactic block, each tactic may
optionally have a suffix of the form `| filter?`.
Examples:
```lean
instantiate | gen > 0 -- Displays terms in the `grind` state after executing `instantiate` with generation greater than zero
```
```lean
instantiate | -- Displays the `grind` state after executing `instantiate`
```
Remark: If the user places the cursor one space before `|`, the state
*before* executing `instantiate` is displayed.
This PR removes the code that was silently displaying the `grind` state
after each tactic step, as it was too noisy.
It also updates the notation for the `first` combinator in the `grind`
tactic mode to avoid conflicts with the new syntax.
This PR changes match compilation to reject some pattern matches that
were previously accepted due to inaccessible patterns sometimes treated
like accessible ones. Fixes#10794.
This PR adds more selectors for TCP and Signals.
It also fixes a problem with `Selectors` that they cannot be closures
over a promise, otherwise it causes the waiter promise to never be
dropped.
This PR introduces the `backward.privateInPublic` option to aid in
porting projects to the module system by temporarily allowing access to
private declarations from the public scope, even across modules. A
warning will be generated by such accesses unless
`backward.privateInPublic.warn` is disabled.
This PR fixes `getHexNumSize` to consider underscores. Previously, only
the amount of bytes was counted, making it output 9 for `1234_abcd`
instead of the actual number of digits, which is 8.
This PR adds adds union operation on `DHashMap`/`HashMap`/`HashSet` and
their raw variants and provides lemmas about union operations.
---------
Co-authored-by: Paul-Lez <paul.lezeau@gmail.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR fixes a bug in the unknown identifier code actions where the
identifiers wouldn't be correctly minimized in nested namespaces. It
also fixes a bug where identifiers would sometimes be minimized to
`[anonymous]`.
The first bug was introduced in #10619.
This PR adds a silent info message with the `grind` state in its
interactive mode. The message is shown only when there is exactly one
goal in the grind interactive mode. The condition is a workaround for
current limitations of our `InfoTree`.
This PR lets match compilation look only at the first remaining
alternative in `processLeaf`. At this point we have no further variables
we can split on, so if the first one isn’t applicable, match compilation
should fail.
This PR fixes a regression introduced by #10307, where hovering the name
of an inductive type or constructor in its own declaration didn't show
the docstring. In the process, a bug in docstring handling for
coinductive types was discovered and also fixed. Tests are added to
prevent the regression from repeating in the future.
This PR ensures that `grind` interactive mode is hygienic. It also adds
tactics for renaming inaccessible names: `rename_i h_1 ... h_n` and
`next h_1 ... h_n => ..`, and `expose_names` for automatically generated
tactic scripts. The PR also adds helper functions for implementing
case-split actions.
This PR introduces a no-op version of `Shrink`, a type that should allow
shrinking small types into smaller universes given a proof that the type
is small enough, and uses it in the iterator library. Because this type
would require special compiler support, the current version is just a
wrapper around the inner type so that the wrapper is equivalent, but not
definitionally equivalent.
While `Shrink` is unable to shrink universes right now, but introducing
it now will allow us to generalize the universes in the iterator library
with fewer breaking changes as soon as an actual `Shrink` is possible.
This PR fixes a bug in combination with VS Code where Lean code that
looks like CSS color codes would display a color picker decoration.
VS Code displays this decoration by default for all languages, not just
CSS. Due to https://github.com/microsoft/vscode/issues/91533, this
setting cannot be disabled in the client on a per-language basis.
However, we can override the default behavior by providing a color
provider of our own. This PR implements an empty color provider to
override the VS Code one.
This PR adds support for interactivity to the combined "try this"
messages that were introduced in #9966. In doing so, it moves the link
to apply a suggestion to a separate `[apply]` button in front of the
suggestion. Hints with diffs remain unchanged, as they did not
previously support interacting with terms in the diff, either.
<img width="379" height="256" alt="Suggestion with interactive message"
src="https://github.com/user-attachments/assets/7838ebf6-0613-46e7-bc88-468a05acbf51"
/>
This PR restores the change in #8656, which removed `autoImplicit =
false` from the default lake template (per previous discussions linked
there). This was accidentally reverted in #8866.
