stdpp issueshttps://gitlab.mpi-sws.org/iris/stdpp/issues2019-09-16T10:49:12Zhttps://gitlab.mpi-sws.org/iris/stdpp/issues/44`Hint Mode` for `QuoteLookup` and `Quote`2019-09-16T10:49:12ZDan Frumin`Hint Mode` for `QuoteLookup` and `Quote`Would it be beneficial to have `Hint Mode Lookup` annotations for input and output parameters?
https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/list.v#L4049Would it be beneficial to have `Hint Mode Lookup` annotations for input and output parameters?
https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/list.v#L4049https://gitlab.mpi-sws.org/iris/stdpp/issues/43Provide a total version of `!!` for finite maps and lists2019-09-16T10:51:10ZRobbertProvide a total version of `!!` for finite maps and listsIn case the type is inhabited, we can define a total version of the `lookup` function as follows:
```coq
l !!! i = match l !! i with Some x => x | None => inhabitant end
```
Having such a total lookup function is often convenient. It came up in some discussions with Arthur and also @dfrumin requested having such a feature recently.
I would like to implement this by defining a type class `LookupTotal` with its own notation (suggestion `!!!`) and then have instances and lemmas for all of the usual data structures like maps and lists. For maps, we can define an instance like the above. For lists I would like to have an instance that is not just `m !!! i = if m !! i is Some x then x else inhabitant` but something that is defined by structural recursion, so you can use it more easily in induction proofs.
We could furthermore provide an instance `LookupTotal (vec A n) (fin n) A` for vectors. This operation is always total, regardless of whether `A` is inhabited. Note that we already use the notation `!!!` for vectors, so generalizing it to the type class based version as proposed here makes sense.In case the type is inhabited, we can define a total version of the `lookup` function as follows:
```coq
l !!! i = match l !! i with Some x => x | None => inhabitant end
```
Having such a total lookup function is often convenient. It came up in some discussions with Arthur and also @dfrumin requested having such a feature recently.
I would like to implement this by defining a type class `LookupTotal` with its own notation (suggestion `!!!`) and then have instances and lemmas for all of the usual data structures like maps and lists. For maps, we can define an instance like the above. For lists I would like to have an instance that is not just `m !!! i = if m !! i is Some x then x else inhabitant` but something that is defined by structural recursion, so you can use it more easily in induction proofs.
We could furthermore provide an instance `LookupTotal (vec A n) (fin n) A` for vectors. This operation is always total, regardless of whether `A` is inhabited. Note that we already use the notation `!!!` for vectors, so generalizing it to the type class based version as proposed here makes sense.https://gitlab.mpi-sws.org/iris/stdpp/issues/42Inconsistent notations for Haskell-like partially applied operators2019-09-08T09:35:08ZRobbertInconsistent notations for Haskell-like partially applied operatorsWe currently have notations like:
```coq
Notation "( m !!)" := (λ i, m !! i) (only parsing) : stdpp_scope.
Notation "(!! i )" := (lookup i) (only parsing) : stdpp_scope.
Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : stdpp_scope.
```
Some of these notations include a period, and some don't. I think at some point I started to include the period because I ran into some parsing ambiguities, so I think we should do that for **all** such notations.
@wmansky confirmed this problem. When combining VST and std++ the `(!! i )` notation causes problems, because VST uses `!!` also as a prefix notation.
I don't think it's strange to use a notation as both an infix and prefix, the most common example is negation `-`. So IMHO we should fix this.
I think the impact of the proposed change is relatively small: a.) these notations are hardly used b.) most of them can easily be ported using a `sed` script.We currently have notations like:
```coq
Notation "( m !!)" := (λ i, m !! i) (only parsing) : stdpp_scope.
Notation "(!! i )" := (lookup i) (only parsing) : stdpp_scope.
Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : stdpp_scope.
```
Some of these notations include a period, and some don't. I think at some point I started to include the period because I ran into some parsing ambiguities, so I think we should do that for **all** such notations.
@wmansky confirmed this problem. When combining VST and std++ the `(!! i )` notation causes problems, because VST uses `!!` also as a prefix notation.
I don't think it's strange to use a notation as both an infix and prefix, the most common example is negation `-`. So IMHO we should fix this.
I think the impact of the proposed change is relatively small: a.) these notations are hardly used b.) most of them can easily be ported using a `sed` script.https://gitlab.mpi-sws.org/iris/stdpp/issues/40Provide a better `inversion` tactic2019-08-24T17:10:36ZRobbertProvide a better `inversion` tacticSee the discussion [here](https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/87#note_39649): `inversion_clear` often doesn't work (it produces too weak goals).
[CompCert](http://compcert.inria.fr/doc/html/compcert.lib.Coqlib.html) fixes the issue by providing the following tactic:
```coq
Ltac inv H := inversion H; clear H; subst.
```
Maybe std++ should provide a similar tactic, and replace all occurrences of `inversion` and `inversion_clear` with that tactic. We probably want to improve some aspects:
- Include a version with an intro pattern to name the results.
- Don't just perform `subst`, but only substitute the equalities generated by `inversion`.
- Allow `H` to be an arbitrary term instead of just an `ident`.See the discussion [here](https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/87#note_39649): `inversion_clear` often doesn't work (it produces too weak goals).
[CompCert](http://compcert.inria.fr/doc/html/compcert.lib.Coqlib.html) fixes the issue by providing the following tactic:
```coq
Ltac inv H := inversion H; clear H; subst.
```
Maybe std++ should provide a similar tactic, and replace all occurrences of `inversion` and `inversion_clear` with that tactic. We probably want to improve some aspects:
- Include a version with an intro pattern to name the results.
- Don't just perform `subst`, but only substitute the equalities generated by `inversion`.
- Allow `H` to be an arbitrary term instead of just an `ident`.https://gitlab.mpi-sws.org/iris/stdpp/issues/39Create list of tactics provided by std++2019-07-04T13:23:52ZRobbertCreate list of tactics provided by std++E.g. `set_solver`, `naive_solver`, `simplify_option_eq`, etc.
As suggested by @msammler in https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/78#note_38387E.g. `set_solver`, `naive_solver`, `simplify_option_eq`, etc.
As suggested by @msammler in https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/78#note_38387https://gitlab.mpi-sws.org/iris/stdpp/issues/38Add a test for solve_proper on a unary function2019-07-02T21:35:35ZRalf Jungjung@mpi-sws.orgAdd a test for solve_proper on a unary functionSee https://gitlab.mpi-sws.org/iris/stdpp/commit/3b8eed3c6cf6af9749c17b6a7f553054c664a55eSee https://gitlab.mpi-sws.org/iris/stdpp/commit/3b8eed3c6cf6af9749c17b6a7f553054c664a55ehttps://gitlab.mpi-sws.org/iris/stdpp/issues/37Extend `solve_proper` to better handle HO functions2019-08-22T19:17:21ZRobbertExtend `solve_proper` to better handle HO functionsSee the report here: https://gitlab.mpi-sws.org/iris/iris/issues/249
I ran into a problem that's related in @dfrumin's ReLoC https://gitlab.mpi-sws.org/iris/reloc/commit/3266aca9e46999500a8b0cfaf6d5a461eddc7b15#3a3f55df8c140d39b939dfa9625c8ff87b47c094_263_261See the report here: https://gitlab.mpi-sws.org/iris/iris/issues/249
I ran into a problem that's related in @dfrumin's ReLoC https://gitlab.mpi-sws.org/iris/reloc/commit/3266aca9e46999500a8b0cfaf6d5a461eddc7b15#3a3f55df8c140d39b939dfa9625c8ff87b47c094_263_261RobbertRobberthttps://gitlab.mpi-sws.org/iris/stdpp/issues/35Unify case_bool_decide / case_decide2019-06-22T08:54:15ZRalf Jungjung@mpi-sws.orgUnify case_bool_decide / case_decideWe have `case_bool_decide` and `case_decide`, but things still get annoying when the goal contains both a `decide` and a `bool_decide` for the same proposition: you have to either destruct twice or manually `rewrite /bool_decide_decie`. See e.g. [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/274#note_37658).
Maybe the two tactics should be unified by just making `case_decide` start with `rewrite /bool_decide_decie` or so.We have `case_bool_decide` and `case_decide`, but things still get annoying when the goal contains both a `decide` and a `bool_decide` for the same proposition: you have to either destruct twice or manually `rewrite /bool_decide_decie`. See e.g. [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/274#note_37658).
Maybe the two tactics should be unified by just making `case_decide` start with `rewrite /bool_decide_decie` or so.https://gitlab.mpi-sws.org/iris/stdpp/issues/32Map singleton notation overlaps with Coq record syntax2019-06-10T13:34:43ZRalf Jungjung@mpi-sws.orgMap singleton notation overlaps with Coq record syntaxSee https://gitlab.mpi-sws.org/iris/iris/merge_requests/249#note_36760: `{[ i := x ]}` might be either a singleton map or constructing a record where field `i` has value `x`.See https://gitlab.mpi-sws.org/iris/iris/merge_requests/249#note_36760: `{[ i := x ]}` might be either a singleton map or constructing a record where field `i` has value `x`.https://gitlab.mpi-sws.org/iris/stdpp/issues/31Addition is only declared as `Commutative` in iris2019-06-14T16:05:58ZPaolo G. GiarrussoAddition is only declared as `Commutative` in irisJust learned that addition on naturals is not "commutative" for stdpp, but only in Iris. Take the following proof:
```coq
Require Import iris.algebra.base iris.algebra.cmra.
Lemma foo i j: i + j = j + i. Proof. rewrite {1}[_ + _]comm //. Qed.
```
That works, but the instance found for `Commutative` is `@cmra_comm natR`.
But if we load the whole stdpp (and algebra.base to get ssreflect), no instance is found. After:
```coq
Require Import iris.algebra.base stdpp.prelude.
Lemma foo i j: i + j = j + i. Proof. Fail rewrite {1}[_ + _]comm //. Qed.
```
we get:
```
The command has indeed failed with message:
Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
pattern (i + j) does not match LHS of comm
```
I'm creating an issue because this instance might have been omitted on purpose, and code might be relying on its absence accidentally. But I expect this isn't for performance reasons — or the instance we currently get would already be a problem.
Instance `@cmra_assoc natR` might cause similar concerns, but I haven't checked; other instances might as well, but it's less clear how.
I also wonder whether something more should be `Typeclasses Opaque` (say, `nat_op`?), to avoid this instance triggering accidentally, tho I'm not sure that's possible.Just learned that addition on naturals is not "commutative" for stdpp, but only in Iris. Take the following proof:
```coq
Require Import iris.algebra.base iris.algebra.cmra.
Lemma foo i j: i + j = j + i. Proof. rewrite {1}[_ + _]comm //. Qed.
```
That works, but the instance found for `Commutative` is `@cmra_comm natR`.
But if we load the whole stdpp (and algebra.base to get ssreflect), no instance is found. After:
```coq
Require Import iris.algebra.base stdpp.prelude.
Lemma foo i j: i + j = j + i. Proof. Fail rewrite {1}[_ + _]comm //. Qed.
```
we get:
```
The command has indeed failed with message:
Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
pattern (i + j) does not match LHS of comm
```
I'm creating an issue because this instance might have been omitted on purpose, and code might be relying on its absence accidentally. But I expect this isn't for performance reasons — or the instance we currently get would already be a problem.
Instance `@cmra_assoc natR` might cause similar concerns, but I haven't checked; other instances might as well, but it's less clear how.
I also wonder whether something more should be `Typeclasses Opaque` (say, `nat_op`?), to avoid this instance triggering accidentally, tho I'm not sure that's possible.https://gitlab.mpi-sws.org/iris/stdpp/issues/21More generic `FMap` type class that also supports collections2019-02-20T21:59:08ZRobbertMore 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/19What about `Universe Minimization ToSet`?2018-06-09T11:59:31ZRalf Jungjung@mpi-sws.orgWhat about `Universe Minimization ToSet`?Follow-up from https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/34/diffs#note_28380 :
@janno:
> The problem only really comes up when you build more layers of definitions on top of this. At some point, Coq will decide that you don't really need all those universes and `Set` is good enough for some of them. (But it's never good enough..)
>
> Although maybe this might really not be a problem here since this would be an issue in other universe polymorphic files, not this one. In any case, if you ever wanted to add more definitions to this file, you might still benefit from unsetting minimization.
@robbertkrebbers
> In that base, it may make more sense to add it globally to `base.v` ?
> Maybe we should investigate why this option is not enabled by default.
@jung
> Probably performance? Minimizing to `Set` reduces the universe graph.
@robbertkrebbers
> @amintimany Could you give us some advice here?Follow-up from https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/34/diffs#note_28380 :
@janno:
> The problem only really comes up when you build more layers of definitions on top of this. At some point, Coq will decide that you don't really need all those universes and `Set` is good enough for some of them. (But it's never good enough..)
>
> Although maybe this might really not be a problem here since this would be an issue in other universe polymorphic files, not this one. In any case, if you ever wanted to add more definitions to this file, you might still benefit from unsetting minimization.
@robbertkrebbers
> In that base, it may make more sense to add it globally to `base.v` ?
> Maybe we should investigate why this option is not enabled by default.
@jung
> Probably performance? Minimizing to `Set` reduces the universe graph.
@robbertkrebbers
> @amintimany Could you give us some advice here?https://gitlab.mpi-sws.org/iris/stdpp/issues/11Notation for type class logic connectives as `TCAnd`, `TCOr`, ...2018-02-20T00:53:27ZRobbertNotation for type class logic connectives as `TCAnd`, `TCOr`, ...In order to use them in a more readable manner, it would be good to have the usual notations for these in a specific scope.In order to use them in a more readable manner, it would be good to have the usual notations for these in a specific scope.https://gitlab.mpi-sws.org/iris/stdpp/issues/10Inconsistent `RewriteRelation` instances2019-07-03T13:30:51ZRobbertInconsistent `RewriteRelation` instancesWe currently have just the following instance (add by @jjourdan):
```coq
Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).
```
No such instances exist for other binary relations.
In order to make the Ssrreflect `rewrite` tactic to work for `⊑`, we need such an instance. It turns out that for `equiv` we do not need it, since the Coq standard library contains the following instance:
```
equivalence_rewrite_relation:
∀ (A : Type) (eqA : relation A), Equivalence eqA → RewriteRelation eqA
```
Now there are some solutions:
- Add `RewriteRelation` instances for all operational type classes for binary operations, e.g. `subseteq`.
- Add a `RewriteRelation` instance for any `PreOrder`.
- The latter, but by making an pull request for the Coq standard library.We currently have just the following instance (add by @jjourdan):
```coq
Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).
```
No such instances exist for other binary relations.
In order to make the Ssrreflect `rewrite` tactic to work for `⊑`, we need such an instance. It turns out that for `equiv` we do not need it, since the Coq standard library contains the following instance:
```
equivalence_rewrite_relation:
∀ (A : Type) (eqA : relation A), Equivalence eqA → RewriteRelation eqA
```
Now there are some solutions:
- Add `RewriteRelation` instances for all operational type classes for binary operations, e.g. `subseteq`.
- Add a `RewriteRelation` instance for any `PreOrder`.
- The latter, but by making an pull request for the Coq standard library.https://gitlab.mpi-sws.org/iris/stdpp/issues/9Make more consistent use of coqdoc for web doc2019-06-17T08:18:06ZRalf Jungjung@mpi-sws.orgMake more consistent use of coqdoc for web docIt would be nice to have some form of web doc for std++ (and, if this works, maybe even for Iris?). The simplest thing I can imagine is letting the CI run coqtop and putting that somewhere.It would be nice to have some form of web doc for std++ (and, if this works, maybe even for Iris?). The simplest thing I can imagine is letting the CI run coqtop and putting that somewhere.https://gitlab.mpi-sws.org/iris/stdpp/issues/8`f_equiv` with different functions in head position produces a Leibniz equality2019-08-22T19:17:21ZRobbert`f_equiv` with different functions in head position produces a Leibniz equality```coq
From iris Require Import ofe.
Lemma foo {A C : ofeT} {B : Type} (f g : A -n> B -c> C) (x : A) (y : B) n :
f ≡{n}≡ g → f x y ≡{n}≡ g x y.
Proof.
intros. f_equiv.
```
This results in `f = g`, which cannot be proven.```coq
From iris Require Import ofe.
Lemma foo {A C : ofeT} {B : Type} (f g : A -n> B -c> C) (x : A) (y : B) n :
f ≡{n}≡ g → f x y ≡{n}≡ g x y.
Proof.
intros. f_equiv.
```
This results in `f = g`, which cannot be proven.RobbertRobberthttps://gitlab.mpi-sws.org/iris/stdpp/issues/7Improve support of simplify_option_eq (and simplify_map_eq?) for setoids2019-02-20T22:00:27ZRobbertImprove 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`https://gitlab.mpi-sws.org/iris/stdpp/issues/6`done` loops because it repeatedly applies `split`2017-11-01T10:12:51ZRobbert`done` loops because it repeatedly applies `split`For example:
```coq
From stdpp Require Import streams.
Lemma foo (x y : stream nat) : x ≡ y.
Proof. done. (* loops *)
```
Is there any sensible way of only letting it apply `split` for the case of inductive types (rather than also coinductive types)?
Or are there alternatives to avoid this?For example:
```coq
From stdpp Require Import streams.
Lemma foo (x y : stream nat) : x ≡ y.
Proof. done. (* loops *)
```
Is there any sensible way of only letting it apply `split` for the case of inductive types (rather than also coinductive types)?
Or are there alternatives to avoid this?https://gitlab.mpi-sws.org/iris/stdpp/issues/5Something in std++ enables implicit generalization of instances2017-11-14T00:14:05ZRalf Jungjung@mpi-sws.orgSomething in std++ enables implicit generalization of instancesThe following script fails, as I would expect because `k` is not bound:
```
Class Even (n: nat) := even : exists m, 2 * m = n.
Global Instance even_even: Even (2*k).
```
However, the following script works:
```
From stdpp Require Export prelude.
Class Even (n: nat) := even : exists m, 2 * m = n.
Global Instance even_even: Even (2*k).
```The following script fails, as I would expect because `k` is not bound:
```
Class Even (n: nat) := even : exists m, 2 * m = n.
Global Instance even_even: Even (2*k).
```
However, the following script works:
```
From stdpp Require Export prelude.
Class Even (n: nat) := even : exists m, 2 * m = n.
Global Instance even_even: Even (2*k).
```https://gitlab.mpi-sws.org/iris/stdpp/issues/2Big ops and lattices in stdpp?2019-02-17T17:11:30ZHai DangBig ops and lattices in stdpp?Hi,
I currently have a meet-semilattice, and I want to show that if a map `m1` is "less" than `m2`, in the sense that `m1`'s values are pointwise less than those of `m2`'s by the lattice order, then the meet of `m1` values is also less than that of `m2`. I don't see a clean way to prove this, as I define the meet as a fold over the list of values.
I'd like a more structure way to define the meet as big ops in Iris. Is is possible to generalize big ops so that they need not depend on ofe's?
Also, I believe lattices would be useful enough to be in stdpp, although our development of them in iGPS is a bit under-developed.
What do you think?Hi,
I currently have a meet-semilattice, and I want to show that if a map `m1` is "less" than `m2`, in the sense that `m1`'s values are pointwise less than those of `m2`'s by the lattice order, then the meet of `m1` values is also less than that of `m2`. I don't see a clean way to prove this, as I define the meet as a fold over the list of values.
I'd like a more structure way to define the meet as big ops in Iris. Is is possible to generalize big ops so that they need not depend on ofe's?
Also, I believe lattices would be useful enough to be in stdpp, although our development of them in iGPS is a bit under-developed.
What do you think?