stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2018-06-09T09:47:09Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/34add telescopic versions of the Coq quantifiers2018-06-09T09:47:09ZRalf Jungjung@mpi-sws.orgadd telescopic versions of the Coq quantifiershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/33add telescopes and a bit of theory about them2018-06-06T21:28:48ZRalf Jungjung@mpi-sws.orgadd telescopes and a bit of theory about themI think the basic definitions are pretty solid by now, though I am still fighting with making high-level telescope-based definitions that have nice pretty-printing.
Open question: Telescopes generalize hlists to the dependent case. Shou...I think the basic definitions are pretty solid by now, though I am still fighting with making high-level telescope-based definitions that have nice pretty-printing.
Open question: Telescopes generalize hlists to the dependent case. Should we get rid of hlists? Does anyone want to attempt porting hlist users over to telescopes? Restricting the dependency can actually be useful because it makes them easier to use.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/32introduce [default] as abbreviation for [from_option id], and use it2018-05-29T13:56:27ZRalf Jungjung@mpi-sws.orgintroduce [default] as abbreviation for [from_option id], and use itThere's some more uses in Iris, so this seems worth it. Over std++ and Iris together, the new default will actually be used *more often* than the old one I removed in !31.There's some more uses in Iris, so this seems worth it. Over std++ and Iris together, the new default will actually be used *more often* than the old one I removed in !31.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/31Remove the `default` notation for options2018-05-28T17:09:06ZRalf Jungjung@mpi-sws.orgRemove the `default` notation for optionsThe notation was parsing-only and all it did was reorder the arguments for
from_option. This creates just a needless divergence between what is written
and what is printed. Also, removing it frees the name for maybe introducing a
funct...The notation was parsing-only and all it did was reorder the arguments for
from_option. This creates just a needless divergence between what is written
and what is printed. Also, removing it frees the name for maybe introducing a
function or notation `default` with a type like `T -> option T -> T`.
I volunteer to fix all reverse deps that we know about.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/30Notations for relations with explicit type arguments2018-04-06T12:27:13ZRobbert KrebbersNotations for relations with explicit type argumentsWe discussed this already here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/134
The consensus was that `@{A}` would be a good fit, and would not cause conflicts. I implemented it here for hopefully all relations in std++: `=`,...We discussed this already here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/134
The consensus was that `@{A}` would be a good fit, and would not cause conflicts. I implemented it here for hopefully all relations in std++: `=`, `≡`, `⊆`, `⊂`, `⊑`, `##`, `∈`, `≡ₚ`, and adopted the code at many places to make use of these notations.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/29Add `seq_set_pred_disjoint`2020-04-10T09:46:35ZDan FruminAdd `seq_set_pred_disjoint`A sort of "dual" to `seq_set_S_disjoint`.A sort of "dual" to `seq_set_S_disjoint`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/27Add a `NoBackTrack` type class.2018-02-09T08:57:26ZRobbert KrebbersAdd a `NoBackTrack` type class.`NoBackTrack P` requires `P` but will never backtrack on it
once a result for `P` has been found.
See also https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112`NoBackTrack P` requires `P` but will never backtrack on it
once a result for `P` has been found.
See also https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/26A simple type class based canceler for natural numbers.2018-02-08T15:27:18ZRobbert KrebbersA simple type class based canceler for natural numbers.See also https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/109
Main question: where to put this? In `numbers.v` or in a separate file (as in this MR).See also https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/109
Main question: where to put this? In `numbers.v` or in a separate file (as in this MR).Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/25Add a Notation for `sn`: strongly normalizing.2018-01-13T22:46:59ZRobbert KrebbersAdd a Notation for `sn`: strongly normalizing.As requested by @jung in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/65
I made this a notation to avoid unfolding issues.As requested by @jung in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/65
I made this a notation to avoid unfolding issues.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.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/23Lattices notation for order, join, meet, top and bot.2017-12-05T19:14:14ZJacques-Henri JourdanLattices notation for order, join, meet, top and bot.They are needed both for `monPred` and the weak memory lifetime logic.They are needed both for `monPred` and the weak memory lifetime logic.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/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/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/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/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/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 Krebbers