When `discharge?` failed, the `usedSimps` was being restored, but the
cache wasn't. This bug was exposed by issue #3710.
This PR makes the following changes:
- We restore the `cache` at `discharge?`. We use `SMap` to ensure the
operation is efficient.
- We don't need the field `dischargeDepth` anymore at `Simp.Result`.
- `UsedSimps` should use `PHashMap` since it is not used linearly.
closes#3710
---------
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
This makes changes to the `GetElem` class so that it does not lead to
unnecessary overhead in container like `RBMap`.
The changes are to:
1. Make `getElem?` and `getElem!` part of the `GetElem` class so they
can be overridden in instances.
2. Introduce a `LawfulGetElem` class that contains correctness theorems
for `getElem?` and `getElem!` using the original definitions.
3. Reorganize definitions (e.g, by moving `GetElem` out of
`Init.Prelude`) so that the `GetElem` changes are feasible.
4. Provide `LawfulGetElem` instances to complement all existing
`GetElem` instances in Lean core.
To reduce the size of the PR, this doesn't do the work of providing new
`GetElem` instances for `RBMap`, `HashMap` etc. That will be done in a
separate PR (#3688) that depends on this.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
[Before](https://github.com/leanprover/lean4/files/14772220/oi.pdf) and
[after](https://github.com/leanprover/lean4/files/14772226/oi2.pdf).
This gets `ByteArray`, `String.Extra`, `ToString.Macro` and `RCases` out
of the imports of `omega`. I'd hoped to get `Array.Subarray` too, but
it's tangled up in the list literal syntax. Further progress could come
from make `split` use available `Decidable` instances, so we could pull
out `Classical` (and possibly some of `PropLemmas`).
- Removes the public definitions `Array.eraseIdxAux` and
`Array.eraseIdxSzAux` which were implementation details.
- Motivation: `Array.eraseIdxAux` and `Array.eraseIdxSzAux` were clearly
not intended to remain public, but simply making them private would make
it inconvenient to unfold them when writing proofs in Std.
- Adds documentation comments to the public `Array.eraseIdx`-related
definitions which remain.
- Removes `Array.eraseIdx'` which was just `Array.feraseIdx` wrapped in
a subtype and adds `Array.size_feraseIdx` to prove the subtype property
as a standalone theorem.
Co-Authored-By: Daniel Windham <daniel@atlascomputing.org>
