stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-07-14T19:40:57Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/295strengthened solve_decision ltac2021-07-14T19:40:57ZAbhishek Anandstrengthened solve_decision ltachttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/291Fix priority of `Permutation_app'`.2021-07-15T11:01:57ZRobbert KrebbersFix priority of `Permutation_app'`.This is a workaround for https://github.com/coq/coq/issues/14571
This fixes #114.
This fixes a regression caused by !270.This is a workaround for https://github.com/coq/coq/issues/14571
This fixes #114.
This fixes a regression caused by !270.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/293Make `done` work on `is_Some`.2021-07-15T12:21:39ZRobbert KrebbersMake `done` work on `is_Some`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/296Do not call `done` recursively when solving `is_Some`.2021-07-15T18:03:56ZRobbert KrebbersDo not call `done` recursively when solving `is_Some`.!293 broke Iris, this MR fixes that.!293 broke Iris, this MR fixes that.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/289add mk_evar tactic (to replace Coq's strange evar tactic) and use it2021-07-16T13:57:06ZRalf Jungjung@mpi-sws.orgadd mk_evar tactic (to replace Coq's strange evar tactic) and use itSee [discussion on Mattermost](https://mattermost.mpi-sws.org/iris/pl/m88qt68ggiyhmyb3bqa7yant1w)See [discussion on Mattermost](https://mattermost.mpi-sws.org/iris/pl/m88qt68ggiyhmyb3bqa7yant1w)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/294handle more goals in solve_ndisj2021-07-19T10:52:46ZRalf Jungjung@mpi-sws.orghandle more goals in solve_ndisjWe should only land this after the deadline since solving more goals can break things.We should only land this after the deadline since solving more goals can break things.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/297Swap `curry` and `uncurry` to be consistent with Haskell and friends.2021-07-20T10:03:27ZRobbert KrebbersSwap `curry` and `uncurry` to be consistent with Haskell and friends.This also applies to `(un)curry{3,4}`, `gmap_(un)curry`, and `h(un)curry`.
This fixes issue #76.
The code includes a horrible hack that should removed once support for Coq versions prior
to 8.13 is dropped, see https://github.com/coq/c...This also applies to `(un)curry{3,4}`, `gmap_(un)curry`, and `h(un)curry`.
This fixes issue #76.
The code includes a horrible hack that should removed once support for Coq versions prior
to 8.13 is dropped, see https://github.com/coq/coq/pull/12716.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/299alternative implementation of mk_evar that keeps naive_solver working2021-07-21T07:06:02ZRalf Jungjung@mpi-sws.orgalternative implementation of mk_evar that keeps naive_solver workingThis uses [a hack](https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884) to have side-effects in an ltac that returns a value.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issu...This uses [a hack](https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884) to have side-effects in an ltac that returns a value.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/115https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/301rename map_union_subseteq_l_alt → map_union_subseteq_l' (and likewise for _r)2021-07-21T11:04:34ZRalf Jungjung@mpi-sws.orgrename map_union_subseteq_l_alt → map_union_subseteq_l' (and likewise for _r)This is more consistent with `or_intro_{l,r}'` and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/300.This is more consistent with `or_intro_{l,r}'` and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/300.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/300solve_ndisj: solve more goals involving chains of differences2021-07-21T11:16:09ZRalf Jungjung@mpi-sws.orgsolve_ndisj: solve more goals involving chains of differencesThis improves `solve_ndisj` to handle goals that came up in iris/examples as part of the logically atomic triple mask change.This improves `solve_ndisj` to handle goals that came up in iris/examples as part of the logically atomic triple mask change.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/302`Params` and `Proper` instances for `curry` and friends2021-07-21T17:11:43ZRobbert Krebbers`Params` and `Proper` instances for `curry` and friendshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/303solve_ndisj: handle goals containing _ ∖ _ ∖ _2021-07-23T09:16:51ZRalf Jungjung@mpi-sws.orgsolve_ndisj: handle goals containing _ ∖ _ ∖ _This resolves the last remaining `solve_ndisj` FIXME in lambda-rust. :)This resolves the last remaining `solve_ndisj` FIXME in lambda-rust. :)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/304Add lemmas that say that `curry{3,4}?` and `uncurry{3,4}?` are inverses.2021-07-24T09:38:56ZRobbert KrebbersAdd lemmas that say that `curry{3,4}?` and `uncurry{3,4}?` are inverses.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/306Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼`2021-07-27T10:35:23ZRobbert KrebbersMake singleton/`⊆` lemmas consistent with Iris's singleton/`≼`See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/305#note_71807
I decided to use Iris's names and argument because:
- It's shorter
- Iris's `singleton_included` lemmas have been there for longer than the multise...See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/305#note_71807
I decided to use Iris's names and argument because:
- It's shorter
- Iris's `singleton_included` lemmas have been there for longer than the multiset lemmas, so are (probably) more widely usedhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/308Add lemma `map_singleton_subseteq_l` and `map_singleton_subseteq`.2021-07-27T10:46:26ZRobbert KrebbersAdd lemma `map_singleton_subseteq_l` and `map_singleton_subseteq`.Similar to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/306Similar to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/306https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/305some lemmas about list submseteq2021-07-27T10:58:15ZRalf Jungjung@mpi-sws.orgsome lemmas about list submseteqFound in Simuliris, original proofs by @simonspies.
I am not at all sure about the names...Found in Simuliris, original proofs by @simonspies.
I am not at all sure about the names...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/189Draft: use SProp for well-formedness condition in Pmap and gmap2021-07-27T21:03:00ZTej Chajedtchajed@gmail.comDraft: use SProp for well-formedness condition in Pmap and gmapProof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only `simpl` (ordinarily you can get this to work with `vm_compute`, which breaks th...Proof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only `simpl` (ordinarily you can get this to work with `vm_compute`, which breaks the opacity of proofs).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/310Generalize `map_filter_insert` so that it covers both the True and False case.2021-07-28T07:08:19ZRobbert KrebbersGeneralize `map_filter_insert` so that it covers both the True and False case.The new lemma is
```coq
Lemma map_filter_insert m i x :
filter P (<[i:=x]> m)
= if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).
```
We need the `delete` because there might be another entry with key `i` ...The new lemma is
```coq
Lemma map_filter_insert m i x :
filter P (<[i:=x]> m)
= if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).
```
We need the `delete` because there might be another entry with key `i` in `m`.
In addition there are the lemmas:
```coq
Lemma map_filter_insert_True m i x : (* used to be map_filter_insert *)
P (i, x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
Lemma map_filter_insert_False m i x : (* used to be map_filter_insert_not_delete *)
¬ P (i, x) → filter P (<[i:=x]> m) = filter P (delete i m).
```
I use the `_True` and `_False` suffixes similar to `decide_True` and `decide_False`.
See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/245?commit_id=335bc4d65a65bfeb247fa86853b057920c44feb0#note_72118 for the discussion that led to this MR.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/312add binder_list2021-07-28T13:43:27ZRalf Jungjung@mpi-sws.orgadd binder_listanother bit from Simulirisanother bit from Simulirishttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/313add lookup_take_Some2021-07-28T13:43:44ZRalf Jungjung@mpi-sws.orgadd lookup_take_Someanother bit from Simuliris, original proof by @msammleranother bit from Simuliris, original proof by @msammler