stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-10-26T14:00:05Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/332base.v: fix typo in comment about MonadSet, and extend2021-10-26T14:00:05ZPaolo G. Giarrussobase.v: fix typo in comment about MonadSet, and extendThe comment hints at `listset_nodup`, which does _not_ have a MonadSet instance.The comment hints at `listset_nodup`, which does _not_ have a MonadSet instance.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/327countable.v: prove choose_proper2021-11-05T17:07:35ZPaolo G. Giarrussocountable.v: prove choose_proper~~Needs the misplaced `Acc_rect_max`.~~
Add missing properness lemma for choose.
Very first step towards "Pragmatic quotients" (haven't done the others yet), but meaningful on its own.~~Needs the misplaced `Acc_rect_max`.~~
Add missing properness lemma for choose.
Very first step towards "Pragmatic quotients" (haven't done the others yet), but meaningful on its own.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/333std++ 1.6.0 release notes2021-11-05T17:28:26ZTej Chajedtchajed@gmail.comstd++ 1.6.0 release notesCreating a new std++ release will fix #119, and allow us to release Iris 3.5.0.
This is a pretty big release, with over 400 commits from 14 authors!
I got the author list with `git shortlog --summary coq-stdpp-1.5.0..HEAD | gsed -E 's/...Creating a new std++ release will fix #119, and allow us to release Iris 3.5.0.
This is a pretty big release, with over 400 commits from 14 authors!
I got the author list with `git shortlog --summary coq-stdpp-1.5.0..HEAD | gsed -E 's/[ \\t]+/ /g' | cut -d' ' -f3-100`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/334normalize for Fail printing locations2021-11-13T02:07:06ZRalf Jungjung@mpi-sws.orgnormalize for Fail printing locationsAdjusts test suite for https://github.com/coq/coq/pull/15174Adjusts test suite for https://github.com/coq/coq/pull/15174https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/335Add lemma `map_subseteq_inv`.2021-11-22T15:12:14ZRobbert KrebbersAdd lemma `map_subseteq_inv`.As pointed out by @swils in https://mattermost.mpi-sws.org/iris/pl/wzsucg5swtrttqhsawdd8pzama this lemma is missing
It's all the way down the file since I need properties of ∖. If someone knows a (short) proof without, we can move the p...As pointed out by @swils in https://mattermost.mpi-sws.org/iris/pl/wzsucg5swtrttqhsawdd8pzama this lemma is missing
It's all the way down the file since I need properties of ∖. If someone knows a (short) proof without, we can move the property up, closer towards other properties on the order.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/336Fix coq-lint.sh on macOS2021-11-23T20:43:21ZTej Chajedtchajed@gmail.comFix coq-lint.sh on macOSFixes the build on macOS. Once this is merged I'll make the same fix to Iris.Fixes the build on macOS. Once this is merged I'll make the same fix to Iris.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/338Add reverse_lookup, reverse_lookup_Some and alternative version of sublist_lookup_Some2021-11-24T20:50:26ZMichael SammlerAdd reverse_lookup, reverse_lookup_Some and alternative version of sublist_lookup_SomeThis MR adds `reverse_lookup`, `reverse_lookup_Some` and an alternative version of `sublist_lookup_Some`This MR adds `reverse_lookup`, `reverse_lookup_Some` and an alternative version of `sublist_lookup_Some`https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/337Upstreaming a small collection of lemmas2021-11-25T02:33:50ZMichael SammlerUpstreaming a small collection of lemmasThis MR upstreams a small collection of lemmas from Islaris.This MR upstreams a small collection of lemmas from Islaris.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/10Add monadic `;;` and change level of the do-notation to 1002021-11-25T13:17:03ZRobbert KrebbersAdd monadic `;;` and change level of the do-notation to 100While trying to port some of the IPM tactics from Ltac to Mtac2 (formerly MetaCoq) I ran into the issue that `_ ;; _` was used at a different level in both Iris and Mtac2, making it impossible to combine both projects. The current levels...While trying to port some of the IPM tactics from Ltac to Mtac2 (formerly MetaCoq) I ran into the issue that `_ ;; _` was used at a different level in both Iris and Mtac2, making it impossible to combine both projects. The current levels are as follows:
| | `_ ;; _` | `_ <- _; _` |
|------------------|----------------|--------------|
| std++ | not present | 65 |
| Iris's heap_lang | 100 | not present |
| Mtac2 | 81 | 81 |
As you can see, the levels are all different!
Some notes:
- I think `_ ;; _` and `_ <- _; _` should be at the same level.
- The notation `_ ;; _` is not present in stdpp, but it should be there:
```coq
Notation "x ;; z" := (x ≫= λ _, z).
```
- If we currently add this notation, using the same level as `_ <- _; _`, namely 65, it will currently Iris.
This MR changes the level of `_ <- _; _` in std++ into 100, which is consistent with Iris. When we accept this MR, a one line fix for Iris is needed.
The main consequence of this MR is how these notations will interact with equality. Consider:
```
m1 = m2 ;; m3
```
Should that be parsed as:
1. `(m1 = m2) ;; m3` (now)
2. `m1 = (m2 ;; m3)` (before)
I'd say that when the notation is used for an imperative programming language, like Iris's `heap_lang`, it should definitely be (1). However, in the case of monadic code, (1) makes very little sense (at least for equality, but maybe it makes sense for other relations), as it will never type check.
Note that many other relations like setoid equality and inequality of numbers are also at level 70.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/340Lemmas for lookup on mjoin2021-11-26T09:48:47ZMichael SammlerLemmas for lookup on mjoinhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/341Add bool_to_Z2021-12-01T07:42:29ZMichael SammlerAdd bool_to_ZThis MR adds `bool_to_Z` which has been used as `Z_of_bool` in both RefinedC and [RustBelt](https://gitlab.mpi-sws.org/search?search=Z_of_bool&group_id=1795&project_id=178&scope=&search_code=true&snippets=false&repository_ref=master&nav_...This MR adds `bool_to_Z` which has been used as `Z_of_bool` in both RefinedC and [RustBelt](https://gitlab.mpi-sws.org/search?search=Z_of_bool&group_id=1795&project_id=178&scope=&search_code=true&snippets=false&repository_ref=master&nav_source=navbar).
There is not much theory for it as most of the time one can reason about it by computation.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/343some more lemmas about list folding2021-12-01T17:04:08ZRalf Jungjung@mpi-sws.orgsome more lemmas about list foldinghttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/339`zip_with_take_{l,r,both}{,'}` (was: Add lemma `zip_with_take_both`)2021-12-02T12:40:43ZGlen Mével`zip_with_take_{l,r,both}{,'}` (was: Add lemma `zip_with_take_both`)Merge it if you like it.Merge it if you like it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/342drop support for Coq 8.102021-12-03T15:31:40ZRalf Jungjung@mpi-sws.orgdrop support for Coq 8.10The successor, Coq 8.11, has been released in Jan 2020, almost 2 years ago. I think it is fine for us to drop earlier versions of Coq. Iris has also dropped support for 8.10 quite a while ago already.
This will also let us use https://g...The successor, Coq 8.11, has been released in Jan 2020, almost 2 years ago. I think it is fine for us to drop earlier versions of Coq. Iris has also dropped support for 8.10 quite a while ago already.
This will also let us use https://github.com/coq/coq/issues/7910, which should help make telescopes more ergonomic (see https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/762).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/346Avoid using Arith libraries deprecated in v8.162021-12-07T09:38:50ZTej Chajedtchajed@gmail.comAvoid using Arith libraries deprecated in v8.16Coq v8.16 will deprecate several libraries in `Arith` (see https://github.com/coq/coq/pull/14736). This results in warnings like:
```
File "./theories/numbers.v", line 1374, characters 13-23:
Warning: Notation plus_assoc is deprecated ...Coq v8.16 will deprecate several libraries in `Arith` (see https://github.com/coq/coq/pull/14736). This results in warnings like:
```
File "./theories/numbers.v", line 1374, characters 13-23:
Warning: Notation plus_assoc is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_assoc instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/list.v", line 1207, characters 29-47:
Warning: Notation Min.min_idempotent is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_id instead.
[deprecated-syntactic-definition,deprecated]
```
These changes seem to be backwards-compatible to Coq 8.11 so we might as well fix them now. In several cases the recommended fix is incorrect because it isn't the same lemma (for example, `minus_plus` has no replacement lemma, at least with the current imports); in those cases I changed the proof script to use `replace` and `lia` rather than introduce a lemma identical to the old one to continue using `rewrite`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/345Add is_closed_term tactic2021-12-08T06:53:44ZMichael SammlerAdd is_closed_term tacticThis MR adds a tactic that has been proven quite useful in RefinedC. An example usecase can be found here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/4168f736be2fd735dc9680fda0a3b3a6af2b1b5e/theories/bitvector.v#L294 (There it is still...This MR adds a tactic that has been proven quite useful in RefinedC. An example usecase can be found here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/4168f736be2fd735dc9680fda0a3b3a6af2b1b5e/theories/bitvector.v#L294 (There it is still called checked_closed).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/344Add list_fmap_inj1, Z_to_little_endian_lookup_Some and little_endian_to_Z_spec2021-12-08T07:39:26ZMichael SammlerAdd list_fmap_inj1, Z_to_little_endian_lookup_Some and little_endian_to_Z_specSome more lemmas...Some more lemmas...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/349Fix list_fmap_inj_12021-12-08T19:49:25ZMichael SammlerFix list_fmap_inj_1`list_fmap_inj_1` introduced by https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/344 accidentally has a superfluous `(?A → ?B)` due to `Set Default Proof Using "Type*".` :
```
Check list_fmap_inj_1.
=> list_fmap_inj_1
: (?A →...`list_fmap_inj_1` introduced by https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/344 accidentally has a superfluous `(?A → ?B)` due to `Set Default Proof Using "Type*".` :
```
Check list_fmap_inj_1.
=> list_fmap_inj_1
: (?A → ?B)
→ ∀ (f1 f2 : ?A → ?B) (l : list ?A) (x : ?A),
f1 <$> l = f2 <$> l → x ∈ l → f1 x = f2 x
```
This MR fixes this such that `list_fmap_inj_1` has the intended type:
```
Check list_fmap_inj_1.
=> list_fmap_inj_1
: ∀ (f f' : ?A → ?B) (l : list ?A) (x : ?A),
f <$> l = f' <$> l → x ∈ l → f x = f' x
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/348Homomorphism properties for `bool_decide` + rename (bool_)decide_iff.2021-12-09T12:03:11ZRobbert KrebbersHomomorphism properties for `bool_decide` + rename (bool_)decide_iff.- Add homomorphism properties for bool_decide and True, False, →, ↔
- Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext` because `_iff` is now used for the above property for `↔`. This is also more consistent wi...- Add homomorphism properties for bool_decide and True, False, →, ↔
- Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext` because `_iff` is now used for the above property for `↔`. This is also more consistent with other extensionality properties.