stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2017-02-07T13:48:35Zhttps://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/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/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/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/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/11Resolve "Disjoint uses ⊥ (U+22A5 -- UP TACK) but should use ⟂ (U+27C2 -- PERPENDICULAR)"2017-10-27T12:29:49ZJacques-Henri JourdanResolve "Disjoint uses ⊥ (U+22A5 -- UP TACK) but should use ⟂ (U+27C2 -- PERPENDICULAR)"Closes #3Closes #3https://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/6Add filter for gmap2017-10-27T14:49:51ZHai DangAdd filter for gmapA filter for (M : gmap K A) creates a submap of M whose (key,value) pairs satisfy the filter predicate (P : K * A → Prop).A filter for (M : gmap K A) creates a submap of M whose (key,value) pairs satisfy the filter predicate (P : K * A → Prop).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/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/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/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/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/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/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/18Pattern matching notation for monadic binds2017-11-22T18:00:36ZRobbert KrebbersPattern matching notation for monadic bindsThis gets rid of the old hack to have specific notations for pairs up to a fixed arity, and moreover allows to do fancy things like:
```
Record test := Test { t1 : nat; t2 : nat }.
Definition foo (x : option test) : option nat :=
...This gets rid of the old hack to have specific notations for pairs up to a fixed arity, and moreover allows to do fancy things like:
```
Record test := Test { t1 : nat; t2 : nat }.
Definition foo (x : option test) : option nat :=
''(Test a1 a2) ← x;
Some a1.
```
There are some problems, however:
- It conflicts with Coq's notation `' x` for `Zpos x`. Fortunately, the breakage is in the right direction: the proposed monadic notation breaks Coq's `' x`. Furthermore, I believe said notation should be removed from Coq, see https://github.com/coq/coq/pull/6155
- It breaks backwards compatibility. Since Coq only allows to use binders in recursive notations, the notation must start with at least one symbol, for which I picked `'`. As such, this means we need a double `'`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/20Allow compiling against "dev" version of Coq2017-11-29T12:25:56ZRalf Jungjung@mpi-sws.orgAllow compiling against "dev" version of CoqThis matches e.g. Iris allowing a "dev" version of std++: You can install a
"dev" version to test stuff, but then you are responsible for making sure that
these versions actually work together. We rely on that when testing things
aga...This matches e.g. Iris allowing a "dev" version of std++: You can install a
"dev" version to test stuff, but then you are responsible for making sure that
these versions actually work together. We rely on that when testing things
against Iris master every night, for which purpose we install Iris master as
"dev" version.
Cc @jjourdan who, IIRC, argue for removing the `dev` version some time ago.
If we accept this here, I will send similar patches to (some of?) our other projects.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/21Make x.1, x.2 notation compatible with ssrfun.2017-11-29T15:10:24ZDavid SwaseyMake x.1, x.2 notation compatible with ssrfun.Enable one to import both stdpp's base and ssrfun.
Note that (f x.1) now parses as (f (fst x)) rather than (fst (f x)).
(This change affects one proof in Iris.)Enable one to import both stdpp's base and ssrfun.
Note that (f x.1) now parses as (f (fst x)) rather than (fst (f x)).
(This change affects one proof in Iris.)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/24typeclass comments2017-12-05T19:13:59ZRalf Jungjung@mpi-sws.orgtypeclass commentsI only now understood why `Equiv` is called the way it is. Let's document that.I only now understood why `Equiv` is called the way it is. Let's document that.