feat: elaborate theorem bodies in parallel #5864
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This reverts commit cc66581.
Manual update stage0 is required to get the test suite green.
This PR adds support for extensionality theorems (using the `[ext]` attribute) to the `grind` tactic. Users can disable this functionality using `grind -ext` . Below are examples that demonstrate problems now solvable by `grind`. ```lean open List in example : (replicate n a).map f = replicate n (f a) := by grind only [Option.map_some', Option.map_none', getElem?_map, getElem?_replicate] ``` ```lean @[ext] structure S where a : Nat b : Bool example (x y : S) : x.a = y.a → y.b = x.b → x = y := by grind ```
This PR fixes parameter processing, initialization, and attribute handling issues in the `grind` tactic.
This PR fixes the issue that `#check_failure`'s output is warning Closes leanprover#6684
This PR fixes a very small typo in the docstring of `mkMVar` that misspelled the function it recommends to use instead.
…over#5145) This PR splits the environment used by the kernel from that used by the elaborator, providing the foundation for tracking of asynchronously elaborated declarations, which will exist as a concept only in the latter. Minor changes: * kernel diagnostics are moved from an environment extension to a direct environment as they are the only extension used directly by the kernel * `initQuot` is moved from an environment header field to a direct environment as it is the only header field used by the kernel; this also makes the remaining header immutable after import
…or (leanprover#6214) Kernel checking will be moved to a different thread but namespace registration should stay on the elaboration thread
Continuation from leanprover#5429: eliminates uses of these two functions that care about something other than reducible defs/theorems, then restricts the function definition to these cases to be more true to its name.
…r#6688) Adapts, with permission, unit tests from `lean-egg` written by Marcus Rossel as regression tests for `grind`.
Motivation: we will remove the `[grind_norm]` attribute.
This PR introduces the central API for making parallel changes to the environment
This PR removes the `[grind_norm]` attribute. The normalization theorems used by `grind` are now fixed and cannot be modified by users. We use normalization theorems to ensure the built-in procedures receive term wish expected "shapes". We use it for types that have built-in support in grind. Users could misuse this feature as a simplification rule. For example, consider the following example: ```lean def replicate : (n : Nat) → (a : α) → List α | 0, _ => [] | n+1, a => a :: replicate n a -- I want `grind` to instantiate the equations theorems for me. attribute [grind] replicate -- I want it to use the equation theorems as simplication rules too. attribute [grind_norm] replicate /-- info: [grind.assert] n = 0 [grind.assert] ¬replicate n xs = [] [grind.ematch.instance] replicate.eq_1: replicate 0 xs = [] [grind.assert] True -/ set_option trace.grind.ematch.instance true in set_option trace.grind.assert true in example (xs : List α) : n = 0 → replicate n xs = [] := by grind -- fails :( ``` In this example, `grind` starts by asserting the two propositions as expected: `n = 0`, and `¬replicate n xs = []`. The normalizer cannot reduce `replicate n xs` as expected. Then, the E-matching module finds the instance `replicate 0 xs = []` for the equation theorem `replicate.eq_1` also as expected. But, then the normalizer kicks in and reduces the new instance to `True`. By removing `[grind_norm]` we elimninate this kind of misuse. Users that want to preprocess a formula before invoking `grind` should use `simp` instead.
This PR aligns `List/Array/Vector.reverse` lemmas.
This PR removes deprecations in the standard library from June 2024.
…nprover#6697) This PR changes the arguments of `List/Array.mapFinIdx` from `(f : Fin as.size → α → β)` to `(f : (i : Nat) → α → (h : i < as.size) → β)`, in line with the API design elsewhere for `List/Array`.
A small boost before leanprover#6691 made `modifyState` more complex, a larger boost after.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Draft in need of cleanups, smaller fixes, and incremental upstreaming, opened for benchmarking