Kim Morrison
0b7debe376
chore: fix List.countP lemmas ( #5311 )
2024-09-11 10:09:37 +00:00
Kim Morrison
f5146c6edb
chore: fix List.all/any lemmas ( #5310 )
2024-09-11 10:02:47 +00:00
Kim Morrison
325a058893
feat: more List.findIdx theorems ( #5300 )
2024-09-11 04:53:59 +00:00
Kim Morrison
7a5a08960a
feat: cleanup of List.findIdx / List.take lemmas ( #5293 )
2024-09-10 06:17:38 +00:00
Kim Morrison
e41e305479
chore: rename Array.data to Array.toList
2024-09-10 15:24:23 +10:00
Kim Morrison
7eedf6467f
feat: List.mem_ite_nil_left and analogues ( #5289 )
2024-09-09 14:08:01 +00:00
Kim Morrison
64b35ba555
chore: use boolean predicates in List.filter ( #5287 )
2024-09-09 12:15:04 +00:00
Kim Morrison
ec7ae59473
feat: List.count lemmas ( #5285 )
2024-09-09 07:04:57 +00:00
Kim Morrison
c96fbdda44
chore: remove @[simp] from List.head_mem and similar ( #5271 )
...
These attributes do not seem particularly useful after all.
2024-09-09 06:05:06 +00:00
Kim Morrison
7432a6f01f
feat: more List.attach lemmas ( #5277 )
2024-09-07 05:29:40 +00:00
Kim Morrison
fcfead8cde
feat: lemmas about List.attach ( #5273 )
...
#5272 should be merged first; this contains some material from that PR.
2024-09-06 22:14:56 +00:00
Kim Morrison
e5eea67020
chore: reverse direction of List.tail_map ( #5275 )
2024-09-06 11:55:50 +00:00
Kim Morrison
76ea33c4c6
chore: review of List API ( #5264 )
2024-09-05 13:08:31 +00:00
Kim Morrison
7c364543a3
chore: review of List API ( #5260 )
2024-09-05 06:27:08 +00:00
Kim Morrison
d08051cf0b
chore: variables appearing on both sides of an iff should be implicit ( #5254 )
2024-09-04 08:33:24 +00:00
Kim Morrison
f1b2850aa4
chore: split Init.Data.Array.Lemmas for better bootstrapping ( #5255 )
...
This allows significantly reducing the imports of `Init.Data.List.Impl`.
2024-09-04 08:33:13 +00:00
Kim Morrison
05fe436bda
chore: don't use simp_arith when simp will do ( #5256 )
2024-09-04 07:56:25 +00:00
Kim Morrison
52bc8dcb40
chore: remove redundant simp annotations ( #5251 )
2024-09-04 04:36:09 +00:00
Kim Morrison
744b68358e
chore: cleanup imports of Array.Lemmas ( #5246 )
2024-09-04 01:48:14 +00:00
Kim Morrison
318e455d96
chore: avoid importing List.Basic without List.Impl ( #5245 )
...
This doesn't completely resolve the danger (only relevant in `prelude`
files) of importing `Init.Data.List.Basic` but not `Init.Data.List.Impl`
and thereby not having `@[csimp]` lemmas installed for some list
operations.
I'm going to address this better while working on `Array`.
2024-09-04 01:25:50 +00:00
Kim Morrison
b053403238
chore: improve naming for List.mergeSort lemmas ( #5242 )
2024-09-03 06:42:33 +00:00
Kim Morrison
a50ed83560
feat: List.erase_range ( #5215 )
2024-08-30 06:46:42 +00:00
Kim Morrison
bb87a3314d
chore: move @[csimp] lemmas earlier where possible ( #5214 )
2024-08-30 06:42:05 +00:00
Kim Morrison
0a0405f4fb
chore: List.getElem_drop, add @[simp] and switch primes ( #5210 )
...
This is a breaking change, as it reverses the meaning of
`List.getElem_drop` and `List.getElem_drop'`.
2024-08-30 02:48:59 +00:00
Kim Morrison
6b62fed82e
feat: proposed change to BitVec API ( #5200 )
...
This renames `BitVec.getLsb` to `getLsbD` (`D` for "default" value, i.e.
false), and introduces `getLsb?` and `getLsb'` (which we can rename to
`getLsb` after a deprecation cycle).
(Similarly for `getMsb`.)
Also adds a `GetElem` class so we can use `x[i]` and `x[i]?` notation.
Later, we will turn
```
theorem getLsbD_eq_getElem?_getD (x : BitVec w) (i : Nat) (h : i < w) :
x.getLsbD i = x[i]?.getD false
```
on as a `@[simp]` lemma.
This PR doesn't attempt to demonstrate the benefits, but I think both
arguments are going to get easier, and this will bring the BitVec API
closer in line to List/Array, etc.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
2024-08-30 02:00:57 +00:00
Kim Morrison
6d0b00885e
feat: List.Pairwise_erase and related lemmas ( #5196 )
2024-08-28 23:11:02 +00:00
Kim Morrison
9ce15fb0c6
chore: remove bad simp lemmas ( #5180 )
...
This disables some simp lemmas with bad discrimination tree keys, as
identified by @mattrobball on
[zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infrastructure.20for.20tracking.20frequently.20applied.20simp.20theorems/near/459926416 ).
2024-08-28 02:55:17 +00:00
Kim Morrison
c4e4248487
chore: remove @[simp] from List.getLast_eq_iff_getLast_eq_some ( #5178 )
...
This was not a great simp lemma, and hurts simp confluence. Better to
just use it locally where it is useful.
Similarly `List.head_eq_iff_head?_eq_some`.
2024-08-27 03:23:39 +00:00
Kim Morrison
b518091bd4
chore: better statement for List.find?_filterMap ( #5177 )
2024-08-27 00:22:59 +00:00
Leonardo de Moura
f917f811c8
chore: cleanup #5167 workarounds after update stage0 ( #5175 )
...
PR #5167 implemented RFC #5046 , but it required several workarounds due
to staging issues. This PR cleans up these workarounds.
2024-08-26 17:53:30 +00:00
Leonardo de Moura
45475d6434
feat: allow users to disable simpCtorEq simproc ( #5167 )
...
`simp only` will not apply this simproc anymore. Users must now write
`simp only [reduceCtorEq]`. See RFC #5046 for motivation.
This PR also renames simproc to `reduceCtorEq`.
close #5046
@semorrison A few `simp only ...` tactics will probably break in
Mathlib. Fix: include `reduceCtorEq`.
2024-08-26 13:51:21 +00:00
Matthew Robert Ballard
b54a9ec9b9
feat: swap arguments to Membership.mem ( #5020 )
...
We swap the arguments for `Membership.mem` so that when proceeded by a
`SetLike` coercion, as is often the case in Mathlib, the resulting
expression is recognized as eta expanded and reduce for many
computations. The most beneficial outcome is that the discrimination
tree keys for instances and simp lemmas concerning subsets become more
robust resulting in more efficient searches.
Closes `RFC` #4932
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
2024-08-26 12:35:47 +00:00
Kim Morrison
f0b0c60e0f
chore: running simpNF linter ( #5168 )
2024-08-26 07:07:52 +00:00
Kim Morrison
9305049f1e
feat: lemmas about List.find? and range'/range/iota ( #5164 )
2024-08-26 04:44:17 +00:00
Kim Morrison
70c1e5690d
feat: more improvements to List simp confluence ( #5163 )
2024-08-26 03:04:58 +00:00
Kim Morrison
7e5d1103c2
feat: more lemmas about List.pmap/attach ( #5160 )
2024-08-26 02:15:58 +00:00
Kim Morrison
2d9cbdb450
feat: more List.findSome? lemmas ( #5161 )
2024-08-26 01:51:40 +00:00
Kim Morrison
fcdecacc4f
feat: head/getLast lemmas for List.range ( #5158 )
2024-08-26 01:48:45 +00:00
Kim Morrison
92b271ee64
feat: lemmas about List.erase(|P|Idx) ( #5152 )
2024-08-25 07:01:46 +00:00
Kim Morrison
cee84286e6
feat: improving confluence of List simp lemmas ( #5151 )
...
More theorems coming shortly that are easier after these changes, but
I'll test Mathlib on these simp changes first.
2024-08-25 04:32:45 +00:00
Kim Morrison
75781b46f5
feat: lemmas about List.attach/pmap ( #5153 )
2024-08-25 03:58:54 +00:00
Kim Morrison
07013da720
chore: running the simpNF linter over Lean ( #5133 )
...
This should resolve nearly all of the simpNF lints. This is a follow-up
to #4620 .
2024-08-24 07:10:07 +00:00
Kim Morrison
bf304769e0
feat: misc List lemma updates ( #5127 )
2024-08-23 01:17:17 +00:00
Kim Morrison
7488b27b0d
feat: lemmas about membership of sublists ( #5132 )
2024-08-23 01:16:53 +00:00
Kim Morrison
b33d08078d
feat: more lemmas about List.append ( #5131 )
2024-08-22 12:42:57 +00:00
Kim Morrison
e9025bdf79
feat: lemmas about List.join ( #5130 )
2024-08-22 12:09:45 +00:00
Kim Morrison
481894e95d
feat: range/iota lemmas ( #5123 )
2024-08-22 06:09:42 +00:00
Kim Morrison
7213583c8d
feat: lemmas about List.find? ( #5124 )
2024-08-22 06:09:42 +00:00
Kim Morrison
a58da122b9
feat: change statement of List.getLast?_cons ( #5106 )
...
To avoid using `getLastD`, which is not simp-normal-form.
2024-08-21 10:59:34 +00:00
Kim Morrison
3b1af163eb
feat: adjust List simp lemmas ( #5102 )
...
I'll do this in a few stages, testing against Mathlib as we go.
2024-08-21 07:25:36 +00:00
