stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-03-05T23:03:32Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/118Generalize (e)feed pose proof to intro patterns2020-03-05T23:03:32ZPaolo G. GiarrussoGeneralize (e)feed pose proof to intro patternsThis appears a simple oversight, since `pose proof` takes an intro pattern
anyway; `feed inversion` and `feed destruct` already take intro patterns, and
I've been using the generalized `efeed pose proof` for a while.This appears a simple oversight, since `pose proof` takes an intro pattern
anyway; `feed inversion` and `feed destruct` already take intro patterns, and
I've been using the generalized `efeed pose proof` for a while.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/120Rename `fin_of_nat` → `nat_to_fin` to follow the conventions.2020-03-05T22:13:06ZRobbert KrebbersRename `fin_of_nat` → `nat_to_fin` to follow the conventions.Rename `fin_of_nat` into `nat_to_fin`, `fin_to_of_nat` into `fin_to_nat_to_fin`, and `fin_of_to_nat` into `nat_to_fin_to_nat`, to follow the conventions in Iris, and also the recent rename for the similar `vec` functions.Rename `fin_of_nat` into `nat_to_fin`, `fin_to_of_nat` into `fin_to_nat_to_fin`, and `fin_of_to_nat` into `nat_to_fin_to_nat`, to follow the conventions in Iris, and also the recent rename for the similar `vec` functions.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/117Add destruct_or tactics to (possibly repeatedly) split disjunctions in an ass...2020-02-28T12:15:58ZArmaël GuéneauAdd destruct_or tactics to (possibly repeatedly) split disjunctions in an assumptionFollowing `split_and`, the new tactics are `split_or H`, `split_or? H` and `split_or! H`. The name `H` is reused for the assumptions that are produced by destructing the disjunction (no fresh name is introduced).
I was pondering wheth...Following `split_and`, the new tactics are `split_or H`, `split_or? H` and `split_or! H`. The name `H` is reused for the assumptions that are produced by destructing the disjunction (no fresh name is introduced).
I was pondering whether the tactic should be `split_or H` or `split_or in H`. The second one follows the usual pattern of `in`+assumption, but at the same time there is not going to be a `split_or` tactic that works on the goal, so...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/119Add a weakening lemma for goals: "is_Some (<[i:=x]>m !! j)"2020-02-26T10:29:23ZArmaël GuéneauAdd a weakening lemma for goals: "is_Some (<[i:=x]>m !! j)"I found this lemma to be quite useful in situations where one just wants to eliminate an `insert` that only updates a value that we know was already in the map.I found this lemma to be quite useful in situations where one just wants to eliminate an `insert` that only updates a value that we know was already in the map.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/114Add Countable instance for vec2020-02-24T16:12:20ZTej Chajedtchajed@gmail.comAdd Countable instance for vecI was surprised to learn this wasn't available and managed to prove it.
Note that this pulls in stdpp.vector into `countable`. The only reason for this is that the proof is really simple with `vec_to_list` as defined in std++, as oppose...I was surprised to learn this wasn't available and managed to prove it.
Note that this pulls in stdpp.vector into `countable`. The only reason for this is that the proof is really simple with `vec_to_list` as defined in std++, as opposed to with Coq's `Vector.of_list`. This only affects users in that `countable` now loads `vector`, which for example changes the implicits on Coq's vectors.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/115Countable instance for vec, and rename `vec_to_list_of_list` into `vec_to_lis...2020-02-24T16:11:55ZRobbert KrebbersCountable instance for vec, and rename `vec_to_list_of_list` into `vec_to_list_to_vec`This is an alternative to !114, which does not involve defining a partial function from lists to vectors, but makes use of the already existing function `list_to_vec`.
Also I renamed `vec_to_list_of_list` into `vec_to_list_to_vec`. The ...This is an alternative to !114, which does not involve defining a partial function from lists to vectors, but makes use of the already existing function `list_to_vec`.
Also I renamed `vec_to_list_of_list` into `vec_to_list_to_vec`. The former appears to be a leftover of the big `X_of_Y` into `Y_to_X` rename.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/116Add `set_solver` support for `dom`2020-02-24T14:12:11ZRobbert KrebbersAdd `set_solver` support for `dom`This MR closes issue #53.
@armael can you review/check if this sufficient for what you had in mind?This MR closes issue #53.
@armael can you review/check if this sufficient for what you had in mind?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/113Rename `cogpick` to `coGpick` (oops).2020-02-23T14:44:32ZDavid SwaseyRename `cogpick` to `coGpick` (oops).We renamed `cogset` to `coGset`, but my search and replace missed `cogpick`.
Pinging @robbertkrebbers.We renamed `cogset` to `coGset`, but my search and replace missed `cogpick`.
Pinging @robbertkrebbers.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/108cogset2020-02-20T22:24:17ZDavid SwaseycogsetAdd a type `cogset A` of finite/cofinite sets of elements of countable type `A`. When `A` is also infinite, all the usual operations are decidable. The implementation uses a pair of constructors (finite or infinite) each carrying a finit...Add a type `cogset A` of finite/cofinite sets of elements of countable type `A`. When `A` is also infinite, all the usual operations are decidable. The implementation uses a pair of constructors (finite or infinite) each carrying a finite set.
The file includes efficient conversions to and from `gset A` (for finite cogsets) and to `coPset` (for arbitrary cogsets), as well as less efficient conversions to and from other finite sets and other sets with a top element.
Two things are marked TODO in the source, which really means "to discuss".https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/112move coPset-generic hint to coPset.v2020-02-19T15:13:29ZRalf Jungjung@mpi-sws.orgmove coPset-generic hint to coPset.vI see no good reason for it to be in `namespaces.v`. The old one that got removed in e09f7ce35f22efb51bc1dd1f04f7b54b30280ea1 was in `coPset.v` as well.I see no good reason for it to be in `namespaces.v`. The old one that got removed in e09f7ce35f22efb51bc1dd1f04f7b54b30280ea1 was in `coPset.v` as well.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/111Add class `TopSet` for sets with ⊤ element2020-02-18T12:14:11ZRobbert KrebbersAdd class `TopSet` for sets with ⊤ elementThis closes issue #49. Some remarks:
- It's called `TopSet`, which corresponds with `SemiSet`.
- We now have a generic `SetUnfoldElemOf` for any `TopSet`.
- The `Hint Resolve coPset_top_subseteq : core` no longer works because the lemma...This closes issue #49. Some remarks:
- It's called `TopSet`, which corresponds with `SemiSet`.
- We now have a generic `SetUnfoldElemOf` for any `TopSet`.
- The `Hint Resolve coPset_top_subseteq : core` no longer works because the lemma is generic in a type class. AFAIK it is only used for `solve_ndisjoint`, so I added a specialized version to the `ndisj` hint database. We already have specialized versions of other set lemmas there.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/110Add decidability instances for Z.gt and Z.ge2020-02-13T21:16:07ZTej Chajedtchajed@gmail.comAdd decidability instances for Z.gt and Z.geUnfortunately these are not just defined as flipped versions of `Z.lt` and `Z.ge`.Unfortunately these are not just defined as flipped versions of `Z.lt` and `Z.ge`.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/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/107Added TCForall2_Forall2 lemma2020-01-30T12:07:51ZMichael SammlerAdded TCForall2_Forall2 lemmaThis lemma existed for TCForall but not for TCForall2.This lemma existed for TCForall but not for TCForall2.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/105Add lemmas regarding set_seq2019-11-11T11:15:16ZSimon Friis VindumAdd lemmas regarding set_seqAdds a few potentially useful lemmas regarding `set_seq`.
`subset_of_set_seq` can be seen as a generalization of the existing `elem_of_set_seq`. It gives equations that one can extract from knowing that one `set_seq` is a subset of anot...Adds a few potentially useful lemmas regarding `set_seq`.
`subset_of_set_seq` can be seen as a generalization of the existing `elem_of_set_seq`. It gives equations that one can extract from knowing that one `set_seq` is a subset of another `set_seq`.
The lemmas `subset_of_set_seq_len` and `elem_of_set_seq_len` are small variants of the same lemmas without the `_len` suffix. They extract information about the length or size of a `set_seq`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/104Remove `:>>` subclass instance declarations2019-11-07T08:18:01ZRobbert KrebbersRemove `:>>` subclass instance declarationsThere are not documented in https://coq.inria.fr/refman/addendum/type-classes.html?highlight=class#coq:cmd.class, and they don't have any advantage, so it's better to stop using them.There are not documented in https://coq.inria.fr/refman/addendum/type-classes.html?highlight=class#coq:cmd.class, and they don't have any advantage, so it's better to stop using them.https://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 lemmas