stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-07-15T12:43:20Zhttps://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/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/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/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/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 forallhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/106Opaquify proofs in gmap_partial_alter (fix #46)2020-05-20T14:58:06ZPaolo G. GiarrussoOpaquify proofs in gmap_partial_alter (fix #46)- Ensure gmap well-formedness proofs are fully opaque.
- Use pattern-matching lambdas over lets.- Ensure gmap well-formedness proofs are fully opaque.
- Use pattern-matching lambdas over lets.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/155Add Countable instances for byte2020-05-12T17:53:49ZTej Chajedtchajed@gmail.comAdd Countable instances for bytehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/136Rotate everything2020-05-12T17:46:34ZMichael SammlerRotate everythingThis MR adds rotate_nat_add, rotate_nat_sub, rotate and rotate_take functions, which allow dealing with wraparound of lists. I don't know where these functions should go so I created a new file for them. But I can also move them somewher...This MR adds rotate_nat_add, rotate_nat_sub, rotate and rotate_take functions, which allow dealing with wraparound of lists. I don't know where these functions should go so I created a new file for them. But I can also move them somewhere else.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.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/134Lemmas for `list_find` in combination with `app` and `insert`.2020-05-12T17:00:22ZRobbert KrebbersLemmas for `list_find` in combination with `app` and `insert`.This MR proposes an alternative to the lemmas for `list_find` by @msammler in #131 (but that he removed later).
All lemmas are stated using a bi-implication, and they are strong enough to prove @msammler's original lemmas:
```coq
Lemma...This MR proposes an alternative to the lemmas for `list_find` by @msammler in #131 (but that he removed later).
All lemmas are stated using a bi-implication, and they are strong enough to prove @msammler's original lemmas:
```coq
Lemma list_find_insert_Some_ne1 l i i' x x':
list_find P l = Some (i', x') → ¬ P x → i ≠ i' →
list_find P (<[i:=x]> l) = Some (i', x').
Proof.
rewrite list_find_insert_Some, !list_find_Some.
destruct (decide (i < i')); naive_solver eauto with lia.
Qed.
Lemma list_find_insert_Some_ne_change2 l i i' x x':
list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x' → i < i' →
list_find P l = Some (i, x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver eauto with lia. Qed.
Lemma list_find_insert_Some_ne_same2 l i i' x x' x'':
list_find P (<[i:=x]>l) = Some (i', x') →
¬ P x → l !! i = Some x'' → (i < i' → ¬ P x'') →
list_find P l = Some (i', x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver. Qed.
Lemma list_find_insert_Some_ne2 l i i' x x' x'':
list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x'' → (x'' = x' ∨ ¬ P x'') →
∃ i'', list_find P l = Some (i'', x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver eauto with lia. Qed.
```
I very much dislike the statement of `list_find_insert_Some`, but I cannot come up with anything better that is true.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/159alternative overlay for coq/coq#121622020-05-08T09:42:13ZOlivier Laurentalternative overlay for coq/coq#12162This is an alternative to !153 which follows the spirit of !156.
It is adapted to the last version of [coq/coq#12162](https://github.com/coq/coq/pull/12162) which takes into account the introduction of `Bool.lt`.This is an alternative to !153 which follows the spirit of !156.
It is adapted to the last version of [coq/coq#12162](https://github.com/coq/coq/pull/12162) which takes into account the introduction of `Bool.lt`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/158add map_Forall_lookup2020-05-07T14:13:20ZRalf Jungjung@mpi-sws.orgadd map_Forall_lookupI was just searching for this lemma for at least 5 minutes until I realized that this is the definition of `map_Forall` -- usually our definitions are such that just `Print`ing stuff doesn't actually get me anywhere useful.
I think it w...I was just searching for this lemma for at least 5 minutes until I realized that this is the definition of `map_Forall` -- usually our definitions are such that just `Print`ing stuff doesn't actually get me anywhere useful.
I think it would be good for a lemma like this to show up in `Search` results.