This PR removes the `NatCast (Fin n)` global instance (both the direct
instance, and the indirect one via `Lean.Grind.Semiring`), as that
instance causes causes `x < n` (for `x : Fin k`, `n : Nat`) to be
elaborated as `x < ↑n` rather than `↑x < n`, which is undesirable. Note
however that in Mathlib this happens anyway!
This PR adds a test case / use case example for `grind`, setting up the
very basics of `IndexMap`, modelled on Rust's
[`indexmap`](https://docs.rs/indexmap/latest/indexmap/). It is not
intended as a complete implementation: just enough to exercise `grind`.
(Thanks to @arthurpaulino for suggesting this as a test case.)
This PR fixes a bug in the equality-resolution procedure used by
`grind`.
The procedure now performs a topological sort so that every simplified
theorem declaration is emitted **before** any place where it is
referenced.
Previously, applying equality resolution to
```lean
h : ∀ x, p x a → ∀ y, p y b → x ≠ y
```
in the example
```lean
example
(p : Nat → Nat → Prop)
(a b c : Nat)
(h : ∀ x, p x a → ∀ y, p y b → x ≠ y)
(h₁ : p c a)
(h₂ : p c b) :
False := by
grind
```
caused `grind` to produce the incorrect term
```lean
p ?y a → ∀ y, p y b → False
```
The patch eliminates this error, and the following correct simplified
theorem is generated
```lean
∀ y, p y a → p y b → False
```
This PR fixes (1) an issue where private names are not unresolved when
they are pretty printed, (2) an issue where in `pp.universes` mode names
were allowed to shadow local names, (3) an issue where in `match`
patterns constants shadowing locals wouldn't use `_root_`, and (4) an
issue where tactics might have an incorrect "try this" when
`pp.fullNames` is set. Adds more delaboration tests for name
unresolution.
It also cleans up the `delabConst` delaborator so that it uses
`unresolveNameGlobalAvoidingLocals`, rather than doing any local context
analysis itself. The `inPattern` logic has been removed; it was a
heuristic added back in #575, but it now leads to incorrect results (and
in `match` patterns, local names shadow constants in name resolution).
This PR implements signature help support. When typing a function
application, editors with support for signature help will now display a
popup that designates the current (remaining) function type. This
removes the need to remember the function signature while typing the
function application, or having to constantly cycle between hovering
over the function identifier and typing the application. In VS Code, the
signature help can be triggered manually using `Ctrl+Shift+Space`.
### Other changes
- In order to support signature help for the partial syntax `f a <|` or
`f a $`, these notations now elaborate as `f a`, not `f a .missing`.
- The logic in `delabConstWithSignature` that delaborates parameters is
factored out into a function `delabForallParamsWithSignature` so that it
can be used for arbitrary `forall`s, not just constants.
- The `InfoTree` formatter is adjusted to produce output where it is
easier to identify the kind of `Info` in the `InfoTree`.
- A bug in `InfoTree.smallestInfo?` is fixed so that it doesn't panic
anymore when its predicate `p` does not ensure that both `pos?` and
`tailPos?` of the `Info` are present.
* Move constant registration with elab env from `Lean.addDecl` to
`Lean.Environment.addDeclCore` for compatibility
* Make module system behavior independent of `Elab.async` value
This PR makes `guard_msgs.diff=true` the default. The main usage of
`#guard_msgs` is for writing tests, and this makes staring at altered
test outputs considerably less tiring.
This PR adds support for server-sided `RpcRef` reuse and fixes a bug
where trace nodes in the InfoView would close while the file was still
being processed.
The core of the trace node issue is that the server always serves new
RPC references in every single response to the client, which means that
the client is forced to reset its UI state.
In a previous attempt at fixing this (#8056), the server would memorize
the RPC-encoded JSON of interactive diagnostics (which includes RPC
references) and serve it for as long as it could reuse the snapshot
containing the diagnostics, so that RPC references are reused. The
problem with this was that the client then had multiple finalizers
registered for the same RPC reference (one for every reused RPC
reference that was served), and once the first reference was
garbage-collected, all other reused references would point into the
void.
This PR takes a different approach to resolve the issue: The meaning of
`$/lean/rpc/release` is relaxed from "Free the object pointed to by this
RPC reference" to "Decrement the RPC reference count of the object
pointed to by this RPC reference", and the server now maintains a
reference count to track how often a given `RpcRef` was served. Only
when every single served instance of the `RpcRef` has been released, the
object is freed. Additionally, the reuse mechanism is generalized from
being only supported for interactive diagnostics, to being supported for
any object using `WithRpcRef`. In order to make use of reusable RPC
references, downstream users still need to memorize the `WithRpcRef`
instances accordingly.
Closes#8053.
### Breaking changes
Since `WithRpcRef` is now capable of tracking its identity to decide
which `WithRpcRef` usage constitutes a reuse, the constructor of
`WithRpcRef` has been made `private` to discourage downstream users from
creating `WithRpcRef` instances with manually-set `id`s. Instead,
`WithRpcRef.mk` (which lives in `BaseIO`) is now the preferred way to
create `WithRpcRef` instances.
This PR uses `grind` to shorten some proofs in the LRAT checker. The
intention is not particularly to improve the quality or maintainability
of these proofs (although hopefully this is a side effect), but just to
give `grind` a work out.
There are a number of remaining notes, either about places where `grind`
fails with an internal error (for which #8608 is hopefully
representative, and we can fix after that), or `omega` works but `grind`
doesn't (to be investigated later).
Only in some of the files have I thoroughly used grind. In many files
I've just replaced leaves or branches of proofs with `grind` where it
worked easily, without setting up the internal annotations in the LRAT
library required to optimize the use of `grind`. It's diminishing
returns to do this in a proof library that is not high priority, so I've
simply drawn a line.
This PR provides the iterator combinator `drop` that transforms any
iterator into one that drops the first `n` elements.
Additionally, the PR removes the specialized `IteratorLoop` instance on
`Take`. It currently does not have a `LawfulIteratorLoop` instance,
which needs to exist for the loop consumer lemmas to work. Having the
specialized instance is low priority.
This PR adds `@[grind]` to `getElem?_pos` and variants.
I'd initially thought these would result in too much case splitting, but
it seems to be only minor, and in use cases the payoff is good.
This PR adds support for the `compiler.extract_closed` option to the new
compiler, since this is used by the definition of `unsafeBaseIO`. We'll
revisit this once we switch to the new compiler and rethink its
relationship with IO.
This PR makes the lemma `BitVec.extractLsb'_append_eq_ite` more usable
by using the "simple case" more often, and uses this simplification to
make `BitVec.extractLsb'_append_eq_of_add_lt` stronger, renaming it to
`BitVec.extractLsb'_append_eq_of_add_le`.
This PR wraps the invocation of the new compiler in `withoutExporting`.
This is not necessary for the old compiler because it uses more direct
access to the kernel environment.
This PR removes incorrect optimizations for strictOr/strictAnd from the
old compiler, along with deleting an incorrect test. In order to do
these optimizations correctly, nontermination analysis is required.
Arguably, the correct way to express these optimizations is by exposing
the implementation of strictOr/strictAnd to a nontermination-aware phase
of the compiler, and then having them follow from more general
transformations.
This PR adjusts the grind annotation on
`Std.HashMap.map_fst_toList_eq_keys` and variants, so `grind` can reason
bidirectionally between `m.keys` and `m.toList`.
This PR avoids the likely unexpected behavior of `removeDirAll` to
delete through symlinks and adds the new function
`IO.FS.symlinkMetadata`.
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR sets `ring := true` by default in `grind`. It also fixes a bug
in the reification procedure, and improves the term internalization in
the ring and cutsat modules.
This PR makes LCNF's simpAppApp? bail out on trivial aliases as
intended. It seems that there was a typo in the original logic, and this
PR also extends it to include aliases of global constants rather than
just local vars.
Just a typo. From my understanding (and the specification otherwise) the
resulting level is the maximum of `r` and `s` instead of the minimum.
No issue opened yet (thus the draft).
