This PR adds the new transparency setting `@[instance_reducible]`. We
used to check whether a declaration had `instance` reducibility by using
the `isInstance` predicate. However, this was not a robust solution
because:
- We have scoped instances, and `isInstance` returns `true` only if the
scope is active.
- We have auxiliary declarations used to construct instances manually,
such as:
```lean
def lt_wfRel : WellFoundedRelation Nat
```
`isInstance` also returns `false` for this kind of declaration.
In both cases, the declaration may be (or may have been) used to
construct an instance, but `isInstance`
returns `false`. Thus, we claim it is a mistake to check the
reducibility status using `isInstance`.
`isInstance` indicates whether a declaration is available for the type
class resolution mechanism,
not its transparency status.
**We are decoupling whether a declaration is available for type class
resolution from its transparency status.**
**Remak**: We need a update stage0 to complete this feature.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR fixes an issue where `grind` fails when trying to unfold a
definition by pattern matching imported by `import all` (or from a
non-`module`).
Fixes#11715
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR fixes an issue where a `by` in the public scope could create an
auxiliary theorem for the proof whose type does not match the expected
type in the public scope.
Fixes#11672
This PR switches the way olean files store identifier suggestions. The
ordering introduced in #11367 and #11529 made sense if we were only
storing incorrect -> correct mappings, but for the reference manual we
want to store the correct -> incorrect mappings as well, and so it is
more sensible to store just the correct -> incorrect mapping that mimics
the author-generated data better.
Also tweaks error messages further in preparation for public-facing
@[suggest_for] annotations and forbids suggestions on non-public names.
Does not make generally-visible changes as there are no introduced uses
of @[suggest_for] annotations yet.
This PR refines several error error messages, mostly involving invalid
use of field notation, generalized field notation, and numeric
projection. Provides a new error explanation for field notation.
## Error message changes
In general:
- Uses a slightly different convention for expression-type pairs, where
the expression is always given `indentExpr` and the type is given
`inlineExpr` treatment. This is something of a workaround for the fact
that the `Format` type is awkward for embedding possibly-linebreaking
expressions in not-linebreaking text, which may be a separate issue
worth addressing.
- Tries to give slightly more "why" reasoning — the environment does not
contain `String.parse`, and _therefore you can't project `.parse` from a
`String`_.
Some specific examples:
### No such projection function
```lean4
#check "".parse
```
before:
```
error: Invalid field `parse`: The environment does not contain `String.parse`
""
has type
String
```
after:
```
error: Invalid field `parse`: The environment does not contain `String.parse`, so it is not possible to project the field `parse` from an expression
""
of type `String`
```
### Type does not have the correct form
```lean4
example (x : α) := (foo x).foo
```
before:
```
error: Invalid field notation: Type is not of the form `C ...` where C is a constant
foo x
has type
α
```
after:
```
error: Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
foo x
has type `α` which does not have the necessary form.
```
## Refactoring
Includes some refactoring changes as well:
- factors out multiple uses of number (1, 2, 3, 212, 222) to ordinal
("first", "second", "third", "212th", "222nd") conversion into
Lean.Elab.ErrorUtils
- significant refactoring of `resolveLValAux` in `Lean.Elab.App` — in
place of five helper functions, a special-case function case analysis,
and a case analysis on the projection type and structure, there's now a
single case analysis on the projection type and structure. This allows
several error messages to be more explicit (there were a number of cases
where index projection was being described as field projection in an
error messages) and gave the opportunity to slightly improve positining
for several errors: field *notation* errors should appear on `foo.bar`,
but field *projection* errors should appear only on the `bar` part of
`foo.bar`.
This PR lets recursive functions defined by well-founded recursion use a
different `fix` function when the termination measure is of type `Nat`.
This fix-point operator use structural recursion on “fuel”, initialized
by the given measure, and is thus reasonable to reduce, e.g. in `by
decide` proofs.
Extra provisions are in place that the fixpoint operator only starts
reducing when the fuel is fully known, to prevent “accidential” defeqs
when the remaining fuel for the recursive calls match the initial fuel
for that recursive argument.
To opt-out, the idiom `termination_by (n,0)` can be used.
We still use `@[irreducible]` as the default for such recursive
definitions, to avoid unexpected `defeq` lemmas. Making these functions
`@[semireducible]` by default showed performance regressions in lean.
When the measure is of type `Nat`, the system will accept an explicit
`@[semireducible]` without the usual warning.
Fixes#5234. Fixes: #11181.
This PR ensures private declarations are accessible from the private
scope iff they are local or imported through an `import all` chain,
including for anonymous notation and structure instance notation.
This PR fixes a potential miscompilation when using non-exposed type
definitions using the module system by turning it into a static error. A
future revision may lift the restriction by making the compiler metadata
independent of the current module.
This PR refines and clarifies the `meta` phase distinction in the module
system.
* `meta import A` without `public` now has the clarified meaning of
"enable compile-time evaluation of declarations in or above `A` in the
current module, but not downstream". This is now checked statically by
enforcing that public meta defs, which therefore may be referenced from
outside, can only use public meta imports, and that global evaluating
attributes such as `@[term_parser]` can only be applied to public meta
defs.
* `meta def`s may no longer reference non-meta defs even when in the
same module. This clarifies the meta distinction as well as improves
locality of (new) error messages.
* parser references in `syntax` are now also properly tracked as meta
references.
* A `meta import` of an `import` now properly loads only the `.ir` of
the nested module for the purposes of execution instead of also making
its declarations available for general elaboration.
* `initialize` is now no longer being run on import under the module
system, which is now covered by `meta initialize`.
This PR addresses a missing check in the module system where private
names that remain in the public environment map for technical reasons
(e.g. inductive constructors generated by the kernel and relied on by
the code generator) accidentally were accessible in the public scope.
This PR updates the formatting of, and adds explanations for, "unknown
identifier" errors as well as "failed to infer type" errors for binders
and definitions.
It attempts to ameliorate some of the confusion encountered in #1592 by
modifying the wording of the "header is elaborated before body is
processed" note and adding further discussion and examples of this
behavior in the corresponding error explanation.
This PR improves the “expected type mismatch” error message by omitting
the type's types when they are defeq, and putting them into separate
lines when not.
I found it rather tediuos to parse the error message when the expected
type is long, because I had to find the `:` in the middle of a large
expression somewhere. Also, when both are of sort `Prop` or `Type` it
doesn't add much value to print the sort (and it’s only one hover away
anyways).
This PR adjusts the experimental module system to make `private` the
default visibility modifier in `module`s, introducing `public` as a new
modifier instead. `public section` can be used to revert the default for
an entire section, though this is more intended to ease gradual adoption
of the new semantics such as in `Init` (and soon `Std`) where they
should be replaced by a future decl-by-decl re-review of visibilities.
This PR introduces an explicit `defeq` attribute to mark theorems that
can be used by `dsimp`. The benefit of an explicit attribute over the
prior logic of looking at the proof body is that we can reliably omit
theorem bodies across module boundaries. It also helps with intra-file
parallelism.
If a theorem is syntactically defined by `:= rfl`, then the attribute is
assumed and need not given explicitly. This is a purely syntactic check
and can be fooled, e.g. if in the current namespace, `rfl` is not
actually “the” `rfl` of `Eq`. In that case, some other syntax has be
used, such as `:= (rfl)`. This is also the way to go if a theorem can be
proved by `defeq`, but one does not actually want `dsimp` to use this
fact.
The `defeq` attribute will look at the *type* of the declaration, not
the body, to check if it really holds definitionally. Because of
different reduction settings, this can sometimes go wrong. Then one
should also write `:= (rfl)`, if one does not want this to be a defeq
theorem. (If one does then this is currently not possible, but it’s
probably a bad idea anyways).
The `set_option debug.tactic.simp.checkDefEqAttr true`, `dsimp` will
warn if could not apply a lemma due to a missing `defeq` attribute.
With `set_option backward.dsimp.useDefEqAttr.get false` one can revert
to the old behavior of inferring rfl-ness based on the theorem body.
Both options will go away eventually (too bad we can’t mark them as
deprecated right away, see #7969)
Meta programs that generate theorems (e.g. equational theorems) can use
`inferDefEqAttr` to set the attribute based on the theorem body of the
just created declaration.
This builds on #8501 to update Init to `@[expose]` a fair amount of
definitions that, if not exposed, would prevent some existing `:= rfl`
theorems from being `defeq` theorems. In the interest of starting
backwards compatible, I exposed these function. Hopefully many can be
un-exposed later again.
A mathlib adaption branch exists that includes both the meta programming
fixes and changes to the theorems (e.g. changing `:= by rfl` to `:=
rfl`).
With the module system there is now no special handling for `defeq`
theorem bodies, because we don’t look at the body anymore. The previous
hack is removed. The `defeq`-ness of the theorem needs to be checked in
the context of the theorem’s *type*; the error message contains a hint
if the defeq check fails because of the exported context.
This PR makes the equational theorems of non-exposed defs private. If
the author of a module chose not to expose the body of their function,
then they likely don't want that implementation to leak through
equational theorems. Helps with #8419.
There is some amount of incidential complexity due to how `private`
works in lean, by mangling the name: lots of code paths that need now do
the right thing™ about private and non-private names, including the
whole reserved name machinery.
So this includes a number of refactorings:
* The logic for calculating an equational theorem name (or similar) is
now done by a single function, `mkEqLikeNameFor`, rather than all over
the place.
* Since the name of the equational theorem now depends on the current
context (in particular whether it’s a proper module, or a non-module
file), the forward map from declaration to equational theorem doesn’t
quite work anymore. This map is deleted; the list of equational theorems
are now always found by looking for declaration of the expected names
(`alreadyGenerated). If users define such theorems themselves (and make
it past the “do not allow reserved names to be declared”) they get to
keep both pieces.
* Because this map was deleted, mathlib’s `eqns` command can no longer
easily warn if equational lemmas have already been generated too early
(adaption branch exists). But in general I think lean could provide a
more principled way of supporting custom unfold lemmas, and ideally the
whole equational theorem machinery is just using that.
* The ReservedNamePredicate is used by `resolveExact`, so we need to
make sure that it returns the right name, including privateness. It is
not ok to just reserve both the private and non-private name but then
later in the ReservedNameAction produce just one of the two.
* We create `foo.def_eq` eagerly for well-founded recursion. This is
needed because we need feed in the proof of the rewriting done by
`wf_preprocess`. But if `foo.def_eq` is private in a module, then a
non-module importing it will still expect a non-private `foo.def_eq` to
exist. To patch that, we install a `copyPrivateUnfoldTheorem :
GetUnfoldEqnFn` that declares a theorem aliasing the private one. Seems
to work.
This PR adjusts the experimental module system to not export the bodies
of `def`s unless opted out by the new attribute `@[expose]` on the `def`
or on a surrounding `section`.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR ensures that for modules opted into the experimental module
system, we do not import module docstrings or declaration ranges.
Excluding declaration docstrings as well would require some more work to
make `[inherit_doc]` leave a mere reference to the other declaration
instead of copying its docstring eagerly.
