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/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/183Swap import of Peano and Utf8 to ensure that Utf8 notations are preferred.2020-10-26T09:46:19ZHugo HerbelinSwap import of Peano and Utf8 to ensure that Utf8 notations are preferred.Coq PR [#12950](https://github.com/coq/coq/pull/12950), among others changes, gives to import the effect of reactivating the imported notations.
This has an impact for stdpp, e.g. on printing `le n m` as either `m <= n` or `m ≤ n`, due ...Coq PR [#12950](https://github.com/coq/coq/pull/12950), among others changes, gives to import the effect of reactivating the imported notations.
This has an impact for stdpp, e.g. on printing `le n m` as either `m <= n` or `m ≤ n`, due to the order of imports between `Utf8.v` and `Peano.v` in `base.v`.
The Coq PR is still at the beginning of a process of discussion but the change to stdpp is backward compatible (as far as I can judge) and it should be safe to merge it anyway.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/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/179Add lemmas and max for Qp2020-10-27T13:54:55ZSimon Friis VindumAdd lemmas and max for QpAdd a few extra lemmas for `Qp` and adds a `max` operation for `Qp`. The lemmas for `max` are not exhaustive. The names of the lemmas are consistent with those in [GenericMinMax](https://coq.inria.fr/library/Coq.Structures.GenericMinMax....Add a few extra lemmas for `Qp` and adds a `max` operation for `Qp`. The lemmas for `max` are not exhaustive. The names of the lemmas are consistent with those in [GenericMinMax](https://coq.inria.fr/library/Coq.Structures.GenericMinMax.html).
The library `GenericMinMax` contains a way to implement `max` (see for instance [how it's used with `Q`](https://coq.inria.fr/library/Coq.QArith.Qminmax.html)). I'm not sure if that's the better way to do it. But, modules aren't used in this way anywhere in stdpp so I opted to not use it.https://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/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/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/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/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/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/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/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/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/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/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/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`).