This PR provides intersection on `DTreeMap`/`TreeMap`/`TreeSet`and
provides several lemmas about it.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR adds union operations on DTreeMap/TreeMap/TreeSet and their raw
variants and provides lemmas about union operations.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR adds the types `Std.ExtDTreeMap`, `Std.ExtTreeMap` and
`Std.ExtTreeSet` of extensional tree maps and sets. These are very
similar in construction to the existing extensional hash maps with one
exception: extensional tree maps and sets provide all functions from
regular tree maps and sets. This is possible because in contrast to hash
maps, tree maps are always ordered.
This PR adds an equivalence relation to tree maps akin to the existing
one for hash maps. In order to get many congruence lemmas to eventually
use for defining functions on extensional tree maps, almost all of the
remaining tree map functions have also been given lemmas to relate them
to list functions, although these aren't currently used to prove lemmas
other than congruence lemmas.
This PR provides tests for those tree map functions that are not
verified yet.
---------
Co-authored-by: Paul Reichert <datokrat@users.noreply.github.com>
This PR renames the member `insert_emptyc_eq` of the `LawfulSingleton`
typeclass to `insert_empty_eq` to conform to the recommended spelling of
`∅` as `empty`.
See also #7447.
This PR changes the order of arguments of the folding function expected
by the tree map's `foldr` and `foldrM` functions so that they are
consistent with the API of `List`.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR provides proofs that the raw tree map operations are well-formed
and refactors the file structure of the tree map, introducing new
modules `Std.{DTreeMap,TreeMap,TreeSet}.Raw` and splittting
`AdditionalOperations` into separate files for bundled and raw types.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR implements the functions `modify` and `alter` on the tree map.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR implements the `getKey` functions on the tree map. It also fixes
the naming of the `entryAtIdx` function on the tree set, which should
have been called `atIdx`.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR implements the `getThenInsertIfNew?` and `partition` functions
on the tree map.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR implements the methods `min`, `max`, `minKey`, `maxKey`,
`atIndex`, `getEntryLE`, `getKeyLE` and consorts on the tree map.
In order to implement the proof-based functions such as `min` and
`getEntryLT` in `Queries.lean`, it was necessary to extract `Balanced`
and `Ordered` into new files so that they can be used from
`Queries.lean`.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR implements the methods `insertMany`, `ofList`, `ofArray`,
`foldr` and `foldrM` on the tree map.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR adds some deprecated function aliases to the tree map in order
to ease the transition from the `RBMap` to the tree map.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR introduces ordered map data structures, namely `DTreeMap`,
`TreeMap`, `TreeSet` and their `.Raw` variants, into the standard
library. There are still some operations missing that the hash map has.
As of now, the operations are unverified, but the corresponding lemmas
will follow in subsequent PRs. While the tree map has already been
optimized, more micro-optimization will follow as soon as the new code
generator is ready.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
