This PR adds a logic of stateful predicates SPred to Std.Do in order to
support reasoning about monadic programs. It comes with a dedicated
proof mode the tactics of which are accessible by importing
Std.Tactic.Do.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR introduces ranges that are polymorphic, in contrast to the
existing `Std.Range` which only supports natural numbers.
Breakdown of core changes:
* `Lean.Parser.Basic`: Modified the number parser (`Lean.Parser.Basic`)
so that it will only consider a *single* dot to be part of a decimal
number. `1..` will no longer be parsed as `1.` followed by `.`, but as
`1` followed by `..`.
* The test `ellipsisProjIssue` ensures that `#check Nat.add ...succ`
produces a syntax error. After introducing the new range notation (see
below), it returns a different (less nice) error message. I updated the
test to reflect the new error message. (The error message will become
nicer as soon as a delaborator for the ranges is implemented. This is
out of scope for this PR.)
Breakdown of standard library changes:
Modified modules: `Init.Data.Range.Polymorphic` (added),
`Init.Data.Iterators`, `Std.Data.Iterators`
* Introduced the type `Std.PRange` that is parameterized over the type
in which the range operates and the shapes of the lower and upper bound.
* Introduced a new notation for ranges. Examples for this notation are:
`1...*`, `1...=3`, `1...<3`, `1<...=2`, `*...=3`.
* Defined lots of typeclasses for different capabilities of ranges,
depending on their shape and underlying type.
* Introduced `Iter(M).size`.
* Introduced the `Iter(M).stepSize n` combinator, which iterates over an
iterator with the given step size `n`. It will drop `n - 1` values
between every value it emits.
* Replaced `LawfulPureIterator` with a new and better typeclass
`LawfulDeterministicIterator`.
* Simplified some lemma statements in the iterator library such as
`IterM.toList_eq_match`, which unnecessarily matched over a `Subtype`,
hindering rewrites due to type dependencies.
Reasons for the concrete choice of notation:
* `lean4-cli` uses `...`-based notation for the `Cmd` notation and it
clashes with `...a` range notation.
* test `2461` fails when using two-dot-based notation because of the
existing `{ a.. }` notation.
This PR adds a generic `MonadLiftT Id m` instance. We do not implement a
`MonadLift Id m` instance because it would slow down instance resolution
and because it would create more non-canonical instances. This change
makes it possible to iterate over a pure iterator, such as `[1, 2,
3].iter`, in arbitrary monads.
This PR adds a new monadic interface for `Async` operations.
This is the design for the `Async` monad that I liked the most. The idea
was refined with the help of @tydeu. Before that, I had some
prerequisites in mind:
1. Good performance
2. Explicit `yield` points, so we could avoid using `bindTask` for every
lifted IO operation
3. A way to avoid creating an infinite chain of `Task`s during recursion
The 2 and 3 points are not covered in this PR, I wish I had a good
solution but right now only a few sketches of this.
### Explicit `yield` points
I thought this would be easy at first, but it actually turned out kinda
tricky. I ended up creating the `suspend` syntax, which is just a small
modification of the lift method (`<- ...`) syntax. It desugars to
`Suspend.suspend task fun _ => ...`. So something like:
```lean
do
IO.println "a"
IO.println "b"
let result := suspend (client.recv? 1024)
IO.println "c"
IO.println "d"
```
Would become:
```lean
Bind.bind (IO.println "a") fun _ =>
Bind.bind (IO.println "b") fun _ =>
Suspend.suspend (client.recv? 1024) fun message =>
Bind.bind (IO.println "c") fun _ =>
IO.println "d"
```
This makes things a bit more efficient. When using `bind`, we would try
to avoid creating a `Task` chain, and the `suspend` would be the only
place we use `Task.bind`. But there's a problem if we use `bind` with
something that needs `suspend`, it’ll block the whole task. Blocking is
the only way to prevent task accumulation when using plain `bind` inside
a structure like that:
```
inductive AsyncResult (ε σ α : Type u) where
| ok : α → σ → AsyncResult ε σ α
| error : ε → σ → AsyncResult ε σ α
| ofTask : Task (EStateM.Result ε σ α) → σ →AsyncResult ε σ α
```
Because we simply need to remove the `ofTask` and transform it into an
`ok`.
### Infinite chain of Tasks
If you create an infinite recursive function using `Task` (which is
super common in servers like HTTP ones), it can lead to a lot of memory
usage. Because those tasks get chained forever and won't be freed until
the function returns.
To get around that, I used CPS and instead of just calling `Task.bind`,
I’d spawn a new task and return an "empty" one like:
```lean
fun k => Task.bind (...) fun value => do k value; pure emptyTask
```
This works great with a CPS-style monad, but it generates a huge IR by
itself.
Just doing CPS alone was too much, though, because every lifted
operation created a new continuation and a `Task.bind`. So, I used it
with `suspend` and got a better performance, but the usage is not good
with `suspend`.
### The current monad
Right now, the monad I’m using is super simple. It doesn't solve the
earlier problems, but the API is clean, and the generated IR is small
enough. An example of how we should use it is:
```lean
-- A loop that repeatedly sends a message and waits for a reply.
partial def writeLoop (client : Socket.Client) (message : String) : Async (AsyncTask Unit) := async do
IO.println s!"sending: {message}"
await (← client.send (String.toUTF8 message))
if let some mes ← await (← client.recv? 1024) then
IO.println s!"received: {String.fromUTF8! mes}"
-- use parallel to avoid building up an infinite task chain
parallel (writeLoop client message)
else
IO.println "client disconnected from receiving"
-- Server’s main accept loop, keeps accepting and echoing for new clients.
partial def acceptLoop (server : Socket.Server) (promise : IO.Promise Unit) : Async (AsyncTask Unit) := async do
let client ← await (← server.accept)
await (← client.send (String.toUTF8 "tutturu "))
-- allow multiple clients to connect at the same time
parallel (writeLoop client "hi!!")
-- and keep accepting more clients, parallel again to avoid building up an infinite task chain
parallel (acceptLoop server promise)
-- A simple client that connects and sends a message.
def echoClient (addr : SocketAddress) (message : String) : Async (AsyncTask Unit) := async do
let socket ← Client.mk
await (← socket.connect addr)
parallel (writeLoop socket message)
-- TCP setup: bind, listen, serve, and run a sample client.
partial def mainTCP : Async Unit := do
let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) 8080
let server ← Server.mk
server.bind addr
server.listen 128
-- promise exists since the server is (probably) never going to stop
let promise ← IO.Promise.new
let acceptAction ← acceptLoop server promise
await (← echoClient addr "hi!")
await acceptAction
await promise
-- Entry point
def main : IO Unit := mainTCP.wait
```
---------
Co-authored-by: Henrik Böving <hargonix@gmail.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
This PR adjusts the `lean.redundantMatchAlt` error explanation to remove
the word "unprefixed," which the reference manual's style linter does
not recognize.
This PR refactors the juggling of universes in the linear
`noConfusionType` construction: Instead of using `PUnit.{…} → ` in the
to get the branches of `withCtorType` to the same universe level, we use
`PULift`.
This fixes https://github.com/leanprover/lean4/issues/8962, although
probably doesn’t solve all issues of that kind while level equality
checking is incomplete.
This PR updates the `solveMonoStep` function used in the `monotonicity`
tactic to check for definitional equality between the current goal and
the monotonicity proof obtained from a recursive call. This ensures
soundness by preventing incorrect applications when
`Lean.Order.PartialOrder` instances differ—an issue that can arise with
`mutual` blocks defined using the `partial_fixpoint` keyword, where
different `Lean.Order.CCPO` structures may be involved.
Closes https://github.com/leanprover/lean4/issues/8894.
This PR adds some missing `ToInt.X` typeclass instances for `grind`.
There are still several more to add (in particular, for `ToInt.Pow`),
but I am going to perform an intermediate refactor first.
This PR removes Lake's usage of `lean -R` and `moduleNameOfFileName` to
pass module names to Lean. For workspace names, it now relies on
directly passing the module name through `lean --setup`. For
non-workspace modules passed to `lake lean` or `lake setup-file`, it
uses a fixed module name of `_unknown`.
This means that `lake lean` and `lake setup-file` can be successfully
and consistently used on modules that do not lie under the working
directory or the workspace root.
This PR passes Lean options configured via CMake variables onto the Lake
build. For example, this will ensure CI' setting of `warningAsError` via
`LEAN_EXTRA_MAKE_OPTS` reaches Lake.
This PR both adds initial `@[grind]` annotations for `BitVec`, and uses
`grind` to remove many proofs from `BitVec/Lemmas`.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR adds `BitVec.(getElem, getLsbD, getMsbD)_(smod, sdiv, srem)`
theorems to complete the API for `sdiv`, `srem`, `smod`. Even though the
rhs is not particularly succint (it's hard to find a meaning for what it
means to have "the n-th bit of the result of a signed division/modulo
operation"), these lemmas prevent the need to `unfold` of operations.
---------
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
This PR embeds a NatModule into its IntModule completion, which is
injective when we have AddLeftCancel, and monotone when the modules are
ordered. Also adds some (failing) grind test cases that can be verified
once `grind` uses this embedding.
This PR changes the CI setup to generate `lean-pr-testing-NNNN` branches
for Mathlib on the `leanprover-community/mathlib4-nightly-testing` fork,
rather than on the main repo.
This PR add instances showing that the Grothendieck (i.e. additive)
envelope of a semiring is an ordered ring if the original semiring is
ordered (and satisfies ExistsAddOfLE), and in this case the embedding is
monotone.
This PR improves the case splitting strategy used in `grind`, and
ensures `grind` also considers simple `match`-conditions for
case-splitting. Example:
```lean
example (x y : Nat)
: 0 < match x, y with
| 0, 0 => 1
| _, _ => x + y := by -- x or y must be greater than 0
grind
```
This PR adds configuration options to the `let`/`have` tactic syntaxes.
For example, `let (eq := h) x := v` adds `h : x = v` to the local
context. The configuration options are the same as those for the
`let`/`have` term syntaxes.
This PR changes `toLCNF` to stop caching translations of expressions
upon seeing an expression marked `never_extract`. This is more
coarse-grained than it needs to be, but it is difficult to do any
better, as the new compiler's `Expr` cache is based on structural
identity (rather than the pointer identity of the old compiler).
The newly added `tests/compiler/never_extract.lean` is also converted
into a `run` tests, because during development I found the order of the
output to `stderr` to be a bit finicky. The reason for making it a
`compiler` test in the first place is that closed term decls work
slightly differently between native code and the interpreter, and it
would be good to test both, but we already have separate tests for
`never_extract` and closed term extraction.
Fixes#8944.
This PR adds a procedure that efficiently transforms `let` expressions
into `have` expressions (`Meta.letToHave`). This is exposed as the
`let_to_have` tactic.
It uses the `withTrackingZetaDelta` technique: the expression is
typechecked, and any `let` variables that don't enter the zeta delta set
are nondependent. The procedure uses a number of heuristics to limit the
amount of typechecking performed. For example, it is ok to skip
subexpressions that do not contain fvars, mvars, or `let`s.
This PR implements support for normalization for commutative semirings
that do not implement `AddRightCancel`. Examples:
```lean
variable (R : Type u) [CommSemiring R]
example (a b c : R) : a * (b + c) = a * c + b * a := by grind
example (a b : R) : (a + b)^2 = a^2 + 2 * a * b + b^2 := by grind
example (a b : R) : (a + 2 * b)^2 = a^2 + 4 * a * b + 4 * b^2 := by grind
example (a b : R) : (a + 2 * b)^2 = 4 * b^2 + b * 4 * a + a^2 := by grind
```
