This PR adds a feature to the the mutual def elaborator where the
`instance` command yields theorems instead of definitions when the class
is a `Prop`.
Closes#5672
This default instance makes it possible to write things like `m!"the
constant is {.ofConstName n}"`.
Breaking change: This weakly causes terms to have a type of
`MessageData` if their type is otherwise unknown. For example:
* `m!"... {x} ..."` can cause `x` to have type `MessageData`, causing
the `let` definition of `x` to fail to elaborate. Fix: give `x` an
explicit type.
* Arithmetic expressions in `m!` strings may need a type ascription. For
example, if the type of `i` is unknown at the time the arithmetic
expression is elaborated, then `m!"... {i + 1} ..."` can fail saying
that it cannot find an `HAdd Nat Nat MessageData` instance. Two fixes:
either ensure that the type of `i` is known, or add a type ascription to
guide the `MessageData` coercion, like `m!"... {(i + 1 : Nat)} ..."`.
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
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.
When `set_option diagnostics true`, for each theorem with size >
`diagnostics.threshold.proofSize`, display proof size, and the number of
applications for each constant symbol.
A more restrictive but efficient max sharing primitive.
**Motivation:** Some software verification proofs may contain
significant redundancy that can be eliminated using hash-consing (also
known as `shareCommon`). For example, [theorem
`sha512_block_armv8_test_4_sym`](460fe5d74c/Proofs/SHA512/SHA512Sym.lean (L29))
took a few seconds at [`addPreDefinitions`
](1a12f63f74/src/Lean/Elab/PreDefinition/Main.lean (L155))
and one second at `fixLevelParams` on a MacBook Pro (with M1 Pro). The
proof term initially had over 16 million subterms, but the redundancy
was indirectly and inefficiently eliminated using `Core.transform` at
`addPreDefinitions`. I tried to use `shareCommon` method to fix the
performance issue, but it was too inefficient. This PR introduces a new
`shareCommon'` method that, although less flexible (e.g., it uses only a
local cache and hash-consing table), is much more efficient. The new
procedure minimizes the number of RC operations and optimizes the
caching strategy. It is 20 times faster than the old `shareCommon`
procedure for theorem `sha512_block_armv8_test_4_sym`.
This PR addresses the absence of the `profileitM` function in two
auxiliary functions. The added `profileitM` instances are particularly
useful for diagnosing performance issues in declarations that contain
many repeated sub-terms.
This adds support for mutual structural recursive functions.
For now this is opt-in: The functions must have a `termination_by
structural …` annotation (new since #4542) for this to work:
```lean
mutual
inductive A
| self : A → A
| other : B → A
| empty
inductive B
| self : B → B
| other : A → B
| empty
end
mutual
def A.size : A → Nat
| .self a => a.size + 1
| .other b => b.size + 1
| .empty => 0
termination_by structural x => x
def B.size : B → Nat
| .self b => b.size + 1
| .other a => a.size + 1
| .empty => 0
termination_by structural x => x
end
```
The recursive functions don’t have to be in a one-to-one relation to a
set of mutually recursive inductive data types. It is possible to ignore
some of the types:
```lean
def A.self_size : A → Nat
| .self a => a.self_size + 1
| .other _ => 0
| .empty => 0
termination_by structural x => x
```
or have more than one function per argument type:
```lean
def isEven : Nat → Prop
| 0 => True
| n+1 => ¬ isOdd n
termination_by structural x => x
def isOdd : Nat → Prop
| 0 => False
| n+1 => ¬ isEven n
termination_by structural x => x
```
This does not include
* Support for nested inductive data types or nested recursion
* Inferring mutual structural recursion in the absence of
`termination_by`.
* Functional induction principles for these.
* Mutually recursive functions that live in different universes. This
may be possible,
maybe after beefing up the `.below` and `.brecOn` functions; we can look
into this some
other time, maybe when there are concrete use cases.
---------
Co-authored-by: Richard Kiss <him@richardkiss.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This implements the `termination_by structural` syntax proposed in
#3909.
I went with `termination_by structural` over, say,
`termination_by (config := {method := .structural})` mainly because it
was
easier to get going (otherwise I’d have to look into how to define
recursive
parsers, as `Parser.config` depends on `term` and `termination_by` is
part of
term. But also because I find it more ergonomic and aesthetic as a user.
But syntax can still change.
The `termination_by?` syntax will no longer force well-founded
recursion,
and instead the inferred `termination_by structurally` annotation will
be shown
if structural termination is possible.
While I was it, this fixes#4546 the easy way (log errors about but
otherwise
ignore incomplete `termination_by` sets for mutual recursion). Maybe we
get
multiple replacements (#4551), but even then this this good behavior.
Involves a bit of shuffling around `TerimationHints` (now validated for
a
clique already by `PreDefinition.main`) and `TerminationArguments` (now
lifted
out of the `WF` namespace, and a bit simplified).
Fixes#3909
---------
Co-authored-by: Richard Kiss <him@richardkiss.com>
Implements a new method to generate instance names for anonymous
instances that uses a heuristic that tends to produce shorter names. A
design goal is to make them relatively unique within projects and
definitely unique across projects, while also using accessible names so
that they can be referred to as needed, both in Lean code and in
discussions.
The new method also takes into account binders provided to the instance,
and it adds project-based suffixes. Despite this, a median new name is
73% its original auto-generated length. (Compare: [old generated
names](https://gist.github.com/kmill/b72bb43f5b01dafef41eb1d2e57a8237)
and [new generated
names](https://gist.github.com/kmill/393acc82e7a8d67fc7387829f4ed547e).)
Some notes:
* The naming is sensitive to what is explicitly provided as a binder vs
what is provided via a `variable`. It does not make use of `variable`s
since, when names are generated, it is not yet known which variables are
used in the body of the instance.
* If the instance name refers to declarations in the current "project"
(given by the root module), then it does not add a suffix. Otherwise, it
adds the project name as a suffix to protect against cross-project
collisions.
* `set_option trace.Elab.instance.mkInstanceName true` can be used to
see what name the auto-generator would give, even if the instance
already has an explicit name.
There were a number of instances that were referred to explicitly in
meta code, and these have been given explicit names.
Removes the unused `Lean.Elab.mkFreshInstanceName` along with the
Command state's `nextInstIdx`.
Fixes#2343
This change
* moves `termination_by` and `decreasing_by` next to the function they
apply to
* simplify the syntax of `termination_by`
* apply the `decreasing_by` goal to all goals at once, for better
interactive use.
See the section in `RELEASES.md` for more details and migration advise.
This is a hard breaking change, requiring developers to touch every
`termination_by` in their code base. We decided to still do it as a
hard-breaking change, because supporting both old and new syntax at the
same time would be non-trivial, and not save that much. Moreover, this
requires changes to some metaprograms that developers might have
written, and supporting both syntaxes at the same time would make
_their_ migration harder.
@Kha This is a hack to try to fix the build.
It seems it is the circular dependency issue again.
Remarks:
- The problem doesn't happen on my Mac.
- I managed to reproduce the Linux error on a virtual machine.
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommonT_monadShareCommon___rarg':
ShareCommon.c:(.text+0xc9): undefined reference to `lean_state_sharecommon'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_PShareCommonT_monadShareCommon___rarg':
ShareCommon.c:(.text+0x259): undefined reference to `lean_persistent_state_sharecommon'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommon_Object_hash___boxed':
ShareCommon.c:(.text+0x59a): undefined reference to `lean_sharecommon_hash'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_shareCommon___rarg':
ShareCommon.c:(.text+0x6cf): undefined reference to `lean_state_sharecommon'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommon_Object_eq___boxed':
ShareCommon.c:(.text+0x82d): undefined reference to `lean_sharecommon_eq'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_PShareCommonT_withShareCommon___rarg':
ShareCommon.c:(.text+0x956): undefined reference to `lean_persistent_state_sharecommon'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommonT_withShareCommon___rarg':
ShareCommon.c:(.text+0xae6): undefined reference to `lean_state_sharecommon'
/
@Kha This is a performance bottleneck in a several benchmarks that
create huge proofs. It may negatively affect other files.
I will keep an eye at the speedcenter.
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
