stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2022-08-09T10:52:18Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/383Introduce `set_bind` and associated lemmas.2022-08-09T10:52:18ZDan FruminIntroduce `set_bind` and associated lemmas.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/382Preimage function for finite maps.2022-05-31T11:08:40ZRobbert KrebbersPreimage function for finite maps.This is a possible solution to #140This is a possible solution to #140https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/381Add `set_map_2` and associated lemmas.2022-05-30T19:40:49ZDan FruminAdd `set_map_2` and associated lemmas.The function `set_map_2` generalizes the mapping function `set_map`, in that it ranges over two sets, and applies a given function to all the possible combinations of the elements.
I tried to recreate the same lemmas for set_map_2 as th...The function `set_map_2` generalizes the mapping function `set_map`, in that it ranges over two sets, and applies a given function to all the possible combinations of the elements.
I tried to recreate the same lemmas for set_map_2 as the ones that we already have for set_map.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/380Enable cumulativity for telescopes2022-05-18T02:20:39ZJannoEnable cumulativity for telescopesThis fixes https://gitlab.mpi-sws.org/iris/iris/-/issues/461 by enabling cumulative universe polymorphism in telescopes.v, allowing `tele` at a fixed universe (such as the `Quant` universe in iris) to cumulatively contain telescopes at s...This fixes https://gitlab.mpi-sws.org/iris/iris/-/issues/461 by enabling cumulative universe polymorphism in telescopes.v, allowing `tele` at a fixed universe (such as the `Quant` universe in iris) to cumulatively contain telescopes at smaller universes.
I also re-arranged existing telescope tests slightly in order to make sure the test for `Unset Universe Minimization ToSet` has a chance to fail before the accessor test, which happens to fail for the same reason.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/379Set `Hint Mode` for `FinSet`.2022-05-13T14:55:32ZRobbert KrebbersSet `Hint Mode` for `FinSet`.This fixes issue #139.This fixes issue #139.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/378Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.2022-05-13T07:45:09ZRobbert KrebbersRename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.As discussed in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/778#note_80612As discussed in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/778#note_80612https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/377drop support for Coq 8.112022-05-11T12:55:42ZRalf Jungjung@mpi-sws.orgdrop support for Coq 8.11This lets us make progress in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/376.This lets us make progress in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/376.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/376make dom domain type paremeter (D) implicit2022-05-19T18:37:53ZRalf Jungjung@mpi-sws.orgmake dom domain type paremeter (D) implicitFixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/137Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/137https://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.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/372Draft: Very preliminary version of a quick start guide for sets.2023-02-06T14:42:57ZRobbert KrebbersDraft: Very preliminary version of a quick start guide for sets.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/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/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/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/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/365Draft: Overlay for PR#155182022-05-06T12:11:32ZMatthieu SozeauDraft: Overlay for PR#15518This is an overlay for [Coq PR #15518](https://github.com/coq/coq/pull/15518): moving apply to the evar-based unifier.
This includes a breaking fix for apply of conjunction which has the unnatural behavior of trying Q -> P before P -> Q ...This is an overlay for [Coq PR #15518](https://github.com/coq/coq/pull/15518): moving apply to the evar-based unifier.
This includes a breaking fix for apply of conjunction which has the unnatural behavior of trying Q -> P before P -> Q when applying a `P <-> Q` hypothesis. I think the rest is backwards compatible: mostly about using `eapply` in places where new existential are created, which the new `apply` forbids (rightfully).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.