stdpp issueshttps://gitlab.mpi-sws.org/iris/stdpp/-/issues2024-03-18T16:05:30Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/issues/206Please create a tag for Coq 8.19 in Coq Platform 2024.012024-03-18T16:05:30ZRomain TetleyPlease create a tag for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (1.9.0) **does not work** with Coq `8.19.0`.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.19, **preferably before March 31st, 2024**?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
In case the tag and opam package are available before March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/405https://gitlab.mpi-sws.org/iris/stdpp/-/issues/204The bitvector library should ideally be accessible from the main coq-released...2024-03-11T21:10:46ZThibaut PéramiThe bitvector library should ideally be accessible from the main coq-released repositoryIdeally we would like the bitvector library in `stdpp-unstable` to be accessible from [Coq Released](https://github.com/coq/opam) repository. We need this because we'd like to put the Stdpp version of [`coq-sail`](https://github.com/rems...Ideally we would like the bitvector library in `stdpp-unstable` to be accessible from [Coq Released](https://github.com/coq/opam) repository. We need this because we'd like to put the Stdpp version of [`coq-sail`](https://github.com/rems-project/coq-sail) on it. Options includes:
- Putting `stdpp-unstable` on Coq Released
- Merging it in core Stdpp (Tracking issue #145 and #146)
- Creating a standalone `stdpp-bitvector` or `stdpp-bitvectors` or `stdpp-bv` and ship it to Coq Released separately.
What do you think of those options?https://gitlab.mpi-sws.org/iris/stdpp/-/issues/203simplify_map_eq sometimes fails to rewrite with `lookup_singleton_ne`2023-11-25T09:59:42ZRalf Jungjung@mpi-sws.orgsimplify_map_eq sometimes fails to rewrite with `lookup_singleton_ne`This came up in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/959, see the FIXMEs in gmap_view.v. This is probably related to old unification; `rewrite ->lookup_singleton_ne` fails but `rewrite lookup_singleton_ne` succeeds. So ...This came up in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/959, see the FIXMEs in gmap_view.v. This is probably related to old unification; `rewrite ->lookup_singleton_ne` fails but `rewrite lookup_singleton_ne` succeeds. So something similar to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/497 could help.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/201stdpp constrains the template universe option.u02023-11-16T15:05:47ZKarl Palmskogstdpp constrains the template universe option.u0The file `fin_maps.v` is incompatible with any Coq code that uses `Some id`, due to universe constraints:
```coq
Definition x := Some id.
From stdpp Require Import fin_maps.
(*
Error: Universe inconsistency. Cannot enforce option.u0 <= b...The file `fin_maps.v` is incompatible with any Coq code that uses `Some id`, due to universe constraints:
```coq
Definition x := Some id.
From stdpp Require Import fin_maps.
(*
Error: Universe inconsistency. Cannot enforce option.u0 <= base.Equiv.u0 because base.Equiv.u0
<= Coq.Relations.Relation_Definitions.1 <= ID.u0 < option.u0.
*)
```
Another way to see the problem is the following:
```coq
From stdpp Require Import fin_maps.
Constraint ID.u0 <= option.u0.
(*
Error: Universe inconsistency. Cannot enforce ID.u0 <= option.u0 because option.u0 <= MapFold.u2
< Coq.Relations.Relation_Definitions.1 <= ID.u0.
*)
```
This was diagnosed on the [Coq Zulip](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/stdpp.20universe.20inconistency.20with.20ID.20and.20fin_maps) with help from Gaëtan Gilbert.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/200std++ collides with `Equations`: both define `simplify_eq`, and we mess up th...2023-11-01T14:33:35ZRalf Jungjung@mpi-sws.orgstd++ collides with `Equations`: both define `simplify_eq`, and we mess up their obligation tacticThe equations package seems to also contain a `simplify_eq` tactic
```
Ltac Equations.Init.simplify_eq
Ltac Coq.Init.Ltac.simplify_eq (shorter name to refer to it in current context is Ltac.simplify_eq)
```
stdpp's `simplify_eq` is a not...The equations package seems to also contain a `simplify_eq` tactic
```
Ltac Equations.Init.simplify_eq
Ltac Coq.Init.Ltac.simplify_eq (shorter name to refer to it in current context is Ltac.simplify_eq)
```
stdpp's `simplify_eq` is a notation, and the `Coq.Init` version seems to not be a problem, but when equations is imported, the tactic stops working. Instead one gets an obscure error, just saying "Not a negated primitive equality."
This is when equations is imported after std++. When I import equations first, it behaves in strange ways -- there's a different number of obligations generated and they also look different. I think equations might not like our `Global Obligation Tactic := idtac.`.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/196Ambiguous notations for vectors and telescopes2023-10-20T14:26:18ZRobbert KrebbersAmbiguous notations for vectors and telescopes```coq
From stdpp Require Import telescopes list.
Check [ tele ]. (* prints [tele] : list Type *)
Check [tele]. (* prints [tele] : tele *)
```
This is due to the notations in https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/...```coq
From stdpp Require Import telescopes list.
Check [ tele ]. (* prints [tele] : list Type *)
Check [tele]. (* prints [tele] : tele *)
```
This is due to the notations in https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/telescopes.v?ref_type=heads#L167
```
Notation "'[tele' ]" := (TeleO)
(format "[tele ]").
```
This shows that `[ tele ]` is parsed as a list, but it pretty prints without space, i.e., `[tele]`. When parsing this again, we end up with the empty telescopes.
See @snyke7's post below for a similar issue for vectors.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/194Refer to Iris documentation2023-08-03T17:15:57ZRobbert KrebbersRefer to Iris documentationThere is quite some documentation in Iris (setting up editor, how to use Propers, ...). We should include links to the relevant documentation in the std++ README.There is quite some documentation in Iris (setting up editor, how to use Propers, ...). We should include links to the relevant documentation in the std++ README.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/193Rename Ltac iter into coq_list_iter2023-08-03T21:27:34ZRobbert KrebbersRename Ltac iter into coq_list_iterSee https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931#note_94375
Bikeshed about gallina_list_iter, coq_list_iter, constr_list_iter, ...?See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931#note_94375
Bikeshed about gallina_list_iter, coq_list_iter, constr_list_iter, ...?https://gitlab.mpi-sws.org/iris/stdpp/-/issues/184Name mangling light causes noise in printing2023-07-17T15:38:42ZRobbert KrebbersName mangling light causes noise in printing```coq
From stdpp Require Import options.
Check forall x, x = 0.
(** Prints forall __x : nat, __x = 0 *)
```
This becomes worse when considering goals with quantifiers:
```coq
Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
...```coq
From stdpp Require Import options.
Check forall x, x = 0.
(** Prints forall __x : nat, __x = 0 *)
```
This becomes worse when considering goals with quantifiers:
```coq
Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
Proof.
revert l2.
(* Prints ∀ __l2 : list A, (∀ __i : nat, l1 !! __i = __l2 !! __i) → l1 = __l2 *)
```
This is totally unreadable.
Is there a way to fix this, or does this mean we should revert !475.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/182`Countable` → `Finite` instance gives ambigous `encode`/`decode`.2023-05-03T08:38:53ZRobbert Krebbers`Countable` → `Finite` instance gives ambigous `encode`/`decode`.See discussion in https://mattermost.mpi-sws.org/iris/pl/teh4sqsgx7rjbjifkwjn8y5xee
@simongregersen if you have a self-contained example where it goes wrong, please post it here.See discussion in https://mattermost.mpi-sws.org/iris/pl/teh4sqsgx7rjbjifkwjn8y5xee
@simongregersen if you have a self-contained example where it goes wrong, please post it here.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/180naive_solver does not solve trivial inconsistencies involving is_Some2023-04-12T14:25:20ZMarijn van Wezelmarijn.vanwezel@ru.nlnaive_solver does not solve trivial inconsistencies involving is_Some```
Example ex1 : is_Some (None : option nat) → False.
Proof.
Fail naive_solver. (* No matching clauses for match. *)
unfold is_Some. naive_solver. (* No more goals. *)
Qed.
Example ex2 : is_Some (Some 10).
Proof.
naive_solver. (*...```
Example ex1 : is_Some (None : option nat) → False.
Proof.
Fail naive_solver. (* No matching clauses for match. *)
unfold is_Some. naive_solver. (* No more goals. *)
Qed.
Example ex2 : is_Some (Some 10).
Proof.
naive_solver. (* No more goals. *)
Qed.
```https://gitlab.mpi-sws.org/iris/stdpp/-/issues/176Inconsistent naming of list lemmas2023-03-21T16:58:06ZRalf Jungjung@mpi-sws.orgInconsistent naming of list lemmasUsually the lemmas defined in a "section" of the list files have that "section" as the first component of their name. That is not always the case though, e.g.
```
(** ** Properties of [subseteq] *)
Lemma list_delete_subseteq i l : delet...Usually the lemmas defined in a "section" of the list files have that "section" as the first component of their name. That is not always the case though, e.g.
```
(** ** Properties of [subseteq] *)
Lemma list_delete_subseteq i l : delete i l ⊆ l.
Lemma list_filter_subseteq P `{!∀ x : A, Decision (P x)} l :
(** ** Properties of the [prefix] and [suffix] predicates *)
Lemma elem_of_prefix l1 l2 x :
x ∈ l1 → l1 `prefix_of` l2 → x ∈ l2.
```
So maybe they should be renamed? Though I think basically all `elem_of` lemmas have that as their first component, so `prefix_elem_of` would be somewhat strange...https://gitlab.mpi-sws.org/iris/stdpp/-/issues/175Inconsistent naming of dom lemmas2023-03-21T16:57:05ZRalf Jungjung@mpi-sws.orgInconsistent naming of dom lemmasThe vast majority of `dom` lemmas does not contain `map` in their name since only maps have domains. There are some exceptions though:
```
Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ##ₘ m2 ↔ dom m1 ## dom m2.
Lemma map_disjoint_dom_1 ...The vast majority of `dom` lemmas does not contain `map` in their name since only maps have domains. There are some exceptions though:
```
Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ##ₘ m2 ↔ dom m1 ## dom m2.
Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ##ₘ m2 → dom m1 ## dom m2.
Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom m1 ## dom m2 → m1 ##ₘ m2.
```
Those should probably be renamed to remove the leading `map_`. And maybe move the `dom_` to the front?https://gitlab.mpi-sws.org/iris/stdpp/-/issues/174Improve name of `no_new_unsolved_evars`2023-03-17T13:43:10ZRobbert KrebbersImprove name of `no_new_unsolved_evars`The name should make clear that the tactic either fails or completely solves the goal.
This was discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/429/diffs#note_86720The name should make clear that the tactic either fails or completely solves the goal.
This was discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/429/diffs#note_86720https://gitlab.mpi-sws.org/iris/stdpp/-/issues/171Replace `MGuard` typeclass by uniform definition based on a new `MFail`2023-07-26T16:13:22ZRalf Jungjung@mpi-sws.orgReplace `MGuard` typeclass by uniform definition based on a new `MFail`As proposed [here](https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/436#note_87121) by @Blaisorblade, slightly adjusted:
```coq
Definition guard `{MFail M, MRet M} P `{Decision P} :=
match decide P with
| left H => mret H
| r...As proposed [here](https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/436#note_87121) by @Blaisorblade, slightly adjusted:
```coq
Definition guard `{MFail M, MRet M} P `{Decision P} :=
match decide P with
| left H => mret H
| right _ => mfail
end.
```
`MonadSet` could also have laws for `MFail`.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/170Unify decision tactics2023-03-31T12:28:10ZRalf Jungjung@mpi-sws.orgUnify decision tacticsWe currently have 3 tactics `case_decide`, `case_bool_decide`, `case_option_guard` that are very similar but work on `decide`, `bool_decide`, and `guard`, respectively. Tactics are pretty hard to discover (there is no useful `SearchAbout...We currently have 3 tactics `case_decide`, `case_bool_decide`, `case_option_guard` that are very similar but work on `decide`, `bool_decide`, and `guard`, respectively. Tactics are pretty hard to discover (there is no useful `SearchAbout` for them and we don't document a "tactic index" for std++), so this is bad -- I didn't even know `case_option_guard` was a thing until last week.
I think we should unify these 3 tactics into one, so that one does not have to independently discover all 3 of them.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/168`rewrite decide_True` does not work with ssreflect rewritintg2022-12-22T15:31:45ZRalf Jungjung@mpi-sws.org`rewrite decide_True` does not work with ssreflect rewritintgCode says it all:
```
Lemma bar : (if decide (0 = 0) then 0 else 0) = 0.
Proof.
Succeed by rewrite ->decide_True.
Fail rewrite decide_True.
[...]
```
Because of issues like this, @msammler @blaisorblade and me now [have a general s...Code says it all:
```
Lemma bar : (if decide (0 = 0) then 0 else 0) = 0.
Proof.
Succeed by rewrite ->decide_True.
Fail rewrite decide_True.
[...]
```
Because of issues like this, @msammler @blaisorblade and me now [have a general suspicion](https://mattermost.mpi-sws.org/iris/channels/stdpp) against `decide` and prefer `bool_decide` wherever possible.
With `bool_decide P` one cannot do `destruct` and get a proof of `P`/`¬P`, but the `case_bool_decide` tactic handles that situation nicely. I never ran into situations where I wished I would have used `decide` instead of `bool_decide`. Hypothetically, if there are 2 `bool_decide` in the goal, `case_bool_decide` does not provide enough control to figure out which one to destruct, but one could imagine a `case_bool_deice pat` that pattern-matches `P` against `pat` to solve this problem.
So that leaves the question:
- Can we fix `rewrite decide_True`?
- Should we replace `decide` by `bool_decide` entirely / wherever possible, to steer people towards the more reliable option? It is very rare that you actually need the proof term, so arguably the version that returns `bool` should be the default.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/164set_solver regression: goal with set_map is no longer solved2022-12-01T08:42:54ZRalf Jungjung@mpi-sws.orgset_solver regression: goal with set_map is no longer solvedCode says it all:
```
Lemma test `{Countable A, Countable B} (h : A → B) (x : A) (s : gset A) :
(∀ x0 y : A, x0 ∈ {[x]} ∪ s → y ∈ {[x]} ∪ s → h x0 = h y → x0 = y) →
(x ∉ s) →
{[h x]} ##@{gset B} set_map h s.
Proof.
Fail set_solve...Code says it all:
```
Lemma test `{Countable A, Countable B} (h : A → B) (x : A) (s : gset A) :
(∀ x0 y : A, x0 ∈ {[x]} ∪ s → y ∈ {[x]} ∪ s → h x0 = h y → x0 = y) →
(x ∉ s) →
{[h x]} ##@{gset B} set_map h s.
Proof.
Fail set_solver.
set_solver by idtac.
```https://gitlab.mpi-sws.org/iris/stdpp/-/issues/162Inconsistent tactic notation: `naive_solver tac` vs `set_solver by tac`2022-11-30T11:21:37ZRalf Jungjung@mpi-sws.orgInconsistent tactic notation: `naive_solver tac` vs `set_solver by tac`The title says it all:
```
Tactic Notation "naive_solver" tactic(tac) :=
```
vs
```
Tactic Notation "set_solver" "by" tactic3(tac) :=
```
They are also not using the same tactic level it seems.The title says it all:
```
Tactic Notation "naive_solver" tactic(tac) :=
```
vs
```
Tactic Notation "set_solver" "by" tactic3(tac) :=
```
They are also not using the same tactic level it seems.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/159`gset_to_coPset` shows implementation on `simpl` when called on a empty const...2022-11-24T14:38:20ZJanggun Lee`gset_to_coPset` shows implementation on `simpl` when called on a empty constant set.Consider the following example.
```coq
From stdpp Require Import coPset.
Lemma test :
gset_to_coPset (∅ ∪ ∅) = ∅.
Proof.
simpl. rewrite union_empty_l_L.
Abort.
```
I expected the `simpl` to do nothing, and I can proceed with the `r...Consider the following example.
```coq
From stdpp Require Import coPset.
Lemma test :
gset_to_coPset (∅ ∪ ∅) = ∅.
Proof.
simpl. rewrite union_empty_l_L.
Abort.
```
I expected the `simpl` to do nothing, and I can proceed with the `rewrite`. However, it instead inlined the definition of `gset_to_coPset`, resulting in the following Coq context.
```coq
(let
'{| gmap.gmap_car := gmap_car |} := ∅ ∪ ∅ in
let
'{| pmap.pmap_car := t; pmap.pmap_prf := Ht |} := gmap_car in
Pset_to_coPset_raw t ↾ Pset_to_coPset_wf t Ht) = ∅
```
The rewrite then fails with the following message.
```coq
Unable to satisfy the following constraints:
?H : "ElemOf ?A (gmap.gmap positive ())"
?H1 : "Singleton ?A (gmap.gmap positive ())"
?H3 : "SemiSet ?A (gmap.gmap positive ())"
?LeibnizEquiv0 : "LeibnizEquiv (gmap.gmap positive ())"
```
Not preforming `simpl` makes the `rewrite` work fine.
The easiest solution I found was to do `simpl never` for `gset_to_coPset`. I feel like this should be the default since the user should never need to look at the inner definition of `gset_to_coPset`, being cryptic as it is.
Are there more better/intended solutions?