this makes the ugly `fst`/`snd` variable names in the functional
induction principles go away.
Ironically I thought in order to fix these name, I should touch the
mutual/n-ary argument packing code used for well-founded recursion, and
embarked on a big refactor/rewrite of that code, only to find that at
least this particular instance of the issue was somewhere else. Hence
breaking this into its own PR; the refactoring will follow (and will
also improve some other variable names.)
closes#3022
With this commit, given the declaration
```
def foo : Nat → Nat
| 0 => 2
| n + 1 => foo n
```
when we unfold `foo (n+1)`, we now obtain `foo n` instead of `foo
(Nat.add n 0)`.
This fixes an issue discovered in Mathlib with the meta cache being
poisoned by using a name generator. It is difficult to reproduce due to
the name collisions being rare, but here is a minimal module with
definitions that result in an error:
```lean
prelude
universe u
inductive Unit2 : Type where
| unit : Unit2
inductive Eq2 {α : Sort u} : α → α → Prop where
| refl (a : α) : Eq2 a a
structure Subtype2 {α : Sort u} (p : α → Prop) where
val : α
def End (α) := α → α
theorem end_app_eq (α : Type u) (f : End α) (a : α) : Eq2 (f a) (f a) := Eq2.refl _
theorem Set.coe_eq_subtype {α : Type u} (s : α → Prop) : Eq2 (Subtype2 s) (Subtype2 s) := Eq2.refl _
def succAboveCases {_ : Unit2} {α : Unit2 → Sort u} (i : Unit2) (v : α i) : α i := v
theorem succAbove_cases_eq_insertNth : Eq2 @succAboveCases.{u + 1} @succAboveCases.{u + 1} := Eq2.refl _
```
Removing any of thee last 5 definitions avoids the error. Testing
against Mathlib shows this PR fixes the issue.
This adds the concept of **functional induction** to lean.
Derived from the definition of a (possibly mutually) recursive function,
a **functional
induction principle** is tailored to proofs about that function. For
example from:
```
def ackermann : Nat → Nat → Nat
| 0, m => m + 1
| n+1, 0 => ackermann n 1
| n+1, m+1 => ackermann n (ackermann (n + 1) m)
derive_functional_induction ackermann
```
we get
```
ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
(case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
(case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
(x x : Nat) : motive x x
```
At the moment, the user has to ask for the functional induction
principle explicitly using
```
derive_functional_induction ackermann
```
The module docstring of `Lean/Meta/Tactic/FunInd.lean` contains more
details on the
design and implementation of this command.
More convenience around this (e.g. a `functional induction` tactic) will
follow eventually.
This PR includes a bunch of `PSum`/`PSigma` related functions in the
`Lean.Tactic.FunInd`
namespace. I plan to move these to `PackArgs`/`PackMutual` afterwards,
and do some cleaning
up as I do that.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This adds a number of lemmas for simplification of `Bool` and `Prop`
terms. It pulls lemmas from Mathlib and adds additional lemmas where
confluence or consistency suggested they are needed.
It has been tested against Mathlib using some automated test
infrastructure.
That testing module is not yet included in this PR, but will be included
as part of this.
Note. There are currently some comments saying the origin of the simp
rule. These will be removed prior to merging, but are added to clarify
where the rule came from during review.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Else the `case` will now allow introducing all necessary variables.
Induction principles with `let` in the types of the cases will be more
common with #3432.
This implementation no longer reduces the type as it goes, but really
only counts
manifest foralls and lets. I find this more sensible and predictable: If
you have
```
theorem induction₂_symm {P : EReal → EReal → Prop} (symm : Symmetric P) …
```
then previously, writing
```
case symm =>
```
would actually bring a fresh `x` and `y` and variable `h : P x y` into
scope and produce a
goal of `P y x`, because `Symmetric P` happens to be
```
def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x
```
After this change, after `case symm =>` will leave `Symmetric P` as the
goal.
This gives more control to the author of the induction hypothesis about
the actual
goal of the cases. This shows up in mathlib in two places; fixes in
https://github.com/leanprover-community/mathlib4/pull/11023.
I consider these improvements.
When using `set_option tactic.skipAssignedInstances false`, `simp` and
`rw` will synthesize instance implicit arguments even if they have
assigned by unification. If the synthesized argument does not match the
assigned one the rewrite is not performed. This option has been added
for backward compatibility.
This PR addresses several performance issues in the auto-completion
implementation. It also fixes a number of smaller bugs related to
auto-completion.
In a file with `import Mathlib`, the performance of various kinds of
completions has improved as follows:
- Completing `C`: 49000ms -> 1400ms
- Completing `Cat`: 14300ms -> 1000ms
- Completing `x.` for `x : Nat`: 3700ms -> 220ms
- Completing `.` for an expected type of `Nat`: 11000ms -> 180ms
The following bugs have been fixed as well:
- VS Code never used our custom completion order. Now, the server fuzzy
completion score decides the order that completions appear in.
- Dot auto-completion for private types did not work at all. It does
now.
- Completing `.<identifier>` (where the expected type is used to infer
the namespace) did not filter by the expected type and instead displayed
all matching constants in the respective namespace. Now, it uses the
expected type for filtering. Note that this is not perfect because
sub-namespaces are technically correct completions as well (e.g.
`.Foo.foobar`). Implementing this is future work.
- Completing `.` was often not possible at all. Now, as long as the `.`
is not used in a bracket (where it may be used for the anonymous lambda
feature, e.g. `(. + 1)`), it triggers the correct completion.
- Fixes#3228.
- The auto-completion in `#check` commands would always try to complete
identifiers using the full declaration name (including namespaces) if it
could be resolved. Now it simply uses the identifier itself in case
users want to complete this identifier to another identifier.
## Details
Regarding completion performance, I have more ideas on how to improve it
further in the future.
Other changes:
- The feature that completions with a matching expected type are sorted
to the top of the server-side ordering was removed. This was never
enabled in VS Code because it would use its own completion item order
and when testing it I found it to be more confusing than useful.
- In the server-side ordering, we would always display keywords at the
top of the list. They are now displayed according to their fuzzy match
score as well.
The following approaches have been used to improve performance:
- Pretty-printing the type for every single completion made up a
significant amount of the time needed to compute the completions. We now
do not pretty-print the type for every single completion that is offered
to the user anymore. Instead, the language server now supports
`completionItem/resolve` requests to compute the type lazily when the
user selects a completion item.
- Note that we need to keep the amount of properties that we compute in
a resolve request to a minimum. When the server receives the resolve
request, the document state may have changed from the state it was in
when the initial auto-completion request was received. LSP doesn't tell
us when it will stop sending resolve requests, so we cannot keep this
state around, as we would have to keep it around forever.
LSP's solution for this dilemma is to have servers send all the state
they need to compute a response to a resolve request to the client as
part of the initial auto completion response (which then sends it back
as part of the resolve request), but this is clearly infeasible for all
real language servers where the amount of state needed to resolve a
request is massive.
This means that the only practical solution is to use the current state
to compute a response to the resolve request, which may yield an
incorrect result. This scenario can especially occur when using
LiveShare where the document is edited by another person while cycling
through available completions.
- Request handlers can now specify a "header caching handler" that is
called after elaborating the header of a file. Request handlers can use
this caching handler to compute caches for information stored in the
header. The auto-completion uses this to pre-compute non-blacklisted
imported declarations, which in turn allow us to iterate only over
non-blacklisted imported declarations where we would before iterate over
all declarations in the environment. This is significant because
blacklisted declarations make up about 4/5 of all declarations.
- Dot completion now looks up names modulo private prefixes to figure
out whether a declaration is in the namespace of the type to the left of
the dot instead of first stripping the private prefix from the name and
then comparing it. This has the benefit that we do not need to scan the
full name in most cases.
This PR also adds a couple of regression tests for fixed bugs, but *no
benchmarks*. We will add these in the future when we add proper support
for benchmarking server interaction sessions to our benchmarking
architecture.
All tests that were broken by producing different completion output
(empty `detail` field, added `sortText?` and `data?` fields) have been
manually checked by me to be still correct before replacing their
expected output.
