stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2022-01-12T15:13:03Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/355Added some useful lemmas for the [last] function2022-01-12T15:13:03ZJonas KastbergAdded some useful lemmas for the [last] functionAdded some utility lemmas for the [last] function.
(precursor to the !353 MR)Added some utility lemmas for the [last] function.
(precursor to the !353 MR)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/354Add lemmas `elem_of_prefix` and `elem_of_suffix`2022-01-12T15:13:39ZJonas KastbergAdd lemmas `elem_of_prefix` and `elem_of_suffix`Added a lemma that captures that any element [x] that is in a prefix [l1] is also in the full list [l2].
The property is only trivial from the definition of `l1 prefix_of l2` (i.e. `∃ l, l2 = l1 ++ l2`).
Adding the lemma thus avoids brea...Added a lemma that captures that any element [x] that is in a prefix [l1] is also in the full list [l2].
The property is only trivial from the definition of `l1 prefix_of l2` (i.e. `∃ l, l2 = l1 ++ l2`).
Adding the lemma thus avoids breaking abstraction.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/360Set the priority of the rewrite relation for equiv to not take precedence ove...2022-01-13T16:37:57ZMatthieu SozeauSet the priority of the rewrite relation for equiv to not take precedence over...Set the priority of the rewrite relation for equiv to not take precedence over the eq instance from Coq.
This is more backwards compatible performance-wise with the old resolution where `eq` was favored (otherwise we get a 70% slowdown i...Set the priority of the rewrite relation for equiv to not take precedence over the eq instance from Coq.
This is more backwards compatible performance-wise with the old resolution where `eq` was favored (otherwise we get a 70% slowdown in perennial).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/358Add lemmas about empty `filter` on list, map, and set2022-08-08T13:37:43ZJonas KastbergAdd lemmas about empty `filter` on list, map, and setAdded an advanced lemma about [filter] on lists.
Whenever a filter with a proposition [P] on a list [l] results in an empty list,
we can derive that `x ∉ l` for any [x] where `P x`.Added an advanced lemma about [filter] on lists.
Whenever a filter with a proposition [P] on a list [l] results in an empty list,
we can derive that `x ∉ l` for any [x] where `P x`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/362Set the priority of the rewrite relation for sqsubseteq to not take precedenc...2022-01-14T10:59:45ZMatthieu SozeauSet the priority of the rewrite relation for sqsubseteq to not take precedence over...Set the priority of the rewrite relation for sqsubseteq to not take precedence over the eq instance from Coq or equiv.Set the priority of the rewrite relation for sqsubseteq to not take precedence over the eq instance from Coq or equiv.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/359Added some useful lemmas about [list_subseteq]2022-01-14T11:03:41ZJonas KastbergAdded some useful lemmas about [list_subseteq]Added some generally useful lemmas about the [list_subseteq] functionAdded some generally useful lemmas about the [list_subseteq] functionhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/361Add `last_cons_Some_ne` lemma for the `last` function2022-01-14T11:58:54ZJonas KastbergAdd `last_cons_Some_ne` lemma for the `last` functionA useful lemma for the [last] function, to reduce `last (x::l) = Some y` to `last l = Some y` whenever `x ≠ y`.
This is useful since using `last_cons` leaves us with
```{coq}
match last l with
| Some y0 => Some y0
| None => Some x
end = ...A useful lemma for the [last] function, to reduce `last (x::l) = Some y` to `last l = Some y` whenever `x ≠ y`.
This is useful since using `last_cons` leaves us with
```{coq}
match last l with
| Some y0 => Some y0
| None => Some x
end = Some y
```
which only reduces through a subgoal.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/363Add lemmas `app_cons_eq_inv_{l,r}`.2022-01-14T15:31:17ZRobbert KrebbersAdd lemmas `app_cons_eq_inv_{l,r}`.This MR contains two commits: One with the actual lemmas, and one to perform some rearrangements. To prove the `_r` variant, I needed properties of `reverse`. I thus moved the `reverse` lemmas above the `elem_of` lemmas.
The lemmas in t...This MR contains two commits: One with the actual lemmas, and one to perform some rearrangements. To prove the `_r` variant, I needed properties of `reverse`. I thus moved the `reverse` lemmas above the `elem_of` lemmas.
The lemmas in this MR generalize the ones in !356. They also allow proving a variant for `suffix_of`, which is missing in that MR.
/cc @jihgfeehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/353Add `filter_reverse`, `head_filter_Some`, `last_filter_Some` lemmas2022-01-19T09:39:46ZJonas KastbergAdd `filter_reverse`, `head_filter_Some`, `last_filter_Some` lemmasAdded the lemma:
```coq
Lemma last_filter_postfix P `{!∀ x : A, Decision (P x)} l x
last (filter P l) = Some x →
∃ l1 l2, l = l1 ++ [x] ++ l2 ∧ Forall (λ z, ¬ (P z)) l2.
```
(and its counterpart for `head`)
The lemmas seem useful an...Added the lemma:
```coq
Lemma last_filter_postfix P `{!∀ x : A, Decision (P x)} l x
last (filter P l) = Some x →
∃ l1 l2, l = l1 ++ [x] ++ l2 ∧ Forall (λ z, ¬ (P z)) l2.
```
(and its counterpart for `head`)
The lemmas seem useful and general enough to fit in stdpp.
The `last` lemma derives the property `Forall (λ z, ¬ (P z)) l2` of the postfix of a split `l1 ++ [x] ++ l2` for a list `l` whenever `last (filter P l) = Some x`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/356Renamed `app_cons_eq_inv_{l,r}`, and added derived versions for `prefix/suffix`2022-01-19T16:49:29ZJonas KastbergRenamed `app_cons_eq_inv_{l,r}`, and added derived versions for `prefix/suffix`Renamed the lemmas `app_cons_eq_inv_{l,r}`, to `elem_of_app_cons_inv_{l,r}`, to be more descriptive and consistent with existing lemmas.
Additionally, derived versions for `prefix/suffix`, as they recall some non-immediate properties of...Renamed the lemmas `app_cons_eq_inv_{l,r}`, to `elem_of_app_cons_inv_{l,r}`, to be more descriptive and consistent with existing lemmas.
Additionally, derived versions for `prefix/suffix`, as they recall some non-immediate properties of the relations on similar list structures.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/364std++ 1.7.0 release notes2022-01-22T17:44:23ZTej Chajedtchajed@gmail.comstd++ 1.7.0 release notesFirst step towards a release, which will help with #129.First step towards a release, which will help with #129.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/366Add set_unfold_list_bind (+ test)2022-02-20T18:22:59ZPaolo G. GiarrussoAdd set_unfold_list_bind (+ test)`set_unfold_bind` for sets already exists; this brings the list variant on par.`set_unfold_bind` for sets already exists; this brings the list variant on par.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/367Workaround to avoid `injection` from unfolding equalities on `dom`2022-02-24T15:41:35ZRobbert KrebbersWorkaround to avoid `injection` from unfolding equalities on `dom`As reported by @vsiles and @msammler on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/6gkx9t39rpnxmghhdq7jkn45fe) the tactics `simplify_eq` and `injection` accidentally unfold equalities `dom (gset A) m1 = dom (gset A) m2` into `me...As reported by @vsiles and @msammler on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/6gkx9t39rpnxmghhdq7jkn45fe) the tactics `simplify_eq` and `injection` accidentally unfold equalities `dom (gset A) m1 = dom (gset A) m2` into `merge ...`.
The culprit is that the definition of `dom` on `gmap` starts with a constructor `MapSet`. This MR tweaks the definition a bit, by inserting an eta expansion, to avoid that.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/370Avoid universe bumps of `gset`/`mapset` (fixes #134)2022-03-16T10:04:56ZRobbert KrebbersAvoid universe bumps of `gset`/`mapset` (fixes #134)I don't understand universes well enough to see why the previous version does not work. So if anyone can explain that, that would be great :).I don't understand universes well enough to see why the previous version does not work. So if anyone can explain that, that would be great :).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/369Add lemmas list_to_set_disj_elem_of_list and gmultiset_difference_disj_union_...2022-03-16T10:14:29ZLéo StefanescoAdd lemmas list_to_set_disj_elem_of_list and gmultiset_difference_disj_union_{l,r}https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/371Clarify relationship between `gset_to_gmap` and `set_to_map`.2022-04-07T20:10:33ZRobbert KrebbersClarify relationship between `gset_to_gmap` and `set_to_map`.As a response to a question by @jung at Mattermost: https://mattermost.mpi-sws.org/iris/pl/xdgqgkyw9ifcmj3zdsy8dyb18e I added some comments.
Aside from the differences pointed out in the added comments, the `gset` function was there bef...As a response to a question by @jung at Mattermost: https://mattermost.mpi-sws.org/iris/pl/xdgqgkyw9ifcmj3zdsy8dyb18e I added some comments.
Aside from the differences pointed out in the added comments, the `gset` function was there before the generic `set` function.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/368Define [tele_arg] as a fixpoint2022-05-16T00:52:05ZGregory MalechaDefine [tele_arg] as a fixpointThe current definition of `tele_arg` increases the universe level in a way that is unfortunate. In particular,
```coq
Inductive tele_arg : tele@{u} -> Type@{u+1} :=
| ...
```
In Iris, what this means is that `bi_tforall`/`bi_texist` h...The current definition of `tele_arg` increases the universe level in a way that is unfortunate. In particular,
```coq
Inductive tele_arg : tele@{u} -> Type@{u+1} :=
| ...
```
In Iris, what this means is that `bi_tforall`/`bi_texist` have different universe levels than `bi_forall`/`bi_exist`. This MR re-defines `tele_arg` as a fixpoint, which prevents the universe bump. In particular:
```coq
Fixpoint tele_arg (t : tele@{u}) : Type@{u} :=
...
```
With this definition, the universes for the telescopic quantifiers can match the universes of the non-telescopic quantifiers in iris (this enables a separate MR to iris: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/781).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/374Add induction principle for `tele_arg`.2022-04-12T16:23:52ZRobbert KrebbersAdd induction principle for `tele_arg`.This induction principle was automatically generated prior to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/368, but no longer exists. This MR includes a manual proof.
Unfortunately, Coq does not use it automatically, so you ha...This induction principle was automatically generated prior to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/368, but no longer exists. This MR includes a manual proof.
Unfortunately, Coq does not use it automatically, so you have to use it with `induction ... using tele_arg_ind`. But that's the same for `map_ind` and friends.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/373Add Pigeon Hole principle.2022-04-12T19:24:40ZRobbert KrebbersAdd Pigeon Hole principle.I was surprised that we do not have the Pigeon hole principle. It's a trivial consequence of results we already have on Finite types and cardinalities.I was surprised that we do not have the Pigeon hole principle. It's a trivial consequence of results we already have on Finite types and cardinalities.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/375Annotate telescope notations to support literal telescope arguments.2022-05-04T12:00:37ZJannoAnnotate telescope notations to support literal telescope arguments.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/368 had the unfortunate consequence that literal telescope arguments would not typecheck any more. This MR fixes this by adding copious (but nonetheless minimal) amounts of casts and...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/368 had the unfortunate consequence that literal telescope arguments would not typecheck any more. This MR fixes this by adding copious (but nonetheless minimal) amounts of casts and annotations to make the `[tele_arg ..]` notation work again. I added tests for both new and old unification.
I am currently running a full test with these changes on all BedRock proofs which should tell us a bit about the compatibility. I expect no problems here.
Something that is not reflected in the MR but is still interesting is that old unification, i.e. `apply` and friends, work even without the cast in the `TargS` notation. New unification, i.e. `refine`, does not. There might be a Coq bug to report here but I don't have time to dig into that right now.