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.
This adds a simplification lemma for `(x - y).toNat` when the
subtraction is known to not overflow (i.e., `y ≤ x`).
We make a new section for this for two reasons:
1. Definitions of subtraction occur before the definition of
`BitVec.le_def`, so we cannot directly place this lemma at `sub`.
2. There are other theorems of this kind, for addition and
multiplication, which can morally live in the same section.
The theorem
```lean
namespace Int
theorem ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a / b := by
match a, b with
| ofNat a, b =>
match Int.le_antisymm Ha (ofNat_zero_le a) with
| h1 =>
rw [h1, zero_ediv,]
exact Int.le_refl 0
| a, ofNat b =>
match Int.le_antisymm Hb (ofNat_zero_le b) with
| h1 =>
rw [h1, Int.ediv_zero]
exact Int.le_refl 0
| negSucc a, negSucc b =>
rw [Int.div_def, ediv]
have le_succ {a: Int} : a ≤ a+1 := (le_add_one (Int.le_refl a))
have h2: 0 ≤ ((↑b:Int) + 1) := Int.le_trans (ofNat_zero_le b) le_succ
have h3: (0:Int) ≤ ↑a / (↑b + 1) := (ediv_nonneg (ofNat_zero_le a) h2)
exact Int.le_trans h3 le_succ
```
is nontrivial to prove from existing theorems and would be nice to add
as standard theorem in DivModLemmas.
See the zullip conversation
[here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Adding.20theorem.20theorem.20ediv_nonneg'.20for.20negative.20a.20and.20b)
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
From the new doc-string:
```quote
In early versions of Lean, the typeclasses provided by `/` and `%`
were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
However we decided it was better to use `ediv` and `emod`,
as they are consistent with the conventions used in SMTLib, Mathlib,
and often mathematical reasoning is easier with these conventions.
At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
In September 2024, we decided to do this rename (with deprecations in place),
and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
ever need to use these functions and their associated lemmas.
```
Proves that `<` and `<=` on `BitVec` are (strict) (total) partial
orders. This is required for the `UInt` as `BitVec` refactor.
This does open the question how to state these theorems "correctly" for
`BitVec`, we have both `<` living in `Prop` and `BitVec.ult` living in
`Bool`. We might of course say to always use `<` but: Once we start
adding `IntX` we need to prove the same results for `BitVec.slt` to
provide an equivalent API. So it would appear that it is unavoidable to
have a `= true` variant of these theorems there?
Question answered: Use `<` and `slt`.
Refactors the derive handlers for `ToJson` and `FromJson` in preparation
for #3160.
This splits up the different parts of the handler according to how other
similar handlers are implemented while keeping the original logic
intact. This makes the changes necessary to adapt the file in #3160 much
easier.
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>
I found that the kernel has special support for `e =?= true`, and will
in this case aggressively whnf `e`. This explains the following behavior
(for a `sqrt` function with fuel):
```lean
theorem foo : sqrt 100000000000000000002 == 10000000000 := rfl -- fast
theorem foo : sqrt 100000000000000000002 = 10000000000 := rfl -- slow
theorem foo : sqrt 100000000000000000002 = 10000000000 := by decide -- fast
```
The special support in the kernel only applies for closed `e` and `true`
on the RHS. It could be generlized (also open terms, also `false`, other
data type's constructors, different orientation). But maybe I should
wait for evidence that this generaziation really matters, or whether
all applications (proof by reflection) can be made to have this form.
This PR enables the use of incrementality for completion in tactic
blocks. Consider the following example:
```lean
example : True := by
have : True := T
sleep 10000
```
Before this PR, in order to respond to a completion request after `T`,
`sleep 10000` has to complete first since the command must be fully
elaborated. After this PR, the completion request is responded to
immediately.
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
