This PR implements basic support for handling of enum inductives in
`bv_decide`. It now supports equality on enum inductive variables (or
other uninterpreted atoms) and constants.
This PR adds `simp +arith` for integers. It uses the new `grind`
normalizer for linear integer arithmetic. We still need to implement
support for dividing the coefficients by their GCD. It also fixes
several bugs in the normalizer.
This PR implements the normalizer for linear integer arithmetic
expressions. It is not connect to `simp +arith` yet because of some
spurious `[simp]` attributes.
This PR adds the `Try.Config.merge` flag (`true` by default) to the
`try?` tactic. When set to `true`, `try?` compresses suggestions such
as:
```lean
· induction xs, ys using bla.induct
· grind only [List.length_reverse]
· grind only [bla]
```
into:
```lean
induction xs, ys using bla.induct <;> grind only [List.length_reverse, bla]
```
This PR also ensures `try?` does not generate suggestions that mixes
`grind` and `grind only`, or `simp` and `simp only` tactics.
This PR also adds the `try? +harder` option (previously called `lib`),
but it has not been fully implemented yet.
This PR extends the behavior of the `sync` flag for `Task.map/bind` etc.
to encompass synchronous execution even when they first have to wait on
completion of the first task, drastically lowering the overhead of such
tasks. Thus the flag is now equivalent to e.g. .NET's
`TaskContinuationOptions.ExecuteSynchronously`.
This PR adds new configuration options to `try?`.
- `try? -only` omits `simp only` and `grind only` suggestions
- `try? +missing` enables partial solutions where some subgoals are
"solved" using `sorry`, and must be manually proved by the user.
- `try? (max:=<num>)` sets the maximum number of suggestions produced
(default is 8).
This PR adds support for more complex suggestions in `try?`. Example:
```lean
example (as : List α) (a : α) : concat as a = as ++ [a] := by
try?
```
suggestion
```
Try this: · induction as, a using concat.induct
· rfl
· simp_all
```
As per dicussion with team colleages, the feature shouldn’t be called
“auto attach” but rather “well-founded recursion preprocessing” to avoid
(imprecise) jargon.
This PR adds the `binderNameHint` gadget. It can be used in rewrite and
simp rules to preserve a user-provided name where possible.
The expression `binderNameHint v binder e` defined to be `e`.
If it is used on the right-hand side of an equation that is applied by a
tactic like `rw` or `simp`,
and `v` is a local variable, and `binder` is an expression that (after
beta-reduction) is a binder
(so `fun w => …` or `∀ w, …`), then it will rename `v` to the name used
in the binder, and remove
the `binderNameHint`.
A typical use of this gadget would be as follows; the gadget ensures
that after rewriting, the local
variable is still `name`, and not `x`:
```
theorem all_eq_not_any_not (l : List α) (p : α → Bool) :
l.all p = !l.any fun x => binderNameHint x p (!p x) := sorry
example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by
rw [all_eq_not_any_not]
-- ⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true
```
This gadget is supported by `simp`, `dsimp` and `rw` in the
right-hand-side of an equation, but not
in hypotheses or by other tactics.
This PR adds a convenience command `#info_trees in`, which prints the
info trees generated by the following command. It is useful for
debugging or learning about `InfoTree`.
This PR starts on the process of cleaning up variable names across
List/Array/Vector. For now, we just rename "numerical index" variables
in one file. This is driven by a custom linter.
This PR adds SMT-LIB operators to detect overflow
`BitVec.(uadd_overflow, sadd_overflow)`, according to the definitions
[here](https://github.com/SMT-LIB/SMT-LIB-2/blob/2.7/Theories/FixedSizeBitVectors.smt2),
and the theorems proving equivalence of such definitions with the
`BitVec` library functions (`uaddOverflow_eq`, `saddOverflow_eq`).
Support theorems for these proofs are `BitVec.toNat_mod_cancel_of_lt,
BitVec.toInt_lt, BitVec.le_toInt, Int.bmod_neg_iff`. The PR also
includes a set of tests.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com>
This PR adds preliminary support for inlay hints, as well as support for
inlay hints that denote the auto-implicits of a function. Hovering over
an auto-implicit displays its type and double-clicking the auto-implicit
inserts it into the text document.
This PR is an extension of #3910.
### Known issues
- In VS Code, when inserting an inlay hint, the inlay hint may linger
for a couple of seconds before it disappears. This is a defect of the VS
Code implementation of inlay hints and cannot adequately be resolved by
us.
- When making a change to the document, it may take a couple of seconds
until the inlay hints respond to the change. This is deliberate and
intended to reduce the amount of inlay hint flickering while typing. VS
Code has a mechanism of its own for this, but in my experience it is
still far too sensitive without additional latency.
- Inserting an auto-implicit inlay hint that depends on an auto-implicit
meta-variable causes a "failed to infer binder type" error. We can't
display these meta-variables in the inlay hint because they don't have a
user-displayable name, so it is not clear how to resolve this problem.
- Inlay hints are currently always resolved eagerly, i.e. we do not
support the `textDocument/inlayHint/resolve` request yet. Implementing
support for this request is future work.
### Other changes
- Axioms did not support auto-implicits due to an oversight in the
implementation. This PR ensures they do.
- In order to reduce the amount of inlay hint flickering when making a
change to the document, the language server serves old inlay hints for
parts of the file that have not been processed yet. This requires LSP
request handler state (that sometimes must be invalidated on
`textDocument/didChange`), so this PR introduces the notion of a
stateful LSP request handler.
- The partial response mechanism that we use for semantic tokens, where
we simulate incremental LSP responses by periodically emitting refresh
requests to the client, is generalized to accommodate both inlay hints
and semantic tokens. Additionally, it is made more robust to ensure that
we never emit refresh requests while a corresponding request is in
flight, which causes VS Code to discard the respond of the request, as
well as to ensure that we keep prompting VS Code to send another request
if it spuriously decides not to respond to one of our refresh requests.
- The synthetic identifier of an `example` had the full declaration as
its (non-canonical synthetic) range. Since we need a reasonable position
for the identifier to insert an inlay hint for the auto-implicits of an
`example`, we change the (canonical synthetic) range of the synthetic
identifier to that of the `example` keyword.
- The semantic highlighting request handling is moved to a separate
file.
### Breaking changes
- The semantic highlighting request handler is not a pure request
handler anymore, but a stateful one. Notably, this means that clients
that extend the semantic highlighting of the Lean language server with
the `chainLspRequestHandler` function must now use the
`chainStatefulLspRequestHandler` function instead.
This PR adds theorems `BitVec.(getElem_umod_of_lt, getElem_umod,
getLsbD_umod, getMsbD_umod)`. For the defiition of these theorems we
rely on `divRec`, excluding the case where `d=0#w`, which is treated
separately because there is no infrastructure to reason about this case
within `divRec`. In particular, our implementation follows the mathlib
standard [where division by 0 yields
0](c7c1e091c9/src/Init/Data/BitVec/Basic.lean (L217)),
while in [SMTLIB this yields
`allOnes`](c7c1e091c9/src/Init/Data/BitVec/Basic.lean (L237)).
Co-authored by @bollu.
---------
Co-authored-by: Siddharth <siddu.druid@gmail.com>
This PR adds `BitVec.(getMsbD, msb)_replicate, replicate_one` theorems,
corrects a non-terminal `simp` in `BitVec.getLsbD_replicate` and
simplifies the proof of `BitVec.getElem_replicate` using the `cases`
tactic.
Co-authored with @bollu.
---------
Co-authored-by: Alex Keizer <alex@keizer.dev>
This PR adds the tactic `expose_names`. It creates a new goal whose
local context has been "exposed" so that every local declaration has a
clear, accessible name. If no local declarations require renaming, the
original goal is returned unchanged.
This tactic will be used to improve `try?`.
This PR adds `LawfulBEq` instances for `Array` and `Vector`.
(Note this replaces a contribution of @mehbark to Batteries for the
LawfulBEq instance for Vector, which was dropped during the release
process due to conflicts. Thanks for that contribution!)
In #6818, I removed this small section of reductions from BitVec to Nat
since it seemed unnecessary. Since then, I saw that there are equivalent
sections for shiftLeft/sshiftRight that are more substantial and that I
should have not made this change.
This PR adds a builtin tactic and a builtin attribute that are required
for the tree map. The tactic, `as_aux_lemma`, can generally be used to
wrap the proof term generated by a tactic sequence into a separate
auxiliary lemma in order to keep the proof term small. This can, in rare
cases, be necessary if the proof term will appear multiple times in the
encompassing term. The new attribute, `Std.Internal.tree_tac`, is
internal and should not be used outside of `Std`.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR aligns current coverage of `find`-type theorems across
`List`/`Array`/`Vector`. There are still quite a few holes in this API,
which will be filled later.
This PR adds the `try?` tactic. This is the first draft, but it can
already solve examples such as:
```lean
example (e : Expr) : e.simplify.eval σ = e.eval σ := by
try?
```
in `grind_constProp.lean`. In the example above, it suggests:
```lean
induction e using Expr.simplify.induct <;> grind?
```
In the same test file, we have
```lean
example (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
try?
```
and the following suggestion is produced
```lean
induction σ₁, σ₂ using State.join.induct <;> grind?
```
This PR adds the `grind` configuration option `verbose`. For example,
`grind -verbose` disables all diagnostics. We are going to use this flag
to implement `try?`.
This PR teaches bv_normalize to replace subtractions on one side of an
equality with an addition on the other side, this re-write eliminates a
not + addition in the normalized form so it is easier on the solver.
Note that I also make a point to normalize (1 + ~~~x) to (~~~x + 1) to
limit the amount of boilerplate symmetry theorems we require.
This PR adds the new attributes `[grind =>]` and `[grind <=]` for
controlling pattern selection and minimizing the number of places where
we have to use verbose `grind_pattern` command. It also fixes a bug in
the new pattern selection procedure, and improves the automatic pattern
selection for local lemmas.
The tests `grind_constProp.lean` and `no_grind_constProp.lean` are the
same use case with and without `grind`.
