stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-09-29T09:14:09Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/185Add "options" file2020-09-29T09:14:09ZRalf Jungjung@mpi-sws.orgAdd "options" fileFixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/81
There is a slight chance that setting `Set Default Proof Using "Type*"` in a file where the option was not present before adds some extra assumptions to lemmas. I made sure everyth...Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/81
There is a slight chance that setting `Set Default Proof Using "Type*"` in a file where the option was not present before adds some extra assumptions to lemmas. I made sure everything still compiles and will also test Iris against this branch. But @robbertkrebbers if you want to be extra sure this doesn't add any unnecessary assumptions elsewhere, I will make those files `Unset Default Proof Using`; someone will have to manually investigate each lemma to check the assumptions.
Thanks to @tchajed we can even set the default goal selector. :)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/49silence fewer warnings, add comment about overwriting notation2020-09-25T08:44:33ZRalf Jungjung@mpi-sws.orgsilence fewer warnings, add comment about overwriting notation@robbertkrebbers could you expand the comment to explain *why* we are doing this? Seems rather unfortunate.@robbertkrebbers could you expand the comment to explain *why* we are doing this? Seems rather unfortunate.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/184Switch to strict bulleting everywhere2020-09-15T20:51:25ZTej Chajedtchajed@gmail.comSwitch to strict bulleting everywhereSolve iris/stdpp#82.
The flag isn't enforced anywhere, but with this we can add it seamlessly (ideally soon after so there aren't more violations that creep in).Solve iris/stdpp#82.
The flag isn't enforced anywhere, but with this we can add it seamlessly (ideally soon after so there aren't more violations that creep in).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/182make sure std++ does not rely on generated names2020-08-31T16:11:27ZRalf Jungjung@mpi-sws.orgmake sure std++ does not rely on generated nameshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/178Add `insert_replicate_strong`.2020-08-28T13:21:34ZDan FruminAdd `insert_replicate_strong`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/180list.v: avoid using mangled names2020-08-28T09:47:03ZRalf Jungjung@mpi-sws.orglist.v: avoid using mangled namesThis is needed to fix list.v compilation with name mangling enabled. I stopped after this file.This is needed to fix list.v compilation with name mangling enabled. I stopped after this file.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/176Remove `map` infix in lemmas about `dom` and `filter`.2020-07-17T12:51:49ZRobbert KrebbersRemove `map` infix in lemmas about `dom` and `filter`.The combination of `dom` and `filter` only makes sense for maps, so the `map` infix is useless. Other similar lemmas do not have such an infix either, so it's also inconsistent.
Rename `dom_map filter` → `dom_filter`, `dom_map_filter_...The combination of `dom` and `filter` only makes sense for maps, so the `map` infix is useless. Other similar lemmas do not have such an infix either, so it's also inconsistent.
Rename `dom_map filter` → `dom_filter`, `dom_map_filter_L` → `dom_filter_L`, and `dom_map_filter_subseteq` → `dom_filter_subseteq`.
This was pointed out by @atrieu in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/175#note_53746https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/175Additional lemmas about map_imap2020-07-16T12:02:33ZAlix TrieuAdditional lemmas about map_imapSome lemmas that were useful to me in a development.Some lemmas that were useful to me in a development.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/172Lemmas about "filter" on maps2020-07-15T17:07:02ZRalf Jungjung@mpi-sws.orgLemmas about "filter" on mapsThese are some lemmas from Perennial about "filter" on maps. Most are by me; `map_filter_insert_not_delete` is by @tchajed (original name: `map_filter_insert_not_strong`).These are some lemmas from Perennial about "filter" on maps. Most are by me; `map_filter_insert_not_delete` is by @tchajed (original name: `map_filter_insert_not_strong`).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/173prove NoDup_fmap_2_strong2020-07-15T16:45:29ZRalf Jungjung@mpi-sws.orgprove NoDup_fmap_2_strongAnother lemma that I just needed in Perennial.Another lemma that I just needed in Perennial.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/169Fix #70: add pattern variant of bind notation2020-07-15T12:43:20ZPaolo G. GiarrussoFix #70: add pattern variant of bind notationUse that in place of the old encoding:
https://gitlab.mpi-sws.org/iris/stdpp/-/issues/70#note_52817
Requires dropping support for Coq 8.7 (in a separate MR).Use that in place of the old encoding:
https://gitlab.mpi-sws.org/iris/stdpp/-/issues/70#note_52817
Requires dropping support for Coq 8.7 (in a separate MR).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/174LICENSE: Clarify which BSD license is being used2020-07-10T21:50:17ZPaolo G. GiarrussoLICENSE: Clarify which BSD license is being usedSister MR to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/472.Sister MR to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/472.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/171Sketch docs for computation on [gmap], since they're a FAQ2020-07-02T15:14:03ZPaolo G. GiarrussoSketch docs for computation on [gmap], since they're a FAQTODO:
- [x] fix line breaks, when the rest is reviewed (it destructs diffs till then).TODO:
- [x] fix line breaks, when the rest is reviewed (it destructs diffs till then).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/170drop support for Coq 8.72020-07-02T07:03:43ZRalf Jungjung@mpi-sws.orgdrop support for Coq 8.7https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/167Add solver `multiset_solver` for multisets2020-06-29T11:53:21ZRobbert KrebbersAdd solver `multiset_solver` for multisetsThe code contains some documentation how it works.
I added a number of tests, and used it to automate many existing lemmas in the `gmultiset` file.
Note that this required restructuring the file quite a bit, since I needed some bas...The code contains some documentation how it works.
I added a number of tests, and used it to automate many existing lemmas in the `gmultiset` file.
Note that this required restructuring the file quite a bit, since I needed some basic lemmas (now in section `basic_lemmas`) to define the tactic, and wanted to use the tactic subsequently to prove many of the existing lemmas (now in section `multiset_unfold`). None of the lemma statements changed, only many proofs are replaced by a mere call to `multiset_solver`.
/cc @msammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/162Prove theorem about delete of gset_to_gmap2020-06-23T21:33:04ZTej Chajedtchajed@gmail.comProve theorem about delete of gset_to_gmapBasically the opposite of `gset_to_gmap_union_singleton`.
I was going to call this `gset_to_gmap_delete` but I decided to follow the convention from the other lemma (which isn't called `gset_to_gmap_insert`).Basically the opposite of `gset_to_gmap_union_singleton`.
I was going to call this `gset_to_gmap_delete` but I decided to follow the convention from the other lemma (which isn't called `gset_to_gmap_insert`).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/164Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)2020-06-18T19:17:26ZsarahzrfAdded sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)I've added an instance `sig_finite` along with a couple of minor things used to define/prove it. This is a `Finite` instance for `sig`s over `Finite` types whose predicates are decidable and proof irrelevant:
```coq
(* Not a direct excer...I've added an instance `sig_finite` along with a couple of minor things used to define/prove it. This is a `Finite` instance for `sig`s over `Finite` types whose predicates are decidable and proof irrelevant:
```coq
(* Not a direct excerpt. *)
Context `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)} `{∀ x, ProofIrrel (P x)}.
Global Instance sig_finite : Finite (sig P).
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/166Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #125122020-06-17T08:54:53ZRobbert KrebbersAvoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512This MR provides an alternative to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/165, but avoids the `epose` horribleness. Instead, it just spells out some proofs, which IMHO makes things easier to maintain.This MR provides an alternative to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/165, but avoids the `epose` horribleness. Instead, it just spells out some proofs, which IMHO makes things easier to maintain.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/163Remove type scope from forall notation2020-05-27T22:12:37ZTej Chajedtchajed@gmail.comRemove type scope from forall notationFixes #67.Fixes #67.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/152notation for forall2020-05-27T21:51:21ZGregory Malechanotation for forall