WIP: multiplication circuit for bit blasting #2
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
otherwise it remains in the equational theorem and may cause the “unused have linter” to trigger. By moving the proof into `decreasing_by`, the equational theorems are unencumbered by termination arguments. see also leanprover-community/batteries#690 (comment)
It has had a long history going back [10 years](leanprover-community/lean@3afad10#diff-4e22e2bb74f004d2ff7cdabcb5c01429abbc906e20befe2517679e257b4387e4R41), but its time has come to an end since this instance is never applicable.
…lean` (leanprover#4080) This PR also fixes: - Fields caching specific `Options` at `CoreM` are now properly set. - `nextMacroScope` was not being propagated at `liftCoreM`.
We now also track which declarations have been unfolded by the kernel when using ```lean set_option diagnostics true ```
This makes the `leanArts` in `library_data leanArts : BuildJob Unit` get a hover for the generated axiom. It also simplifies the `quoteFrom` function so that it delaborates properly by using a name literal (which elaborates to `mkStr1`, `mkStr2` etc) instead of a `mkStr` application.
…4095) Identity 2-2 (a) (Section: Addition Combined with Logical Operations) from Hacker's Delight, 2nd edition.
This issue was affecting several Mathlib files. @mattrobball @semorrison This is a different solution for the issue. The comment at `Extra.lean` describes the new solution and documents the new issues found with the previous one. closes leanprover#4085
…eanprover#4001) Add docstrings and usage examples for `String.length`, `.push`, `.append`, `.get?`, `.set`, `.modyify`, and `.next`. Update docstrings and add usage examples for `String.toList`, `.get`, and `.get!`. --------- Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: David Thrane Christiansen <[email protected]>
…es and proofs (leanprover#3944) The deriving handler would use `_` for types and proofs for structures but not for inductives. Reported by Graham Leach-Krouse on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Deriving.20Repr.20for.20an.20inductive.20with.20proof.20parameters/near/434181985).
As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/Find.20references.20broken.20in.20lean.20core/near/437051935). The `mainModuleName` was being set incorrectly when browsing lean core sources, resulting in failure of cross-file server requests like "Find References". Because the `srcSearchPath` is generated asynchronously, we store it as a `Task Name` which is resolved some time before the header is finished parsing. (I don't think the `.get` here will ever block, because the srcSearchPath will be ready by the time the initial command snap is requested.) --------- Co-authored-by: Sebastian Ullrich <[email protected]>
https://live.lean-lang.org/#project=lean-nightly now allows users to play around with the latest lean nightly, and it seems prudent to ask them to test bug reports, if possible, there, and not just with whatever release they use. Also reformatted the descriptions to look well in a text area. Users will not see this as rendered markdown, but as plain text. --------- Co-authored-by: Sebastian Ullrich <[email protected]>
…r#4098) this is in preparation for leanprover#4061. Once that lands, `1 % 42 = 1` will no longer hold definitionally (at least not without an ungly `unseal Nat.modCore in` around). This affects mathlib in a few places, essentially every time a `1 : Fin (n+1)` literal is written. So this extends the existing special case for `0 % n = 0` to `1 % n`.
…over#4096) closes leanprover#4051 cc @semorrison
Fixes leanprover#3270 by moving the deprecation check from `Lean.Elab.Term.mkConsts` to `Lean.Elab.Term.mkConst`, so `Lean.Elab.Term.mkBaseProjections`, `.elabAppLValsAux`, `.elabAppFn`, and `.elabForIn` also hit the check. Not all of these really need to hit the check, so I'll run `!bench` to see if it's a problem.
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
…ver#2903) This fixes leanprover#2901, a bug in the old compiler which causes a segfault. The issue is that when visiting `noConfusion` applications, it assumes that each constructor case has `nfields` arguments, e.g. `head1 = head2 -> tail1 = tail2 -> P` has two arguments because `List.cons` has 2 fields, but in fact propositional fields are skipped by the noConfusion type generator, so for example `Subtype.noConfusionType` is: ```lean @[reducible] protected def Subtype.noConfusionType.{u_1, u} : {α : Sort u} → {p : α → Prop} → Sort u_1 → Subtype p → Subtype p → Sort u_1 := fun {α} {p} P v1 v2 ↦ Subtype.casesOn v1 fun val property ↦ Subtype.casesOn v2 fun val_1 property ↦ (val = val_1 → P) → P ``` where `val = val_1 → P` only has the one argument even though `Subtype.mk` has two fields, presumably because it is useless to have an equality of propositions. Unfortunately there isn't any easy cache or getter to use here to get the number of non-propositional fields, so we just calculate it on the spot.
Fixes a bug in `Lake.Toml.ppTable` where root table keys could be printed after a subtable header. Closes leanprover#4099.
we keep running into examples where working with well-founded recursion is slow because defeq checks (which are all over the place, including failing ones that are back-tracked) unfold well-founded definitions. The definition of a function defined by well-founded recursion should be an implementation detail that should only be peeked inside by the equation generator and the functional induction generator. We now mark the mutual recursive function as irreducible (if the user did not set a flag explicitly), and use `withAtLeastTransparency .all` when producing the equations. Proofs can be fixed by using rewriting, or – a bit blunt, but nice for adjusting existing proofs – using `unseal` (a.k.a. `attribute [local semireducible]`). Mathlib performance does not change a whole lot: http://speed.lean-fro.org/mathlib4/compare/08b82265-75db-4a28-b12b-08751b9ad04a/to/16f46d5e-28b1-41c4-a107-a6f6594841f8 Build instructions -0.126 %, four modules with significant instructions decrease. To reduce impact, these definitions were changed: * `Nat.mod`, to make `1 % n` reduce definitionally, so that `1` as a `Fin 2` literal works nicely. Theorems with larger `Fin` literals tend to need a `unseal Nat.modCore` leanprover#4098 * `List.ofFn` rewritten to be structurally recursive and not go via `Array.ofFn`: leanprover-community/batteries#784 Alternative designs explored were * Making `WellFounded.fix` irreducible. One benefit is that recursive functions with equal definitions (possibly after instantiating fixed parameters) are defeq; this is used in mathlib to relate [`OrdinalApprox.gfpApprox`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Ordinal/FixedPointApproximants.html#OrdinalApprox.gfpApprox) with `.lfpApprox`. But the downside is that one cannot use `unseal` in a targeted way, being explicit in which recursive function needs to be reducible here. And in cases where Lean does unwanted unfolding, we’d still unfold the recursive definition once to expose `WellFounded.fix`, leading to large terms for often no good reason. * Defining `WellFounded.fix` to unroll defintionally once before hitting a irreducible `WellFounded.fixF`. This was explored in leanprover#4002. It shares most of the ups and downs with the previous variant, with the additional neat benefit that function calls that do not lead to recursive cases (e.g. a `[]` base case) reduce nicely. This means that the majority of existing `rfl` proofs continue to work. Issue leanprover#4051, which demonstrates how badly things can go if wf recursive functions can be unrolled, showed that making the recursive function irreducible there leads to noticeably faster elaboration than making `WellFounded.fix` irreducible; this is good evidence that the present PR is the way to go. This fixes leanprover#3988 --------- Co-authored-by: Leonardo de Moura <[email protected]>
This reverts commit 706a4cf introduced in leanprover#3970 As explained in leanprover#4124, `findM?` can become a footgun if used in monads which induce side-effects such as caching. This PR removes that function, and fixes the code introduced by leanprover#3398 for which the function was first added. cc @semorrison.
…t` (leanprover#4128) Fix stack overflow crash. Closes leanprover#4117 The fix can be improved: we could try to avoid creating hundreds of auto implicits before failing.
The main loop logic could be simplified, and `if let` could be used to make control flow more obvious. Also adds a check for macro scopes to prevent `unresolveNameGlobal` from returning names with macro scopes in the event there's an alias with one. This is a follow up to leanprover#3946.
Adds `IO.getTaskState` which returns the state of a `Task` in the Lean runtime's task manager. The `TaskState` inductive has 3 constructors: `waiting`, `running`, and `finished`. The `waiting` constructor encompasses the waiting and queued states within the C task object documentation, because the task object does not provide a low cost way to distinguish these different forms of waiting. Furthermore, it seems unlikely for consumers to wish to distinguish between these internal states. The `running` constructor encompasses both the running and promised states in C docs. While not ideal, the C implementation does not provide a way to distinguish between a running `Task` and a waiting `Promise.result` (they both have null closures).
Issue has been fixed by another PR. closes leanprover#2558
I did not introduce `inductTheoremSuffix` etc, it seems more direct to just spell out the suffix here. If we ever change it there are many occurrences where they need to be changed anyways, so the definition doesn't seem to save much work or add that much robustness.
Currently this causes linter warnings downstream in proofs that unfold substrEq.loop.
…rover#4148) Closes two `sorry`s at https://github.com/leanprover/leansat/pull/64/files. --------- Co-authored-by: Kim Morrison <[email protected]>
bollu
pushed a commit
that referenced
this pull request
Jun 13, 2024
…anprover#4410) Closes leanprover#4375 The following example raises `error: (kernel) declaration has free variables '_example'`: ```lean example: Nat → Nat := let a : Nat := Nat.zero fun (_ : Nat) => let b : Nat := Nat.zero (fun (_ : a = b) => 0) (Eq.refl a) ``` During elaboration of `0`, `elabNumLit` creates a synthetic mvar `?_uniq.16` which gets abstracted by `elabFun` to `?_uniq.16 := ?_uniq.50 _uniq.6 _uniq.12`. The `isDefEq` to `instOfNatNat 0` results in: ``` ?_uniq.50 := fun ([email protected]._hyg.13 : Nat) => let b : Nat := Nat.zero fun ([email protected]._hyg.23 : Eq.{1} Nat _uniq.4 b) => instOfNatNat 0 ``` This has a free variable `_uniq.4` which was `a`. When the application of `?_uniq.50` to `#[#2, #0]` is instantiated, the `let b : Nat := Nat.zero` blocks the beta-reduction and `_uniq.4` remains in the expression. fix: add `(useZeta := true)` here: https://github.com/leanprover/lean4/blob/ea46bf2839ad1c98d3a0c3e5caad8a81f812934c/src/Lean/MetavarContext.lean#L567
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.
No description provided.