This PR adds union operations on DTreeMap/TreeMap/TreeSet and their raw
variants and provides lemmas about union operations.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR enables Lake users to require Reservoir dependencies by a
semantic version range. On a `lake update`, Lake will fetch the
package's version information from Reservoir and select the newest
version of the package that satisfies the range.
### Using Version Ranges
Version ranges can be specified through the `version` field of a TOML
`require` or the `@` clause of a Lean `require`. They are only
meaningful on Reservoir dependencies.
**lakefile.lean**
```lean-4
require "Seasawher" / "mdgen" @ "2.*"
```
**lakefile.toml**
```toml
[[require]]
name = "mdgen"
scope = "Seasawher"
version = "2.*"
```
The syntax for these versions ranges is a mix of
[Rust's](https://doc.rust-lang.org/stable/cargo/reference/specifying-dependencies.html?highlight=caret#version-requirement-syntax)
and
[Node's](https://github.com/npm/node-semver/tree/v7.7.3?tab=readme-ov-file#ranges)
with some Lean-friendly deviations.
### Comparators
The basic unit of semantic version ranges are version comparators. They
take a base version and a comparison operator and match versions which
compare positively with their base. Lake supports the following
comparison operators.
* `<`, `<=` / `≤`, `>`, `>=` / `≥`, `=`, `!=` / `≠`
Unlike Rust and Node, Lake supports Unicode alternatives for the
operators. It also adds the not-equal operator (`!=` / `≠`) to make
excluding broken versions easier.
Comparators can be combined into clauses via conjunction or disjunction:
* **AND clauses**: Rust-style `≥1.2.3, <1.8.0` or Node-style `1.2.3
<1.8.0`
* **OR clauses**: Node-style `1.2.7 || >=1.2.9, <2.0.0`
When the base version of a comparator has a `-` suffix (e.g.,
`>1.2.3-alpha.3`) it will match versions of the same core (`1.2.3`) with
suffixes that lexicographically compare (e.g., `1.2.3-alpha.7` or
`1.2.3-beta.2`) but will not match suffixed versions of different cores
(e.g., `3.4.5-rc5`). An empty `-` suffix can be used to disable this
behavior. For example, `<2.0.0-` will match `1.2.3-beta.2` and
`2.0.0-alpha.1`.
### Range Macros
In addition to the basic comparators, Lake also supports standard
shorthand for specifying more complex ranges. Namely, it supports the
caret (`^`) and tilde (`~`) operator along with wildcard ranges.
**Caret Ranges**
* `^1` => `≥1.0.0, <2.0.0-`
* `^1.2` => `≥1.2.0, <2.0.0-`
* `^1.2.3` => `≥1.2.3, <2.0.0-`
* `^1.2.3-beta.2` => `≥1.2.3-beta.2, <2.0.0-`
* `^0.2` => `≥0.0.0, <0.3.0-`
* `^0.2.3` => `≥0.2.3, <0.3.0-`
* `^0.0.3` => `≥0.0.3, <0.0.4-`
* `^0` => `≥0.0.0, <1.0.0-`
* `^0.0` => `≥0.0.0, <0.1.0-`
**Tilde Ranges**
* `~1` => `≥1.0.0, <2.0.0-`
* `~1.2` => `≥1.2.0, <1.3.0-`
* `~1.2.3` => `≥1.2.3, <1.3.0-`
* `~1.2.3-beta.2` => `≥1.2.3-beta.2, <1.3.0-`
* `^0` => `≥0.0.0, <1.0.0-`
* `^0.2.3` => `≥0.2.3, <0.3.0-`
* `^0.0.3` => `≥0.0.3, <0.0.4-`
* `~0` => `≥0.0.0, <1.0.0-`
* `~0.0` => `≥0.0.0, <0.1.0-`
* `~0.0.0` => `≥0.0.0, <0.1.0-`
**Wildcard Ranges**
* `*` => `≥0.0.0`
* `1.x` => `≥1.0.0, <2.0.0-`
* `1.*.x` => `≥1.0.0, <2.0.0-`
* `1.2.*` => `≥1.2.0, <1.3.0-`
These ranges closely follow Rust's and Node's syntax. Like Node but
unlike Rust, wildcard ranges support `x` and `X` as alternative syntax
for wildcards.
This PR implements `simp? +suggestions`, which uses the configured
library suggestion engine to add relevant theorems to the `simp` call.
`simp +suggestions` without the `?` prints a message requiring adding
the `?`.
This PR changes Lake's debug build type to use `-O0` instead of `-Og`
when compiling C code. `-Og` was found to be insufficient for debugging
compiled Lean code -- relevant code was stilled optimized out.
This PR changes `Nat.ble` by joining the two `Nat.ble Nat.zero _` cases
into one, allowing `decide (0 <= x) = true` and `decide (0 < succ x) =
true` to be solvable by `rfl`.
This PR fixes `ST.Ref.ptrEq` to act as described in the docs. This fixes
two bugs:
1. The recent `IO.RealWorld` elimination PR overlooked this function
(afaik this is the only one),
causing its return value to be generally wrong.
2. The implementation of `ptrEq` would previously always consider two
different cells with pointer
equivalent value to be pointer equal. However, the function is supposed
to check whether two
`Ref` are the same cell, not whether the contained elements are.
This PR implements equality propagation for `Nat` in `grind order`.
`grind order` supports offset equalities for rings, but it has an
adapter for `Nat`. Example:
```lean
example (a b : Nat) (f : Nat → Int) : a ≤ b + 1 → b + 1 ≤ a → f (1 + a) = f (1 + b + 1) := by
grind -offset -mbtc -lia -linarith (splits := 0)
```
This PR implements (nested term) equality propagation in `grind order`.
That is, it propagates implied equalities from `grind order` back to the
`grind` core. Examples:
```lean
open Lean Grind Std
example [LE α] [IsPartialOrder α] (a b : α) (f : α → Nat) : a ≤ b → b ≤ c → c ≤ a → f a = f b := by
grind (splits := 0)
example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrder α] [OrderedRing α]
(a b : α) (f : α → Int) : a ≤ b + 1 → b ≤ a - 1 → f a = f (2 + b - 1) := by
grind -mbtc -lia -linarith (splits := 0)
example (a b : Int) (f : Int → Int) : a ≤ b + 1 → b ≤ a - 1 → f a = f (2 + b - 1) := by
grind -mbtc -lia -linarith (splits := 0)
```
`prelude-injectivity.lean` was testing inj thm generation for all
inductives in core, including private ones, which could lead to name
clashes that should not be able to occur in actual files. Put it under
the module system to not load private decls in the first place.
This PR enforces users of the constant folder API to provide proofs of
their algebraic properties,
thus hopefully avoiding bugs such as #11042 and #11043 in the future.
This PR fixes a case of overeager constant folding on Nat where the
compiler would mistakenly assume `0 - x = x` (see also #11042 for the
same bug on UInts).
This PR adds a new suggestion to `finish?`. It now generates the `grind`
tactic script as before, and a `finish only` tactic. Example:
```lean
/--
info: Try these:
[apply] ⏎
instantiate only [findIdx, insert, = mem_indices_of_mem]
instantiate only [= getElem?_neg, = getElem?_pos]
cases #1bba
· instantiate only [findIdx]
· instantiate only
instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
[apply] finish only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
= HashMap.getElem_insert, #1bba]
-/
example (m : IndexMap α β) (a : α) (b : β) :
(m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
grind => finish?
```
This PR establishes `String.ofList` and `String.toList` as the preferred
method for converting between strings and lists of characters and
deprecates the alternatives `String.mk`, `List.asString` and
`String.data`.
This PR adds a library suggestion engine for local theorems. To be
useful, I still need to write more combinators to re-rank and combine
suggestions from multiple engines.
This is stacked on top of #11029.
This PR changes the terminology used from "premise selection" to
"library suggestions". This will be more understandable to users (we
don't assume anyone is familiar with the premise selection literature),
and avoids a conflict with the existing use of "premise" in Lean
terminology (e.g. "major premise" in induction, as well as generally the
synonym for "hypothesis"/"argument").
This PR improves match compilation: Branch on variables in the order
suggested by the first remaining alternative, and do not branch when the
first remaining alternative does not require it. This fixes
https://github.com/leanprover/lean4/issues/10749. With `set_option
backwards.match.rowMajor false` the old behavior can be turned on.
(For now this is an experiment to get familiar with the code and the
whole
problem domain. It is likely overly naive.)
This PR renames theorems that use `sorted` in their name to instead use
`pairwise`.
Closes#10742.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR improves the detection of situations where we branch multiple
times on the same value in the
code generator. Previously this would only consider repeated branching
on function arguments, now on
arbitrary values.
Closes: #11018
When documenting smul : M → α → α, it is unintuitive and confusing to
use variables a:M and b:α. It is better to use m:M and a:α. I also
specified the types of all involved terms in the documentation text.
This PR improves join point finding in the compiler through two means:
1. We now handle situations where a function `f` can only become a join
point when a function `g`
becomes a join point as well correctly.
2. We introduce a second join point finding pass after specialisation
and before the following
simplification pass, as the specialiser might have introduced new join
point opportunities for
the simplifier to exploit.
Notably in the code from #10995 we now correctly detect the missing join
point which required both
of these changes to be made.
Closes: #10995
This PR extracts some refactorings from #10763, including dropping dead
code and not failing in `inaccessibleAsCtor`, which leadas to (slightly)
better error messages, and also on the grounds that the failing
alternative may actually be unreachable.
This PR makes the eager lambda lifting heuristic more predictable by
blocking it from lifting from
any kind of inlineable function, not just `@[inline]`. It also adapts
the doc-string to describe
what is actually going on.
This PR inlines several Decidable instances for performance reasons.
Unlike the previous #10934 it does not attempt to also simplify the
Decidable instance system as
that has proven to have non trivial performance impact.
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR fixes a memleak caused by the Lean based `IO.waitAny`
implementation by reverting it.
This the faulty Lean implementation:
```lean
def IO.waitAny (tasks : @& List (Task α)) (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) :
BaseIO α := do
have : Nonempty α := ⟨tasks[0].get⟩
let promise : IO.Promise α ← IO.Promise.new
tasks.forM <| fun t => BaseIO.chainTask (sync := true) t promise.resolve
return promise.result!.get
```
In a situation where we call this function repeatedly in a loop with a
pair of tasks `[t1, t2]`
where `t2` is a long lived task that we pass every time and `t1` is
fresh a short lived task, `t2` will
accumlate more and more children from `BaseIO.chainTask` that fill
memory over time. The old C++
implementation did not have this issue so we are reverting.
This PR defines `String.Slice.replace` and redefines `String.replace` to
use the `Slice` version.
The new implementation is generic in the pattern, so it supports things
like `"education".replace isVowel "☃!" = "☃!d☃!c☃!t☃!☃!n"`. Since it
uses the `ForwardSearcher` infrastructure, `String` patterns are
searched using KMP, unlike the previous implementation which had
quadratic runtime. As a side effect, the behavior when replacing an
empty string now matches that of most other programming languages,
namely `"abc".replace "" "k" = "kakbkck"`.
This PR fixes the KMP implementation, which did incorrect bookkeeping of
the backtracking process, leading to incorrect starting ranges of
matches.
The new implementation does not require `partial` anywhere.
