This PR fixes an issue reported a while ago at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60Monad.2Emap.60.20is.20a.20namespace.3F/near/425662846
where `Monad.map` was incorrectly reported by the autocompletion as a
namespace.
The underlying issue is that `Monad.map` contains an internal
declaration `_default`. This PR ensures that no namespaces are
registered that only contain internal declarations.
This also means that `open`ing namespaces that only contain internal
declarations will now fail.
The Mathlib adaption for this is a minor change where a declaration
(i.e. a namespace that only contains internal declarations) was `open`ed
by accident.
This solves the issue where certain subexpressions are lacking syntax
hovers because the hover text is not "builtin" - it only shows up if the
`Parser` constant is imported in the environment. For top level syntaxes
this is not a problem because `builtin_term_parser` will automatically
add this doc information, but nested syntaxes don't get the same
treatment.
We could walk the expression and add builtin docs recursively, but this
is somewhat expensive and unnecessary given that it's a fixed list of
declarations in lean core. Moreover, there are reasons to want to
control which syntax nodes actually get hovers, and while a better
system for that is forthcoming, for now it can be achieved by
strategically not applying the `@[builtin_doc]` attribute.
Fixes#3842
When the elaborator doesn't provide us with any `CompletionInfo`, we
currently provide no completions whatsoever. But in many cases, we can
still provide some helpful identifier completions without elaborator
information. This PR adds a fallback mode for this situation.
There is more potential here, but this should be a good start.
In principle, this issue alleviates #5172 (since we now provide
completions in these contexts). I'll leave it up to an elaboration
maintainer whether we also want to ensure that the completion infos are
provided correctly in these cases.
Fixes#4455, fixes#4705, fixes#5219
Also fixes a minor bug where a dot in brackets would report incorrect
completions instead of no completions.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Currently, `ll_infer_type` is responsible for telling the user about
`noncomputable` when a definition depends on one without executable
code. However, this is imperfect because type inference does not check
every subexpression. This leads to errors later on that users find to be
hard to interpret.
Now, `Lean.IR.checkDecls` has a friendlier error message when it
encounters constants without compiled definitions, suggesting to
consider using `noncomputable`. While this function is an internal IR
consistency check, it is also reasonable to have it give an informative
error message in this particular case. The suggestion to use
`noncomputable` is limited to just unknown constants.
Some alternatives would be to either (1) create another checker just for
missing constants, (2) change `ll_infer_type` to always visit every
subexpression no matter if they are necessary for inferring the type, or
(3) investigate whether `tests/lean/run/1785.lean` is due to a deeper
issue.
Closes#1785
This is "upstreaming" mathlib's `unfold_let` tactic by incorporating its
functionality into `unfold`. Now `unfold` can, in addition to unfolding
global definitions, unfold local definitions. The PR also updates the
`conv` version of the tactic.
An improvement over `unfold_let` is that it beta reduces unfolded local
functions.
Two features not present in `unfold` are that (1) `unfold_let` with no
arguments does zeta delta reduction of *all* local definitions, and also
(2) `unfold_let` can interleave unfoldings (in contrast, `unfold a b c`
is exactly the same as `unfold a; unfold b; unfold c`).
Closes RFC #4090
When an eliminator was overapplied with more than one additional
argument, elaboration produced an incorrect term because the list of
processed arguments was being reversed. Now these arguments are not
reversed.
We change the `bv_decide` to understand `BitVec.extractLsb'` as a
primitive, and add a normalization lemma for `extractLsb`.
It's important to pick the primed version as a primitive, because it is
not always possible to rewrite `extractLsb'` back into `extractLsb` (see
#5007 for that direction, and the relevant side-conditions).
That is, with this PR, `bv_decide` is able to bitblast both versions of
extracting bits.
This doesn't completely resolve the danger (only relevant in `prelude`
files) of importing `Init.Data.List.Basic` but not `Init.Data.List.Impl`
and thereby not having `@[csimp]` lemmas installed for some list
operations.
I'm going to address this better while working on `Array`.
Sebastian mentioned that the use of the kernel defeq was to work around
a performance issue that was fixed since. Let's see if we can do
without.
This is also a semantic change: Ground terms (no free vars, no mvars)
are reduced at
“all” transparency even if the the transparency setting is default. This
was the case
even before 03f6b87647 switched to the
kernel defeq
checking for performance. It seems that this is rather surprising
behavior from the user
point of view. The fallout on batteries and mathlib is rather limited,
only a few
`rfl` proofs seem to have (inadvertently or not) have relied on this.
The speedcenter reports no significant regressions on core or mathlib.
These commands were trusting that elaboration resulted in type-correct
terms, but users testing custom elaborators have found it to be
surprising that they do not do typechecking. This adds a `Meta.check`
step.
This renames `BitVec.getLsb` to `getLsbD` (`D` for "default" value, i.e.
false), and introduces `getLsb?` and `getLsb'` (which we can rename to
`getLsb` after a deprecation cycle).
(Similarly for `getMsb`.)
Also adds a `GetElem` class so we can use `x[i]` and `x[i]?` notation.
Later, we will turn
```
theorem getLsbD_eq_getElem?_getD (x : BitVec w) (i : Nat) (h : i < w) :
x.getLsbD i = x[i]?.getD false
```
on as a `@[simp]` lemma.
This PR doesn't attempt to demonstrate the benefits, but I think both
arguments are going to get easier, and this will bring the BitVec API
closer in line to List/Array, etc.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
in #4154 and #5129 the rules for equational lemmas have changed, and new
options were introduced that can be used to revert to the pre-4.12
behavior. Hopefully nobody really needs these options besides for
backwards compatibility, therefore we put these options in the
`backward` option name space.
So the previous behavior can be achieved by setting
```lean
set_option backward.eqns.nonrecursive false
set_option backward.eqns.deepRecursiveSplit false
```
With this, lean produces the following zoo of rewrite rules:
```
Option.map.eq_1 : Option.map f none = none
Option.map.eq_2 : Option.map f (some x) = some (f x)
Option.map.eq_def : Option.map f p = match o with | none => none | (some x) => some (f x)
Option.map.eq_unfold : Option.map = fun f p => match o with | none => none | (some x) => some (f x)
```
The `f.eq_unfold` variant is especially useful to rewrite with `rw`
under
binders.
This implements and fixes#5110
This PR roughly halves the time needed to load the .ilean files by
optimizing the JSON parser and the conversion from JSON to Lean data
structures.
The code is optimized roughly as follows:
- String operations are inlined more aggressively
- Parsers are changed to use new `String.Iterator` functions `curr'` and
`next'` that receive a proof and hence do not need to perform an
additional check
- The `RefIdent` of .ilean files now uses a `String` instead of a `Name`
to avoid the expensive parse step from `String` to `Name` (despite the
fact that we only very rarely actually need a `Name` in downstream code)
- Instead of `List`s and `Subarray`s, the JSON to Lean conversion now
directly passes around arrays and array indices to avoid redundant
boxing
- Parsec's `peek?` sometimes generates redundant `Option` wrappers
because the generation of basic blocks interferes with the ctor-match
optimization, so it is changed to use an `isEof` check where possible
- Early returns and inline-do-blocks cause the code generator to
generate new functions, which then interfere with optimizations, so they
are now avoided
- Mutual defs are used instead of unspecialized passing of higher-order
functions to generate faster code
- The object parser is made tail-recursive
This PR also fixes a stack overflow in `Lean.Json.compress` that would
occur with long lists and adds a benchmark for the .ilean roundtrip
(compressed pretty-printing -> parsing).
`simp only` will not apply this simproc anymore. Users must now write
`simp only [reduceCtorEq]`. See RFC #5046 for motivation.
This PR also renames simproc to `reduceCtorEq`.
close#5046
@semorrison A few `simp only ...` tactics will probably break in
Mathlib. Fix: include `reduceCtorEq`.
We swap the arguments for `Membership.mem` so that when proceeded by a
`SetLike` coercion, as is often the case in Mathlib, the resulting
expression is recognized as eta expanded and reduce for many
computations. The most beneficial outcome is that the discrimination
tree keys for instances and simp lemmas concerning subsets become more
robust resulting in more efficient searches.
Closes `RFC` #4932
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
This is part of #3983.
After #4154 introduced equational lemmas for non-recursive functions and
#5055
unififed the lemmas for structural and wf recursive funcitons, this now
disables the special handling of recursive functions in
`findMatchToSplit?`, so that the equational lemmas should be the same no
matter how the function was defined.
The new option `eqns.deepRecursiveSplit` can be disabled to get the old
behavior.
### Breaking change
This can break existing code, as there now can be extra equational
lemmas:
* Explicit uses of `f.eq_2` might have to be adjusted if the numbering
changed.
* Uses of `rw [f]` or `simp [f]` may no longer apply if they previously
matched (and introduced a `match` statement), when the equational
lemmas got more fine-grained.
In this case either case analysis on the parameters before rewriting
helps, or setting the option `opt.deepRecursiveSplit false` while
defining the function
This is part of #3983.
Fine-grained equational lemmas are useful even for non-recursive
functions, so this adds them.
The new option `eqns.nonrecursive` can be set to `false` to have the old
behavior.
### Breaking channge
This is a breaking change: Previously, `rw [Option.map]` would rewrite
`Option.map f o` to `match o with … `. Now this rewrite will fail
because the equational lemmas require constructors here (like they do
for, say, `List.map`).
Remedies:
* Split on `o` before rewriting.
* Use `rw [Option.map.eq_def]`, which rewrites any (saturated)
application of `Option.map`
* Use `set_option eqns.nonrecursive false` when *defining* the function
in question.
### Interaction with simp
The `simp` tactic so far had a special provision for non-recursive
functions so that `simp [f]` will try to use the equational lemmas, but
will also unfold `f` else, so less breakage here (but maybe performance
improvements with functions with many cases when applied to a
constructor, as the simplifier will no longer unfold to a large
`match`-statement and then collapse it right away).
For projection functions and functions marked `[reducible]`, `simp [f]`
won’t use the equational theorems, and will only use its internal
unfolding machinery.
### Implementation notes
It uses the same `mkEqnTypes` function as for recursive functions, so we
are close to a consistency here. There is still the wrinkle that for
recursive functions we don't split matches without an interesting
recursive call inside. Unifying that is future work.
