stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-09-27T14:17:27Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/326f_equiv: slightly better support for function relations2021-09-27T14:17:27ZRalf Jungjung@mpi-sws.orgf_equiv: slightly better support for function relationsThis makes f_equiv more powerful: with it we can solve goals of the form `f x ≡ g x` where `f, g: X -d> OFE` and `f ≡ g`. We still make no attempt at solving goals where the arguments are different. I think in all cases where this applie...This makes f_equiv more powerful: with it we can solve goals of the form `f x ≡ g x` where `f, g: X -d> OFE` and `f ≡ g`. We still make no attempt at solving goals where the arguments are different. I think in all cases where this applies, it will finish the proof, so I added a `solve`.
I also added the testcases from https://gitlab.mpi-sws.org/iris/stdpp/-/commit/d16ab1aaa77ed3a9b052d12496d92c102288b704.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/323add size_set_seq2021-09-13T21:16:30ZRalf Jungjung@mpi-sws.orgadd size_set_seqhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/324add size_difference2021-09-10T15:07:06ZRalf Jungjung@mpi-sws.orgadd size_differencehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/322Revert "Merge branch 'robbert/sprop' into 'master'"2021-09-08T21:26:20ZRalf Jungjung@mpi-sws.orgRevert "Merge branch 'robbert/sprop' into 'master'"This reverts merge request !309. It turned out to be a breaking change due to shadowing imports, and also cause performance regression in at least one case (see https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/732#note_73457).This reverts merge request !309. It turned out to be a breaking change due to shadowing imports, and also cause performance regression in at least one case (see https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/732#note_73457).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/319add lemma list_in_dec2021-09-06T18:03:40ZRalf Jungjung@mpi-sws.orgadd lemma list_in_decI think this lemma is by @haidang, but it might also be by @lgaeher.
Maybe this should be an `Instance`? Not sure.I think this lemma is by @haidang, but it might also be by @lgaeher.
Maybe this should be an `Instance`? Not sure.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/318treat Forall2 constructors like we treat Forall constructors2021-09-06T16:19:42ZRalf Jungjung@mpi-sws.orgtreat Forall2 constructors like we treat Forall constructorsIn particular, have a lemma `Forall2_cons` that is an `↔`.
For consistency, rename `Forall2_cons_inv` to `Forall2_cons_1` (matching `Forall_cons_1`).
Someone should probably do the same for `Forall3`...In particular, have a lemma `Forall2_cons` that is an `↔`.
For consistency, rename `Forall2_cons_inv` to `Forall2_cons_1` (matching `Forall_cons_1`).
Someone should probably do the same for `Forall3`...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/320relate size of map to size of its domain2021-09-05T03:04:45ZRalf Jungjung@mpi-sws.orgrelate size of map to size of its domainhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/321add map_size_disj_union2021-09-05T02:48:55ZRalf Jungjung@mpi-sws.orgadd map_size_disj_unionhttps://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/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/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/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 := ()]} |} = ∅
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/245Add more lemmas for FinMaps (for union, filter, difference)2021-07-28T14:24:18ZHai DangAdd more lemmas for FinMaps (for union, filter, difference)Some lemmas that I believe worth upstreaming.Some lemmas that I believe worth upstreaming.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/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`