### Preliminary PRs:
- [x] #4597
- [x] #4599
- [x] #4600
- [x] #4602
- [x] #4603
- [x] #4604
- [x] #4605
- [x] #4607
- [x] #4627
- [x] #4629
### Quick overview over API/naming changes compared to `Lean.HashMap`
and `Batteries.HashMap`:
#### Lean
* `find?` -> `get?`/`getElem?`
* `find!` -> `get!`/`gtetElem!`
* `findD` -> `getD`
* `findEntry?` -> not implemented for now
* `insert'` -> `containsThenInsert` (order reversed in result)
* `insertIfNew` -> `getThenInsertIfNew?` (order reversed in result)
* `numBuckets` -> `Internal.numBuckets`
* `ofListWith` -> not implemented for now
* `Array.groupByKey` -> not implemented for now
* `merge` -> not implemented for now, but you can use `insertMany`
#### Batteries
* `modify` -> not implemented for now
* `mergeWith` -> not implemented for now
* `mergeWithM` -> not implemented for now
Split from #4583
There are two open questions, opinions appreciated:
- Should this material be part of `Init` or `Std`?
- Should the typeclasses be in the `Std` namespace?
Split from #4583
`exists_of_set` appears in Batteries as `exists_of_set'`. The
`exists_of_set` version is unused in batteries and mathlib at least and
I would argue that the primed version (i.e., the one added in this PR)
is always better anyway.
`isEmpty_iff` appears in mathlib as `isEmpty_iff_eq_nil`.
This implements the recurrence theorems `getLsb_mul`, `mulRec_zero_eq`,
`mulRec_succ_eq` to allow bitblasting multiplication.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
This example, reported from LNSym, started failing when we changed the
definition of `Fin.sub` in
https://github.com/leanprover/lean4/pull/4421.
When we use the new definition, `omega` produces a proof term that the
kernel is very slow on.
To work around this for now, I've removed `BitVec.toNat_sub` from the
`bv_toNat` simp set,
and replaced it with `BitVec.toNat_sub'` which uses the old definition
for subtraction.
This is only a workaround, and I would like to understand why the term
chokes the kernel.
```
example
(n : Nat)
(addr2 addr1 : BitVec 64)
(h0 : n ≤ 18446744073709551616)
(h1 : addr2 + 18446744073709551615#64 - addr1 ≤ BitVec.ofNat 64 (n - 1))
(h2 : addr2 - addr1 ≤ addr2 + 18446744073709551615#64 - addr1) :
n = 18446744073709551616 := by
bv_omega
```
We add a new definition `BitVec.twoPow w i` to represent `(1#w <<< i)`.
This expression is used to test bits when building the multiplication
bitblaster.
Patch 1/?, being peeled from https://github.com/opencompl/lean4/pull/6.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
This PR introduces complete simprocs for all the Int versions of
div/mod, and makes some small refactoring of Int lemmas and
library_search.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
The linters in Batteries can be used to spot mistakes in Lean. See the
message on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Go-to-def.20on.20typeclass.20fields.20and.20type-dependent.20notation/near/442613564).
These are the different linters with errors:
- unusedArguments:
There are many unused instance arguments, especially a redundant `[Monad
m]` is very common
- checkUnivs:
There was a problem with universes in a definition in
`Init.Control.StateCps`. I fixed it by adding a `variable` statement for
the implicit arguments in the file.
- defLemma:
many proofs are written as `def` instead of `theorem`, most notably
`rfl`. Because `rfl` is used as a match pattern, it must be a def. Is
this desirable?
The keyword `abbrev` is sometimes used for an alias of a theorem, which
also results in a def. I would want to replace it with the `alias`
keyword to fix this, but it isn't available.
- dupNamespace:
I fixed some of these, but left `Tactic.Tactic` and `Parser.Parser` as
they are as these seem intended.
- unusedHaveSuffices:
I cleaned up a few proofs with unused `have` or `suffices`
- explicitVarsOfIff:
I didn't fix any of these, because that would be a breaking change.
- simpNF:
I didn't fix any of these, because I think that requires knowing the
intended simplification order.
Continuation of #3958. To ensure that lean code is able to uphold the
invariant that `String`s are valid UTF-8 (which is assumed by the lean
model), we have to make sure that no lean objects are created with
invalid UTF-8. #3958 covers the case of lean code creating strings via
`fromUTF8Unchecked`, but there are still many cases where C++ code
constructs strings from a `const char *` or `std::string` with unclear
UTF-8 status.
To address this and minimize accidental missed validation, the
`(lean_)mk_string` function is modified to validate UTF-8. The original
function is renamed to `mk_string_unchecked`, with several other
variants depending on whether we know the string is UTF-8 or ASCII and
whether we have the length and/or utf8 char count on hand. I reviewed
every function which leads to `mk_string` or its variants in the C code,
and used the appropriate validation function, defaulting to `mk_string`
if the provenance is unclear.
This PR adds no new error handling paths, meaning that incorrect UTF-8
will still produce incorrect results in e.g. IO functions, they are just
not causing unsound behavior anymore. A subsequent PR will handle adding
better error reporting for bad UTF-8.
This is not the most exciting place to start, but I started here to:
* pick a function with little development in Batteries and Mathlib, so I
wouldn't have conflicts
* that is easy!
* to see how much effort it is to get fairly complete coverage
* and to set up some infrastructure to be used later, i.e.
`tests/lean/run/list_simp.lean`
`Nat.succ_eq_add_one` and `Nat.pred_eq_sub_one` are now simp lemmas. For
theorems about `Nat.succ` or `Nat.pred` without corresponding theorem
for `+ 1` or `- 1`, this adds the corresponding theorem.
This PR neither adds nor removes material, but improves the organization
of `Init/Data/List/*`.
These files are essentially completely re-ordered, to ensure that
material is developed in a consistent order between `List.Basic`,
`List.Impl`, `List.BasicAux`, and `List.Lemmas`.
Everything is organised in subsections, and I've added some module docs.
We recently discovered inconsistencies in Mathlib and Std over the
ordering of the arguments for `==`.
The most common usage puts the "more variable" term on the LHS, and the
"more constant" term on the RHS, however there are plenty of exceptions,
and they cause unnecessary pain when switching (particularly, sometimes
requiring otherwise unneeded `LawfulBEq` hypotheses).
This convention is consistent with the (obvious) preference for `x == 0`
over `0 == x` when one term is a literal.
We recently updated Std to use this convention
https://github.com/leanprover/std4/pull/430
This PR changes the two major places in Lean that use the opposite
convention, and adds a suggestion to the docstring for `BEq` about the
preferred convention.
The performance issue at #4413 is due to our `Fin.sub` definition.
```
def sub : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩
```
Thus, the following runs out of stack space
```
example (a : UInt64) : a - 1 = a :=
rfl
```
at the `isDefEq` test
```
(a.val.val + 18446744073709551615) % 18446744073709551616 =?= a.val.val
```
From the user's perspective, this timeout is unexpected since they are
using small numerals, and none of the other `Fin` basic operations (such
as `Fin.add` and `Fin.mul`) suffer from this problem.
This PR implements an inelegant solution for the performance issue. It
redefines `Fin.sub` as
```
def sub : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, mlt h⟩
```
This approach is unattractive because it relies on the fact that
`Nat.add` is defined using recursion on the second argument.
The impact on this repo was small, but we want to evaluate the impact on
Mathlib.
closes#4413
It seems:
* there was no actual need for the UInt32 valued version
* downstream we were getting duplicative lemmas about both
* so lets reduce the API surface area!
If anyone would prefer the remaining function is still called
`Char.utf8Size` I will happily change it. (`size` is hopefully still
unambiguous, and it's helpful to rename here so we can give a
deprecation warning that explains the type signature change.)
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
The type uses `PUnit`, but the `pure ()` in the body was forcing the
implicit universe level at `PUnit` to be `1`.
We should probably elaborate `def`s like we elaborate theorems when the
resulting type is provided. This kind of mistake is hard to spot.
