building upon #3714, this (almost) implements the second half of #3302.
The main effect is that we now get a better error message when `rfl`
fails. For
```lean
example : n+1+m = n + (1+m) := by rfl
```
instead of the wall of text
```
The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
`exact HEq.rfl` etc.
n m : Nat
⊢ n + 1 + m = n + (1 + m)
```
we now get
```
error: tactic 'rfl' failed, the left-hand side
n + 1 + m
is not definitionally equal to the right-hand side
n + (1 + m)
n m : Nat
⊢ n + 1 + m = n + (1 + m)
```
Unfortunately, because of very subtle differences in semantics (which
transparency setting is used when reducing the goal and whether the
“implicit lambda” feature applies) I could not make this simply the only
`rfl` implementation. So `rfl` remains a macro and is still expanded to
`eq_refl` (difference transparency setting) and `exact Iff.rfl` and
`exact HEq.rfl` (implicit lambda) to not break existing code. This can
be revised later, so this still closes: #3302.
A user might still be puzzled *why* to terms are not defeq. Explaining
that better (“reduced to… and reduces to… etc.”) would also be great,
but that’s not specific to `rfl`, so better left for some other time.
Previously the formatter was using the builtin token table rather that
the one in the current environment. This could lead to round-tripping
failures for user-defined notations.
For an illustrative example, given the following notation
```lean
infixl:65 "+'" => Int.add
notation:65 a:65 "+'-" b:66 => Int.add a (id b)
```
then `5 +' -1` would parse as `Int.add 5 (-1)` and incorrectly pretty
print as `5+'-1`, which in turn would parse as `Int.add 5 (id 1)`. Now
it pretty prints as `5+' -1`.
Modifies how the declaration command elaborator reports when there are
unassigned metavariables. The visible effects are that (1) now errors
like "don't know how to synthesize implicit argument" and "failed to
infer 'let' declaration type" take precedence over universe level
issues, (2) universe level metavariables are reported as metavariables
(rather than as `u_1`, `u_2`, etc.), and (3) if the universe level
metavariables appear in `let` binding types or `fun` binder types, the
error is localized there.
Motivation: Reporting unsolved expression metavariables is more
important than universe level issues (typically universe issues are from
unsolved expression metavariables). Furthermore, `let` and `fun` binders
can't introduce universe polymorphism, so we can "blame" such bindings
for universe metavariables, if possible.
Example 1: Now the errors are on `x` and `none` (reporting expression
metavariables) rather than on `example` (which reported universe level
metavariables).
```lean
example : IO Unit := do
let x := none
pure ()
```
Example 2: Now there is a "failed to infer universe levels in 'let'
declaration type" error on `PUnit`.
```lean
def foo : IO Unit := do
let x : PUnit := PUnit.unit
pure ()
```
In more detail:
* `elabMutualDef` used to turn all level mvars into fresh level
parameters before doing an analysis for "hidden levels". This analysis
turns out to be exactly the same as instead creating fresh parameters
for level mvars in only pre-definitions' types and then looking for
level metavariables in their bodies. With this PR, error messages refer
to the same level metavariables in the Infoview, rather than obscure
generated `u_1`, `u_2`, ... level parameters.
* This PR made it possible to push the "hidden levels" check into
`addPreDefinitions`, after the checks for unassigned expression mvars.
It used to be that if the "hidden levels" check produced an "invalid
occurrence of universe level" error it would suppress errors for
unassigned expression mvars, and now it is the other way around.
* There is now a list of `LevelMVarErrorInfo` objects in the `TermElabM`
state. These record expressions that should receive a localized error if
they still contain level metavariables. Currently `let` expressions and
binder types in general register such info. Error messages make use of a
new `exposeLevelMVars` function that adds pretty printer annotations
that try to expose all universe level metavariables.
* When there are universe level metavariables, for error recovery the
definition is still added to the environment after assigning each
metavariable to level 0.
* There's a new `Lean.Util.CollectLevelMVars` module for collecting
level metavariables from expressions.
Closes#2058
Resolve cases when the `To/FromJSON` type classes are used with `Empty`,
e.g. in the following motivating example.
```
import Lean
structure Foo (α : Type) where
y : Option α
deriving Lean.ToJson
#eval Lean.toJson (⟨none⟩ : Foo Empty) -- fails
```
This is a follow-up to this PR
https://github.com/leanprover/lean4/pull/5415, as suggested by
@eric-wieser. It expands on the original suggestion by also handling
`FromJSON`.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Previously, it was not possible to use `decide` with most Array
functions (including `==`).
Later, we may replace some of these functions with defeqs that go via
the `List` operations, and use `csimp` lemmas for fast runtime
behaviour. In the meantime, this allows using `decide`.
Given the derived `Repr` instance for types with parameters, the absence
of `Repr Empty` can cause `Repr` instance synthesis to fail. For
example, given
```lean
inductive Prim (special : Type) where
| plus
| other : special → Prim special
deriving Repr
```
this works:
```lean
#eval (Prim.plus : Prim Int)
```
but this fails:
```lean
#eval (Prim.plus : Prim Empty)
```
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This implements the first half of #3302: It improves the extensible
`apply_rfl` tactic (the one that looks at `refl` attributes, part of
the `rfl` macro) to
* Check itself and ahead of time that the lhs and rhs are defEq, and
give
a nice consistent error message when they don't (instead of just passing
on
the less helpful error message from `apply Foo.refl`), and using the
machinery that `apply` uses to elaborate expressions to highlight diffs
in implicit arguments.
* Also handle `Eq` and `HEq` (built in) and `Iff` (using the attribute)
Care is taken that, as before, the current transparency setting affects
comparing the lhs and rhs, but not the reduction of the relation
So before we had
```lean
opaque P : Nat → Nat → Prop
@[refl] axiom P.refl (n : Nat) : P n n
/--
error: tactic 'apply' failed, failed to unify
P ?n ?n
with
P 42 23
⊢ P 42 23
-/
#guard_msgs in
example : P 42 23 := by apply_rfl
opaque withImplicitNat {n : Nat} : Nat
/--
error: tactic 'apply' failed, failed to unify
P ?n ?n
with
P withImplicitNat withImplicitNat
⊢ P withImplicitNat withImplicitNat
-/
#guard_msgs in
example : P (@withImplicitNat 42) (@withImplicitNat 23) := by apply_rfl
```
and with this PR the messages we get are
```
error: tactic 'apply_rfl' failed, The lhs
42
is not definitionally equal to rhs
23
⊢ P 42 23
```
resp.
```
error: tactic 'apply_rfl' failed, The lhs
@withImplicitNat 42
is not definitionally equal to rhs
@withImplicitNat 23
⊢ P withImplicitNat withImplicitNat
```
A test file checks the various failure modes and error messages.
I believe this `apply_rfl` can serve as the only implementation of
`rfl`, which would then complete #3302, and actually expose these
improved
error messages to the user. But as that seems to require a
non-trivial bootstrapping dance, it’ll be separate.
closes#5333
This PR tries to address issue #5333.
My conjecture is that the binder annotations for `C.toB` and
`Algebra.toSMul` are not ideal. `Algebra.toSMul` is one of declarations
where the new command `set_synth_order` was used. Both classes, `C` and
`Algebra`, are parametric over instances, and in both cases, the issue
arises due to projection instances: `C.toB` and `Algebra.toSMul`. Let's
focus on the binder annotations for `C.toB`. They are as follows:
```
C.toB [inst : A 20000] [self : @C inst] : @B ...
```
As a projection, it seems odd that `inst` is an instance-implicit
argument instead of an implicit one, given that its value is fixed by
`self`. We observe the same issue in `Algebra.toSMul`:
```
Algebra.toSMul {R : Type u} {A : Type v} [inst1 : CommSemiring R] [inst2 : Semiring A]
[self : @Algebra R A inst1 inst2] : SMul R A
```
The PR changes the binder annotations as follows:
```
C.toB {inst : A 20000} [self : @C inst] : @B ...
```
and
```
Algebra.toSMul {R : Type u} {A : Type v} {inst1 : CommSemiring R} {inst2 : Semiring A}
[self : @Algebra R A inst1 inst2] : SMul R A
```
In both cases, the `set_synth_order` is used to force `self` to be
processed first.
In the MWE, there is no instance for `C ...`, and `C.toB` is quickly
discarded. I suspect a similar issue occurs when trying to use
`Algebra.toSMul`, where there is no `@Algebra R A ... ...`, but Lean
spends unnecessary time trying to synthesize `CommSemiring R` and
`Semiring A` instances. I believe the new binder annotations make sense,
as if there is a way to synthesize `Algebra R A ... ...`, it will tell
us how to retrieve the instance-implicit arguments.
TODO:
- Impact on Mathlib.
- Document changes.
---------
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
We need to follow the fvar aliases registered by `match` in both
directions
Fixes#4714, fixes#2837
---------
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
In LNSym we often use the pattern `ofBool (a.getLsbD i)` to pick out a
specific bit (`i`) from a bitvector (`a`).
By adding a rewrite to `extractLsb` to `bv_decide`s normalization set,
we can still automatically close goals that have this pattern. In the
process, I also added a simp-lemma about the value of a `Fin 1`.
A round of clean-up for the context of the functional induction
principle cases.
* Already previously, with `match e with | p => …`, functional induction
would ensure that `h : e = p` is in scope, but it wouldn’t work in
dependent cases. Now it introduces heterogeneous equality where needed
(fixes#4146)
* These equalities are now added always (previously we omitted them when
the discriminant was a variable that occurred in the goal, on the
grounds that the goal gets refined through the match, but it’s more
consistent to introduce the equality in any case)
* We no longer use `MVarId.cleanup` to clean up the goal; it was
sometimes too aggressive (fixes#5347)
* Instead, we clean up more carefully and with a custom strategy:
* First, we substitute all variables without a user-accessible name, if
we can.
* Then, we substitute all variable, if we can, outside in.
* As we do that, we look for `HEq`s that we can turn into `Eq`s to
substitute some more
* We substitute unused `let`s.
**Breaking change**: In some cases leads to a different functional
induction principle (different names and order of assumptions, for
example).
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.
