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/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/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/543Cleanup bitblast_mod after dropping support for Coq 8.132024-03-12T17:55:50ZMichael SammlerCleanup bitblast_mod after dropping support for Coq 8.13https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/541Fix slowdown in bv_saturate from https://github.com/coq/coq/pull/179842024-03-11T20:52:26ZMichael SammlerFix slowdown in bv_saturate from https://github.com/coq/coq/pull/17984https://github.com/coq/coq/pull/17984 causes a significant slowdown in Islaris since the changed `Z.euclidean_division_equations_cleanup` function can be become very slow if there are many hypothesis of the form `0 <= ... < ...` in the c...https://github.com/coq/coq/pull/17984 causes a significant slowdown in Islaris since the changed `Z.euclidean_division_equations_cleanup` function can be become very slow if there are many hypothesis of the form `0 <= ... < ...` in the context. This MR works around this by changing `bv_saturate` to generate hypothesis of the form `-1 < ... < ...` instead of `0 <= ... < ...`. This change speeds up some case studies in Islaris by up to 30%, see [here](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=isla-coq&var-branch1=time%2Fcoq-8.19&var-commit1=4e341b0cc59a121860f224e6237156fad40b2cb1&var-config1=build-coq.8.19.0-timing&var-branch2=time%2Fcoq-8.19&var-commit2=2ccb19c5025a147047121188dd9b5b638b6143df&var-config2=build-coq.8.19.0-timing&var-metric=instructions&var-group=%28.%2A%29).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/540Add lemma `join_app`.2024-03-05T06:15:18ZRobbert KrebbersAdd lemma `join_app`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/539drop support for Coq 8.16 and 8.172024-02-07T14:50:35ZRalf Jungjung@mpi-sws.orgdrop support for Coq 8.16 and 8.17https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/538test on Coq 8.192024-02-02T10:50:57ZRalf Jungjung@mpi-sws.orgtest on Coq 8.19https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/537Adapt to https://github.com/coq/coq/pull/185902024-02-09T12:48:28ZPierre RouxAdapt to https://github.com/coq/coq/pull/18590Note that this requires dropping support for Coq 8.16 and 8.17.
Alternatively, we could implement a less ice intermediate solution that would still support 8.16.
Also note that there is a mention of 8.17 in numbers.v which I didn't han...Note that this requires dropping support for Coq 8.16 and 8.17.
Alternatively, we could implement a less ice intermediate solution that would still support 8.16.
Also note that there is a mention of 8.17 in numbers.v which I didn't handle here.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/536Adapt to https://github.com/coq/coq/pull/182242024-02-02T15:26:23ZPierre RouxAdapt to https://github.com/coq/coq/pull/18224This should be backward compatibleThis should be backward compatiblehttps://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/199