stdpp issueshttps://gitlab.mpi-sws.org/iris/stdpp/-/issues2020-05-25T18:34:47Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/issues/21More generic `FMap` type class that also supports collections2020-05-25T18:34:47ZRobbertMore generic `FMap` type class that also supports collectionsCurrently, `collection_map`, which turns a set (e.g. a `gset`) with elements of type `A` into a set with elements of type `B` cannot be an instance of the `FMap` type class. Let's take a look at the `FMap` class to see why:
```coq
Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
```
The problem here is that `M` has type `Type → Type` while `gset` has type `∀ (A : Type) ``{Countable A}, Type`. For most other set implementations we would have the same problem, e.g. if we were to have some kind of binary search trees, the type would be something like `∀ (A : Type) ``{TotalOrder A}, Type`.
In fact, our generic mapping operation for `FinCollection` has the following type:
```coq
Definition collection_map `{Elements A C, Singleton B D, Empty D, Union D}
(f : A → B) (X : C) : D :=
of_list (f <$> elements X).
```
I know this is also a problem in Haskell where the `fmap` operation on sets (which are implemented as trees, and thus needs to have access to the order) is not an instance of the `Functor` type class, so it may be worth taking a look at what they're doing.Currently, `collection_map`, which turns a set (e.g. a `gset`) with elements of type `A` into a set with elements of type `B` cannot be an instance of the `FMap` type class. Let's take a look at the `FMap` class to see why:
```coq
Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
```
The problem here is that `M` has type `Type → Type` while `gset` has type `∀ (A : Type) ``{Countable A}, Type`. For most other set implementations we would have the same problem, e.g. if we were to have some kind of binary search trees, the type would be something like `∀ (A : Type) ``{TotalOrder A}, Type`.
In fact, our generic mapping operation for `FinCollection` has the following type:
```coq
Definition collection_map `{Elements A C, Singleton B D, Empty D, Union D}
(f : A → B) (X : C) : D :=
of_list (f <$> elements X).
```
I know this is also a problem in Haskell where the `fmap` operation on sets (which are implemented as trees, and thus needs to have access to the order) is not an instance of the `Functor` type class, so it may be worth taking a look at what they're doing.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/7Improve support of simplify_option_eq (and simplify_map_eq?) for setoids2020-08-26T14:06:45ZRobbertImprove support of simplify_option_eq (and simplify_map_eq?) for setoidsBy @jung, see https://gitlab.mpi-sws.org/FP/iris-coq/issues/49.
> Some testcases:
> * <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d#59b3a9376af7e8ce6a745e02cef554707e5c7419_585_585>
> * in lambdaRust, lifetime/primitive.v, proof of `own_ilft_auth_agree`By @jung, see https://gitlab.mpi-sws.org/FP/iris-coq/issues/49.
> Some testcases:
> * <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d#59b3a9376af7e8ce6a745e02cef554707e5c7419_585_585>
> * in lambdaRust, lifetime/primitive.v, proof of `own_ilft_auth_agree`