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/560Rename `X_length` into `length_X`.2024-08-14T16:56:06ZRobbert KrebbersRename `X_length` into `length_X`.This follows https://github.com/coq/coq/pull/18564
This closes #213
We didn't include our own copies of `app_length` and `seq_length`, but used those from the standard library. To make sure we can use them (without deprecation warnings...This follows https://github.com/coq/coq/pull/18564
This closes #213
We didn't include our own copies of `app_length` and `seq_length`, but used those from the standard library. To make sure we can use them (without deprecation warnings) until support for Coq 8.19 is dropped, I included our own copies for the transition period. This was also suggested by @tchajed in #213.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/559Use gmake for BSD systems2024-07-31T17:00:23ZYiyun LiuUse gmake for BSD systemsThis PR modifies the `make-package` script so it runs on systems whose default `make` executable is BSD Make rather than GNU Make. It checks the os type and decides whether to run `gmake` or `make`. This is exactly how `opam` determines ...This PR modifies the `make-package` script so it runs on systems whose default `make` executable is BSD Make rather than GNU Make. It checks the os type and decides whether to run `gmake` or `make`. This is exactly how `opam` determines which `make` executable to use.
I also changed the script to use `sh` instead of `bash` because `make-package` doesn't seem to depend on bash-specific features and sh has a more standard path.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/558docs: quick typo fixes2024-07-19T19:16:21ZSanjit Bhatdocs: quick typo fixeshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/557docs(gmap): add galina escaping2024-07-19T13:47:03ZSanjit Bhatdocs(gmap): add galina escapingThis fixes #211. I checked this locally with coqdoc.This fixes #211. I checked this locally with coqdoc.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/556Fix convention in gitlab config.2024-06-17T08:34:27ZRodolphe LepigreFix convention in gitlab config.Something I messed up in the dune MR.Something I messed up in the dune MR.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555Don't constraint template polymorphic universes of list and option redefining `MBind` and related typeclasses2024-06-10T08:07:46ZMichael SammlerDon't constraint template polymorphic universes of list and option redefining `MBind` and related typeclassesThis is an idea how to fix https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 and #207 . Since `M` never appears unapplied, it should not introduce the universe constraints. Note that the universe of `gmap` and `gset` and similar remain c...This is an idea how to fix https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 and #207 . Since `M` never appears unapplied, it should not introduce the universe constraints. Note that the universe of `gmap` and `gset` and similar remain constrained due to the `MonadSet` and `FinMap` typeclasses.
In particular, with
```
Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
Global Instance x : MBind list.
Admitted.
Print Universes.
```
one gets the contraint `list.u0 = MBind.u0`.
But with
```
Class MBind' (A MA MB : Type) := mbind : (A → MB) → MA → MB.
Notation MBind M := (∀ A B, MBind' A (M A) (M B)).
Global Instance x : MBind list.
Admitted.
Print Universes.
```
one only gets the constraints
```
x.u0 <= list.u0
x.u0 <= MBind'.u0
x.u0 <= MBind'.u1
x.u1 <= list.u0
x.u1 <= MBind'.u2
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/554Prepare for https://github.com/coq/coq/pull/190592024-06-04T14:19:04ZPierre RouxPrepare for https://github.com/coq/coq/pull/19059Prepare for next version number bump in Coq.
Could you please encode the test in the other direction to avoid having to do that kind of PR again for next Coq version (no hurry, this can be done in the next six months).Prepare for next version number bump in Coq.
Could you please encode the test in the other direction to avoid having to do that kind of PR again for next Coq version (no hurry, this can be done in the next six months).