feat: add Bitvec.toFin_twoPow
#51
Closed
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
…ver#6903) Bumps [dawidd6/action-download-artifact](https://github.com/dawidd6/action-download-artifact) from 7 to 8. <details> <summary>Release notes</summary> <p><em>Sourced from <a href="https://github.com/dawidd6/action-download-artifact/releases">dawidd6/action-download-artifact's releases</a>.</em></p> <blockquote> <h2>v8</h2> <h2>New features</h2> <ul> <li><code>use_unzip</code> boolean input (defaulting to false) - if set to true, the action will use system provided <code>unzip</code> utility for unpacking downloaded artifact(s) (note that the action will first download the .zip artifact file, then unpack it and remove the .zip file)</li> </ul> <h2>What's Changed</h2> <ul> <li>README: v7 by <a href="https://github.com/haines"><code>@haines</code></a> in <a href="https://github.com/dawidd6/action-download-artifact/pull/318">dawidd6/action-download-artifact#318</a></li> <li>Unzip by <a href="https://github.com/dawidd6"><code>@dawidd6</code></a> in <a href="https://github.com/dawidd6/action-download-artifact/pull/325">dawidd6/action-download-artifact#325</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/haines"><code>@haines</code></a> made their first contribution in <a href="https://github.com/dawidd6/action-download-artifact/pull/318">dawidd6/action-download-artifact#318</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/dawidd6/action-download-artifact/compare/v7...v8">https://github.com/dawidd6/action-download-artifact/compare/v7...v8</a></p> </blockquote> </details> <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/dawidd6/action-download-artifact/commit/20319c5641d495c8a52e688b7dc5fada6c3a9fbc"><code>20319c5</code></a> README: v8</li> <li><a href="https://github.com/dawidd6/action-download-artifact/commit/e58a9e5d14231715ece082f2068a0bd148cb72e6"><code>e58a9e5</code></a> Unzip (<a href="https://github.com/dawidd6/action-download-artifact/issues/325">#325</a>)</li> <li><a href="https://github.com/dawidd6/action-download-artifact/commit/6d05268723e4080b84fe8d5c0c5cd83226a81e5f"><code>6d05268</code></a> node_modules: update</li> <li><a href="https://github.com/dawidd6/action-download-artifact/commit/c03fb0c92813d0d9b088539572090518f7797df4"><code>c03fb0c</code></a> README: v7 (<a href="https://github.com/dawidd6/action-download-artifact/issues/318">#318</a>)</li> <li>See full diff in <a href="https://github.com/dawidd6/action-download-artifact/compare/v7...v8">compare view</a></li> </ul> </details> <br /> [](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores) Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) --- <details> <summary>Dependabot commands and options</summary> <br /> You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot merge` will merge this PR after your CI passes on it - `@dependabot squash and merge` will squash and merge this PR after your CI passes on it - `@dependabot cancel merge` will cancel a previously requested merge and block automerging - `@dependabot reopen` will reopen this PR if it is closed - `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually - `@dependabot show <dependency name> ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself) </details> Signed-off-by: dependabot[bot] <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
This PR completes the alignment of `List/Array/Vectors` lemmas for `insertIdx`.
…ver#6844) Unreverts leanprover#6598 I'll combine leanprover#6825 into this before merging.
…r#6326) This PR adds `BitVec.(getMsbD, msb)_replicate, replicate_one` theorems, corrects a non-terminal `simp` in `BitVec.getLsbD_replicate` and simplifies the proof of `BitVec.getElem_replicate` using the `cases` tactic. Co-authored with @bollu. --------- Co-authored-by: Alex Keizer <[email protected]>
…er#6891) This PR modifies `rewrite`/`rw` to abort rewriting if the elaborated lemma has any immediate elaboration errors (detected by presence of synthetic sorries). Rewriting still proceeds if there are elaboration issues arising from pending synthetic metavariables, like instance synthesis failures. The purpose of the change is to avoid obscure "tactic 'rewrite' failed, equality or iff proof expected ?m.5" errors when for example a lemma does not exist. This helps error reporting for the natural number game. https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Why.20doesn't.20add_left_comm.20work.20here.3F/near/497060022
This PR adds line breaks and indentations to simp's trace messages to make them easier to read (IMHO).
…tMsbD_umod)` (leanprover#6795) This PR adds theorems `BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod)`. For the defiition of these theorems we rely on `divRec`, excluding the case where `d=0#w`, which is treated separately because there is no infrastructure to reason about this case within `divRec`. In particular, our implementation follows the mathlib standard [where division by 0 yields 0](https://github.com/leanprover/lean4/blob/c7c1e091c9f07ae6f8e8ff7246eb7650e2740dcb/src/Init/Data/BitVec/Basic.lean#L217), while in [SMTLIB this yields `allOnes`](https://github.com/leanprover/lean4/blob/c7c1e091c9f07ae6f8e8ff7246eb7650e2740dcb/src/Init/Data/BitVec/Basic.lean#L237). Co-authored by @bollu. --------- Co-authored-by: Siddharth <[email protected]>
…ver#6853) This PR adds support for anonymous equality proofs in `match` expressions of the form `match _ : e with ...`. Closes leanprover#6759.
This PR adds preliminary support for inlay hints, as well as support for inlay hints that denote the auto-implicits of a function. Hovering over an auto-implicit displays its type and double-clicking the auto-implicit inserts it into the text document.  This PR is an extension of leanprover#3910. ### Known issues - In VS Code, when inserting an inlay hint, the inlay hint may linger for a couple of seconds before it disappears. This is a defect of the VS Code implementation of inlay hints and cannot adequately be resolved by us. - When making a change to the document, it may take a couple of seconds until the inlay hints respond to the change. This is deliberate and intended to reduce the amount of inlay hint flickering while typing. VS Code has a mechanism of its own for this, but in my experience it is still far too sensitive without additional latency. - Inserting an auto-implicit inlay hint that depends on an auto-implicit meta-variable causes a "failed to infer binder type" error. We can't display these meta-variables in the inlay hint because they don't have a user-displayable name, so it is not clear how to resolve this problem. - Inlay hints are currently always resolved eagerly, i.e. we do not support the `textDocument/inlayHint/resolve` request yet. Implementing support for this request is future work. ### Other changes - Axioms did not support auto-implicits due to an oversight in the implementation. This PR ensures they do. - In order to reduce the amount of inlay hint flickering when making a change to the document, the language server serves old inlay hints for parts of the file that have not been processed yet. This requires LSP request handler state (that sometimes must be invalidated on `textDocument/didChange`), so this PR introduces the notion of a stateful LSP request handler. - The partial response mechanism that we use for semantic tokens, where we simulate incremental LSP responses by periodically emitting refresh requests to the client, is generalized to accommodate both inlay hints and semantic tokens. Additionally, it is made more robust to ensure that we never emit refresh requests while a corresponding request is in flight, which causes VS Code to discard the respond of the request, as well as to ensure that we keep prompting VS Code to send another request if it spuriously decides not to respond to one of our refresh requests. - The synthetic identifier of an `example` had the full declaration as its (non-canonical synthetic) range. Since we need a reasonable position for the identifier to insert an inlay hint for the auto-implicits of an `example`, we change the (canonical synthetic) range of the synthetic identifier to that of the `example` keyword. - The semantic highlighting request handling is moved to a separate file. ### Breaking changes - The semantic highlighting request handler is not a pure request handler anymore, but a stateful one. Notably, this means that clients that extend the semantic highlighting of the Lean language server with the `chainLspRequestHandler` function must now use the `chainStatefulLspRequestHandler` function instead.
This includes the examples from issues leanprover#2961, leanprover#3219 and leanprover#5667 in our test suite, so that we know when (accidentially) fix them. In fact this closes leanprover#3219, which (judging from the nightlies) was fixed last week by leanprover#6901.
This PR adds support for plugins to the frontend and server. Implementation-wise, this adds a `plugins` argument to `runFrontend`, `processHeader`, amd `importModules`, a `plugins` field to `SetupImportsResult` and `FileSetupResult`. and a `pluginsPath` field to `LeanPaths`, and then threads the value through these.
…over#6939) This PR adds error messages for `inductive` declarations with conflicting constructor names and `mutual` declarations with conflicting names. Closes leanprover#6694.
…verflow, sadd_overflow, uadd_overflow_eq, sadd_overflow_eq)` and support theorems (leanprover#6628) This PR adds SMT-LIB operators to detect overflow `BitVec.(uadd_overflow, sadd_overflow)`, according to the definitions [here](https://github.com/SMT-LIB/SMT-LIB-2/blob/2.7/Theories/FixedSizeBitVectors.smt2), and the theorems proving equivalence of such definitions with the `BitVec` library functions (`uaddOverflow_eq`, `saddOverflow_eq`). Support theorems for these proofs are `BitVec.toNat_mod_cancel_of_lt, BitVec.toInt_lt, BitVec.le_toInt, Int.bmod_neg_iff`. The PR also includes a set of tests. --------- Co-authored-by: Tobias Grosser <[email protected]> Co-authored-by: Alex Keizer <[email protected]> Co-authored-by: Tobias Grosser <[email protected]> Co-authored-by: Siddharth Bhat <[email protected]>
This PR starts on the process of cleaning up variable names across List/Array/Vector. For now, we just rename "numerical index" variables in one file. This is driven by a custom linter.
) this PR helps with bootstrapping leanprover#6744.
leanprover#6634) This PR adds support for changing the binder annotations of existing variables to and from strict-implicit and instance-implicit using the `variable` command. This PR requires a stage0 update to fully take effect. Closes leanprover#6078
This PR adds the auxiliary tactic `evalAndSuggest`. It will be used to refactor `try?`.
This PR improves the doc-string for `List.toArray`. Thanks to @jt0202 for pointing this out.
This PR adds a convenience command `#info_trees in`, which prints the info trees generated by the following command. It is useful for debugging or learning about `InfoTree`.
This PR re-implements the `try?` tactic using the new `evalAndSuggest` infrastructure.
…rover#6966) This PR adds an internal-use-only strict linter for the variable names of `List`/`Array`/`Vector` variables, and begins cleaning up.
This PR ensures `try?` can suggest tactics that need to reference inaccessible local names. Example: ```lean /-- info: Try these: • · expose_names; induction as, bs_1 using app.induct <;> grind [= app] • · expose_names; induction as, bs_1 using app.induct <;> grind only [app] -/ #guard_msgs (info) in example : app (app as bs) cs = app as (app bs cs) := by have bs := 20 -- shadows `bs` in the target try? ```
This PR removes a reference to Trepplein (Lean 3) in the documentation. Co-authored-by: euprunin <[email protected]>
This PR does some stage0 cleanup after leanprover#7100, and enables a warning when the old `structure S extends P : Type` syntax is used. It also updates the library to put resulting types in the new correct place (`structure S : Type extends P`). The `structure` elaborator also has some additional docstrings, and `StructFieldKind.fromParent` is renamed to `StructFieldKind.fromSubobject`.
…message (leanprover#7169) This PR adds an addition newline before the "Additional diagnostic information may be available using the `set_option ... true` command." messages, to provide better visual separation from the main error message.
…d/fmod` (leanprover#7199) This PR adds theorems comparing `Int.ediv` with `tdiv` and `fdiv`, for all signs of arguments. (Previously we just had the statements about the cases in which they agree.)
This PR adds `Array/Vector.left/rightpad`. These will not receive any verification theorems; simp just unfolds them to an `++` operation.
This PR adds support for internalizing terms relevant to the cutsat module. This is required to implement equality propagation.
This PR improves the support for equalities in cutsat. It also simplifies a few support theorems used to justify cutsat rules.
…7200) This PR allows the debug form of DiscrTree.Key to line-wrap.
This PR provides tree map lemmas about the interaction of `containsThenInsert(IfNew)` with `contains` and `insert(IfNew)`. --------- Co-authored-by: Paul Reichert <[email protected]>
…eanprover#7205) This PR completes alignment of `List.getLast`/`List.getLast!`/`List.getLast?` lemmas with the corresponding lemmas for Array and Vector.
This PR adds the first batch of lemmas about iterated conversions between finite types starting with something of type `UIntX`.
This PR provides tree map lemmas for the interaction of `get?` with the other operations for which lemmas already exist. --------- Co-authored-by: Paul Reichert <[email protected]>
This PR adds theorem `BitVec.toFin_abs`, completing the API for `BitVec.*_abs`. --------- Co-authored-by: Tobias Grosser <[email protected]>
This PR fixes broken Lake tests on Windows' new MSYS2. As of MSYS2 0.0.20250221, `OSTYPE` is now reported as `cygwin` instead of `msys`, which must be accounted for in a few Lake tests. See https://www.msys2.org/news/#2025-02-14-moving-msys2-closer-to-cygwin for more details.
This PR moves the RHS of getElem theorems to use getElem. This is a cleanup after the recent move to getElem as simp normal form. We also turn `((!decide (i < n)) && getLsbD x (i - n))` into `if h' : i < n then false else x[i - n]` to preserve the bounds, but keep the decide if the dependent if is not needed to maintain a getElem on the RHS.
This PR adds a `ForIn` instance for the `PersistentHashSet` type.
Turns back on the variable names linters across List/Array/Vector.
This PR improves the support for equalities in cutsat.
This PR aligns lemmas for `List.dropLast` / `Array.pop` / `Vector.pop`.
…nprover#7220) This PR implements the missing cases for equality propagation from the `grind` core to the cutsat module.
This PR changes the job monitor to perform run job computation itself as a separate job. Now progress will be reported eagerly, even before all outstanding jobs have been discovered. Thus, the total job number reported can now grow while jobs are still being computed (e.g., the `Y` in `[X/Y[` may increase).
… oleans (leanprover#7190) This PR makes the stage2 Leanc build use the stage2 oleans rather than stage1 oleans. This was happening because Leanc's own OLEAN_OUT is at the build root rather than the lib/lean subdirectory, so when the build added this OLEAN_OUT to LEAN_PATH no oleans were found there and the search fell back to the stage1 installation location.
…eanprover#7222) This PR removes the `simp` attribute from `ReflCmp.compare_self` because it matches arbitrary function applications. Instead, a new `simp` lemma `ReflOrd.compare_self` is introduced, which only matches applications of `compare`. --------- Co-authored-by: Paul Reichert <[email protected]>
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.
This PR adds theorems
BitVec.toInt_twoPowandBitVec.toFin_twoPow, completing theBitvec.*_twoPowAPI.