stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-05-04T12:42:48Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/461More canonical maps2023-05-04T12:42:48ZRobbert KrebbersMore canonical mapsThis MR:
- Provides new implementations of `gmap`/`gset`, `Pmap`/`Pset`, `Nmap`/`Nset` and
`Zmap`/`Zset` based on the "canonical" version of binary tries by Appel and
Leroy (see https://inria.hal.science/hal-03372247) that avoid the...This MR:
- Provides new implementations of `gmap`/`gset`, `Pmap`/`Pset`, `Nmap`/`Nset` and
`Zmap`/`Zset` based on the "canonical" version of binary tries by Appel and
Leroy (see https://inria.hal.science/hal-03372247) that avoid the use of Sigma
types and enjoy:
+ More definitional equalities, because maps are no longer equipped with a
proof of canonicity. This means more equalities can be proved by
`reflexivity` or even by conversion as part of unification. For example,
`{[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]}` and `{[ 1 ]} ∖ {[ 1 ]} = ∅`
hold definitionally.
+ The use in nested recursive definitions. For example,
`Inductive gtest := GTest : gmap nat gtest → gtest`. (The old map types
would violate Coq's strict positivity condition due to the Sigma type.)
- Makes `map_fold` a primitive of the `FinMap`, and derive `map_to_list` from it.
(Before `map_fold` was derived from `map_to_list`.) This makes it possible to
use `map_fold` in nested-recursive definitions on maps. For example,
`Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts`.
This MR contains a bunch of tests:
- To show that we indeed have more definitional equalities that can be proved by `reflexivity`.
- We can use `gmap` and `pmap` in nested recursive definitions.
- Computations with `vm_compute` on "big" `pmap`/`gmap`s (size >100.000), which would only terminate if the complexity is n-log-n.
- Compared to the old versions, the computations with `vm_compute` are slightly faster.
- Computations with `reflexivity` on small `pmap`/`gmap`s (size 1000), showing that the even with Coq's naive reduction computation is reasonable (<1 second).
- More tests for `simpl`/`cbn` for `Pmap` (and a fix akin to `Opaque gmap_empty` to make those work). We also should have such tests for `Pset`, but I leave that for a future MR.
/cc @amintimany since we were chatting about this during the PKVM meeting in Aarhus.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/441Add some list lemmas2023-03-24T15:54:25ZRalf Jungjung@mpi-sws.orgAdd some list lemmasThis fixes some inconsistencies and gaps that I noticed while working on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439, and ports some list lemmas from Perennial.This fixes some inconsistencies and gaps that I noticed while working on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439, and ports some list lemmas from Perennial.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/383Introduce `set_bind` and associated lemmas.2022-08-09T10:52:18ZDan FruminIntroduce `set_bind` and associated lemmas.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/368Define [tele_arg] as a fixpoint2022-05-16T00:52:05ZGregory MalechaDefine [tele_arg] as a fixpointThe current definition of `tele_arg` increases the universe level in a way that is unfortunate. In particular,
```coq
Inductive tele_arg : tele@{u} -> Type@{u+1} :=
| ...
```
In Iris, what this means is that `bi_tforall`/`bi_texist` h...The current definition of `tele_arg` increases the universe level in a way that is unfortunate. In particular,
```coq
Inductive tele_arg : tele@{u} -> Type@{u+1} :=
| ...
```
In Iris, what this means is that `bi_tforall`/`bi_texist` have different universe levels than `bi_forall`/`bi_exist`. This MR re-defines `tele_arg` as a fixpoint, which prevents the universe bump. In particular:
```coq
Fixpoint tele_arg (t : tele@{u}) : Type@{u} :=
...
```
With this definition, the universes for the telescopic quantifiers can match the universes of the non-telescopic quantifiers in iris (this enables a separate MR to iris: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/781).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/267Add lemma `set_fold_disj_union_strong`.2021-06-02T15:44:40ZRobbert KrebbersAdd lemma `set_fold_disj_union_strong`.Stronger version of a lemma suggested by @jihgfee.
TODO: Not sure about the name.Stronger version of a lemma suggested by @jihgfee.
TODO: Not sure about the name.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/228Avoid relying on buggy simpl never behavior2021-02-12T13:33:42ZTej Chajedtchajed@gmail.comAvoid relying on buggy simpl never behaviorWhat's going on in this proof is that `simpl` is unfolding both `decode_nat` _and_ `decode`, even though `decode` is marked `simpl never`. This is a bug in Coq and std++ should not rely on it.
Alternate take on
https://gitlab.inria.fr/b...What's going on in this proof is that `simpl` is unfolding both `decode_nat` _and_ `decode`, even though `decode` is marked `simpl never`. This is a bug in Coq and std++ should not rely on it.
Alternate take on
https://gitlab.inria.fr/bertot/stdpp/-/commit/895121f919c6f1332f41f658ce7f850e391eb49e,
which is used as an overlay in Coq for
https://github.com/coq/coq/pull/13448.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/203Replace unused pattern variables with underscore2020-11-26T10:24:52ZTej Chajedtchajed@gmail.comReplace unused pattern variables with underscoreAddresses new unused-pattern-matching-variable warning on Coq master (see https://github.com/coq/coq/pull/12768).
I'm pretty sure the `hlist.v` warning is a bug in Coq's heuristics for this, since those variables are used as implicit ar...Addresses new unused-pattern-matching-variable warning on Coq master (see https://github.com/coq/coq/pull/12768).
I'm pretty sure the `hlist.v` warning is a bug in Coq's heuristics for this, since those variables are used as implicit arguments and I don't see why the pattern matches more than one case (the warning is also printed twice for the same definition). Maybe there's something in the elaborated term I'm missing, which Coq doesn't even print back?
Regardless of what's going on in Coq, it's much easier for us to suppress the warning than to try to fix this upstream.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/197Remove dead type classes and notations.2020-10-28T19:00:01ZRobbert KrebbersRemove dead type classes and notations.These were very specific, there were no lemmas about them. They were used back in the days for some specific things in my C semantics.
Thanks to @blaisorblade for pointing out.These were very specific, there were no lemmas about them. They were used back in the days for some specific things in my C semantics.
Thanks to @blaisorblade for pointing out.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/164Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)2020-06-18T19:17:26ZsarahzrfAdded sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)I've added an instance `sig_finite` along with a couple of minor things used to define/prove it. This is a `Finite` instance for `sig`s over `Finite` types whose predicates are decidable and proof irrelevant:
```coq
(* Not a direct excer...I've added an instance `sig_finite` along with a couple of minor things used to define/prove it. This is a `Finite` instance for `sig`s over `Finite` types whose predicates are decidable and proof irrelevant:
```coq
(* Not a direct excerpt. *)
Context `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)} `{∀ x, ProofIrrel (P x)}.
Global Instance sig_finite : Finite (sig P).
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/129Fix `Export` order for `length`. Remove `length` hack in strings.2020-04-11T10:35:00ZRobbert KrebbersFix `Export` order for `length`. Remove `length` hack in strings.The notation in `strings` was a hack to shadow the `length` function on strings with those on lists.
@msammler and I figured out how to change the imports to fix this problem without the hack. Basically, `stdpp.base` exports `Coq.Stri...The notation in `strings` was a hack to shadow the `length` function on strings with those on lists.
@msammler and I figured out how to change the imports to fix this problem without the hack. Basically, `stdpp.base` exports `Coq.Strings` and `Coq.List` in the right order, so the shadowing is done right. As a consequence `Coq.Strings` should never be exported by hand.
This approach seems to work among all supported Coq versions.
We also added a test.https://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/96More lemmas for `filter` w.r.t. maps2019-09-12T13:32:31ZRobbert KrebbersMore lemmas for `filter` w.r.t. maps- `filter P m ##ₘ filter (λ v, ¬ P v) m`
- `filter P m ∪ filter (λ v, ¬ P v) m = m`
- `(∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) → dom D (filter P m) ≡ X`
For the last one, I have repurposed the name `dom_map_filter`, which was pre...- `filter P m ##ₘ filter (λ v, ¬ P v) m`
- `filter P m ∪ filter (λ v, ¬ P v) m = m`
- `(∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) → dom D (filter P m) ≡ X`
For the last one, I have repurposed the name `dom_map_filter`, which was previously used for `dom D (filter P m) ⊆ dom D m`. I have renamed the old lemma into `dom_map_filter_subseteq`. This follows current naming conventions.
This MR received partial contributions from @dfrumin.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/535Remove Import NPeano2023-11-17T06:59:47ZPierre RousselinRemove Import NPeanoRemove Import NPeano in numbers: this is necessary for
https://github.com/coq/coq/pull/18164Remove Import NPeano in numbers: this is necessary for
https://github.com/coq/coq/pull/18164https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/534Make `inv` and `oinv` work with numbers2023-10-30T20:51:23ZRalf Jungjung@mpi-sws.orgMake `inv` and `oinv` work with numbersI also replaced all `inversion_clear` by `inv`. In `list.v` I furthermore replaced most `inversion` by `inv` just to get a whole lot of extra testcases. However sometimes, follow-up automation fails when the inverted hypothesis is cleare...I also replaced all `inversion_clear` by `inv`. In `list.v` I furthermore replaced most `inversion` by `inv` just to get a whole lot of extra testcases. However sometimes, follow-up automation fails when the inverted hypothesis is cleared.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/199https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533Allow pattern and type annotations in propset notation2023-10-19T14:50:00ZThibaut PéramiAllow pattern and type annotations in propset notationThis allows to use patterns and type annotations in the `propset` notation, Like `{[ (x,y) | ... ]}` or `{[ x : T | ...]}` or even `{[ (x, y) : A * B | ...]}`.
However, for both the old and new notation, this notation immediately break...This allows to use patterns and type annotations in the `propset` notation, Like `{[ (x,y) | ... ]}` or `{[ x : T | ...]}` or even `{[ (x, y) : A * B | ...]}`.
However, for both the old and new notation, this notation immediately break if someone adds a binary infix `|` notation downstream, In which case this will be parsed as a singleton of whatever the result of the `|` operation is. This was already the case before, so anyone that did that already broke the original `propset` notationhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/532Draft: Staging MR for various refactorings2023-12-02T09:45:08ZRobbert KrebbersDraft: Staging MR for various refactoringsIt turns out that properly fixing !507 opened quite a can of worms. We have the following related MRs now:
- [x] !526
- [ ] !530
- [x] !531
- [ ] `non_empty` change as discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_reques...It turns out that properly fixing !507 opened quite a can of worms. We have the following related MRs now:
- [x] !526
- [ ] !530
- [x] !531
- [ ] `non_empty` change as discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/526#note_97794
- [ ] Direction of equality in `fmap`/`omap`/`alter` lemmas, see https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531#note_97789
The plan is to merge all these MRs into a staging branch (the one linked to this MR) and then merge the staging branch to master. This way we have to fix reverse dependencies just once.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531Fix inconsistencies in `lookup` and `elem_of` lemmas for `list`2023-10-20T12:54:40ZRobbert KrebbersFix inconsistencies in `lookup` and `elem_of` lemmas for `list`- Rename lemmas `elem_of_list_X` into `list_elem_of_X` to be consistent with the `list_lookup_X` lemmas. Some lemmas contained other inconsistencies (e.g., `_1` and `_2` swapped), see CHANGELOG for details.
- Change the order of the conj...- Rename lemmas `elem_of_list_X` into `list_elem_of_X` to be consistent with the `list_lookup_X` lemmas. Some lemmas contained other inconsistencies (e.g., `_1` and `_2` swapped), see CHANGELOG for details.
- Change the order of the conjunction in `list_lookup_fmap_Some`. The new
version is `(f <$> l) !! i = Some y ↔ ∃ x, y = f x ∧ l !! i = Some x`, which
makes it consistent with `list_elem_of_fmap` and the corresponding lemmas for
sets and maps. **To be continued in other MR, insert link**
- Rename `list_alter_fmap` → `list_fmap_alter` and remove `list_alter_fmap_mono` which was a monomorphic duplicate.
With the exception of the `list_elem_of_fmap` change, all changes in this MR can be applied by `sed`. It would be best to merge it together with !526 so we only have to run a giant `sed` script once on reverse dependencies.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/530Add lemma `lookup_total_fmap`.2023-10-16T17:55:15ZRobbert KrebbersAdd lemma `lookup_total_fmap`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/529Add `prod_swap` and some basic results for it.2023-10-14T16:04:35ZRobbert KrebbersAdd `prod_swap` and some basic results for it.I was surprised this function is not in the stdlib...I was surprised this function is not in the stdlib...