stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-03-10T16:41:16Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/57Rename multiset "union" into "disjoint union"2021-03-10T16:41:16ZRobbert KrebbersRename multiset "union" into "disjoint union"This fixes #13. Now `∪` and `∩` are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas `⊎` is the "sum" (i.e. adding the multiplicities).
Some questions/remarks:
- `⊎` and `∪` have different heig...This fixes #13. Now `∪` and `∩` are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas `⊎` is the "sum" (i.e. adding the multiplicities).
Some questions/remarks:
- `⊎` and `∪` have different heights in my font (see `⊎∪`). Is there maybe a better disjoint union symbol in unicode?
- There are probably all kinds of laws about the interaction between `∪`, `∩`, and `⊎`, like distributivity. I did not attempt to prove a comprehensive set of such laws.
- `∖` is still the operation that subtracts multiplicity. I think that's fine, since there is no sensible difference operator for multisets that matches up with the union operator.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/56Notion of (in)finite predicates2019-02-21T20:33:00ZRobbert KrebbersNotion of (in)finite predicatesAs discussed in https://gitlab.mpi-sws.org/iris/iris/merge_requests/217
I have directly taken the opportunity to state `set_finite` using the new `pred_finite`.As discussed in https://gitlab.mpi-sws.org/iris/iris/merge_requests/217
I have directly taken the opportunity to state `set_finite` using the new `pred_finite`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/55Additionally lemmas for insert, nth, take, and list_find2019-02-21T16:57:32ZHai DangAdditionally lemmas for insert, nth, take, and list_findJust some several useful lemmas for lists.Just some several useful lemmas for lists.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/54Seal `fresh_generic`.2019-02-07T13:00:52ZRobbert KrebbersSeal `fresh_generic`.Since `fresh_generic` is too inefficient for all practical purposes, we seal
off its definition. That way, Coq will not accidentally unfold it during
unification or other tactics.
This issue actually occurred in iGPS, as reported by...Since `fresh_generic` is too inefficient for all practical purposes, we seal
off its definition. That way, Coq will not accidentally unfold it during
unification or other tactics.
This issue actually occurred in iGPS, as reported by Hai.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/53Confluent relations2019-02-10T20:44:10ZRobbert KrebbersConfluent relationsThis MR adds:
- The symmetric and reflexive/transitive/symmetric closure of a relation
- Different notions of confluence: diamond property, confluence, local confluence (following the naming conventions in https://www21.in.tum.de/~nipko...This MR adds:
- The symmetric and reflexive/transitive/symmetric closure of a relation
- Different notions of confluence: diamond property, confluence, local confluence (following the naming conventions in https://www21.in.tum.de/~nipkow/TRaAT/)
- Standard properties such as diamond ⊢ confluence ⊢ local confluence, the Church-Rosser property, Newman's lemma
As part of this MR, I removed the hint database `ars`. The name made no sense and it was not used anywhere to my knowledge. If it was used anywhere, it would be very unreliable as it contained hints like `rtc_trans` that would generally lead to loops.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/52fix or silence Coq 8.10 warnings2019-02-20T21:54:22ZRalf Jungjung@mpi-sws.orgfix or silence Coq 8.10 warningshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/51fix λ.. printing and test it2019-01-24T18:27:52ZRalf Jungjung@mpi-sws.orgfix λ.. printing and test ithttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/50Make trivial instances explicit2019-01-24T08:32:46ZMaxime DénèsMake trivial instances explicitThis is in preparation for coq/coq#9274.
Should be backward compatible but that remains to be tested.This is in preparation for coq/coq#9274.
Should be backward compatible but that remains to be tested.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/49silence fewer warnings, add comment about overwriting notation2020-09-25T08:44:33ZRalf Jungjung@mpi-sws.orgsilence fewer warnings, add comment about overwriting notation@robbertkrebbers could you expand the comment to explain *why* we are doing this? Seems rather unfortunate.@robbertkrebbers could you expand the comment to explain *why* we are doing this? Seems rather unfortunate.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/48`tc_to_bool` to turn a type class into a Boolean that expresses if there is a...2019-02-06T14:01:10ZRobbert Krebbers`tc_to_bool` to turn a type class into a Boolean that expresses if there is an instanceThis MR introduces the following function:
```coq
(** Given a proposition [P] that is a type class, [bool_of_tc P] will return
[true] iff there is an instance of [P]. *)
Definition bool_of_tc (P : Prop)
{p : bool} `{TCIf P (TCEq...This MR introduces the following function:
```coq
(** Given a proposition [P] that is a type class, [bool_of_tc P] will return
[true] iff there is an instance of [P]. *)
Definition bool_of_tc (P : Prop)
{p : bool} `{TCIf P (TCEq p true) (TCEq p false)} : bool := p.
```
It's particularly useful in Ltac, where it's sometimes needed to figure out if an instance exists or not. An example use can be found in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/199https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/47Get rid of the awk.Makefile references2018-12-15T12:01:55ZDan FruminGet rid of the awk.Makefile referencesDoesn't seem that its necessaryDoesn't seem that its necessaryhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/46Add results about deleting and inserting filtered out elements2018-12-16T09:39:46ZMichael SammlerAdd results about deleting and inserting filtered out elementshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/45Consistently use `set_` prefix.2019-02-20T17:58:14ZRobbert KrebbersConsistently use `set_` prefix.The MR closes #24.
- Consistently `set_` prefixes (instead of `collection_`).
- Rename the `Collection` type class into `Set_`. Likewise, `SimpleCollection` is called `SemiSet`, and `FinCollection` is called `FinSet`, and `Collection...The MR closes #24.
- Consistently `set_` prefixes (instead of `collection_`).
- Rename the `Collection` type class into `Set_`. Likewise, `SimpleCollection` is called `SemiSet`, and `FinCollection` is called `FinSet`, and `CollectionMonad` is called `MonadSet`.
- Rename `collections.v` and `fin_collections.v` into `sets.v` and `fin_sets.v`, respectively.
- Rename `set A := A → Prop` (`theories/set.v`) into `propset`, and likewise `bset` into `boolset`.
- Consistently prefer `X_to_Y` for conversion functions, e.g. `list_to_map` instead of the former `map_of_list`.
## Sed script uses
This MR is the result of the following `sed` script. It only had one bug, it wrongly replaced `Vector.of_list` into `Vector.set_of_list`. Note that I'm not using `\b` all the time because I also wanted to fix up lemma names.
```
sed '
s/SimpleCollection/SemiSet/g;
s/FinCollection/FinSet/g;
s/CollectionMonad/MonadSet/g;
s/Collection/Set\_/g;
s/collection\_simple/set\_semi\_set/g;
s/fin\_collection/fin\_set/g;
s/collection\_monad\_simple/monad\_set\_semi\_set/g;
s/collection\_equiv/set\_equiv/g;
s/\bbset/boolset/g;
s/mkBSet/BoolSet/g;
s/mkSet/PropSet/g;
s/set\_equivalence/set\_equiv\_equivalence/g;
s/collection\_subseteq/set\_subseteq/g;
s/collection\_disjoint/set\_disjoint/g;
s/collection\_fold/set\_fold/g;
s/collection\_map/set\_map/g;
s/collection\_size/set\_size/g;
s/collection\_filter/set\_filter/g;
s/collection\_guard/set\_guard/g;
s/collection\_choose/set\_choose/g;
s/collection\_ind/set\_ind/g;
s/collection\_wf/set\_wf/g;
s/map\_to\_collection/map\_to\_set/g;
s/map\_of\_collection/set\_to\_map/g;
s/map\_of\_list/list\_to\_map/g;
s/map\_of\_to_list/list\_to\_map\_to\_list/g;
s/map\_to\_of\_list/map\_to\_list\_to\_map/g;
s/\bof\_list/list\_to\_set/g;
s/\bof\_option/option\_to\_set/g;
s/elem\_of\_of\_list/elem\_of\_list\_to\_set/g;
s/elem\_of\_of\_option/elem\_of\_option\_to\_set/g;
s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g;
s/seq\_set/set\_seq/g;
s/collections/sets/g;
s/collection/set/g;
s/to\_gmap/gset\_to\_gmap/g;
s/of\_bools/bools\_to\_natset/g;
s/to_bools/natset\_to\_bools/g;
' -i $(find -name "*.v")
```
# Impact on dependencies
I have patches for Iris, lambdarust, Iron, fri-coq and iris-examples. The amount of renaming that had to be done was fairly minimal, and was mostly done automatically using the above `sed` script.
- Iris: 42 lines changed
- Iris-examples: 8 lines changed
- Iron: no changes needed
- Lambdarust: 17 lines changed
- Fri-coq: 83 lines changed (mostly changing `set` into `propset` by hand)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/44New `seq` operation on maps + consistency tweaks for `seq` operation on sets2019-02-20T16:50:48ZRobbert KrebbersNew `seq` operation on maps + consistency tweaks for `seq` operation on setsThis MR introduces a `seq` operation on maps, which turns a list `x_0; ...; x_n` into a map:
```
{[ i := x_0; ... i+n := x_n ]}
```
On top of that, I made various improvements to the already existing `seq` operation on sets:
-...This MR introduces a `seq` operation on maps, which turns a list `x_0; ...; x_n` into a map:
```
{[ i := x_0; ... i+n := x_n ]}
```
On top of that, I made various improvements to the already existing `seq` operation on sets:
- ~~Rename it from `seq_set` into `set_seq`. Having `_set` as a suffix instead of a prefix is inconsistent, see also #24.~~ This is done as part of !45 now.
- Provide `set_solver` support for `set_seq`.
- Make the lemmas for `set_seq` more consistent w.r.t. those for maps.
Due to the rename, it is not backwards compatible. I'm happy to fix Iris and friends.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/43Explicitly use core hint database2018-11-30T08:57:53ZTej Chajedtchajed@gmail.comExplicitly use core hint databaseAdding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/42Add link to docs to the Readme2018-11-30T09:50:53ZMichael SammlerAdd link to docs to the Readme@jung will make sure, that this link resolves to toc.html instead of index.html.@jung will make sure, that this link resolves to toc.html instead of index.html.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/41Consistently block `simpl` on all `Z` operations2018-11-08T09:53:58ZRobbert KrebbersConsistently block `simpl` on all `Z` operationsWe used to do this some operations (`Z.add`, `Z.mul`), but not for others (`Z.sub`, `Z.of_nat`); this MR blocks `simpl` consistently for all operations involving `Z` that I could think of.
The rationale for blocking everything is that...We used to do this some operations (`Z.add`, `Z.mul`), but not for others (`Z.sub`, `Z.of_nat`); this MR blocks `simpl` consistently for all operations involving `Z` that I could think of.
The rationale for blocking everything is that `simpl` produces very bad results, e.g. try:
```coq
Require Import ZArith.
Eval simpl in (fun n y => Z.of_nat (S n) + y)%Z.
(*
Yields:
fun (n : nat) (y : Z) =>
match y with
| 0%Z => Z.pos (Pos.of_succ_nat n)
| Z.pos y' => Z.pos (Pos.of_succ_nat n + y')
| Z.neg y' => Z.pos_sub (Pos.of_succ_nat n) y'
end
*)
```
Note that blocking `simpl` for `Z.of_nat` used to break `lia` and `omega` in the past, see https://github.com/coq/coq/issues/5039. For `lia` this has been fixed, but for `omega` not yet. However, in !37 we decided to use `lia` everywhere in both std++ and Iris because it's faster, and moreover, I believe the Coq devs intend to deprecate `omega` in favor of `lia` in the future. So, I don't think we should care about `omega` anymore.
I also updated the item "Side-effects" in the README to document that we block `simpl` on `Z` operations.
@jjourdan @jung Any objections to this MR?
I have fixes for Iris, iris-examples, Iron, lambdaRust (which are mostly a couple of one-liners). I thus would like to merge this ASAP (so I don't get merge conflicts on my fixes).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/40Add `Countable` instance for `gset`.2018-06-29T11:25:47ZJannoAdd `Countable` instance for `gset`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/39begin a test suite2018-06-25T12:31:27ZRalf Jungjung@mpi-sws.orgbegin a test suiteTest that https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38 doesn't regress, and also add some tests for `solve_proper` because I remember being annoyed at some point that I had to go all the way to Iris to test even...Test that https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38 doesn't regress, and also add some tests for `solve_proper` because I remember being annoyed at some point that I had to go all the way to Iris to test even the most basic functionality.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/38decrease priority for rtc_reflexive instance2018-06-25T12:12:27ZRalf Jungjung@mpi-sws.orgdecrease priority for rtc_reflexive instanceWe give this instance a lower-than-usual priority because when it is applied to `Reflexive ?`, it leads to a new evar being created for `R`. Unfortunately, we cannot set `Hint Mode` for `Reflexive` in a way that just rules out `Reflexive...We give this instance a lower-than-usual priority because when it is applied to `Reflexive ?`, it leads to a new evar being created for `R`. Unfortunately, we cannot set `Hint Mode` for `Reflexive` in a way that just rules out `Reflexive ?` [1], but we can at least stop TC search from using this instance. This helps performance because it gives TC search less freedom in the remainder of the search. It doesn't seem like backtracking is happening here.
Also see the discussion below https://gitlab.mpi-sws.org/FP/iris-coq/commit/8e8c722870b36c23032d9bc10019e40e6eb6be62. I think this is useful even if we decide to roll back the `IntoVal` change as there may be other places where `rtc_reflexive` inadvertently gets chosen.
[1] That would break https://gitlab.mpi-sws.org/FP/iris-coq/blob/38ba379fae88865ed3a06ba44bf22938b6524610/theories/algebra/list.v#L213