This PR adds in more normalization for the routine that computes a
parent type. Some mathlib adaptations are the result of not reducing the
type parameters.
This PR improves how `grind` normalizes dependent implications during
introduction.
Previously, `grind` would introduce a hypothesis `h : p` for a goal of
the form `.. ⊢ (h : p) → q h`, and then normalize and assert a
non-dependent copy of `p`. As a result, the local context would contain
both `h : p` and a separate `h' : p'`, where `p'` is the normal form of
`p`. Moreover, `q` would still depend on the original `h`.
After this commit, `grind` avoids creating a copy. The context will now
contain only `h : p'`, and the new goal becomes `.. ⊢ q (he.mpr_prop
h)`, where `he` is a proof of `p = p'`.
This PR replaces `assert!` with `assertBEq` to fix issues where asserts
didn't trigger the `ctest` due to being in a separate task. This was
caused by panics not being caught in tasks, while IO errors were handled
by the `AsyncTask` if we use the `block` function on them.
---------
Co-authored-by: Henrik Böving <hargonix@gmail.com>
This PR deletes an unused invariant from the AIG to CNF conversion.
Interestingly despite being listed in the AIGNET paper it is actually
not used in the proof so we can just remove it.
This PR adds `Std.BaseMutex.tryLock` and `Std.Mutex.tryAtomically` as
well as unit tests for our locking and condition variable primitives.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR adds some new information to the release checklist,
as well as some new automated checks to help with the release process.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR enables the use of the build-time configuration of the Lean
reference manual URL and updates the release checklist to account for
the reference manual.
This is a follow-up to #7240, after the required `stage0` update.
The release process described here uses the same location for the
reference manual for RCs and stable releases. This is for two reasons:
1. The only changes between them should be a modification of the
embedded version string and updates to the final release's release
notes, once those are included.
2. It ensures that a compatible manual is available at the moment that
the new release appears, so any delay getting it deployed won't be
visible to users.
This PR makes the BitVec docstrings match each other and the rest of the
API in style.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: Siddharth <siddu.druid@gmail.com>
This PR adds declaration ranges to structure fields that were copied
from parents that aren't represented as subobjects, supporting "go to
definition". The declaration range is the parent in the `extends`
clause.
This PR fixes an oversight in #7717, and now fields get a FieldInfo node
with the correct projection function.
Note that for copied fields "go to definition" still does not go
anywhere, since copied projection function has no declaration range. We
probably should make such fields instead go to the origin projection
function.
This PR adds a feature to `structure`/`class` where binders without
types on a field definition are interpreted as overriding the type's
parameters binder kinds in that field's projection function. The rules
are (1) only a prefix of the binders are interpreted this way, (2)
multi-identifier binders are allowed but they must all be for
parameters, (3) only parameters that appear in the declaration itself
(not from `variables`) can be overridden and (4) the updates will be
applied after parameter binder kind inference is done. Binder updates
are not allowed in default value redefinitions. Example application: In
the following, `(R p)` causes the `R` and `p` parameters to be explicit,
where normally they would be implicit.
```
class CharP (R : Type u) [AddMonoidWithOne R] (p : Nat) : Prop where
cast_eq_zero_iff (R p) : ∀ x : Nat, (x : R) = 0 ↔ p ∣ x
#guard_msgs in #check CharP.cast_eq_zero_iff
/-
info: CharP.cast_eq_zero_iff.{u} (R : Type u) {inst✝ : AddMonoidWithOne R} (p : Nat) [self : CharP R p] (x : Nat) :
↑x = 0 ↔ p ∣ x
-/
```
The rationale for (3) is that there are cases where a module starts with
a large `variables` list and a field only incidentally uses the binder.
Without the restriction, the field ends up depending on that variable,
counterintuitively causing it to be introduced as an additional
parameter for the type. Instead, there is an explicit error. The easy
fix is to add `: _`, which is the bare minimum to make the binder have a
type.
We should consider warning when binders shadow parameters.
Closes#3574
[Zulip
discussion](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/RFC.3A.20adjust.20argument.20explicitness.20on.20typeclass.20projections/near/508584627)
Mathlib fixes:
https://github.com/leanprover-community/mathlib4/pull/23469
This PR changes how `{...}`/`where` notation ("structure instance
notation") elaborates. The notation now tries to simulate a flat
representation as much as possible, without exposing the details of
subobjects. Features:
- When fields are elaborated, their expected types now have a couple
reductions applied. For all projections and constructors associated to
the structure and its parents, projections of constructors are reduced
and constructors of projections are eta reduced, and also implementation
detail local variables are zeta reduced in propositions (so tactic
proofs should never see them anymore). Furthermore, field values are
beta reduced automatically in successive field types. The example in
[mathlib4#12129](https://github.com/leanprover-community/mathlib4/issues/12129#issuecomment-2056134533)
now shows a goal of `0 = 0` rather than `{ toFun := fun x => x }.toFun 0
= 0`.
- All parents can now be used as field names, not just the subobject
parents. These are like additional sources but with three constraints:
every field of the value must be used, the fields must not overlap with
other provided fields, and every field of the specified parent must be
provided for. Similar to sources, the values are hoisted to `let`s if
they are not already variables, to avoid multiple evaluation. They are
implementation detail local variables, so they get unfolded for
successive fields.
- All class parents are now used to fill in missing fields, not just the
subobject parents. Closes#6046. Rules: (1) only those parents whose
fields are a subset of the remaining fields are considered, (2) parents
are considered only before any fields are elaborated, and (3) only those
parents whose type can be computed are considered (this can happen if a
parent depends on another parent, which is possible since #7302).
- Default values and autoparams now respect the resolution order
completely: each field has at most one default value definition that can
provide for it. The algorithm that tries to unstick default values by
walking up the subobject hierarchy has been removed. If there are
applications of default value priorities, we might consider it in a
future release.
- The resulting constructors are now fully packed. This is implemented
by doing structure eta reduction of the elaborated expressions.
- "Magic field definitions" (as reported [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Where.20is.20sSup.20defined.20on.20submodules.3F/near/499578795))
have been eliminated. This was where fields were being solved for by
unification, tricking the default value system into thinking they had
actually been provided. Now the default value system keeps track of
which fields it has actually solved for, and which fields the user did
not provide. Explicit structure fields (the default kind) without any
explicit value definition will result in an error. If it was solved for
by unification, the error message will include the inferred value, like
"field 'f' must be explicitly provided, its synthesized value is v"
- When the notation is used in patterns, it now no longer inserts fields
using class parents, and it no longer applies autoparams or default
values. The motivation is that one expects patterns to match only the
given fields. This is still imperfect, since fields might be solved for
indirectly.
- Elaboration now attempts error recovery. Extraneous fields log errors
and are ignored, missing fields are filled with `sorry`.
This is a breaking change, but generally the mitigation is to remove
`dsimp only` from the beginnings of proofs. Sometimes "magic fields"
need to be provided — four possible mitigations are (1) to provide the
field, (2) to provide `_` for the value of the field, (3) to add `..` to
the structure instance notation, (4) or decide to modify the `structure`
command to make the field implicit. Lastly, sometimes parent instances
don't apply when they should. This could be because some of the provided
fields overlap with the class, or it could be that the parent depends on
some of the fields for synthesis — and as parents are only considered
before any fields are elaborated, such parents might not be possible to
use — we will look into refining this further.
There is also a change to elaboration: now the `afterTypeChecking`
attributes are run with all `structure` data set up (e.g. the list of
parents, along with all parent projections in the environment). This is
necessary since attributes like `@[ext]` use structure instance
notation, and the notation needs all this data to be set up now.
This PR ensures that in the AIG the constant circuit node is always
stored at the first spot. This allows us to skip performing a cache
lookup when we require a constant node.
This PR deprecates `extraDepTargets` and fixes a bug caused by the
configuration refactor.
Unfortunately, defaults with inter-field dependencies are not handled
correctly by the auto-generated TOML decoders. Thus, a special case hack
is used to fix this for `globs` (the one field that needs it).
This PR compresses the AIG representation by storing the inverter bit in
the lowest bit of the gate descriptor instead of as a separate `Bool`.
Note that this is only the first step, we also need to compress the
representation in `Ref` though this is a potentially more difficult
refactor as `Ref`'s constructor is being referred to all over the place.
This PR adds the `moreLinkObjs` and `moreLinkLibs` options for Lean
packages, libraries, and executables. These serves as functional
replacements for `extern_lib` and provided additional flexibility.
External libraries applied to the whole package and were necessarily
static. This options are configured on a per-target basis and support
shared-only libraries.
**Breaking change:** `precompileModules` now only loads modules of the
current library individually. Modules of other libraries are loaded
together via that library's shared library.
This PR fixes the `markNestedProofs` procedure used in `grind`. It was
missing the case where the type of a nested proof may contain other
nested proofs.
This PR adds `dite_eq_ite` normalization rule to `grind`. This rule is
important to adjust mismatches between a definition and its function
induction principle.
This PR adds a benchmark that produces a gigantic AIG out of a
relatively small input, allowing us to measure performance bottlenecks
in the AIG framework itself.
This PR adds lemmas about the modulo operation defined on signed bounded
integers.
The results depend on the lemma
```lean
theorem BitVec.toInt_srem (a b : BitVec w) : (a.srem b).toInt = a.toInt.tmod b.toInt := sorry
```
which is missing at the time of posting the PR.
This PR adds `input_file` and `input_dir` as new target types. It also
adds the `needs` configuration option for Lean libraries and
executables. This option generalizes `extraDepTargets` (which will be
deprecated in the future), providing much richer support for declaring
dependencies across package and target type boundaries.
Closes#2761.
This PR skips computation of the hash of `BVExpr.Cache.Key` as the
expression's hash is a computed field and the width is already mixed in
by its hash function. This will probably only have a very minor effect
but is visible in large SMTLIB benchmarks.
