stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2019-11-02T09:33:06Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/103Update gitignore for compatibility with Coq master2019-11-02T09:33:06ZTej Chajedtchajed@gmail.comUpdate gitignore for compatibility with Coq masterSee https://github.com/coq/coq/pull/10947 (.coqdeps.d now uses the name
of the Coq Makefile) and https://github.com/coq/coq/pull/8642 (Coq now
generates empty interface files *.vos when compiling).See https://github.com/coq/coq/pull/10947 (.coqdeps.d now uses the name
of the Coq Makefile) and https://github.com/coq/coq/pull/8642 (Coq now
generates empty interface files *.vos when compiling).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/102Add congruence lemmas for closures2019-11-01T14:46:40ZAmin TimanyAdd congruence lemmas for closureshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/101Add two useful lemmas2019-11-01T14:25:53ZAmin TimanyAdd two useful lemmashttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/99Generalize `list_find` lemmas to become bi-implications.2019-10-07T06:19:23ZRobbert KrebbersGeneralize `list_find` lemmas to become bi-implications.Thanks to @jules for the suggestion and an initial proof.
PS: I moved the block of code down because it now depends on some of the `Forall` lemmas that only appear later in the `list.v` file.Thanks to @jules for the suggestion and an initial proof.
PS: I moved the block of code down because it now depends on some of the `Forall` lemmas that only appear later in the `list.v` file.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/98Fix w.r.t. coq/coq#10764.2019-09-19T12:35:33ZGhost UserFix w.r.t. coq/coq#10764.Backward compatible, mergeable as-is.Backward compatible, mergeable as-is.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/97LookupTotal2020-02-11T08:55:39ZDan FruminLookupTotalThis is aimed at addressing https://gitlab.mpi-sws.org/iris/stdpp/issues/43.
Some TODOs:
- [x] Update the notation in accordance with https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/93
- [x] Direct definition of `LookupTotal` o...This is aimed at addressing https://gitlab.mpi-sws.org/iris/stdpp/issues/43.
Some TODOs:
- [x] Update the notation in accordance with https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/93
- [x] Direct definition of `LookupTotal` on vectors, so that its more friendlier towards simplification.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/96More lemmas for `filter` w.r.t. maps2019-09-12T13:32:31ZRobbert KrebbersMore lemmas for `filter` w.r.t. maps- `filter P m ##ₘ filter (λ v, ¬ P v) m`
- `filter P m ∪ filter (λ v, ¬ P v) m = m`
- `(∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) → dom D (filter P m) ≡ X`
For the last one, I have repurposed the name `dom_map_filter`, which was pre...- `filter P m ##ₘ filter (λ v, ¬ P v) m`
- `filter P m ∪ filter (λ v, ¬ P v) m = m`
- `(∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) → dom D (filter P m) ≡ X`
For the last one, I have repurposed the name `dom_map_filter`, which was previously used for `dom D (filter P m) ⊆ dom D m`. I have renamed the old lemma into `dom_map_filter_subseteq`. This follows current naming conventions.
This MR received partial contributions from @dfrumin.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/94Fix Open/Close scope2019-09-11T21:45:17ZJacques-Henri JourdanFix Open/Close scopeUse Open/Close Scope without Local (i.e., export the scope opening)
only when the scope corresponds to the main purpose of the module.Use Open/Close Scope without Local (i.e., export the scope opening)
only when the scope corresponds to the main purpose of the module.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/93Disambiguate Haskell-style notations for partially applied operators2020-02-11T08:46:19ZRobbert KrebbersDisambiguate Haskell-style notations for partially applied operatorsFor example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as
a prefix, as done in VST for example.
This closes issue #42.
I have used the `sed` script below. This script took care of nearly all uses
apart from a f...For example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as
a prefix, as done in VST for example.
This closes issue #42.
I have used the `sed` script below. This script took care of nearly all uses
apart from a few occurrences where a space was missing, e.g. `(,foo)`. In
this case, `coqc` will just fail, allowing one to patch up things manually.
The script is slightly too eager on Iris developments, where it also replaces
`($ ...)` introduction patterns. When porting Iris developments you thus may
want to remove the line for `$`.
```
sed '
s/(= /(.= /g;
s/ =)/ =.)/g;
s/(≠ /(.≠ /g;
s/ ≠)/ ≠.)/g;
s/(≡ /(.≡ /g;
s/ ≡)/ ≡.)/g;
s/(≢ /(.≢ /g;
s/ ≢)/ ≢.)/g;
s/(∧ /(.∧ /g;
s/ ∧)/ ∧.)/g;
s/(∨ /(.∨ /g;
s/ ∨)/ ∨.)/g;
s/(↔ /(.↔ /g;
s/ ↔)/ ↔.)/g;
s/(→ /(.→ /g;
s/ →)/ →.)/g;
s/($ /(.$ /g;
s/(∘ /(.∘ /g;
s/ ∘)/ ∘.)/g;
s/(, /(., /g;
s/ ,)/ ,.)/g;
s/(∘ /(.∘ /g;
s/ ∘)/ ∘.)/g;
s/(∪ /(.∪ /g;
s/ ∪)/ ∪.)/g;
s/(⊎ /(.⊎ /g;
s/ ⊎)/ ⊎.)/g;
s/(∩ /(.∩ /g;
s/ ∩)/ ∩.)/g;
s/(∖ /(.∖ /g;
s/ ∖)/ ∖.)/g;
s/(⊆ /(.⊆ /g;
s/ ⊆)/ ⊆.)/g;
s/(⊈ /(.⊈ /g;
s/ ⊈)/ ⊈.)/g;
s/(⊂ /(.⊂ /g;
s/ ⊂)/ ⊂.)/g;
s/(⊄ /(.⊄ /g;
s/ ⊄)/ ⊄.)/g;
s/(∈ /(.∈ /g;
s/ ∈)/ ∈.)/g;
s/(∉ /(.∉ /g;
s/ ∉)/ ∉.)/g;
s/(≫= /(.≫= /g;
s/ ≫=)/ ≫=.)/g;
s/(!! /(.!! /g;
s/ !!)/ !!.)/g;
s/(⊑ /(.⊑ /g;
s/ ⊑)/ ⊑.)/g;
s/(⊓ /(.⊓ /g;
s/ ⊓)/ ⊓.)/g;
s/(⊔ /(.⊔ /g;
s/ ⊔)/ ⊔.)/g;
s/(:: /(.:: /g;
s/ ::)/ ::.)/g;
s/(++ /(.++ /g;
s/ ++)/ ++.)/g;
s/(≡ₚ /(.≡ₚ /g;
s/ ≡ₚ)/ ≡ₚ.)/g;
s/(≢ₚ /(.≢ₚ /g;
s/ ≢ₚ)/ ≢ₚ.)/g;
s/(::: /(.::: /g;
s/ :::)/ :::.)/g;
s/(+++ /(.+++ /g;
s/ +++)/ +++.)/g;
' -i $(find -name "*.v")
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/92Avoid relying on `Export` bugs2019-09-05T21:39:11ZMaxime DénèsAvoid relying on `Export` bugsSee https://github.com/coq/coq/issues/10480 and
https://github.com/coq/coq/issues/10474.
This should be compatible with Coq's master, but I haven't tested.See https://github.com/coq/coq/issues/10480 and
https://github.com/coq/coq/issues/10474.
This should be compatible with Coq's master, but I haven't tested.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/91Lemmas for fin_maps2019-08-29T20:48:16ZMichael SammlerLemmas for fin_mapshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/90more instances for the empty type2019-08-26T12:32:40ZRalf Jungjung@mpi-sws.orgmore instances for the empty typehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/89add Equiv instance for Empty_set2019-08-26T12:22:03ZRalf Jungjung@mpi-sws.orgadd Equiv instance for Empty_setSeems like we have unit, sums and products, but the empty type was forgotten?Seems like we have unit, sums and products, but the empty type was forgotten?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/88Add `map_zip_with_flip`.2019-08-24T17:07:25ZDan FruminAdd `map_zip_with_flip`.I use it for `big_sepM2_swap` https://gitlab.mpi-sws.org/iris/iris/merge_requests/307I use it for `big_sepM2_swap` https://gitlab.mpi-sws.org/iris/iris/merge_requests/307https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/87relations.nsteps: add inversion lemma for `nsteps R 1 a b`2019-08-23T10:42:50ZPaolo G. Giarrussorelations.nsteps: add inversion lemma for `nsteps R 1 a b`https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/86std++ 1.2.1 release notes2019-08-13T14:01:01ZRalf Jungjung@mpi-sws.orgstd++ 1.2.1 release notesCc @robbertkrebbersCc @robbertkrebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/85Several simple lemmas.2019-08-14T22:11:03ZPaulo Emílio de VilhenaSeveral simple lemmas.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/84More lemmas about [map_imap].2019-08-13T14:17:31ZRodolphe LepigreMore lemmas about [map_imap].I hope these are at the right place!I hope these are at the right place!https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/83Proofs about binders2019-08-27T11:59:15ZMichael SammlerProofs about bindersNow that POPL deadline is over, here are some more lemmata. As always let me know if I should change anything.Now that POPL deadline is over, here are some more lemmata. As always let me know if I should change anything.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/82some list lemmas2019-07-13T10:10:01ZRalf Jungjung@mpi-sws.orgsome list lemmasJust needed these for a proof, seems general enough.Just needed these for a proof, seems general enough.