If here is only one plausible measure, there is no point having the
`GuessLex` code see if it
is terminating, running all the tactics, only for the `MkFix` code then
run the tactics again.
So if there is only one plausible measure (non-mutual recursion with
only one varying
parameter), just use that measure.
Side benefit: If the function isn’t terminating, more detailed error
messages are shown
(failing proof goals), located at the recursive calls.
This improves Lean’s capabilities to guess the termination measure for
well-founded
recursion, by also trying lexicographic orders. For example:
def ackermann (n m : Nat) := match n, m with
| 0, m => m + 1
| .succ n, 0 => ackermann n 1
| .succ n, .succ m => ackermann n (ackermann (n + 1) m)
now just works.
The module docstring of `Lean.Elab.PreDefinition.WF.GuessLex` tells the
technical story.
Fixes#2837
This PR adds per-package server options to resolve#2455. It is based on
the previous work in #2456, but takes a different approach: options are
loaded for the specific file in the file worker when `print-paths` is
called, instead of loading them in the watchdog with a separate Lake
command. This change addresses review comments made in #2456.
In doing so, it introduces two new Lake config fields:
- `leanOptions`: `-D` flag options that are passed to both the language
server and `lean` when building.
- `moreServerOptions`: `-D` flag options that are passed to the language
server.
Since `print-paths` must also accept a file path to compute the options
for that file, this PR is changing the API for `print-paths`. As there
have been numerous complaints about the name `print-paths`, I also
decided to change it to `setup-file` in this PR, since it would break
compatibility with the old Lake API anyways.
This PR deprecates the Lakefile field `moreServerArgs` in favor of
`moreGlobalServerArgs`, as suggested in the review for #2456.
Fixes#2455
---------
Co-authored-by: digama0 <mcarneir@andrew.cmu.edu>
This was a Lean 3 pretty printer option. While this pretty printer
option tends to lead to confusing situations when set, it has been
frequently requested. [It is
possible](https://github.com/leanprover-community/mathlib4/pull/7910) to
implement this pretty printer option as a user, but it comes with some
artifacts -- for instance, expressions in hovers are not beta reduced.
Adding this as a core pp option is cleanest.
(We should consider having hooks into the tactic evaluator to allow
users to transform the tactic state between tactics. This would enable
beta reducing the entire local context for real, which would be useful
for teaching.)
Closes#715
The `packMutual` code ought to reliably replace all recursive calls to
the functions in `preDefs`, even when they are under- or over-applied.
Therefore eta-expand if need rsp. keep extra arguments around.
Needs a tweak to `Meta.transform` to avoid mistaking the `f` in
`f x1 x2` as a zero-arity application.
Includes a test case.
This fixes#2628 and #2883.
This didn't work before
```
def f (n : Nat) : Nat :=
match n with
| 0 => 0
| n + 1 => (f) n
```
because the `RecApp` metadata marker gets in the way. More practically
relevant, such code is to be produced when using `rw` or `simp` in
recursive theorems (see included test case).
We can fix this by preprocessing the definitions and floating the
`.mdata` marker out of applications.
For structural recursion, there already exists a `preprocess` function;
this now also floats out `.mdata` markers.
For well-founded recursion, this introduces an analogous `preprocess`
function.
Fixes#2810.
One test case output changes: With the `.mdata` out of the way, we get a
different error message. Seems fine.
Alternative approaches are:
* Leaving the `.mdata` marker where it is, and looking around it.
Tried in #2813, but not nice (many many places where `withApp` etc.
need to be adjusted).
* Moving the `.mdata` _inside_ the application, so that `withApp` still
works. Tried in #2814. Also not nice, the invariant that the `.mdata`
is around the `.const` is tedious to maintain.
the code stumbled over recursive functions whose type doesn’t have
enough manifest foralls, like:
```
def FunType := Nat → Nat
mutual
def foo : FunType
| .zero => 0
| .succ n => bar n
def bar : FunType
| .zero => 0
| .succ n => foo n
end
termination_by foo n => n; bar n => n
```
This can be fixed by using `whnf` in appropriate places, to expose the
`.forall` constructor.
Fixes#2925, comes with test case.
This implements a request handler for the `textDocument/rename` LSP
request, enabling renames via F2. It handles both local renames (e.g.
`let x := 1; x` to `let y := 1; y`) as well as global renames
(definitions).
Unfortunately it does not work for "orphan" files outside a project, as
it uses ilean data for the current file and this does not seem to be
saved for orphan files. As a result, the test file does not work,
although one can manually test the implementation against a project such
as mathlib. (This issue already exists for the "references" request,
e.g. ctrl click on the first `x` in `let x := 1; x` takes you to the
second one only if you are not in an orphan file.)
* Fixesleanprover-community/mathlib4#7124
previously, it would ignore a recursive call that has extra arguments,
which can happen when the recursive functions return something of
function type. Therefore just leave them extra arguments in place.
Fixes#2883.
previously, only the WellFounded code was making use of the error
location in the RecApp-metadata. We can do the same for structural
recursion. This way,
```
def f (n : Nat) : Nat :=
match n with
| 0 => 0
| n + 1 => f (n + 1)
```
will show the error with squiggly lines under `f (n + 1)`, and not at
`def f`.
`simp` was previously swallowing runtime exceptions and masking an
issue with this example.
`runT` is defined by well-founded recursion, but reducing the ground
term `runT x` takes a long time when `decide := true`.
Remark PR #2722 changes the `decide` default value to `false`.
When `decide := true`, we should probably have better diagnostics /
error messages for this kind of situation.
This is the same flag that the C test uses. Previously this was hidden
in the Lean compiler itself but now that the optimization pass is phased
out of the compiler we need to put it here.
Co-authored-by: Henrik Böving <hargonix@gmail.com>
The notation `a ∈ as` for Arrays was previously only defined with
`DecidableEq` on the elements, for (apparently) no good reason. This
drops this requirements (by using `a ∈ as.data`), and simplifies a bunch
of proofs by simply lifting the corresponding proof from lists.
Also, `sizeOf_lt_of_mem` was defined, but not set up to be picked up by
`decreasing_trivial` in the same way that the corresponding List lemma
was set up, so this adds the tactic setup.
The definition for `a ∈ as` is intentionally not defeq to `a ∈ as.data`
so that the termination tactics for Arrays don’t spuriously apply when
recursing through lists.
This commit also removes parameter `simpleReduce` from discrimination
trees, and take WHNF configuration options.
Reason: it is more dynamic now. For example, the simplifier
will be able to use different configurations for discrimination tree insertion
and retrieval. We need this feature to address issues #2669 and #2281
This commit also removes the dead Meta.Config field `zetaNonDep`.
