stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2017-11-18T14:36:48Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/19Factor out solve_proper_prepare2017-11-18T14:36:48ZRalf Jungjung@mpi-sws.orgFactor out solve_proper_prepareThis helps when debugging solve_proper_core failures.This helps when debugging solve_proper_core failures.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/16Make `fmap` left associative.2017-11-12T20:40:10ZRobbert KrebbersMake `fmap` left associative.This follows the associativity in Haskell. So, something like
```coq
f <$> g <$> h
```
Is now parsed as:
```coq
(f <$> g) <$> h
```
Since the functor is a generalized form of function application, this also now also corresponds with ...This follows the associativity in Haskell. So, something like
```coq
f <$> g <$> h
```
Is now parsed as:
```coq
(f <$> g) <$> h
```
Since the functor is a generalized form of function application, this also now also corresponds with the associativity of function application, which is also left associative.
# Todo
What should be the level? It used to be at level 60, which was already an arbitrary choice. However, this has to be changed since that level (60) is right associative. I tentatively put it at level 61, which is totally arbitrary too.
Clearly, the level should be above list append and cons (`++` and `::`, which are both at level 60). Things like `f <$> xs ++ ys` should be parsed as `f <$> (xs ++ ys)`, similarly to what happens in Haskell. Are there other constraints? How should it interact with the monad notations (`>>=`, do notation, ...).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/17Use `stdpp_scope` for all notations.2017-11-11T00:05:12ZRobbert KrebbersUse `stdpp_scope` for all notations.A long time ago, `stdpp` was part of my C formalization, and as such, I used `C_scope` for all notations in the development. These days, the name of this scope totally makes no sense, and even confuses new users of the library, especiall...A long time ago, `stdpp` was part of my C formalization, and as such, I used `C_scope` for all notations in the development. These days, the name of this scope totally makes no sense, and even confuses new users of the library, especially now that the project has a project name (coq-stdpp)
I thus propose to rename `C_scope` into `stdpp_scope` and the scope delimiter `%C` into `%stdpp`. It should be very trivial to fix this in all dependencies; we should just provide a `sed` script.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/15Provide a pretty-printer for [nat].2017-11-29T17:44:35ZGhost UserProvide a pretty-printer for [nat].Pretty-print nat; this simply reduced to the N pretty printer.Pretty-print nat; this simply reduced to the N pretty printer.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/14Minor documentation fixes2017-10-31T11:45:05ZGhost UserMinor documentation fixesCorrected typeclass names in some of the documentation.Corrected typeclass names in some of the documentation.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/12Notation for disjointness: replace ⊥ with ##, so that ⊥ can be used for bottom.2017-10-29T15:10:54ZJacques-Henri JourdanNotation for disjointness: replace ⊥ with ##, so that ⊥ can be used for bottom.As discussed in #3.
I completely removed support for the old notation. Should I provide a deprecated support for maintaining compatibility ?As discussed in #3.
I completely removed support for the old notation. Should I provide a deprecated support for maintaining compatibility ?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/9Add more lemmas for gmap uncurry2017-10-27T16:45:34ZHai DangAdd more lemmas for gmap uncurryhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/7Add more properties of intersection_with for fin_maps2017-10-27T14:20:07ZHai DangAdd more properties of intersection_with for fin_mapshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/8Add lemma lookup_gmap_uncurry_empty2017-10-17T09:24:57ZJacques-Henri JourdanAdd lemma lookup_gmap_uncurry_emptyThis lemma is needed to completely characterize what gmap_uncurry is.This lemma is needed to completely characterize what gmap_uncurry is.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/5Some lemmas about `difference` and `delete`2017-10-28T15:35:55ZDan FruminSome lemmas about `difference` and `delete`Those are the lemmas I used in iris-logrel.Those are the lemmas I used in iris-logrel.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/4Add countability for Q, Qc, and Qp2017-08-05T18:53:31ZHai DangAdd countability for Q, Qc, and QpAddded countability proofs for Q, Qc and Qp.Addded countability proofs for Q, Qc and Qp.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/3Some map_zip/map_zip_with properties.2017-06-26T11:12:37ZDan FruminSome map_zip/map_zip_with properties.These are some properties of `map_zip_with` that I am using so far.
Perhaps you want me to port the whole thing first, to see what other functions/lemmas will I need?These are some properties of `map_zip_with` that I am using so far.
Perhaps you want me to port the whole thing first, to see what other functions/lemmas will I need?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/2add target html and gallinahtml2017-02-23T11:54:53ZBenoit Viguieradd target html and gallinahtmlalso add html folder to .gitignore so generated doc is not added to the repoalso add html folder to .gitignore so generated doc is not added to the repohttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/1update build system and README2017-02-07T13:48:35ZRalf Jungjung@mpi-sws.orgupdate build system and READMEWe should have a release on opam ASAP so that we can point to it in the README. We could also have a "dev" version on opam for people that want to depend on that one, but not use our crazy opam.pins hack.We should have a release on opam ASAP so that we can point to it in the README. We could also have a "dev" version on opam for people that want to depend on that one, but not use our crazy opam.pins hack.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/553Misc lemma for sets and `gset_to_gmap`2024-05-28T10:04:05ZLéo StefanescoMisc lemma for sets and `gset_to_gmap`Upstreamed from the Aneris project.Upstreamed from the Aneris project.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/549Adapt to https://github.com/coq/coq/pull/189282024-04-16T12:04:57ZPierre RouxAdapt to https://github.com/coq/coq/pull/18928Adapt output tests to upstream PR on Coq https://github.com/coq/coq/pull/18928Adapt output tests to upstream PR on Coq https://github.com/coq/coq/pull/18928https://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.