chore: make Subrelation reducible
#10464
Open
Conversation
This file contains hidden or 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 PR adds support the Count Trailing Zeros operation `BitVec.ctz` to the bitvector library and to `bv_decide`, relying on the existing `clz` circuit. We also build some theory around `BitVec.ctz` (analogous to the theory existing for `BitVec.clz`) and introduce lemmas `BitVec.[ctz_eq_reverse_clz, clz_eq_reverse_ctz, ctz_lt_iff_ne_zero, getLsbD_false_of_lt_ctz, getLsbD_true_ctz_of_ne_zero, two_pow_ctz_le_toNat_of_ne_zero, reverse_reverse_eq, reverse_eq_zero_iff]`. `ctz` operation is common in numerous compiler intrinsics (see [here](https://clang.llvm.org/docs/LanguageExtensions.html#intrinsics-support-within-constant-expressions)) and architectures (see [here](https://en.wikipedia.org/wiki/Find_first_set)). --------- Co-authored-by: Siddharth <[email protected]>
This PR redefines `String` to be the type of byte arrays `b` for which `b.IsValidUtf8`. This moves the data model of strings much closer to the actual data representation at runtime. In the near future, we will - provide variants of `String.Pos` and `Substring` that only allow for valid positions - redefine all `String` functions to be much closer to their C++ implementations In the near-to-medium future we will then provide comprehensive verification of `String` based on these refactors.
This PR fixes an issue where notations and other overloadings would signal kernel errors even though there exists a successful interpretation.
This PR adds the `reduceCtorIdx` simproc which recognizes and reduces `ctorIdx` applications. This is not on by default yet because it does not use the discrimination tree (yet).
…eanprover#10445) This PR adds helper definitions in preparation for the upcoming injective function support in `grind`.
This PR fixes an overeager insertion of `inc` operations for large uint constants. Closes: leanprover#10443
This PR adds an alternative implementation of `DerivingBEq` based on comparing `.ctorIdx` and using a dedicated matcher for comparing same constructors (added in leanprover#10152), to avoid the quadratic overhead of the default match implementation. The new option `deriving.beq.linear_construction_threshold` sets the constructor count threshold (10 by default) for using the new construction. Such instances also allow `deriving ReflBEq, LawfulBeq`, although these proofs for these properties are still quadratic.
This PR adds the `[grind inj]` attribute for marking injectivity theorems for `grind`.
This PR ensures that issues reported by the E-matching module are displayed only when `set_option grind.debug true` is enabled. Users reported that these messages are too distracting and not very useful. They are more valuable for library developers when annotating their libraries.
(This test is currently failing. We either need to change the failing line to `grind [!factorial_pos]`, or again change the behaviour of grind.)
This PR makes `mvcgen` reduce through `let`s, so that it progresses over `(have t := 42; fun _ => foo t) 23` by reduction to `have t := 42; foo t` and then introducing `t`.
This PR changes `mkNoConfusionCtors` so that its use of `inferType` does not have to reduce `noConfusionType`, to make leanprover#10315 really effective.
…dules (leanprover#10418) This PR fixes a potential miscompilation when using non-exposed type definitions using the module system by turning it into a static error. A future revision may lift the restriction by making the compiler metadata independent of the current module.
…#10456) This PR implements `mvcgen invariants?` for providing initial invariant skeletons for the user to flesh out. When the loop body has an early return, it will helpfully suggest `Invariant.withEarlyReturn ...` as a skeleton. ```lean def mySum (l : List Nat) : Nat := Id.run do let mut acc := 0 for x in l do acc := acc + x return acc /-- info: Try this: invariants · ⇓⟨xs, acc⟩ => _ -/ #guard_msgs (info) in theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by generalize h : mySum l = r apply Id.of_wp_run_eq h mvcgen invariants? all_goals admit def nodup (l : List Int) : Bool := Id.run do let mut seen : HashSet Int := ∅ for x in l do if x ∈ seen then return false seen := seen.insert x return true /-- info: Try this: invariants · Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _) -/ #guard_msgs (info) in theorem nodup_suggest_invariant (l : List Int) : nodup l ↔ l.Nodup := by generalize h : nodup l = r apply Id.of_wp_run_eq h mvcgen invariants? all_goals admit ```
This PR adds an alternative implementation of `Deriving Ord` based on comparing `.ctorIdx` and using a dedicated matcher for comparing same constructors (added in leanprover#10152). The new option `deriving.ord.linear_construction_threshold` sets the constructor count threshold (10 by default) for using the new construction. It also (unconditionally) changes the implementation for enumeration types to simply compare the `ctorIdx`.
|
WIP |
github-actions
bot
added
the
WIP
fgdorais
force-pushed
the
reducible-subrelation
branch
from
9e14e44 to
fb3eab5
Compare
fgdorais
force-pushed
the
reducible-subrelation
branch
from
fb3eab5 to
492f3b4
Compare
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
Reference manual CI status:
|
fgdorais
requested review from
datokrat,
sgraf812,
hargoniX,
TwoFX,
digama0,
kim-em,
Vtec234,
leodemoura,
zwarich and
tydeu
as code owners
|
awaiting-review |
github-actions
bot
added
awaiting-review
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 makes
Subrelationreducible.Closes #10471