stdpp issueshttps://gitlab.mpi-sws.org/iris/stdpp/-/issues2020-05-25T18:34:46Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/issues/66Better documentation for sets2020-05-25T18:34:46ZTej ChajedBetter documentation for setsDue to the proliferation of type classes related to sets, finding things is extremely difficult. I almost convinced myself std++ doesn't have `list_to_set` (it's in base and doesn't depend on `Set_` or `SemiSet`, so my searches all failed) or `set_map` (it's not an instance of `FMap` due to #21).
It would be good to provide a short introduction to the overall structure of sets in std++, including the typeclasses, notations, and important instances.Due to the proliferation of type classes related to sets, finding things is extremely difficult. I almost convinced myself std++ doesn't have `list_to_set` (it's in base and doesn't depend on `Set_` or `SemiSet`, so my searches all failed) or `set_map` (it's not an instance of `FMap` due to #21).
It would be good to provide a short introduction to the overall structure of sets in std++, including the typeclasses, notations, and important instances.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/65Weird unfolding by `cbn` with `gset`2020-05-25T07:01:31ZRodolphe LepigreWeird unfolding by `cbn` with `gset`Consider the following code.
```coq
From stdpp Require Import gmap.
Goal ∀ (k : Z) (s : gset Z), {[k]} ∪ s = s ∪ {[k]} ∪ {[k]}.
cbn. (* <-- weird unfolding. *)
```
Evaluating the `cbn` tactic turns the goal into:
```
∀ (k : Z) (s : gset Z), (let (m2) := s in {| mapset.mapset_car := {[k := ()]} ∪ m2 |}) = s ∪ {[k]} ∪ {[k]}
```
which is not what I was expecting. Why does this unfolding take place?Consider the following code.
```coq
From stdpp Require Import gmap.
Goal ∀ (k : Z) (s : gset Z), {[k]} ∪ s = s ∪ {[k]} ∪ {[k]}.
cbn. (* <-- weird unfolding. *)
```
Evaluating the `cbn` tactic turns the goal into:
```
∀ (k : Z) (s : gset Z), (let (m2) := s in {| mapset.mapset_car := {[k := ()]} ∪ m2 |}) = s ∪ {[k]} ∪ {[k]}
```
which is not what I was expecting. Why does this unfolding take place?https://gitlab.mpi-sws.org/iris/stdpp/-/issues/64Further issues with in-Coq computation for pmap and gmap2020-05-20T14:58:06ZPaolo G. GiarrussoFurther issues with in-Coq computation for pmap and gmapThese issues are discussed on Mattermost starting at https://mattermost.mpi-sws.org/iris/pl/o9tme6imrfdtf8chhwi6fr1kor.
Basically, reducing gmaps will also reduce their well-formedness checks; I expect continuing the work in !106 and sealing well-formedness predicates would avoid the issue.
Of most interest are [these comments](https://mattermost.mpi-sws.org/iris/pl/t4aehh1izpyg9yiqtu6z3mgbcy):
> Let me point out that computing gmap_wf_aux takes time linear in the sum of key sizes, and that plausibly explains the performance numbers that I saw back then, and the problem Greg mentions with large keys. Meanwhile, Pmap_wf has a smaller variant of the same problem (its cost does not depend on key sizes).
and Robbert's [idea for Pmap](https://mattermost.mpi-sws.org/iris/pl/ftex8frjr3r4ue8cccfa6xqwyc):
> Also, at some point I looked into a more intrinsic representation of finite maps that ensures the well-formedness condition without a Sigma-type. I have never finished that, but if someone wants to help working on this, feel free to get in touch.
The code is in https://mattermost.mpi-sws.org/iris/pl/6mkua571y7g35cqndt455y74rc; I expect some sealing would still be needed.These issues are discussed on Mattermost starting at https://mattermost.mpi-sws.org/iris/pl/o9tme6imrfdtf8chhwi6fr1kor.
Basically, reducing gmaps will also reduce their well-formedness checks; I expect continuing the work in !106 and sealing well-formedness predicates would avoid the issue.
Of most interest are [these comments](https://mattermost.mpi-sws.org/iris/pl/t4aehh1izpyg9yiqtu6z3mgbcy):
> Let me point out that computing gmap_wf_aux takes time linear in the sum of key sizes, and that plausibly explains the performance numbers that I saw back then, and the problem Greg mentions with large keys. Meanwhile, Pmap_wf has a smaller variant of the same problem (its cost does not depend on key sizes).
and Robbert's [idea for Pmap](https://mattermost.mpi-sws.org/iris/pl/ftex8frjr3r4ue8cccfa6xqwyc):
> Also, at some point I looked into a more intrinsic representation of finite maps that ensures the well-formedness condition without a Sigma-type. I have never finished that, but if someone wants to help working on this, feel free to get in touch.
The code is in https://mattermost.mpi-sws.org/iris/pl/6mkua571y7g35cqndt455y74rc; I expect some sealing would still be needed.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/63Non-canonical FinMap?2020-05-13T03:46:07ZGregory MalechaNon-canonical FinMap?Is there any interest in generalizing FinMap to use a setoid equality? I have a non-canonical finite map that I need to use, but I can't leverage lemmas built from the `FinMap` class.Is there any interest in generalizing FinMap to use a setoid equality? I have a non-canonical finite map that I need to use, but I can't leverage lemmas built from the `FinMap` class.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/62Add Countable instance for `Byte.byte`2020-05-12T17:53:49ZTej ChajedAdd Countable instance for `Byte.byte`Once support for Coq v8.9 is dropped, resurrect !155 and add a `Countable` instance for `Coq.Init.Byte.byte`.Once support for Coq v8.9 is dropped, resurrect !155 and add a `Countable` instance for `Coq.Init.Byte.byte`.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/61solve_ndisj doesn't work for goals of the form `∅ ## ↑N`2020-05-06T13:38:01ZDan Fruminsolve_ndisj doesn't work for goals of the form `∅ ## ↑N`However, `set_solver` works in this case.
Minimal example:
```coq
From stdpp Require Import namespaces coPset.
Goal (∅ : coPset) ## ↑(nroot.@0).
Proof. set_solver. (* solve_ndisj does not work *) Qed.
Goal (↑(nroot.@1) : coPset) ## ↑(nroot.@0).
Proof. solve_ndisj. (* set_solver. does not work *) Qed.
```However, `set_solver` works in this case.
Minimal example:
```coq
From stdpp Require Import namespaces coPset.
Goal (∅ : coPset) ## ↑(nroot.@0).
Proof. set_solver. (* solve_ndisj does not work *) Qed.
Goal (↑(nroot.@1) : coPset) ## ↑(nroot.@0).
Proof. solve_ndisj. (* set_solver. does not work *) Qed.
```https://gitlab.mpi-sws.org/iris/stdpp/-/issues/60Notation for list with fixed type2020-05-04T08:00:54ZMichael SammlerNotation for list with fixed typeI am using the following notations in RefinedC:
```coq
Notation "'[@{' A '}' x ; y ; .. ; z ]" := (@cons A x (@cons A y .. (@cons A z (@nil A)) ..)) (only parsing) : list_scope.
Notation "'[@{' A '}' x ]" := (@cons A x nil) (only parsing) : list_scope.
Notation "'[@{' A '}' ]" := (@nil A) (only parsing) : list_scope.
```
Would it be useful to upstream them to stdpp?I am using the following notations in RefinedC:
```coq
Notation "'[@{' A '}' x ; y ; .. ; z ]" := (@cons A x (@cons A y .. (@cons A z (@nil A)) ..)) (only parsing) : list_scope.
Notation "'[@{' A '}' x ]" := (@cons A x nil) (only parsing) : list_scope.
Notation "'[@{' A '}' ]" := (@nil A) (only parsing) : list_scope.
```
Would it be useful to upstream them to stdpp?Michael SammlerMichael Sammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/issues/59Associativity of insert notation is awkard: `<[ k := v ]> m`2020-04-03T07:02:50ZGregory MalechaAssociativity of insert notation is awkard: `<[ k := v ]> m`Because the notation parses only as `<[ k := v ]>` as a function, you can't chain them together without parens.
```coq
<[ k := v ]> <[ k' := v' ]> m
```
doesn't parse, you need parentheses. How much of a problem would it be to extend the notation to `<[ k := v ]> m` that is right associative? Are there a lot of users that use this as partial application?Because the notation parses only as `<[ k := v ]>` as a function, you can't chain them together without parens.
```coq
<[ k := v ]> <[ k' := v' ]> m
```
doesn't parse, you need parentheses. How much of a problem would it be to extend the notation to `<[ k := v ]> m` that is right associative? Are there a lot of users that use this as partial application?https://gitlab.mpi-sws.org/iris/stdpp/-/issues/58stdpp breaks setoid rewriting2020-04-01T08:10:05Zsarahzrfstdpp breaks setoid rewritingThe setoid rewriting mechanism uses a bunch of typeclass machinery to infer `Proper` instances for the contexts being rewritten in, and it uses `flip` to talk about contravariance. stdpp breaks its ability to infer lots of cases it ordinarily can, because it makes `flip` typeclass transparent when the setoid rewriting mechanism is built with the assumption that it is typeclass opaque! In `base.v`, we have:
```coq
Typeclasses Transparent id compose flip const.
```
This nullifies the effect of the very first non-comment non-import line of `Classes/Init.v` in the Coq stdlib:
```coq
Typeclasses Opaque id const flip compose arrow impl iff not all.
```
Here's a minimal demonstration of the problems this causes:
```coq
From Coq Require Import ssreflect ssrfun ssrbool.
Require Import Morphisms.
Require Import PeanoNat.
Instance plus_proper_le : Proper (le ++> le ++> le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
Require Import stdpp.base.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
Fail setoid_rewrite <- H1 in H2 at 1.
Abort.
Section FlippedInstance.
(* Thus seemingly necessitating: *)
Local Instance plus_proper_le' : Proper (le --> le --> flip le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
End FlippedInstance.
(* But alternatively: *)
Typeclasses Opaque flip.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
```The setoid rewriting mechanism uses a bunch of typeclass machinery to infer `Proper` instances for the contexts being rewritten in, and it uses `flip` to talk about contravariance. stdpp breaks its ability to infer lots of cases it ordinarily can, because it makes `flip` typeclass transparent when the setoid rewriting mechanism is built with the assumption that it is typeclass opaque! In `base.v`, we have:
```coq
Typeclasses Transparent id compose flip const.
```
This nullifies the effect of the very first non-comment non-import line of `Classes/Init.v` in the Coq stdlib:
```coq
Typeclasses Opaque id const flip compose arrow impl iff not all.
```
Here's a minimal demonstration of the problems this causes:
```coq
From Coq Require Import ssreflect ssrfun ssrbool.
Require Import Morphisms.
Require Import PeanoNat.
Instance plus_proper_le : Proper (le ++> le ++> le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
Require Import stdpp.base.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
Fail setoid_rewrite <- H1 in H2 at 1.
Abort.
Section FlippedInstance.
(* Thus seemingly necessitating: *)
Local Instance plus_proper_le' : Proper (le --> le --> flip le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
End FlippedInstance.
(* But alternatively: *)
Typeclasses Opaque flip.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
```https://gitlab.mpi-sws.org/iris/stdpp/-/issues/51stdpp.base.decide := Coq.Classes.DecidableClass.decide?2020-02-17T18:25:41ZAbhishek Anandstdpp.base.decide := Coq.Classes.DecidableClass.decide?`stdpp.base.decide` duplicates the functionality of `Coq.Classes.DecidableClass.decide`. It is not clear that `stdpp.base.decide` provides something better. If so, would it be better to just reuse the functionality `Coq.Classes.DecidableClass`?`stdpp.base.decide` duplicates the functionality of `Coq.Classes.DecidableClass.decide`. It is not clear that `stdpp.base.decide` provides something better. If so, would it be better to just reuse the functionality `Coq.Classes.DecidableClass`?https://gitlab.mpi-sws.org/iris/stdpp/-/issues/48Make coPset operations TC opaque2020-02-18T09:25:45ZRobbertMake coPset operations TC opaqueSee https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/108/diffs#note_43736
This would be consistent with other set implementations.See https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/108/diffs#note_43736
This would be consistent with other set implementations.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/47solve_ndisj taking a long time2019-12-04T15:50:54ZJonas Kastbergsolve_ndisj taking a long timeThe `solve_ndisj` tactic takes a long time in certain situations. One such situation is captured by the included code.
```
From stdpp Require Import namespaces strings.
Section with_Σ.
Context (N : namespace).
Definition name_parentA := "Jesper".
Definition nameA := "Freya".
Definition name_parentB := "Robbert".
Definition nameB := "Jonas".
Lemma test : (((↑N ∖ ↑N.@name_parentB.@"children".@nameB.@"children"
∖ (↑N.@name_parentB.@"children" ∖ ↑N.@name_parentB.@"childreN".@nameB)):coPset) ⊆
((↑N ∖ ↑N.@name_parentA.@"children".@nameA.@"children".@"self".@"inv"):coPset)).
Proof.
time try solve_ndisj. (* This takes a long time *)
Admitted.
End with_Σ.
```
When run with `Typeclasses eauto := debug` it produces ~25k lines of debug messages, which seem to be looping.
A snippet of the print outs can be seen here:
```
Debug: 1: looking for (Symmetric disjoint) without backtracking
Debug: 1.1: simple apply @Equivalence_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.1-1 : (Equivalence disjoint)
Debug: 1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.2: simple apply @PER_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.2-1 : (RelationClasses.PER disjoint)
Debug: 1.2-1: looking for (RelationClasses.PER disjoint) without backtracking
Debug: 1.2-1.1: simple apply @Equivalence_PER on (RelationClasses.PER disjoint), 1 subgoal(s)
Debug: 1.2-1.1-1 : (Equivalence disjoint)
Debug: 1.2-1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.2-1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.3: simple eapply @disjoint_sym on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.3-1 : (SemiSet positive coPset)
Debug: 1.3-1: looking for (SemiSet positive coPset) with backtracking
Debug: 1.3-1.1: exact set_semi_set on (SemiSet positive coPset), 0 subgoal(s)
Debug: 1: looking for (Symmetric disjoint) without backtracking
Debug: 1.1: simple apply @Equivalence_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.1-1 : (Equivalence disjoint)
Debug: 1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.2: simple apply @PER_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.2-1 : (RelationClasses.PER disjoint)
Debug: 1.2-1: looking for (RelationClasses.PER disjoint) without backtracking
Debug: 1.2-1.1: simple apply @Equivalence_PER on (RelationClasses.PER disjoint), 1 subgoal(s)
Debug: 1.2-1.1-1 : (Equivalence disjoint)
Debug: 1.2-1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.2-1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.3: simple eapply @disjoint_sym on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.3-1 : (SemiSet positive coPset)
Debug: 1.3-1: looking for (SemiSet positive coPset) with backtracking
Debug: 1.3-1.1: exact set_semi_set on (SemiSet positive coPset), 0 subgoal(s)
```The `solve_ndisj` tactic takes a long time in certain situations. One such situation is captured by the included code.
```
From stdpp Require Import namespaces strings.
Section with_Σ.
Context (N : namespace).
Definition name_parentA := "Jesper".
Definition nameA := "Freya".
Definition name_parentB := "Robbert".
Definition nameB := "Jonas".
Lemma test : (((↑N ∖ ↑N.@name_parentB.@"children".@nameB.@"children"
∖ (↑N.@name_parentB.@"children" ∖ ↑N.@name_parentB.@"childreN".@nameB)):coPset) ⊆
((↑N ∖ ↑N.@name_parentA.@"children".@nameA.@"children".@"self".@"inv"):coPset)).
Proof.
time try solve_ndisj. (* This takes a long time *)
Admitted.
End with_Σ.
```
When run with `Typeclasses eauto := debug` it produces ~25k lines of debug messages, which seem to be looping.
A snippet of the print outs can be seen here:
```
Debug: 1: looking for (Symmetric disjoint) without backtracking
Debug: 1.1: simple apply @Equivalence_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.1-1 : (Equivalence disjoint)
Debug: 1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.2: simple apply @PER_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.2-1 : (RelationClasses.PER disjoint)
Debug: 1.2-1: looking for (RelationClasses.PER disjoint) without backtracking
Debug: 1.2-1.1: simple apply @Equivalence_PER on (RelationClasses.PER disjoint), 1 subgoal(s)
Debug: 1.2-1.1-1 : (Equivalence disjoint)
Debug: 1.2-1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.2-1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.3: simple eapply @disjoint_sym on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.3-1 : (SemiSet positive coPset)
Debug: 1.3-1: looking for (SemiSet positive coPset) with backtracking
Debug: 1.3-1.1: exact set_semi_set on (SemiSet positive coPset), 0 subgoal(s)
Debug: 1: looking for (Symmetric disjoint) without backtracking
Debug: 1.1: simple apply @Equivalence_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.1-1 : (Equivalence disjoint)
Debug: 1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.2: simple apply @PER_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.2-1 : (RelationClasses.PER disjoint)
Debug: 1.2-1: looking for (RelationClasses.PER disjoint) without backtracking
Debug: 1.2-1.1: simple apply @Equivalence_PER on (RelationClasses.PER disjoint), 1 subgoal(s)
Debug: 1.2-1.1-1 : (Equivalence disjoint)
Debug: 1.2-1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.2-1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.3: simple eapply @disjoint_sym on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.3-1 : (SemiSet positive coPset)
Debug: 1.3-1: looking for (SemiSet positive coPset) with backtracking
Debug: 1.3-1.1: exact set_semi_set on (SemiSet positive coPset), 0 subgoal(s)
```https://gitlab.mpi-sws.org/iris/stdpp/-/issues/44`Hint Mode` for `QuoteLookup` and `Quote`2019-09-19T08:37:03ZDan Frumin`Hint Mode` for `QuoteLookup` and `Quote`Would it be beneficial to have `Hint Mode` 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` 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/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 functions2020-02-13T22:40:01ZRobbertExtend `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.