stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-04-29T13:39:11Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/259Don't use Z.to_nat in definition of rotate2021-04-29T13:39:11ZMichael SammlerDon't use Z.to_nat in definition of rotateSee https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/257#note_66496See https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/257#note_66496https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/258make Qc_of_Z not a Coercion any more2021-04-29T12:00:09ZRalf Jungjung@mpi-sws.orgmake Qc_of_Z not a Coercion any moreThis implements https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102 for `Qc_of_Z` -- `Qc` is not a widely used type (any more) so I think the fallout from this should be quite limited.This implements https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102 for `Qc_of_Z` -- `Qc` is not a widely used type (any more) so I think the fallout from this should be quite limited.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/257make Z.of_nat not a coercion inside std++2021-04-30T14:32:36ZRalf Jungjung@mpi-sws.orgmake Z.of_nat not a coercion inside std++This takes a first step towards https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102 by not declaring the coercion in std++. We will add it back in Iris. This can help gauge the fallout of https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102...This takes a first step towards https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102 by not declaring the coercion in std++. We will add it back in Iris. This can help gauge the fallout of https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102, and it would have caught [this problem](https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/254/diffs#note_66469).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/256`_True`/`_False` lemmas for `decide` and `mguard`2021-05-04T10:05:59ZRobbert Krebbers`_True`/`_False` lemmas for `decide` and `mguard`For `decide` we currently have the following lemmas:
```coq
Lemma decide_True {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x.
Lemma decide_False {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y.
Lemm...For `decide` we currently have the following lemmas:
```coq
Lemma decide_True {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x.
Lemma decide_False {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y.
Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
```
The first two are most commonly used, whereas the last two are also applicable if you do a `match` on `decide` and use the proof of `P` or `¬P`.
For `guard` we have similar lemmas that correspond to the first two lemmas for `decide`.
```coq
Lemma option_guard_True {A} P `{Decision P} (mx : option A) : P → (guard P; mx) = mx.
Lemma option_guard_False {A} P `{Decision P} (mx : option A) : ¬P → (guard P; mx) = None.
```
However, these don't work for `guard P as HP; ... something containing HP ...`, so I wanted to have lemmas like the last two for `decide`. The one for `False` can be generalized trivially, but (like `decide`) the one for `True` only works if the proposition is proof irrelevant:
```coq
Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A) (HP : P) : mguard P f = f HP.
Lemma option_guard_False {A} P `{Decision P} (f : P → option A) : ¬P → mguard P f = None.
```
(Note that `guard P as HP; y` is notation for `mguard P (λ HP, y)`).
The main problem, as usual, is naming... The `_left` and `_right` suffixes for `decide` make no sense for `guard`. So instead, I propose the `_pi` suffix for proof irrelevant. Opinions about that?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/255add Countable instance for decidable Sigma types2021-05-06T07:05:11ZSimon Gregersenadd Countable instance for decidable Sigma typesThis instance became useful when working with, e.g., a type for elements of a set `{ a : A | a ∈ X }` and wanting to construct a `gmap` with this domain.This instance became useful when working with, e.g., a type for elements of a set `{ a : A | a ∈ X }` and wanting to construct a `gmap` with this domain.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/254Add little endian encoding of Z2021-05-17T20:30:33ZMichael SammlerAdd little endian encoding of Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/253Fix pretty printing of multset literals + add tests2021-04-21T07:03:32ZRobbert KrebbersFix pretty printing of multset literals + add testshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/252Fix inconsistent arguments of `subset_difference_elem_of`.2021-04-20T09:36:50ZRobbert KrebbersFix inconsistent arguments of `subset_difference_elem_of`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/251Introduce `SingletonMS` class for multiset singletons.2021-04-20T16:44:32ZRobbert KrebbersIntroduce `SingletonMS` class for multiset singletons.- Define set-like notation `{[+ x1; ..; xn ]}` for multisets in terms of the new
singleton class and disjoint union `⊎`.
- Remove `SemiSet` instance for multisets.
- Prove lemmas regarding `∈` and `∉` for multisets since we no longer g...- Define set-like notation `{[+ x1; ..; xn ]}` for multisets in terms of the new
singleton class and disjoint union `⊎`.
- Remove `SemiSet` instance for multisets.
- Prove lemmas regarding `∈` and `∉` for multisets since we no longer get the
generic versions for sets.
- Provide `SetUnfoldElemOf` instances for multisets since we no longer get the
generic versions for sets.
- Prove lemmas new regarding `∈` and `∉` for `∩`
Fixes #100, #98 and #87.
This MR is an alternative to !232.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/250WIP: bitvector library2021-12-08T16:36:56ZMichael SammlerWIP: bitvector libraryhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/249Add list_to_map_app2021-04-20T08:41:11ZMichael SammlerAdd list_to_map_appSee discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244#note_65864See discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244#note_65864https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/248Add lemmas about testbit on bounded integers2021-04-19T10:13:23ZMichael SammlerAdd lemmas about testbit on bounded integersThese proofs are originally by @paulzhu, which is why I put him as the author of this commit. This is a part of !244.These proofs are originally by @paulzhu, which is why I put him as the author of this commit. This is a part of !244.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/247Add tactic `learn_hyp`, fixes #732021-04-19T12:30:59ZMichael SammlerAdd tactic `learn_hyp`, fixes #73This is another part of !244 and fixes #73.This is another part of !244 and fixes #73.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/246Add more typeclasses2021-04-15T08:03:48ZMichael SammlerAdd more typeclassesThis adds the typeclasses from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244. See also the discussion here: https://mattermost.mpi-sws.org/iris/pl/37b8m6pmdfr3pfwwjssre3oqjcThis adds the typeclasses from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244. See also the discussion here: https://mattermost.mpi-sws.org/iris/pl/37b8m6pmdfr3pfwwjssre3oqjchttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/245Add more lemmas for FinMaps (for union, filter, difference)2021-07-28T14:24:18ZHai DangAdd more lemmas for FinMaps (for union, filter, difference)Some lemmas that I believe worth upstreaming.Some lemmas that I believe worth upstreaming.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244Random collection of lemmas from RefinedC2021-04-15T13:18:41ZMichael SammlerRandom collection of lemmas from RefinedCThese are some things from RefinedC that I would like to upstream to stdpp. There are still some open questions, see the comments for them. Please let me know which of these changes make sense in stdpp.These are some things from RefinedC that I would like to upstream to stdpp. There are still some open questions, see the comments for them. Please let me know which of these changes make sense in stdpp.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/243Add lemma `lookup_app`, and derive other `lookup_app` lemmas from it.2021-04-15T09:13:25ZRobbert KrebbersAdd lemma `lookup_app`, and derive other `lookup_app` lemmas from it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/242Add lemma `lookup_map_seq`, derive other `lookup_map_seq` lemmas from that.2021-04-14T10:16:43ZRobbert KrebbersAdd lemma `lookup_map_seq`, derive other `lookup_map_seq` lemmas from that.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/241Hint Mode Equiv: update link to blocking Coq issue2021-04-11T18:06:52ZPaolo G. GiarrussoHint Mode Equiv: update link to blocking Coq issueBased on
https://github.com/coq/coq/issues/9058#issuecomment-496479506.
The goal is to track when this can be fixed.Based on
https://github.com/coq/coq/issues/9058#issuecomment-496479506.
The goal is to track when this can be fixed.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/240Future proof rotate_nat_add_add_mod2021-04-08T09:22:35ZAndrej DudenhefnerFuture proof rotate_nat_add_add_modThis prepares `rotate_nat_add_add_mod` for https://github.com/coq/coq/pull/14086 in a backwards compatible manner. Crucially, the design decision `n mod 0 = 0` could change to `n mod 0 = n` in future. This merge request makes `rotate_nat...This prepares `rotate_nat_add_add_mod` for https://github.com/coq/coq/pull/14086 in a backwards compatible manner. Crucially, the design decision `n mod 0 = 0` could change to `n mod 0 = n` in future. This merge request makes `rotate_nat_add_add_mod` agnostic of the particular design decision.