Kim Morrison
ebc02fc6e8
feat: lemmas relating Array.findX and List.findX ( #5985 )
...
This PR relates the operations `findSomeM?`, `findM?`, `findSome?`, and
`find?` on `Array` with the corresponding operations on `List`, and also
provides simp lemmas for the `Array` operations `findSomeRevM?`,
`findRevM?`, `findSomeRev?`, `findRev?` (in terms of `reverse` and the
usual forward find operations).
2024-11-07 03:30:11 +00:00
Kim Morrison
05caf1bda9
feat: interactions between List.foldX and List.filterX ( #5984 )
...
This PR adds lemmas for `List` for the interactions between {`foldl`,
`foldr`, `foldlM`, `foldlrM`} and {`filter`, `filterMap`}.
2024-11-07 02:37:20 +00:00
Kim Morrison
b1dee4a42e
chore: upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas ( #5969 )
...
To follow, connecting this to `Array.insertAt` (and renaming).
2024-11-06 23:29:27 +00:00
Kim Morrison
a54226196d
feat: minor lemmas about List.ofFn ( #5982 )
...
`List.ofFn` still has very incomplete API.
2024-11-06 23:05:42 +00:00
Henrik Böving
196b1e9250
feat: BitVec.twoPow in bv_decide ( #5979 )
2024-11-06 17:51:44 +00:00
Kim Morrison
1e98fd7f2d
feat: add another List.find?_eq_some lemma ( #5974 )
...
Inspired by https://github.com/leanprover-community/mathlib4/pull/18593
2024-11-06 10:02:25 +00:00
Kim Morrison
15139b6ef6
feat: relate Array.zipWith/zip/unzip with List versions ( #5972 )
2024-11-06 09:22:08 +00:00
Kim Morrison
910b20fb2c
chore: consolidate decide_True and decide_true_eq_true ( #5949 )
2024-11-06 05:12:25 +00:00
Kim Morrison
4df71ed24f
feat: relate Array.isPrefixOf with List.isPrefixOf ( #5971 )
2024-11-06 02:44:14 +00:00
Kim Morrison
5d2bd1e2e4
chore: deprecate Array.split in favour of identical Array.partition ( #5970 )
2024-11-06 00:37:33 +00:00
Henrik Böving
c77b6a2c64
feat: define ISize and basic operations on it ( #5961 )
2024-11-05 15:08:19 +00:00
Kim Morrison
128b049904
feat: relate Array.eraseIdx with List.eraseIdx ( #5952 )
2024-11-05 06:13:29 +00:00
Kim Morrison
0e3f26e6df
feat: relate Array.takeWhile with List.takeWhile ( #5950 )
2024-11-05 05:05:53 +00:00
Kim Morrison
1148e6e142
chore: remove @[simp] from BitVec.ofFin_sub and sub_ofFin ( #5951 )
...
Unused, and hurts confluence.
2024-11-05 04:56:21 +00:00
Violeta Hernández
02baaa42ff
feat: add Option.or_some' ( #5926 )
...
`o.or (some a) = o.getD a`.
As discussed on
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/a.2Eor.20.28some.20b.29.20.3D.20a.2EgetD.20b/near/472785093 ).
2024-11-05 01:39:02 +00:00
Violeta Hernández
e573676db1
feat: List.pmap_eq_self ( #5927 )
...
This is a `pmap` analog of
[`List.map_id''`](https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/Lemmas.html#List.map_id '').
As discussed on
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.60pmap_eq_self.60/near/472496933 ).
2024-11-05 01:38:13 +00:00
Henrik Böving
93dd6f2b36
feat: add Int16/Int32/Int64 ( #5885 )
...
This adds all fixed width integers with the exception of `ssize_t` so
the code is quick to review as everything just behaves the same.
2024-11-04 13:18:05 +00:00
Kim Morrison
c779f3a039
feat: List.mapFinIdx, lemmas, relate to Array version ( #5941 )
2024-11-04 05:29:41 +00:00
Kim Morrison
fc17468f78
chore: upstream List.ofFn and relate to Array.ofFn ( #5938 )
2024-11-04 01:35:29 +00:00
Kim Morrison
8b7e3b8942
chore: upstream lemmas about Fin.foldX ( #5937 )
2024-11-04 00:52:59 +00:00
Kyle Miller
b75cc35db2
feat: update omega/solve_by_elim to use new tactic syntax, use new tactic syntax ( #5932 )
...
Following up #5928 , updates the syntax for `omega` and `solve_by_elim`
and restores the syntax quotations in their implementations.
Following up #5898 , uses the new tactic syntax in the library, replacing
all uses of `(config := ...)`.
2024-11-03 16:23:37 +00:00
Kim Morrison
a75a03c077
feat: relate for loops over List with foldlM ( #5913 )
...
There are many more lemmas about `foldlM`, so this may be useful for
reasoning about for loops by transforming them into folds.
The transformation includes accounting for monad effects, but does have
a mild performance difference in that short-circuiting on
`ForInStep.done` is replaced by traversing the rest of the list with a
noop.
2024-11-01 02:41:05 +00:00
Kim Morrison
6922832327
chore: minor tweaks to Array lemmas ( #5912 )
2024-11-01 02:20:16 +00:00
Luisa Cicolini
7730ddd1a0
feat: add BitVec.(msb, getMsbD, getLsbD)_(neg, abs) ( #5721 )
...
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: FR <zhao.yu-yang@foxmail.com>
Co-authored-by: Aaron Tomb <aarontomb@gmail.com>
Co-authored-by: Arthur Adjedj <arthur.adjedj@gmail.com>
Co-authored-by: Yann Herklotz <git@yannherklotz.com>
Co-authored-by: Lean stage0 autoupdater <>
2024-11-01 01:27:34 +00:00
Kim Morrison
c2391c45b9
chore: remove @[simp] from Sum.forall and Sum.exists ( #5900 )
2024-11-01 01:21:04 +00:00
Henrik Böving
844e7ae7eb
chore: remove native code for UInt8.modn ( #5901 )
...
Closes #5818
2024-10-31 12:42:24 +00:00
Kim Morrison
218601009b
chore: rename Array.back to back! ( #5897 )
2024-10-31 09:18:18 +00:00
Kim Morrison
4af93813f2
chore: move @[simp] from back_eq_back? to back_push ( #5896 )
2024-10-31 08:25:19 +00:00
Kim Morrison
34be25620f
feat: LawfulBEq (Array α) ↔ LawfulBEq α ( #5895 )
2024-10-31 08:00:06 +00:00
Kim Morrison
a826de8a3d
chore: remove duplicated ForIn instances ( #5892 )
...
I'd previously added an instance from `ForIn'` to `ForIn`, but this then
caused some non-defeq duplication. It seems fine to just remove the
concrete `ForIn` instances in cases where the `ForIn'` instance exists
too. We can even remove a number of type-specific lemmas in favour of
the general ones.
2024-10-31 07:40:09 +00:00
Kim Morrison
38c39482f4
chore: add missing deprecation dates ( #5884 )
2024-10-30 05:37:36 +00:00
Alex Keizer
b5bbc57059
feat: prove that intMin is indeed the smallest signed bitvector ( #5778 )
2024-10-30 02:45:16 +00:00
Kim Morrison
5e7d02e4ea
feat: Hashable (BitVec n) ( #5881 )
2024-10-30 02:26:18 +00:00
Kim Morrison
5357fd2369
chore: rename List.groupBy to splitBy ( #5879 )
...
This makes room for adding a function that returns a HashMap, parallel
to `Array.groupByKey` (which I may also rename to `Array.groupBy`.
2024-10-30 00:56:52 +00:00
えび (ebi_chan)
3450c2a8ac
feat: add Nat.log2_two_pow ( #5756 )
2024-10-29 23:46:17 +00:00
Henrik Böving
c57d054b87
feat: support all the SMTLIB BitVec divison/remainder operations in bv_decide ( #5869 )
2024-10-28 16:37:06 +00:00
Luisa Cicolini
2f1dc878e4
feat: add BitVec.(msb, getMsbD)_concat ( #5865 )
2024-10-28 12:10:02 +00:00
Tobias Grosser
f558402ab8
feat: add BitVec.[zero_ushiftRight|zero_sshiftRight|zero_mul] and cle… ( #5858 )
...
…an up BVDecide
- Fix names
shiftLeft_zero_eq -> shiftLeft_zero
ushiftRight_zero_eq -> ushiftRight_zero
- Remove duplicate prefixes
BitVec.mul_zero -> mul_zero
BitVec.mul_add -> mul_add
- Adapt BVDecide/Normalize/BitVec by reusing the following functions
zero_add | add_zero
and_self
mul_zero | zero_mul
shiftLeft_zero | zero_shiftLeft
sshiftRight_zero | zero_sshiftRight
ushiftRight_zero | zero_ushiftRight
2024-10-28 08:47:29 +00:00
Henrik Böving
8c7f7484f9
feat: if support and more in bv_decide ( #5855 )
...
Using the same strategy as #5852 this provides `bv_decide` support for
`Bool` and `BitVec` ifs
this in turn instantly enables support for:
- `sdiv`
- `smod`
- `abs`
and thus closes our last discrepancies to QF_BV!
2024-10-27 08:40:38 +00:00
Luisa Cicolini
08c36e4306
feat: add (msb, getMsbD)_twoPow ( #5851 )
2024-10-26 17:27:37 +00:00
Joachim Breitner
8f0328b777
fix: deprecations in Init.Data.Array.Basic ( #5848 )
2024-10-26 10:33:47 +00:00
Kim Morrison
07ea626560
feat: Array.forIn', and relate to List ( #5833 )
...
Adds support for `for h : x in my_array do`, and relates this to the
existing `List` version.
2024-10-25 07:24:39 +00:00
Henrik Böving
193b6f2bec
feat: define Int8 ( #5790 )
2024-10-25 06:06:40 +00:00
Kim Morrison
059674d967
chore: minor fixes in Array lemmas ( #5832 )
2024-10-25 04:28:41 +00:00
Kim Morrison
09e1a05ee9
chore: cleanup imports ( #5825 )
2024-10-23 23:51:13 +00:00
Kim Morrison
c1143d9432
feat: more lemmas for List.modify ( #5816 )
2024-10-23 06:45:20 +00:00
Kim Morrison
07c09ee579
feat: relate Array.forIn and List.forIn ( #5799 )
2024-10-22 01:20:13 +00:00
Kim Morrison
919f64b2e6
chore: upstream List.modify, add lemmas, relate to Array.modify ( #5798 )
...
Note that the order of arguments still differs between `List.modify` and
`Array.modify`. I'll settle this later.
2024-10-22 01:01:32 +00:00
Kim Morrison
71122696a1
feat: rename Array.shrink to take, and relate to List.take ( #5796 )
2024-10-21 23:35:32 +00:00
Tobias Grosser
8d789f7b63
feat: add BitVec.toInt_sub, simplify BitVec.toInt_neg ( #5772 )
...
This also requires us to expand the theory of `Int.bmod`.
---------
Co-authored-by: Alex Keizer <alex@keizer.dev>
2024-10-21 22:38:29 +00:00
