stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-10-02T15:12:18Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/325f_equiv optimizations2021-10-02T15:12:18ZRalf Jungjung@mpi-sws.orgf_equiv optimizationsThis makes f_equiv a lot faster.
The first commit is inspired by looking at [this line](https://github.com/mit-pdos/perennial/blob/3ebb6f05456e2378e687e7eb99c30001930ff396/src/program_logic/crash_weakestpre.v#L105) in Perennial: the ver...This makes f_equiv a lot faster.
The first commit is inspired by looking at [this line](https://github.com/mit-pdos/perennial/blob/3ebb6f05456e2378e687e7eb99c30001930ff396/src/program_logic/crash_weakestpre.v#L105) in Perennial: the very first f_equiv there takes 30s. 20s of that are spent in `simple apply (_ : Proper (R ==> R) f)`, where `f` is `bi_and <some complicated term>` -- basically is tries to treat bi_and as a unary function and takes forever to realize that will not work. There is no TC trace for this, so this must be all unification time. By changing the pattern for this arm from `?R (?f _) _` to `?R (?f _) (?f _)` we avoid entering it unless things match *syntactically*. This seeds up the first f_equiv from 30s to 10s.
The second commit is born from looking at that same line more, and also looking at [the equivalent line in Iris itself](https://gitlab.mpi-sws.org/iris/iris/-/blob/467fa48bc66c2f2459f379a69fd9a41840599e23/iris/program_logic/weakestpre.v#L122): according to the ltac profiler, almost all time is spent in `try simple apply reflexivity` -- again, unification of inequal terms being very slow. So we now do entirely syntactic unification before even trying this. This speeds up the `do 23 (f_contractive || f_equiv)` in Iris from 1.3s to 0.6s, and it speeds up the `do 22 (f_contractive || f_equiv)` in Perennial to 0.75s from originally 42s (22s after the previous commit) -- a whopping 50x overall improvement!
Later commits slightly relax this to fix compatibility, so the fallback cases now do perform unification to match up the functions on the left-hand and right-hand side -- but this barely slows down the benchmarks mentioned above since they do not usually hit those cases. In fact, both in the Iris and Perennial case, 66% of the time is now spent in `f_contractive`.https://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`, `Qp`, and `coPset`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.