in principle we'd like to use the existing parser
```
"?" >> (ident <|> hole)
```
but somehow annotate it so that hovering the `hole` will not show the
hole's hover. But for now it was easier to just change the parser to
```
"?" >> (ident <|> "_")
```
and be done with it.
Fixes#5021
The goal at the crucial step is
```
a : Array Nat
i : Fin ?m.27
⊢ ↑i < a.size
```
and after the `apply Fin.val_lt_of_le;` we have
```
a : Array Nat
i : Fin ?m.27
⊢ ?m.27 ≤ a.size
```
and now `apply Fin.val_lt_of_le` applies again, due to accidential
defeq. Adding `with_reducible` helps here.
fixes#5061
Defines `mergeSort`, a naive stable merge sort algorithm, replaces it
via a `@[csimp]` lemma with something faster at runtime, and proves the
following results:
* `mergeSort_sorted`: `mergeSort` produces a sorted list.
* `mergeSort_perm`: `mergeSort` is a permutation of the input list.
* `mergeSort_of_sorted`: `mergeSort` does not change a sorted list.
* `mergeSort_cons`: proves `mergeSort le (x :: xs) = l₁ ++ x :: l₂` for
some `l₁, l₂`
so that `mergeSort le xs = l₁ ++ l₂`, and no `a ∈ l₁` satisfies `le a
x`.
* `mergeSort_stable`: if `c` is a sorted sublist of `l`, then `c` is
still a sublist of `mergeSort le l`.
@arthur-adjedj was very confused when a mutually recursive definition
didn't work as expected, and the reason was that he used different names
for the fixed parameters.
It seems plausible to simply allow that and calculate the fixed-prefix
up to alpha renaming.
It does mean, though, that, for example, termination proof goals will
mention the names as used by the first function. But probably better
than simply failing. And we could even fix that later (by passing down
the
actual names, and renmaing the variables in the context of the mvar,
depending on the “current function”) should it bother our users.
When elaborating the headers of mutual indexed inductive types, mvars
have to be synthesized and instantiated before replacing the fvars
present there. Otherwise, some fvars present in uninstantiated mvars may
be missed and lead to an error later.
Closes#3242 (again)
Previously, the tactic state shown at `decreasing_by` would leak lots of
details about the translation, and mention `invImage`, `PSigma` etc.
This is not nice.
So this introduces `clean_wf`, which is like `simp_wf` but using
`simp`'s `only` mode, and runs this unconditionally. This should clean
up the goal to a reasonable extent.
Previously `simp_wf` was an unrestricted `simp […]` call, but we
probably don’t want arbitrary simplification to happen at this point, so
this now became `simp only` call. For backwards compatibility,
`decreasing_with` begins with `try simp`. The `simp_wf` tactic
is still available to not break too much existing code; it’s docstring
suggests to no longer use it.
With `set_option cleanDecreasingByGoal false` one can disable the use of
`clean_wf`. I hope this is only needed for debugging and understanding.
Migration advise: If your `decreasing_by` proof begins with `simp_wf`,
either remove that (if the proof still goes through), or replace with
`simp`.
I am a bit anxious about running even `simp only` unconditionally here,
as it may do more than some user might want, e.g. because of options
like `zetaDelta := true`. We'll see if we need to reign in this tactic
some more.
I wonder if in corner cases the `simp_wf` tactic might be able to close
the goal, and if that is a problem. If so, we may have to promote simp’s
internal `mayCloseGoal` parameter to a simp configuration option and use
that here.
fixes#4928
Using `Nat.lt_trans` is too restrictive, and using `Nat.lt_of_lt_of_le`
should make this tactic prove more goals.
This fixes a regression probably introduced by #3991; at least in some
cases before that `apply sizeOf_get` would have solved the goal here.
And it’s true that this is now subsumed by `simp`, but because of the
order that `macro_rules` are tried, the too restrictive variant with
`Nat.lt_trans` would be tried before `simp`, without backtracking.
Fixes#5027
Step 3/~7 in upstreaming LeanSAT.
A few thoughts:
- Why is this not in `Std.Sat`? LeanSAT's bitblaster operates on a
limited internal language. For example it has no idea that signed
comparision operators even exist. This is because it relies on a
normalization pass before being given the goal. For this reason I would
not classify the bitblaster as an API that we should publicly advertise
at this abstraction level
- Sometimes I slightly rebuild parts of the LawfulOperator
infrastructure for operators that work non-tail-recursively. This is
because they do not return an `Entrypoint` but instead an
`ExtendingEntrypoint` in order to even be defined in the first place
(casting Ref's and all that). Given the fact that this barely happens
and I never actually commit to rebuilding the full API I'm hoping that
this is indeed a fine decision?
- The single explicit `decreasing_by` that has a simp only which
*almost* looks like `simp_wf` is missing a singular lemma from `simp_wf`
because it doesn't terminate otherwise.
- I am not using functional induction because it basically always fails
at some generalization step, that is also the reason that there is lots
of explicit `generalize` and manually recursive proofs.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
For structure projections, the pretty printer assumed that the
expression was type correct. Now it checks that the object being
projected is of the correct type. Such terms appear in type mismatch
errors.
Also, fixes and improves `#print` for structures. The types of
projections now use MessageData (so are now hoverable), and the type of
`self` is now the correct type.
Closes#4670
...unless we are about to kill the process anyway (which is not the
default)
Ensures panics are visible as regular messages in the language server
and properly ordered in relation to other messages on the cmdline
Adds `@[app_delab ident]` as a macro for `@[delab app.ident]`. Resolves
the identifier when expanding the macro, saving needing to use the fully
qualified identifiers that `@[delab]` requires. Also, unlike `@[delab]`,
throws an error if the identifier cannot be resolved.
Closes#4899
Fixes an issue where each alternative in choice nodes would get their
own arguments. Now cdot function expansion is aware of choice nodes.
Also modifies the variable naming so that multi-argument functions like
`(· + ·)` expand as `fun x1 x2 => x1 + x2` rather than `fun x x_1 => x +
x_1`.
Closes#4832
This implements a naive version of `getline` because Windows does not
have `getline`. Given the fact that `FILE` has buffered IO, calling
`fgetc` in a loop is not as big of a performance hazard as it might seem
at first glance.
The proper solution to this would of course be to have our own buffered
IO so we are fully in charge of the buffer. In this situation we could
check the entire buffer for a newline at once instead of char by char.
However that is not going to happen for the near future so I propose we
stay with this implementation. If reading individual lines of a file
does truly end up being the performance bottle neck we have already
won^^.
With the recent unification of server and cmdline processing,
`IO.Process` tests that previously broke the server because they
directly wrote to stdout are now flaky on the cmdline because
elaboration and reporting are happening in separate threads. By removing
direct writes to stdout, the race condition is removed and the file can
actually be edited in the language server as well again.
This PR:
- changes the implementation of `readBinFile` and `readFile` to only
require two system calls (`stat` + `read`) instead of one `read` per
1024 byte chunk.
- fixes a bug where `Handle.getLine` would get tripped up by a NUL
character in the line and cut the string off. This is caused by the fact
that the original implementation uses `strlen` and `lean_mk_string`
which is the backer of `mk_string` does so as well.
- fixes a bug where `Handle.putStr` and thus by extension `writeFile`
would get tripped up by a NUL char in the line and cut the string off.
Cause here is the use of `fputs` when a NUL char is possible.
Closes: #4891Closes: #3546Closes: #3741
Autoparam tactic scripts have no source positions, which until recently
made it so that any errors or messages would be logged at the current
ref, which was the application or structure instance being elaborated.
However, with the new incrementality features the ref is now carefully
managed to avoid leakage of outside data. This inhibits the elaborator's
ref from being used for the tactic's ref, causing messages to be placed
at the beginning of the file rather than on the syntax that triggered
the autoparam.
To fix this, now the elaborators insert the ref's source position
everywhere into the autoparam tactic script.
If in the future messages for synthetic tactics appear at the tops of
files in other contexts, we should consider an approach where
`Lean.Elab.Term.withReuseContext` uses something like `replaceRef` to
set the ref while disabling incrementality when the tactic does not
contain source position information.
Closes#4880
Currently, the messages in the diagnostic summaries are created by
appending interpolated strings. We wrap these in `.trace`'s, and the
results are better formatted when expanding child nodes in the info
view. Particularly, the latter diagnostic summaries remain on their own
lines flush to the left instead of on the same line directly adjacent to
the last child node.
For experimentation by @the-sofi-uwu.
I also have an efficient number parser in LeanSAT that I am planning to
upstream after we have sufficiently bikeshed this change.
This modification improves the performance of the example in issue
#4861. It no longer times out but is still expensive.
Here is the analysis of the performance issue: Given `(x : Int)`, to
elaborate `x ^ 1`, a few default instances have to be tried.
First, the homogeneous instance is tried and fails since `Int` does not
implement `Pow Int`. Then, the `NatPow` instance is tried, and it also
fails. The same process is performed for each term of the form `p ^ 1`.
There are seveal of them at #4861. After all of these fail, the lower
priority default instance for numerals is tried, and `x ^ 1` becomes `x
^ (1 : Nat)`. Then, `HPow Int Nat Int` can be applied, and the
elaboration succeeds. However, this process has to be repeated for every
single term of the form `p ^ 1`. The elaborator tries all homogeneous
`HPow` and `NatPow` instances for all `p ^ 1` terms before trying the
lower priority default instance `OfNat`.
This commit ensures `Int` has a `NatPow` instance instead of `HPow Int
Nat Int`. This change shortcuts the process, but it still first tries
the homogeneous `HPow` instance, fails, and then tries `NatPow`. The
elaboration can be made much more efficient by writing `p ^ (1 : Nat)`.
Initial options are now re-parsed and validated after importing. Cmdline
option assignments prefixed with `weak.` are silently discarded if the
option name without the prefix does not exist.
Fixes#3403
