stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2024-10-07T06:13:26Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/576Add cartesian products to all concrete set types2024-10-07T06:13:26ZThibaut PéramiAdd cartesian products to all concrete set typesThis adds a set Cartesian product on:
- `list`
- `gset`
- `propset`
- `boolset`
- `listset`
With the notation `A × B` at level 37. The notation is left associative so that `lA × lB × lC : list (A * B * C)`. This includes corresponding ...This adds a set Cartesian product on:
- `list`
- `gset`
- `propset`
- `boolset`
- `listset`
With the notation `A × B` at level 37. The notation is left associative so that `lA × lB × lC : list (A * B * C)`. This includes corresponding specification lemmas and `SetUnfoldElemOf` instances. I only did a set level specification. There is no lemma in this MR describing the order for the Cartesian product on lists (the only one of those types where order is relevant)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/571Draft: Use `RelDecision` when possible.2024-09-08T10:57:07ZRobbert KrebbersDraft: Use `RelDecision` when possible.This code was probably written before `RelDecision` existed (or based on such code).
Update: do not review yet, I detected a problem and need to change some more things.This code was probably written before `RelDecision` existed (or based on such code).
Update: do not review yet, I detected a problem and need to change some more things.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555Don't constraint template polymorphic universes of list and option redefining `MBind` and related typeclasses2024-10-02T13:48:36ZMichael SammlerDon't constraint template polymorphic universes of list and option redefining `MBind` and related typeclassesThis is an idea how to fix https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 and #207 . Since `M` never appears unapplied, it should not introduce the universe constraints. Note that the universe of `gmap` and `gset` and similar remain c...This is an idea how to fix https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 and #207 . Since `M` never appears unapplied, it should not introduce the universe constraints. Note that the universe of `gmap` and `gset` and similar remain constrained due to the `MonadSet` and `FinMap` typeclasses.
In particular, with
```
Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
Global Instance x : MBind list.
Admitted.
Print Universes.
```
one gets the contraint `list.u0 = MBind.u0`.
But with
```
Class MBind' (A MA MB : Type) := mbind : (A → MB) → MA → MB.
Notation MBind M := (∀ A B, MBind' A (M A) (M B)).
Global Instance x : MBind list.
Admitted.
Print Universes.
```
one only gets the constraints
```
x.u0 <= list.u0
x.u0 <= MBind'.u0
x.u0 <= MBind'.u1
x.u1 <= list.u0
x.u1 <= MBind'.u2
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/532Draft: Staging MR for various refactorings2023-12-02T09:45:08ZRobbert KrebbersDraft: Staging MR for various refactoringsIt turns out that properly fixing !507 opened quite a can of worms. We have the following related MRs now:
- [x] !526
- [ ] !530
- [x] !531
- [ ] `non_empty` change as discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_reques...It turns out that properly fixing !507 opened quite a can of worms. We have the following related MRs now:
- [x] !526
- [ ] !530
- [x] !531
- [ ] `non_empty` change as discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/526#note_97794
- [ ] Direction of equality in `fmap`/`omap`/`alter` lemmas, see https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531#note_97789
The plan is to merge all these MRs into a staging branch (the one linked to this MR) and then merge the staging branch to master. This way we have to fix reverse dependencies just once.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/530Add lemma `lookup_total_fmap`.2023-10-16T17:55:15ZRobbert KrebbersAdd lemma `lookup_total_fmap`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/527Add a comment about `cancel_inj` and `cancel_surj`.2023-10-14T17:42:57ZRobbert KrebbersAdd a comment about `cancel_inj` and `cancel_surj`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439add basic list functionality with Z-based indexing2024-09-23T11:17:54ZRalf Jungjung@mpi-sws.orgadd basic list functionality with Z-based indexingThis starts the work on https://gitlab.mpi-sws.org/iris/stdpp/-/issues/108 by implementing `insert` and `index` for `Z` as well as `lengthZ`, `takeZ`, `dropZ`, and porting much of the associated theory.
I have not ported everything, e.g...This starts the work on https://gitlab.mpi-sws.org/iris/stdpp/-/issues/108 by implementing `insert` and `index` for `Z` as well as `lengthZ`, `takeZ`, `dropZ`, and porting much of the associated theory.
I have not ported everything, e.g. the interactions with `Forall3`, `subseteq`, `submseteq`, `filter`, `mask` are missing. Also there are more operations that would need a Z-based version, such as `lookup_total`, `alter`, `delete`, `inserts`, `find`, `imap`, `imap2`, `resize`, `rotate`, `rotate_take`, `sublist_lookup`, `sublist_alter`. There are also some tactics that will not handle these new operations and so might need adjustments or Z-based tactics: `solve_length`, `simplify_list_eq`.
Still I think this is a useful start that can serve as a foundation for later extensions. :)
Blocked on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/441.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/394Add some _1, _2 lemmas for map_filter2022-11-23T08:43:44ZMichael SammlerAdd some _1, _2 lemmas for map_filterAs discussed with @robbertkrebbersAs discussed with @robbertkrebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/372Draft: Very preliminary version of a quick start guide for sets.2023-02-06T14:42:57ZRobbert KrebbersDraft: Very preliminary version of a quick start guide for sets.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/357Added some lemmas about [sublist]2023-10-13T09:40:52ZJonas KastbergAdded some lemmas about [sublist]Added some generally useful lemmas about the [sublist] functionAdded some generally useful lemmas about the [sublist] function