stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2024-09-08T11:46:49Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/417Add `set_fold_union_strong` and similarly for map2024-09-08T11:46:49ZRobbert KrebbersAdd `set_fold_union_strong` and similarly for map[This discussion at Mattermost](https://mattermost.mpi-sws.org/iris/pl/hf4fown633gtpxf39u1fuqsqfh) nerdsniped me to add the lemma `set_fold_union` and the stronger lemma `set_fold_union_strong` that only requires idempotence/associativit...[This discussion at Mattermost](https://mattermost.mpi-sws.org/iris/pl/hf4fown633gtpxf39u1fuqsqfh) nerdsniped me to add the lemma `set_fold_union` and the stronger lemma `set_fold_union_strong` that only requires idempotence/associativity/commutativity for the elements in the sets.
Interestingly, the already existing "disjoint" versions of the lemma can be derived.
The proofs are pretty long/tricky, so I tried to add some comments what's going on.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/573Make `foldr_cons_permute` lemmas consistent.2024-09-08T11:01:40ZRobbert KrebbersMake `foldr_cons_permute` lemmas consistent.See CHANGELOG.
Addressing issue pointed out in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/417#note_85025See CHANGELOG.
Addressing issue pointed out in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/417#note_85025https://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/570Better use of modules / less global polution for strings2024-09-08T09:01:25ZRobbert KrebbersBetter use of modules / less global polution for stringsSee CHANGELOG for detailsSee CHANGELOG for detailshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/572numbers.v: Don't Qed Decision instances2024-09-08T07:00:12ZPaolo G. Giarrussonumbers.v: Don't Qed Decision instancesNoticed from a `compute_done` failure.
Also, use `abstract` to still hide proof-irrelevant terms from computation.Noticed from a `compute_done` failure.
Also, use `abstract` to still hide proof-irrelevant terms from computation.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/567Stronger sorted unique lemmas2024-09-06T14:07:30ZRobbert KrebbersStronger sorted unique lemmasAdd lemmas `Sorted_unique'` and `StronglySorted_unique'` that only require anti symmetry for the elements that are in the list.Add lemmas `Sorted_unique'` and `StronglySorted_unique'` that only require anti symmetry for the elements that are in the list.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/568Notation for string literals in `stdpp_scope`.2024-09-06T13:26:07ZRobbert KrebbersNotation for string literals in `stdpp_scope`.This removes a giant hack (`Global Open Scope list_scope` in the old `strings` file) and fixes some parsing issues (`=?` not working after importing strings, see test case).This removes a giant hack (`Global Open Scope list_scope` in the old `strings` file) and fixes some parsing issues (`=?` not working after importing strings, see test case).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/569Add `map_Forall2_dom`.2024-09-06T10:54:47ZRobbert KrebbersAdd `map_Forall2_dom`.I didn't add a CHANGELOG, because there is already "Add `map_Forall2` and some basic lemmas about it".I didn't add a CHANGELOG, because there is already "Add `map_Forall2` and some basic lemmas about it".https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/566Stronger induction principle for `map_fold`.2024-09-04T22:07:35ZRobbert KrebbersStronger induction principle for `map_fold`.(Based on a proposal by @johannes, see https://mattermost.mpi-sws.org/iris/pl/uosw3r3xx7dhmgz9o4xy7joxpe)
The new induction principle is:
```coq
map_fold_ind {A} (P : M A → Prop) :
P ∅ →
(∀ i x m,
m !! i = None →
...(Based on a proposal by @johannes, see https://mattermost.mpi-sws.org/iris/pl/uosw3r3xx7dhmgz9o4xy7joxpe)
The new induction principle is:
```coq
map_fold_ind {A} (P : M A → Prop) :
P ∅ →
(∀ i x m,
m !! i = None →
(∀ B (f : K → A → B → B) b,
map_fold f b (<[i:=x]> m) = f i x (map_fold f b m)) →
P m →
P (<[i:=x]> m)) →
∀ m, P m;
```
This induction scheme is like `map_ind`, but it gives an equality for `map_fold` for the current element (`i`/`x`) without any conditions on `f`. This is sound because all uses of `fold` and the induction principle traverse the map in the same way.
- The new scheme implies `map_fold_foldr` from !565
- It also implies the proposed rule `map_to_list_cons_inv` by @johannes in https://mattermost.mpi-sws.org/iris/pl/drduhw8etirftc7bkwdjhj57fr
- I think the new `map_fold_ind` is more usable than the old one since you can just do `induction m as .. using map_fold_ind`. You do not need to `revert` and manually `apply` the scheme. Hence I renamed the old scheme into `map_fold_weak_ind`, which should discourage one from using it.
- Additional bonus: Using the new scheme we can easily prove `map_fold_comm_acc(_strong)?` without needless side-conditions, making it consistent with the versions of sets and multisets.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/564Generalize `map_relation` and `map_included` / Add `map_Forall2`.2024-09-03T10:26:40ZRobbert KrebbersGeneralize `map_relation` and `map_included` / Add `map_Forall2`.`map_Forall` and the big ops in Iris also take the key, so this makes `map_relation` consistent with that.
This also allowed me to add `map_Forall2` (defined using `map_relation`) in a way that is consistent with `map_Forall`.
This cha...`map_Forall` and the big ops in Iris also take the key, so this makes `map_relation` consistent with that.
This also allowed me to add `map_Forall2` (defined using `map_relation`) in a way that is consistent with `map_Forall`.
This change is not backwards compatible, but I expect little breakage. `map_relation` is mostly used internally to define `(⊆)`, `map_disjoint`, `map_agree`. And aside from a `Decision` instance there is very little theory about `map_relation`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/565Draft: Add law `map_fold_foldr` to `FinMap` interface.2024-09-02T19:36:56ZRobbert KrebbersDraft: Add law `map_fold_foldr` to `FinMap` interface.See the discussion at https://mattermost.mpi-sws.org/iris/pl/dmdsga9stjgebfwwnjmike56do
This rule expresses a form of "parametricity": it says that regardless of `A`, `B`, `f`, and `b`, the function `map_fold f b m` will always travers...See the discussion at https://mattermost.mpi-sws.org/iris/pl/dmdsga9stjgebfwwnjmike56do
This rule expresses a form of "parametricity": it says that regardless of `A`, `B`, `f`, and `b`, the function `map_fold f b m` will always traverse the map `m` in the same order. Namely the order of converting the map into a list.
This law holds for all instances of `FinMap` we currently have, and I think without weird non-constructive axioms (that allow one to define non-parametric functions) it is impossible to define a `FinMap` instance that does *not* satisfy this law.
/cc @johannes @ivanbakelhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/562Add lower bound lemma for finite sets2024-08-30T09:47:45ZLennard Gähergaeher@mpi-sws.orgAdd lower bound lemma for finite setsForked off from the discussion here: https://gitlab.mpi-sws.org/iris/lambda-rust/-/merge_requests/38#note_104108
This adds a variant of `minimal_exists` which does not require the set to be non-empty, but in return also does not guarant...Forked off from the discussion here: https://gitlab.mpi-sws.org/iris/lambda-rust/-/merge_requests/38#note_104108
This adds a variant of `minimal_exists` which does not require the set to be non-empty, but in return also does not guarantee that the element is part of the set.
I'm not sure what the best naming for this lemma is. Maybe it should be called `infimum_exists` instead of `lower_bound_exists`? Should it be prefixed by `set`, like many other lemmas in the file for which it is not directly clear it's related to sets? (and should `minimal_exists` be prefixed accordingly?)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/563Add lemma `fmap_insert_inv`.2024-08-30T09:02:59ZRobbert KrebbersAdd lemma `fmap_insert_inv`.For other operations (empty, singleton) we have a similar lemma. This one is missing.
I had to move some things around in the file, and re-proved `map_fmap_singleton_inv` using the new lemma.For other operations (empty, singleton) we have a similar lemma. This one is missing.
I had to move some things around in the file, and re-proved `map_fmap_singleton_inv` using the new lemma.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/561Allow `map_imap` to be used in nested recursive fixpoints.2024-08-27T19:24:27ZRobbert KrebbersAllow `map_imap` to be used in nested recursive fixpoints.See the test file for an example.
I expect this change to be backwards compatible. Since the definition of `map_imap` is awful, I don't expect anyone to use it directly (i.e., perform `unfold map_imap` in proofs), but rather use `map_lo...See the test file for an example.
I expect this change to be backwards compatible. Since the definition of `map_imap` is awful, I don't expect anyone to use it directly (i.e., perform `unfold map_imap` in proofs), but rather use `map_lookup_imap` or other lemmas.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/560Rename `X_length` into `length_X`.2024-08-16T08:44:34ZRobbert KrebbersRename `X_length` into `length_X`.This follows https://github.com/coq/coq/pull/18564
This closes #213
We didn't include our own copies of `app_length` and `seq_length`, but used those from the standard library. To make sure we can use them (without deprecation warnings...This follows https://github.com/coq/coq/pull/18564
This closes #213
We didn't include our own copies of `app_length` and `seq_length`, but used those from the standard library. To make sure we can use them (without deprecation warnings) until support for Coq 8.19 is dropped, I included our own copies for the transition period. This was also suggested by @tchajed in #213.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555Don't constraint template polymorphic universes of list and option redefining `MBind` and related typeclasses2024-08-16T08:33:21ZMichael 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/551Strengthen `map_disjoint_difference_{l,r}` and make them consistent with the lemmas for sets.2024-08-14T15:44:55ZRobbert KrebbersStrengthen `map_disjoint_difference_{l,r}` and make them consistent with the lemmas for sets.This closes #208, if m2 = m3 the precondition is vacuously true.This closes #208, if m2 = m3 the precondition is vacuously true.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/559Use gmake for BSD systems2024-07-31T17:00:23ZYiyun LiuUse gmake for BSD systemsThis PR modifies the `make-package` script so it runs on systems whose default `make` executable is BSD Make rather than GNU Make. It checks the os type and decides whether to run `gmake` or `make`. This is exactly how `opam` determines ...This PR modifies the `make-package` script so it runs on systems whose default `make` executable is BSD Make rather than GNU Make. It checks the os type and decides whether to run `gmake` or `make`. This is exactly how `opam` determines which `make` executable to use.
I also changed the script to use `sh` instead of `bash` because `make-package` doesn't seem to depend on bash-specific features and sh has a more standard path.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/424Prevent [finite_countable] from solving unrelated evars2024-07-26T21:17:27ZPaolo G. GiarrussoPrevent [finite_countable] from solving unrelated evarsFix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/160.
The problem is that `Hint Immediate` translates to (something like) `simple appl...Fix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/160.
The problem is that `Hint Immediate` translates to (something like) `simple apply @finite.finite_countable ; trivial` in the trace, and one (or both) the tactics trigger https://github.com/coq/coq/issues/6583. So I've adapted Iris's work around; I've not confirmed whether all of it is needed, but it worked on first try.
Missing (I assume):
- [ ] `trivial` only uses hints with cost 0, but `typeclasses eauto 0` does not appear to work, so `typeclasses eauto 1` is the closest thing I see. This might be a problem.
- [ ] Testcase
- [ ] Changelog? Probably not needed since this is a bugfix
- [x] Mention this in upstream issue.
Also see Coq issue https://github.com/coq/coq/issues/16893.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/558docs: quick typo fixes2024-07-19T19:16:21ZSanjit Bhatdocs: quick typo fixes