This PR fixes an issue in the theory propagation used in `grind`. When
two equivalence classes are merged, the core may need to push additional
equalities or disequalities down to the satellite theory solvers (e.g.,
`cutsat`, `comm ring`, etc). Some solvers (e.g. `cutsat`) assume that
all of the core’s invariants hold before they receive those facts.
Propagating immediately therefore risks violating a solver’s
pre-conditions midway through the merge. To decouple the merge operation
from propagation and to keep the core solver-agnostic, this PR adds the
helper type `PendingTheoryPropagation`.
This PR improves the E-matching pattern inference procedure in `grind`.
Consider the following theorem:
```lean
@[grind →]
theorem eq_empty_of_append_eq_empty {xs ys : Array α} (h : xs ++ ys = #[]) : xs = #[] ∧ ys = #[] :=
append_eq_empty_iff.mp h
```
Before this PR, `grind` inferred the following pattern:
```lean
@HAppend.hAppend _ _ _ _ #2#1
```
Note that this pattern would match any `++` application, even if it had
nothing to do with arrays. With this PR, the inferred pattern becomes:
```lean
@HAppend.hAppend (Array #3) (Array _) (Array _) _ #2#1
```
With the new pattern, the theorem will not be considered by `grind` for
goals that do not involve `Array`s.
This PR implements **stepwise proof terms** in the commutative ring
procedure used by `grind`. These terms serve as an alternative
representation to the traditional Nullstellensatz certificates, aiming
to address the **exponential worst-case complexity** often associated
with certificate construction.
While various compression techniques for Nullstellensatz certificates
exist, they are not implemented in our procedure. Moreover, many of
these techniques rely on additional properties not available in
arbitrary commutative rings. In contrast, the stepwise proof terms
encode the **actual derivation** used during simplification, offering
significantly better scalability in practice.
Here is a motivating example:
```lean
example {α} [CommRing α] [IsCharP α 0] (d t c : α) (d_inv PSO3_inv : α)
(Δ40 : d^2 * (d + t - d * t - 2) * (d + t + d * t) = 0)
(Δ41 : -d^4 * (d + t - d * t - 2) *
(2 * d + 2 * d * t - 4 * d * t^2 + 2 * d * t^4 + 2 * d^2 * t^4 - c * (d + t + d * t)) = 0)
(_ : d * d_inv = 1)
(_ : (d + t - d * t - 2) * PSO3_inv = 1) :
t^2 = t + 1 := by grind +ring
```
In this case, the Nullstellensatz certificate generated by our procedure
contains **over 20,000 terms**, which overwhelms the Lean kernel during
verification. @kim-em also computed certificates using Mathematica with
various variable orderings, producing results between **500 and 2,000
terms**: still quite large.
By switching to stepwise derivations:
- `grind` completes the goal in **under 10 ms**
- The Lean kernel checks the resulting proof term in **under 1 second**
This change dramatically improves both the performance and robustness of
`grind` for nontrivial algebraic goals.
This PR adds support for inductive and coinductive predicates defined
using lattice theoretic structures on `Prop`. These are syntactically
defined using `greatest_fixpoint` or `least_fixpoint` termination
clauses for recursive `Prop`-valued functions. The functionality relies
on `partial_fixpoint` machinery and requires function definitions to be
monotone. For non-mutually recursive predicates, an appropriate
(co)induction proof principle (given by Park induction) is generated.
Summary of changes:
- `Interal.Order.Basic` now contains `CompleteLattice` class, as well as
version of Knaster-Tarski fixpoint theorem (with an associated Park
induction principle) for the internal use for defining (co)inductive
predicates. `Prop` is shown to have two complete lattice structures (one
given by implication order for defining inductive predicates, and one
given by reverse implication for defining coinductive predicates).
Additionally, proofs that lattices are closed under products and
function spaces are included.
- Partial fixpoint's `EqnInfo` now additionally carries an information
whether something is defined as a lattice-theoretic fixpoint or via
CCPOs.
- When constructing a (co)inductive predicate,`PartialFixpoint/Main`
builds an appropriate lattice structure on the type of the predicate
using product lattice, function space lattice and an appropriate lattice
instance on `Prop`.
- `PartialFixpoint/Eqns` is modified to be able to perform rewrite under
lattice-theoretic fixpoint construction
- `PartialFixpoint/Induction`contains a case split for handling of the
(co)inductive predicates. In the case of lattice-theoretic fixpoints, it
appropriately desugars the Park induction principle.
This PR adds support for the following import variants to the
experimental module system:
* `private import`: Makes the imported constants available only in
non-exported contexts such as proofs. In particular, the import will not
be loaded, or required to exist at all, when the current module is
imported into other modules.
* `import all`: Makes non-exported information such as proofs of the
imported module available in non-exported contexts in the current
module. Main purpose is to allow for reasoning about imported
definitions when they would otherwise be opaque. TODO: adjust name
resolution so that imported `private` decls are accessible through
syntax.
They can be combined into `private import all`, which will likely be the
most common usage of `import all`.
This PR lets `induction` accept eliminator where the motive application
in the conclusion has complex arguments; these are abstracted over using
`kabstract` if possible. This feature will go well with unfolding
induction principles (#8088).
This PR adds simprocs to simplify appends of non-overlapping Bitvector
adds. We add a simproc instead of just a `simp` lemma to ensure that we
correctly rewrite bitvector appends. Since bitvector appends lead to
computation at the bitvector width level, it seems to be more stable to
write a simproc.
As I write this, I realize that I can maybe write the `simp` lemma using
`no_index` to recover the same behaviour, so I'll try that too.
This PR fixes a bug when constructing the proof term for a
Nullstellensatz certificate produced by the new commutative ring
procedure in `grind`. The kernel was rejecting the proof term.
This PR adds some currently failing tests for `grind +ring`, resulting
in either kernel type mismatches (bugs) or a kernel deep recursion
(perhaps just a too-large problem).
This PR is a follow up to #8055 and implements a `Selector` for async
UDP in order to allow IO multiplexing using UDP sockets.
The technical approach taken for this PR is basically a copy of #8078
but adjusted for UDP. The libuv API gives the same guarantee that was
used in that PR.
This PR changes `Lean.Grind.CommRing` to inline the `NatCast` instance
(i.e. to be provided by the user) rather than constructing one from the
existing data. Without this change we can't construct instances in
Mathlib that `grind` can use.
This PR adds the “unfolding” variant of the functional induction and
functional cases principles, under the name `foo.induct_unfolding` resp.
`foo.fun_cases_unfolding`. These theorems combine induction over the
structure of a recursive function with the unfolding of that function,
and should be more reliable, easier to use and more efficient than just
case-splitting and then rewriting with equational theorems.
For example instead of
```
ackermann.induct
(motive : Nat → Nat → Prop)
(case1 : ∀ (m : Nat), motive 0 m)
(case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
(case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
(x x : Nat) : motive x x
```
one gets
```
ackermann.fun_cases_unfolding
(motive : Nat → Nat → Nat → Prop)
(case1 : ∀ (m : Nat), motive 0 m (m + 1))
(case2 : ∀ (n : Nat), motive n.succ 0 (ackermann n 1))
(case3 : ∀ (n m : Nat), motive n.succ m.succ (ackermann n (ackermann (n + 1) m)))
(x✝ x✝¹ : Nat) : motive x✝ x✝¹ (ackermann x✝ x✝¹)
```
This PR is a follow up to #8055 and implements a Selector for
`Std.Channel` in order to allow
multiplexing using channels.
There is one subtlety to the implementation: Suppose we are in a
situation where we run `select` in a loop on two channels. One of the
channels is always quiet while the other has data available occasionally
(however not always as this would trigger the `tryFn` fast path and hide
the issue). In this situation the select receivers that are enqueued on
the silent channel would usually just remain there indefinitely as
nothing ever happens, causing a memleak. To avoid this we want to make a
channel select clean up after itself, even if it fails.
In an imperative programming language we could implement the receive
queue as a doubly linked list and simply make each receive select
maintain a pointer to its element in the queue and then remove itself in
`O(1)` upon failure. As that is not possible in Lean trivially we
decided to go for another approach for now: simply filter the queue for
selects that have failed in `unregisterFn`. While this approach is
`O(n)` we expect the amount of receivers enqueued on a channel to not be
terribly large and thus this to be a reasonably fast operation compared
to the remaining overhead. If it ever ends up becoming an issue, we
could switch to an approach that uses a `TreeMap` with numbered
receivers instead at a certain wait queue size and go to `O(log(n))`.
This PR adds optimized division functions for `Int` and `Nat` when the
arguments are known to be divisible (such as when normalizing
rationals). These are backed by the gmp functions `mpz_divexact` and
`mpz_divexact_ui`. See also leanprover-community/batteries#1202.
This PR fixes a bug where the old compiler's lcnf conversion expr cache
was not including all of the relevant information in the key, leading to
terms inadvertently being erased. The `root` variable is used to
determine whether lambda arguments to applications should get let
bindings or not, which in turn affects later decisions about type
erasure (erase_irrelevant assumes that any non-atomic argument is
irrelevant).
This PR fixes the `grind +splitImp` and the arrow propagator. Given `p :
Prop`, the propagator was incorrectly assuming `A` was always a
proposition in an arrow `A -> p`. This PR also adds a missing
normalization rule to `grind`.
This PR adds an initial set of `@[grind]` annotations for
`List`/`Array`/`Vector`, enough to set up some regression tests using
`grind` in proofs about `List`. More annotations to follow.
This PR makes `realizeConst` to not set a `declPrefix`. This allows the
realization of both `foo.eq_def` and `bar.eq_def`, where `foo` and `bar`
are mutually recursive, all attached to the same function's environment.
This PR improves equality propagation (also known as theory combination)
and polynomial simplification for rings that do not implement the
`NoZeroNatDivisors` class. With these fixes, `grind` can now solve:
```lean
example [CommRing α] (a b c : α) (f : α → Nat)
: a + b + c = 3 →
a^2 + b^2 + c^2 = 5 →
a^3 + b^3 + c^3 = 7 →
f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by
grind +ring
```
This example uses the commutative ring procedure, the linear integer
arithmetic solver, and congruence closure.
For rings that implement `NoZeroNatDivisors`, a polynomial is now also
divided by the greatest common divisor (gcd) of its coefficients when it
is inserted into the basis.
This PR ensures that `set_option grind.debug true` works properly when
using `grind +ring`. It also adds the helper functions `mkPropEq` and
`mkExpectedPropHint`.
This PR fixes the monomial order used by the commutative ring procedure
in `grind`. The following new test now terminates quickly.
```lean
example [CommRing α] (a b c : α)
: a + b + c = 3 →
a^2 + b^2 + c^2 = 5 →
a^3 + b^3 + c^3 = 7 →
a^4 + b^4 + c^4 = 9 := by
grind +ring
```
This PR implements equality propagation in the new commutative ring
procedure in `grind`. The idea is to propagate implied equalities back
to the `grind` core module that does congruence closure. In the
following example, the equalities: `x^2*y = 1` and `x*y^2 - y = 0` imply
that `y*x` is equal to `y*x*y`, which implies by congruence that `f
(y*x) = f (y*x*y)`.
```lean
example [CommRing α] (x y : α) (f : α → Nat) : x^2*y = 1 → x*y^2 - y = 0 → f (y*x) = f (y*x*y) := by
grind +ring
```
This PR updates the If-Normalization example, to separately give an
implementation and subsequently prove the spec (using fun_induction),
instead of previously building a term in the subtype directly. At the
same time, adds a (failing) `grind` test case illustrating a problem
with unused match witnesses.
This PR implements the main loop of the new commutative ring procedure
in `grind`. In the main loop, for each polynomial `p` in the todo queue,
the procedure:
- Simplifies it using the current basis.
- Computes critical pairs with polynomials already in the basis and adds
them to the queue.
After the queue is empty, the disequalities are re-simplified using the
new basis. `grind` can now solve examples such as:
```lean
example [CommRing α] (x y : α) : x*y*x = 1 → x*y*y = y → y = 1 := by
grind +ring
example [CommRing α] (x y : α) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
grind +ring
example (x y : BitVec 16) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
grind +ring
```
This PR implements the generation of compact proof terms for
Nullstellensatz certificates in the new commutative ring procedure in
`grind`. Some examples:
```lean
example [CommRing α] (x y : α) : x = 1 → y = 2 → 2*x + y = 4 := by
grind +ring
example [CommRing α] [IsCharP α 7] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
grind +ring
example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
grind +ring
example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
grind +ring
```
This PR adds the helper type class `NoZeroNatDivisors` for the
commutative ring procedure in `grind`. Core only implements it for
`Int`. It can be instantiated in Mathlib for any type `A` that
implements `NoZeroSMulDivisors Nat A`.
See `findSimp?` and `PolyDerivation` for details on how this instance
impacts the commutative ring procedure.
This PR fixes a parallelism regression where linters that e.g. check for
errors in the command would no longer find such messages.
---------
Co-authored-by: damiano <adomani@gmail.com>
`[wf_preprocess]` expects a dsimp theorem, which in `Init` temporarily
have a simplistic syntactic representation until a more robust solution
is implemented.
This PR fixes the generation of functional induction principles for
functions with nested nested well-founded recursion and late fixed
parameters. This is a follow-up for #7166. Fixes#8093.
This PR is a follow up to #8055 and implements a `Selector` for async
TCP in order to allow IO multiplexing using TCP sockets.
As we must not commit to actually fetching data from the socket buffer
this cannot be implemented by just racing on `recv?`. Instead we perform
a call to `uv_read_start` and pass an `alloc_cb` that allocates no
memory at all. According to the docs of
[`uv_alloc_cb`](https://docs.libuv.org/en/v1.x/handle.html#c.uv_alloc_cb)
this is guaranteed to give us a `UV_ENOBUFS` in the relevant callback.
Thus we can first run this "zero read" and then go into one of three
cases:
1. We get cancelled before the zero read completes, in this case just
cancel the zero read and give up.
2. The zero read completes and we loose the race for completing the
`select`, in this case just don't do anything anymore
3. The zero read completes and we win the race for completing the
`select`, in this case we perform the actual read on the socket. As we
know that data is available already (since the read callback of the zero
read is only triggered if data actually is available) we know that the
subsequent actual read should complete right away.
In this way we avoid any data loss if we loose the race.
This PR contains the theorem proving that signed division x.toInt /
y.toInt only overflows when `x = intMin w` and `y = allOnes w` (for `0 <
w`).
To show that this is the *only* case in which overflow happens, we refer
to overflow for negation
(`BitVec.sdivOverflow_eq_negOverflow_of_neg_one`): in fact,
`x.toInt/(allOnes w).toInt = - x.toInt`, i.e., the overflow conditions
are the same as `negOverflow` for `x`, and then reason about the signs
of the operands with the respective theorems.
These BitVec theorems themselves rely on numerous `Int.ediv_*` theorems,
that carefully set the bounds of signed division for integers.
co-authored by @bollu, @tobiasgrosser
This PR makes sure that the functional induction priciples for mutually
recursive structural functions with extra parameters are split deeply,
as expected.
