stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-05-19T09:31:56Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/260add insert_take_drop2021-05-19T09:31:56ZRalf Jungjung@mpi-sws.orgadd insert_take_drophttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/261add tactic for solving computable goals2021-05-18T08:57:47ZRalf Jungjung@mpi-sws.orgadd tactic for solving computable goalsFixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/83Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/83https://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/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/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/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/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/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/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/232Multiset set notation2021-04-20T14:59:03ZRobbert KrebbersMultiset set notationThis MR adds a notation `{[ x1 ;+ .. ;+ xn ]}` for `{{ x1 ]} ⊎ .. ⊎ {{ xn ]}`.
Todo:
- [x] bikeshed about notation
- [x] port tests in !231 to new notation
Fixes #100This MR adds a notation `{[ x1 ;+ .. ;+ xn ]}` for `{{ x1 ]} ⊎ .. ⊎ {{ xn ]}`.
Todo:
- [x] bikeshed about notation
- [x] port tests in !231 to new notation
Fixes #100https://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/13Provide an Infinite typeclass and a generic implementation of Fresh.2021-04-20T08:43:36ZGhost UserProvide an Infinite typeclass and a generic implementation of Fresh.This provides a generic implementation of Fresh for infinite types.
In detail, it adds:
- An Infinite type class. A type T is infinite if there is an injection from nat to T.
- A generic implementation of Fresh A C for an infinite type ...This provides a generic implementation of Fresh for infinite types.
In detail, it adds:
- An Infinite type class. A type T is infinite if there is an injection from nat to T.
- A generic implementation of Fresh A C for an infinite type A and a finite collection type C, by way of linear search for a fresh element.
- Instances of Infinite for a handful of types, including positive/natural/integer types and string.
- A generic Fresh for finite collections of strings. As an implementation detail, the generated strings are all of the form "~n" for some natural number n.
- Some minor additions (pretty-printer for nat, Fix unfolding lemma for setoids).Robbert KrebbersRobbert Krebbershttps://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/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/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/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/239More lemmas for list's prefix_of and suffix_of2021-04-15T09:58:04ZHai DangMore lemmas for list's prefix_of and suffix_ofMore properties of `prefix_of` and `suffix_of`:
- they are partial orders, not just pre orders
- `prefix_nil_inv` and `prefix_of_down_total`.More properties of `prefix_of` and `suffix_of`:
- they are partial orders, not just pre orders
- `prefix_nil_inv` and `prefix_of_down_total`.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/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/37b8m6pmdfr3pfwwjssre3oqjc