This extends `derive_functional_induction` to work with structural
recursion as well.
It produces the less general, more concrete induction rule where the
induction hypothesis is
specialized for every argument of the recursive call, not just the the
one that the function
is recursing on.
Care is taken so that the induction principle and it's motive take the
arguments in the same
order as the original function.
While I was it, also makes sure that the order of the cases in the
induction principle matches
the order of recursive calls in the function better.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This shortens `Array.findIdx?` code, by using termination_by (and
well-founded recursion) instead of a structural recursion trick, with
the intent to make it more proof friendly.
One motivation is that it makes it easier to write a proof that
`Array.findIdx?` and `List.findIdx?` are equivalent. Furthermore, this
will be useful to prove that more complex functions are equivalent.
Closes#3646
System.FilePath.parent did not return the correct parent path in the
case of absolute file paths
Example of previous behavior
```
(FilePath.mk "/foo").parent -> some (FilePath.mk "")
(System.FilePath.mk "/").parent -> some (FilePath.mk "")
```
The new behavior is based on rust's std::path::Path::parent function (as
previously described in comment in System.FilePath)
Example of updated behavior
```
(System.FilePath.mk "/foo").parent -> some (FilePath.mk "/")
(System.FilePath.mk "/").parent -> none
```
Behavior for relative file paths is unchanged
Closes#3618
Given a definition `foo`, they were previously called `foo._unfold`
until 4.7.0. We tried to rename them to `foo.def`, but it created too
many issues in the Mathlib repo. We decided to rename it again to
`foo.eq_def`. The new name is also consistent with the `eq_<idx>`
theorems generated for different "cases". That is, `foo.eq_def` is the
equality theorem for the whole definition, and `foo.eq_<idx>` is the
equality theorem for case `<idx>`.
cc @semorrison
`FileMap.lines` is an array that seems to be manually managed to have
the form `#[1, 2, ..., n-1, n-1]` with same length as
`FileMap.positions`. Remove this structure field in favour of
calculating the line number as `min(x+1, positions.size-1)` when needed.
Follow-up on #3221
Given
```lean
structure A where
x : Nat
structure B extends A where
y : Nat
```
rather than pretty printing `{ x := 1, y := 2 : B }` as `{ toA := { x :=
1 }, y := 2 }`, it now pretty prints as `{ x := 1, y := 2 }`.
The option `pp.structureInstances.flatten` controls whether to flatten
structure instances like this.
This updates the rw? tactic from Mathlib to use lazy discriminator trees
and upstreams it.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sets the default value to `pp.fieldNotation.generalized` to `true`.
Updates tests, and fixes some minor flaws in the implementation of the
generalized field notation pretty printer.
Now generalized field notation won't be used for any function that has a
`motive` argument. This is intended to prevent recursors from pretty
printing using it as (1) recursors are more like control flow structures
than actual functions and (2) generalized field notation tends to cause
elaboration problems for recursors.
Note: be sure functions that have an `@[app_unexpander]` use
`@[pp_nodot]` if applicable. For example, `List.toArray` needs
`@[pp_nodot]` to ensure the unexpander prints it using `#[...]`
notation.
The concrete dependency that is stale isn't really actionable
information for users (ideally we'd like something like "amount of
dependencies that will be rebuilt when you restart file"). This also
makes the diagnostic an "information" diagnostic so that non-infoview
users can still see it.
Since we are moving away from using notifications for stale dependency
information, we don't need to provide an ID anymore, either.
Refactors app delaborator, merging in the projection delaborator, to
support pretty printing with generalized field notation.
Renames option `pp.structureProjections` to `pp.fieldNotation` and adds
sub-option `pp.fieldNotation.generalized` to enable/disable generalized
field notation. Adds `@[pp_nodot]` attribute to permanently disable
using field notation for a given declaration.
For now, the default value of `pp.fieldNotation.generalized` is false
since we need a stage0 update to add `@[pp_nodot]` to some core
definitions (such as `List.toArray`) before updating the tests.
[Zulip
discussion](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60pp.2EgeneralizedFieldNotation.60/near/425856054)
This attribute, which was implemented in #3640, is applied to the
following structures: `Sigma`, `PSigma`, `PProd`, `And`, `Subtype`, and
`Fin`. These were given this attribute in Lean 3.
This coercion caused difficult-to-diagnose bugs sometimes. Because there
are some situations where converting a string to a name should be done
by parsing the string, and others where it should not, an explicit
choice seems better here.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
I forgot to use the sticky diagnostics in `getInteractiveDiagnostics` in
#3247, leading to them not consistently showing up in the "Messages"
panel of the InfoView.
This lead to incorrect diagnostic spans in the editor and resulted in
header errors that did not show up under "Messages" everywhere in the
file because the `fullRange?` property was missing.
Also changes the "Import out of date" warning diagnostic severity to
"Hint" so that it doesn't show up in the "Problems" view.
This is a rewrite of the `UnusedVariables` lint to inline and simplify
many of the dependent functions to try to improve the performance of
this lint, which quite often shows up in perf reports.
* The mvar assignment scanning is one of the most expensive parts of the
process, so we do two things to improve this:
* Lazily perform the scan only if we need it
* Use an object-pointer hashmap to ensure that we don't have quadratic
behavior when there are many mvar assignments with slight differences.
* The dependency on `Lean.Server` is removed, meaning we don't need to
do the LSP conversion stuff anymore. The main logic of reference finding
is inlined.
* We take `fvarAliases` into account, and union together fvars which are
aliases of a base fvar. (It would be great if we had `UnionFind` here.)
More docs will be added once we confirm an actual perf improvement.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Closes#3706
This derive handler's implementation is very similar to `BEq`'s, which
already ignores unused alternative so as to work correctly on indexed
inductive types. This PR simply implements the same solution as the one
present in
[`BEq.lean`](2c15cdda04/src/Lean/Elab/Deriving/BEq.lean (L94)).
After some tests, it doesn't seem like any other derive handler present
in Core suffers from the same issue (though some handlers don't work on
indexed inductives for other reasons).
Sends a diagnostic informing the user to run Restart File when a file
dependency is saved.
Based on #3014 because this feature was easier to implement with the new
architecture.
ToDo:
- [x] Adjust vscode-lean4 to display a notification when this diagnostic
appears in a non-annoying way
(https://github.com/leanprover/vscode-lean4/pull/393)
- [x] Use a file watcher to identify changes to files not tracked by VS
Code
- [x] Rebase onto master when #3014 is merged
These are used in Mathlib's `congr!` and `convert` tactics, which will
be upstreamed soon.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
