This PR marks `Nat.div` and `Nat.modCore` as `irreducible`, to recover
the behavior from from before #7558.
Fixes#7612. H't to @tobiasgrosser for the good bug report.
This PR bumps the server version so that clients like NeoVim can detect
whether the server supports our recent language server extensions
(modulo the time that has passed since these extension PRs).
I'd like to have server capabilities for this at some point, but this
will have to do for now.
This PR adds the known bits optimization from the multiplication circuit
to the add one, allowing us to discover potentially even more symmetries
before going to the SAT solver.
This PR removes the use of the Lake plugin in the Lake build and in
configuration files.
With #7399, the plugin is no longer necessary and may be the source of
some persistent intermittent Lake test failures.
This PR implements the addition rewrite from the Bitwuzla rewrite
[BV_EXTRACT_ADD_MUL](e09c50818b/src/rewrite/rewrites_bv.cpp (L1495-L1510)),
which witness that the high bits at `i >= len` do not affect the bits of
the sum upto `len`:
```lean
theorem extractLsb'_add {w len} {x y : BitVec w} (hlen : len ≤ w) :
(x + y).extractLsb' 0 len = x.extractLsb' 0 len + y.extractLsb' 0 len
```
---------
Co-authored-by: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
This PR adds short-circuit support to bv_decide to accelerate
multiplications with shared coefficients. In particular, `a * x = b * x`
can be extended to `a = b v (a * x = b * x)`. The latter is faster if `a
= b` is true, as `a = b` may be evaluated without considering the
multiplication circuit. On the other hand, we require the multiplication
circuit, as `a * x = b * x -> a = b` is not always true due to two's
complement wrapping.
We support multiplications through acNF, which takes into account shared
terms across equality canonicalizing `a * (b * c1) = a * (b * c2)` to
`(a * b) * c1 = (a * b) * c2`. As a result, the non-shared terms are
lifted to the top such that canonical rewrites for binary multiplication
with shared terms on the left/right are sufficient.
We add an option `bv_decide +shortCircuit` which controls this feature
(currently disabled by default).
---------
Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
This PR changes the structure instance notation pretty printer so that
fields are omitted if their value is definitionally equal to the default
value for the field (up to reducible transparancy). Setting
`pp.structureInstances.defaults` to true forces such fields to be pretty
printed anyway.
Closes#1100
This PR adds SMT-LIB operators to detect overflow `BitVec.negOverflow`,
according to the [SMTLIB
standard](https://github.com/SMT-LIB/SMT-LIB-2/blob/2.7/Theories/FixedSizeBitVectors.smt2),
and the theorem proving equivalence of such definition with the `BitVec`
library functions (`negOverflow_eq`).
Co-authored by @bollu and @alexkeizer
---------
Co-authored-by: Siddharth <siddu.druid@gmail.com>
As preparation for the module system, and in hopes it will be faster
than and replace the Nix CI. Secondary build jobs do not block merging.
Also makes macOS aarch64 a secondary build job on the PR level, where it
is the current bottleneck.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
This PR provides lemmas about the tree map function `minKey?` and its
interaction with other functions for which lemmas already exist.
---------
Co-authored-by: Paul Reichert <datokrat@users.noreply.github.com>
Asynchronous elaboration means that constants can exist in the elab
environment while failing to be added to the kernel environment, avoid
the latter by falling back to axioms there
This PR adds some documentation to the Lean's `lakefile.toml` and makes
a few tweaks required to get `USE_LAKE` working properly on Windows. It
also adds a `stage1-configure` step target so the Lake configuration
files can be generated without performing a build of stage 1. This
enables one to build stage 0 and configure Lake via CMake and then use
Lake instead of CMake to build stage 1.
Partly adapted from #7505.
This PR changes the `static.export` facet for Lean libraries to produce
thin static libraries.
Static libraries with explicitly exported symbols are only necessary on
Windows (where symbol counts are a concern) and are usually used as part
of local build process and not distributed (as they are in Lean's
build). Thus, it seems reasonable to make them unilaterally thin. They
also need to be thin for the Lean build with Lake.
This PR changes Lake to produce and use response files on Windows when
building executables and libraries (static and shared). This is done to
avoid potentially exceeding Windows command line length limits.
Closes#4159.
This PR improves the counterexamples produced by the cutsat procedure,
and adds proper support for `Nat`. Before this PR, the assignment for an
natural variable `x` would be represented as `NatCast.natCast x`.
This PR introduces TCP socket support using the LibUV library, enabling
asynchronous I/O operations with it.
---------
Co-authored-by: Henrik Böving <hargonix@gmail.com>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR makes functions defined by well-founded recursion use an
`opaque` well-founded proof by default. This reliably prevents kernel
reduction of such definitions and proofs, which tends to be
prohibitively slow (fixes#2171), and which regularly causes
hard-to-debug kernel type-checking failures. This changes renders
`unseal` ineffective for such definitions. To avoid the opaque proof,
annotate the function definition with `@[semireducible]`.
This PR upstreams `bind_congr` from Mathlib and proves that the minimum
of a sorted list is its head and weakens the antisymmetry condition of
`min?_eq_some_iff`. Instead of requiring an `Std.Antisymm` instance,
`min?_eq_some_iff` now only expects a proof that the relation is
antisymmetric *on the elements of the list*. If the new premise is left
out, an autoparam will try to derive it from `Std.Antisymm`, so existing
usages of the theorem will most likely continue to work.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR unifies the configuration declarations of dynamic targets,
external libraries, Lean libraries, and Lean executables into a single
data type stored in a unified map within a package.
As a side-effect of these changes, auto-completion now also works on an
empty configuration (after the `where`).
**Breaking change:** Users can no longer define multiple targets with
the same name but different kinds (e.g., a Lean executable and a Lean
library both named `foo`). This should not effect most users as the Lake
DSL already discouraged this.
This PR fixes the support for nonlinear `Nat` terms in cutsat. For
example, cutsat was failing in the following example
```lean
example (i j k l : Nat) : i / j + k + l - k = i / j + l := by grind
```
because we were not adding the fact that `i / j` is non negative when we
inject the `Nat` expression into `Int`.
This PR changes the definition of `Nat.div` and `Nat.mod` to use a
structurally recursive, fuel-based implementation rather than
well-founded recursion. This leads to more predicable reduction behavior
in the kernel.
`Nat.div` and `Nat.mod` are somewhat special because the kernel has
native reduction for them when applied to literals. But sometimes this
does not kick in, and the kernel has to unfold `Nat.div`/`Nat.mod` (e.g.
in `lazy_delta_reduction` when there are open terms around). In these
cases we want a well-behaved definition.
We really do not want to reduce proofs in the kernel, which we want to
prevent anyways well-founded recursion (to be prevented by #5182).
Hence we avoid well-founded recursion here, and use a (somewhat
standard) translation to a fuel-based definition.
(If this idiom is needed more often we could even support it in Lean
with `termination_by +fuel <measure>` rather easily.)
This PR ensures that we use the same ordering to normalize linear `Int`
terms and relations. This change affects `simp +arith` and `grind`
normalizer.
This consistency is important in the cutsat procedure. We want to avoid
a situation where the cutsat state contains both "atoms":
- `「(NatCast.natCast x + NatCast.natCast y) % 8」`
- `「(NatCast.natCast y + NatCast.natCast x) % 8」`
This was happening because we were using different orderings for
(nested) terms and relations (`=`, `<=`).
This PR changes `isNatCmp` to ignore optional arguments annotations,
when checking for `<`-like comparison between elements of `Nat`. That
previously caused `guessLex` to fail when checking termination of a
function, whose signature involved an optional argument of the type
`Nat`.
Closes https://github.com/leanprover/lean4/issues/7458
This PR revises the docstring for `funext`, making it more concise and
adding a reference to the manual for more details.
This revised docstring is less technical, while still capturing the most
important points of the prior one.
