I'll update `list_simp.lean` (simp normal form testing) and add missing
lemmas in follow-up PRs.
This just upstreams the material, and reorders the lemmas to match the
other sections.
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`
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.
Previously the `ac_rfl` tactic was only really usable when depending on
mathlib. With these instances, `ac_rfl` can deal with the various
operations defined in Lean.
---------
Co-authored-by: Scott Morrison <scott.morrison@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>
This will collect definitions from Std.Logic
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
The example was looping with the new `simp` reduction strategy. Here
is the looping trace.
```
List.reverseAux (List.reverseAux as []) bs
==> rewrite using reverseAux_reverseAux
List.reverseAux [] (List.reverseAux (List.reverseAux as []) bs)
==> unfold reverseAux
List.reverseAux (List.reverseAux as []) bs
==> rewrite using reverseAux_reverseAux
List.reverseAux [] (List.reverseAux (List.reverseAux as []) bs)
==> ...
```
Changes the implementation of `List.all` and `List.any` so they
short-circuit. The implementations are tail-recursive.
This replaces https://github.com/leanprover/std4/pull/392, which was
going to do this with `@[csimp]`.
