stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-07-28T17:51:12Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/317bring back some empty_inv lemmas for rewriting2021-07-28T17:51:12ZRalf Jungjung@mpi-sws.orgbring back some empty_inv lemmas for rewritingSee discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/307#note_72408See discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/307#note_72408https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/316relations lemmas2021-07-28T15:21:24ZRalf Jungjung@mpi-sws.orgrelations lemmasFound the `ex_loop` lemmas in Simuliris. Simuliris dos not actually need them any more, but they seem useful enough.
Proofs by @simonspies.Found the `ex_loop` lemmas in Simuliris. Simuliris dos not actually need them any more, but they seem useful enough.
Proofs by @simonspies.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/315add some lookup_{union,difference} lemmas2021-07-28T15:17:36ZRalf Jungjung@mpi-sws.orgadd some lookup_{union,difference} lemmasmore things from Simuliris
- `lookup_union_Some_l_inv`, `lookup_union_Some_r_inv` allow exploiting statements of the form `(m1 ∪ m2) !! i = Some x`.
- `lookup_union_is_Some`, `lookup_difference_is_Some` match the existing `lookup_insert...more things from Simuliris
- `lookup_union_Some_l_inv`, `lookup_union_Some_r_inv` allow exploiting statements of the form `(m1 ∪ m2) !! i = Some x`.
- `lookup_union_is_Some`, `lookup_difference_is_Some` match the existing `lookup_insert_is_Some`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/314add insert_map_seq_02021-07-28T13:43:58ZRalf Jungjung@mpi-sws.orgadd insert_map_seq_0another bit from Simuliris, original proof by @msammleranother bit from Simuliris, original proof by @msammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/313add lookup_take_Some2021-07-28T13:43:44ZRalf Jungjung@mpi-sws.orgadd lookup_take_Someanother bit from Simuliris, original proof by @msammleranother bit from Simuliris, original proof by @msammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/312add binder_list2021-07-28T13:43:27ZRalf Jungjung@mpi-sws.orgadd binder_listanother bit from Simulirisanother bit from Simulirishttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/311add get_head tactic and use it in solve_proper_unfold2021-07-28T14:24:42ZRalf Jungjung@mpi-sws.orgadd get_head tactic and use it in solve_proper_unfoldTactic taken from Simuliris, originally written by @msammler.Tactic taken from Simuliris, originally written by @msammler.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/310Generalize `map_filter_insert` so that it covers both the True and False case.2021-07-28T07:08:19ZRobbert KrebbersGeneralize `map_filter_insert` so that it covers both the True and False case.The new lemma is
```coq
Lemma map_filter_insert m i x :
filter P (<[i:=x]> m)
= if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).
```
We need the `delete` because there might be another entry with key `i` ...The new lemma is
```coq
Lemma map_filter_insert m i x :
filter P (<[i:=x]> m)
= if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).
```
We need the `delete` because there might be another entry with key `i` in `m`.
In addition there are the lemmas:
```coq
Lemma map_filter_insert_True m i x : (* used to be map_filter_insert *)
P (i, x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
Lemma map_filter_insert_False m i x : (* used to be map_filter_insert_not_delete *)
¬ P (i, x) → filter P (<[i:=x]> m) = filter P (delete i m).
```
I use the `_True` and `_False` suffixes similar to `decide_True` and `decide_False`.
See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/245?commit_id=335bc4d65a65bfeb247fa86853b057920c44feb0#note_72118 for the discussion that led to this MR.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/309Use `SProp` to obtain better definitional equality for `pmap`, `gmap`, `gset...2023-04-18T22:11:37ZRobbert KrebbersUse `SProp` to obtain better definitional equality for `pmap`, `gmap`, `gset`, `Qp`, and `coPset`This MR ensures that more equalities hold definitionally, and can thus be proved by `reflexivity` or even by conversion as part of unification.
For example `1/4 + 3/4 = 1`, or `{[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]}`, or `{[ 1 ]} ∖...This MR ensures that more equalities hold definitionally, and can thus be proved by `reflexivity` or even by conversion as part of unification.
For example `1/4 + 3/4 = 1`, or `{[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]}`, or `{[ 1 ]} ∖ {[ 1 ]} = ∅` can be proved using a mere `reflexivity` with this MR. Moreover, if you have a goal that involves, say `1/4 + 3/4`, then you can just apply a lemma involving `1` because both are convertible.
This MR is based on !189 but makes various changes:
- Use `Squash` instead of `sUnit` to ensure that `coqchk` comes back clean.
- Make the proofs of data structures like `pmap` and `gmap` opaque so that we obtain `O(log n)` operations. This MR includes some tests, but they are commented out because such timings cannot be tested by CI.
- Use `SProp` for `coPset` and `Qp` (!189 only considered `pmap`, `gmap`, and `gset`)
+ The change for `coPset` was pretty simple, but instead of a Sigma type, I had to use a record with an `SProp` field.
+ The change for `Qp` was more involved. `Qp` was originally defined in terms of `Qc` from the Coq standard lib, which itself is a `Q` + a `Prop` proof. Due to the `Prop` proof, I could no longer use `Qc` and had to inline an `SProp` version of `Qp`. In the process, I also decided to no longer use `Q`, which is defined as a pair of a `Z` and a `positive`, but just use pairs of `positives`. That avoids the need for a proof of the fraction being positive. None of these changes should be visible in the `Qp` API.
This MR changes the implementations of the aforementioned data structures, but their APIs should not have changed.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/85https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/308Add lemma `map_singleton_subseteq_l` and `map_singleton_subseteq`.2021-07-27T10:46:26ZRobbert KrebbersAdd lemma `map_singleton_subseteq_l` and `map_singleton_subseteq`.Similar to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/306Similar to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/306https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/307Clean up `empty{',_inv,_iff}` lemmas.2021-07-28T15:43:06ZRobbert KrebbersClean up `empty{',_inv,_iff}` lemmas.Write them all using `↔` and consistently use the `_iff` suffix.
Also:
- Make `map_empty` a biimplication
- Add lemma `map_filter_empty_iff`Write them all using `↔` and consistently use the `_iff` suffix.
Also:
- Make `map_empty` a biimplication
- Add lemma `map_filter_empty_iff`https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/306Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼`2021-07-27T10:35:23ZRobbert KrebbersMake singleton/`⊆` lemmas consistent with Iris's singleton/`≼`See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/305#note_71807
I decided to use Iris's names and argument because:
- It's shorter
- Iris's `singleton_included` lemmas have been there for longer than the multise...See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/305#note_71807
I decided to use Iris's names and argument because:
- It's shorter
- Iris's `singleton_included` lemmas have been there for longer than the multiset lemmas, so are (probably) more widely usedhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/305some lemmas about list submseteq2021-07-27T10:58:15ZRalf Jungjung@mpi-sws.orgsome lemmas about list submseteqFound in Simuliris, original proofs by @simonspies.
I am not at all sure about the names...Found in Simuliris, original proofs by @simonspies.
I am not at all sure about the names...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/304Add lemmas that say that `curry{3,4}?` and `uncurry{3,4}?` are inverses.2021-07-24T09:38:56ZRobbert KrebbersAdd lemmas that say that `curry{3,4}?` and `uncurry{3,4}?` are inverses.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/303solve_ndisj: handle goals containing _ ∖ _ ∖ _2021-07-23T09:16:51ZRalf Jungjung@mpi-sws.orgsolve_ndisj: handle goals containing _ ∖ _ ∖ _This resolves the last remaining `solve_ndisj` FIXME in lambda-rust. :)This resolves the last remaining `solve_ndisj` FIXME in lambda-rust. :)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/302`Params` and `Proper` instances for `curry` and friends2021-07-21T17:11:43ZRobbert Krebbers`Params` and `Proper` instances for `curry` and friendshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/301rename map_union_subseteq_l_alt → map_union_subseteq_l' (and likewise for _r)2021-07-21T11:04:34ZRalf Jungjung@mpi-sws.orgrename map_union_subseteq_l_alt → map_union_subseteq_l' (and likewise for _r)This is more consistent with `or_intro_{l,r}'` and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/300.This is more consistent with `or_intro_{l,r}'` and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/300.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/300solve_ndisj: solve more goals involving chains of differences2021-07-21T11:16:09ZRalf Jungjung@mpi-sws.orgsolve_ndisj: solve more goals involving chains of differencesThis improves `solve_ndisj` to handle goals that came up in iris/examples as part of the logically atomic triple mask change.This improves `solve_ndisj` to handle goals that came up in iris/examples as part of the logically atomic triple mask change.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/299alternative implementation of mk_evar that keeps naive_solver working2021-07-21T07:06:02ZRalf Jungjung@mpi-sws.orgalternative implementation of mk_evar that keeps naive_solver workingThis uses [a hack](https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884) to have side-effects in an ltac that returns a value.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issu...This uses [a hack](https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884) to have side-effects in an ltac that returns a value.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/115https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/298Mark gset methods as simpl never to stop `cbn` from unfolding them2021-07-28T14:15:12ZPaolo G. GiarrussoMark gset methods as simpl never to stop `cbn` from unfolding themThis clarifies what's meant to happen anyway, and is apparently needed for `cbn`. (I haven't yet tried doing this at the `mapset` level).
Example of the problem: without this change, `cbn` mangles the goal in the following:
```
Goal {...This clarifies what's meant to happen anyway, and is apparently needed for `cbn`. (I haven't yet tried doing this at the `mapset` level).
Example of the problem: without this change, `cbn` mangles the goal in the following:
```
Goal {[1; 2; 3]} =@{gset nat} ∅.
Fail progress simpl.
progress cbn. Show.
```
I'd want `progress cbn` to fail, instead the above gives:
```
The command has indeed failed with message:
Failed to progress.
1 subgoal
============================
{| mapset_car := {[1 := ()]} ∪ {[2 := ()]} ∪ {[3 := ()]} |} = ∅
```