stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-10-27T13:54:55Zhttps://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/177[simpl_map]: avoid using [rewrite .. by ..]2020-09-29T09:36:43ZArmaël Guéneau[simpl_map]: avoid using [rewrite .. by ..]We've been using a patched version of [simpl_map] in our project for a while, with the changes included here.
The core issue is that it seems that [rewrite .. by ..] is not available when explicitly importing ssreflect.
The patch uses `...We've been using a patched version of [simpl_map] in our project for a while, with the changes included here.
The core issue is that it seems that [rewrite .. by ..] is not available when explicitly importing ssreflect.
The patch uses `by tac` instead, which is in line with what [simplify_map_eq] does later in the file.
I tried to write a quick test to demonstrate the issue; however it seems that triggering it is a bit subtle
(while it does definitely occur on our development, I wasn't able to easily reproduce it on my synthetic example---
I think there is some interaction with the exact order of the Require Import invocations).
If deemed necessary I could try harder and try to minimize a problematic instance from our development.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/168add singleton_insert_empty2020-06-29T10:17:34ZRalf Jungjung@mpi-sws.orgadd singleton_insert_emptyThis is just an unfolding, but with all the typeclasses that is impossible to find out and also not actually useful when applying lemmas.This is just an unfolding, but with all the typeclasses that is impossible to find out and also not actually useful when applying lemmas.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/165Adapt w.r.t. coq/coq#12512.2020-06-17T18:54:51ZGhost UserAdapt w.r.t. coq/coq#12512.This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.
https://github.com/coq/coq/pull/12512This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.
https://github.com/coq/coq/pull/12512https://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`).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/161rename Z2Nat_inj_div and Z2Nat_inj_mod2020-05-12T21:43:31ZMichael Sammlerrename Z2Nat_inj_div and Z2Nat_inj_modThis MR renames `Z2Nat_inj_div`, `Z2Nat_inj_mod`, `Nat2Z_inj_div` and `Nat2Z_inj_mod` to follow the naming conventions of `Z2Nat` and `Nat2Z`. See https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/136#note_49866
Should I mention ir...This MR renames `Z2Nat_inj_div`, `Z2Nat_inj_mod`, `Nat2Z_inj_div` and `Nat2Z_inj_mod` to follow the naming conventions of `Z2Nat` and `Nat2Z`. See https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/136#note_49866
Should I mention iris-users here already or only if the MR is merged?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/160Revert "Merge branch 'byte-countable' into 'master'"2020-05-12T17:33:24ZRobbert KrebbersRevert "Merge branch 'byte-countable' into 'master'"This reverts merge request !155 because it's incompatible with Coq ≤8.9.This reverts merge request !155 because it's incompatible with Coq ≤8.9.