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.
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
```
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.
