stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-04-12T13:54:05Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/420Use `eauto` as default for `set_solver`.2023-04-12T13:54:05ZRobbert KrebbersUse `eauto` as default for `set_solver`.The `set_solver` tactic roughly calls `set_unfold` and then performs `naive_solver`. @jihgfee noticed that `set_solver` (without tactic argument) calls `naive_solver idtac` by default. This is somewhat strange since `naive_solver` (witho...The `set_solver` tactic roughly calls `set_unfold` and then performs `naive_solver`. @jihgfee noticed that `set_solver` (without tactic argument) calls `naive_solver idtac` by default. This is somewhat strange since `naive_solver` (without tactic argument) defaults to `naive_solver eauto`.
Also @jihgfee found an example where `set_solver by idtac` (the current default) is much slower than `set_solver by eauto`.
So I am wondering what's the reason why `set_solver` uses `idtac`? Is that just some arbitrary legacy choice, or does it actually improve performance?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/432add some union_with lemmas2023-04-14T18:43:12ZRalf Jungjung@mpi-sws.orgadd some union_with lemmasThese are taken verbatim from Perennial, where they already existed and I just needed both of them. So there is clearly some need here.
But the lemmas are kind of weird so I am open for discussions for how to better provide them.
- The...These are taken verbatim from Perennial, where they already existed and I just needed both of them. So there is clearly some need here.
But the lemmas are kind of weird so I am open for discussions for how to better provide them.
- The first has a very specific lemma statement with this `λ x' _, Some x'`. This arises from `lookup_union` on maps.
- The second is the same as `left_id`, but never in a hundred years would I have realized I can use that LeftId instance. `union_with` is not a binary operator; I think we need a readable lemma that shows up in `SearchAbout union_with None`. Yes LeftId does show up in that search but I doubt many people will realize that it is useful in this situation -- I have skipped over it myself.
Basically: not everything that can be written as LeftId / RightId, should be written that way. IMO we should only use these classes for things that are actually binary operators, written with infix notation. I don't object to instances also existing in other cases, but those instances should only exist *in addition to* regular lemmas, not instead of them.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/456Add set_omap to finite sets2023-04-18T18:32:41ZDorian LesbreAdd set_omap to finite setsAdd `omap`-like function to finite sets, aka OCaml's `filter_map` operation.
I needed it to destruct a set of `X + Y` into a set of `X` and a set of `Y`.
Also add a few lemmas to reason about it.Add `omap`-like function to finite sets, aka OCaml's `filter_map` operation.
I needed it to destruct a set of `X + Y` into a set of `X` and a set of `Y`.
Also add a few lemmas to reason about it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/451Add NoDup_bind, vec_enum, vec_finite.2023-04-18T18:34:33ZHerman BergwerfAdd NoDup_bind, vec_enum, vec_finite.This adds a function to enumerate all vectors of a given type and a helper lemma about NoDup and bind.
@robbertkrebbers Can `vec_finite` be used to simplify the proof of `list_finite`?This adds a function to enumerate all vectors of a given type and a helper lemma about NoDup and bind.
@robbertkrebbers Can `vec_finite` be used to simplify the proof of `list_finite`?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/458Add NoDup_bind, vec_enum, vec_finite (new version with proper branch)2023-04-18T18:39:40ZRobbert KrebbersAdd NoDup_bind, vec_enum, vec_finite (new version with proper branch)Follow up of !451, but with a branch where I can push.Follow up of !451, but with a branch where I can push.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/462Add `min` and `max` infix notations for `positive`.2023-04-19T12:00:20ZRobbert KrebbersAdd `min` and `max` infix notations for `positive`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/404Rename plus/minus → add/sub and put number lemmas in modules to be consistent with Coq stdlib2023-04-22T18:02:11ZRobbert KrebbersRename plus/minus → add/sub and put number lemmas in modules to be consistent with Coq stdlibRename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current convention for numbers.
Following the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/821Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current convention for numbers.
Following the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/821Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/467Add lemma `map_zip_fst_snd`.2023-04-24T09:03:54ZRobbert KrebbersAdd lemma `map_zip_fst_snd`.This lemma is analogue to the one on lists.This lemma is analogue to the one on lists.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/463Use `positive` in `gmultiset` representation to avoid off-by-one computations.2023-04-24T09:07:53ZRobbert KrebbersUse `positive` in `gmultiset` representation to avoid off-by-one computations.- The only lemma where the use of internal use `nat` appeared was `gmultiset_subseteq_alt`, but that lemma talks about `gmultiset_car`, which should be private. I thus flagged that lemma as `Local`.
- This change also gives rise to more ...- The only lemma where the use of internal use `nat` appeared was `gmultiset_subseteq_alt`, but that lemma talks about `gmultiset_car`, which should be private. I thus flagged that lemma as `Local`.
- This change also gives rise to more compact representations (that is logarithmic instead of linear in terms of the largest multiplicity), but since the multiplicity and scalar_mult functions (as part of the public API) use `nat`, it's difficult to come up with an example where this improvement can be observed.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/440drop support for Coq 8.12 and 8.132023-04-24T09:15:28ZRalf Jungjung@mpi-sws.orgdrop support for Coq 8.12 and 8.13Dropping 8.12 is needed for `Zify.zify_pre_hook` in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439.
I also propose we document an official support policy of supporting always at least the last 3 stable Coq releases. Looking ...Dropping 8.12 is needed for `Zify.zify_pre_hook` in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439.
I also propose we document an official support policy of supporting always at least the last 3 stable Coq releases. Looking at how we dropped old Coq versions in the past, I think this was always true. Most releases of std++ supported 4 or even 5 Coq versions, but 1.2.0 and 1.2.1 only supported 3 versions. However I feel like more than 3 releases shouldn't really be needed: right now this means the oldest Coq we support, Coq 8.14, is more than 14 months old.
Because we are dropping Coq versions anyway, and to test at least with 1 sample the impact of this policy, I suggest we also drop Coq 8.13, so we are down to the minimal set of 3 supported Coq versions.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/470Remove `left associativity` of `scalar_mult` to be compatible with math-comp.2023-04-28T17:36:44ZRobbert KrebbersRemove `left associativity` of `scalar_mult` to be compatible with math-comp.This addresses #181This addresses #181https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/469Let compilation under Coq 8.17 succeed without warnings.2023-04-30T14:55:56ZRobbert KrebbersLet compilation under Coq 8.17 succeed without warnings.## Warning 1
```
Warning: A coercion will be introduced instead of an instance in future
versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or
use '#[global] Existing Instance field.' for compatibility with Coq < ...## Warning 1
```
Warning: A coercion will be introduced instead of an instance in future
versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or
use '#[global] Existing Instance field.' for compatibility with Coq < 8.17).
Beware that the default locality for '::' is #[export], as opposed to
#[global] for ':>' currently. Add an explicit #[global] attribute to the
field if you need to keep the current behavior. For example: "Class foo := {
#[global] field :: bar }." [future-coercion-class-field,records]
```
Since we support Coq versions before 8.17, I just suppress these warnings using `-future-coercion-class-field`
## Warning 2
Variants of:
```
Warning: Notation N.div_lt_upper_bound is deprecated since 8.17.
Use Div0.div_lt_upper_bound instead.
[deprecated-syntactic-definition,deprecated]
```
See https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Backwards.20compatibility.20w.2Er.2Et.2E.20Div0.20without.20warnings for the workaround that has been implemented.
## Warning 3
```
File "./stdpp/base.v", line 47, characters 0-27:
Warning: The default and global localities for this command outside sections
are currently equivalent to the combination of the standard meaning of
"global" (as described in the reference manual), "export" and re-exporting
for every surrounding module. It will change to just "global" (with the
meaning used by the "Set" command) in a future release.
To preserve the current meaning in a forward compatible way, use the
attribute "#[global,export]" and repeat the command with just "#[export]" in
any surrounding modules. If you are fine with the change of semantics,
disable this warning. [deprecated-tacopt-without-locality,deprecated]
```
This is about `Obligation Tactic := idtac`.
Maybe it should be `Export`, but that would be inconsistent with other choices we make `Global`. Since making it `Export` actually changes things, we should investigate that in a separate MR if we deem it necessary.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/464Set `simpl never` for `Pos` and `N`.2023-05-01T06:28:07ZRobbert KrebbersSet `simpl never` for `Pos` and `N`.Previously, we set `simpl never` for just `Pos.mul` and `N.add`. That's pretty inconsistent and annoying. For example:
```coq
Eval simpl in (2 + x)%positive.
(*
= match x with
| q~1 => match q with
| q0~1 => ...Previously, we set `simpl never` for just `Pos.mul` and `N.add`. That's pretty inconsistent and annoying. For example:
```coq
Eval simpl in (2 + x)%positive.
(*
= match x with
| q~1 => match q with
| q0~1 => (Pos.succ q0)~0
| q0~0 => q0~1
| 1 => 2
end~1
| q~0 => match q with
| q0~1 => (Pos.succ q0)~0
| q0~0 => q0~1
| 1 => 2
end~0
| 1 => 3
end
: positive
*)
```
I copied the list of `simpl never` declarations for `Z` and removed the operations (e.g., `opp`) that are not available for `N` or `Pos`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/465Also put results about `N` in a module.2023-05-01T06:34:07ZRobbert KrebbersAlso put results about `N` in a module.It seems we forgot this for `N` in !404.
(Probably because for `N` we just have type class instances and no real lemmas or operations.)It seems we forgot this for `N` in !404.
(Probably because for `N` we just have type class instances and no real lemmas or operations.)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/468Drop support for Coq 8.14.2023-05-01T17:41:36ZRobbert KrebbersDrop support for Coq 8.14.Coq 8.17 has been released, https://github.com/coq/coq/releases/tag/V8.17.0
In https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/440 we decided to support minimal 3 stable Coq versions, so that's 8.17, 8.16, and 8.15.
This means w...Coq 8.17 has been released, https://github.com/coq/coq/releases/tag/V8.17.0
In https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/440 we decided to support minimal 3 stable Coq versions, so that's 8.17, 8.16, and 8.15.
This means we can finally merge !437.
TODO (for @jung): The CI file still means 8.17.dev, that probably should be turned into the stable 8.17 release and we should add 8.18.dev instead.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/437Enable `Hint Mode Equiv` now that stdpp requires Coq 8.122023-05-02T12:48:11ZPaolo G. GiarrussoEnable `Hint Mode Equiv` now that stdpp requires Coq 8.12Includes fixes for Coq 8.12/8.13 — but we might want to drop those.
Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of _those_ annotations. Back then, stdpp didn't because ...Includes fixes for Coq 8.12/8.13 — but we might want to drop those.
Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of _those_ annotations. Back then, stdpp didn't because it still supported Coq 8.11 which suffered from additional bugs (fixed in 8.12) — Iris still has this comment:
```coq
(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
fixed in Coq >= 8.12, which Iris depends on. *)
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/472Make `union_Some` a `↔`, add `union_None` and `union_is_Some`.2023-05-02T15:59:12ZRobbert KrebbersMake `union_Some` a `↔`, add `union_None` and `union_is_Some`.This makes it more consistent with other `Some` lemmas, that are also bidirectional.
See also the discussion https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/466#note_91517
The change to `union_Some` is not backwards compatible, ...This makes it more consistent with other `Some` lemmas, that are also bidirectional.
See also the discussion https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/466#note_91517
The change to `union_Some` is not backwards compatible, so we need to either provide a new lemma (with a new name, but what?) for the `→` direction, or we need to update existing code. It's not clear to me how much `union_Some` is used in reverse dependencies.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/461More canonical maps2023-05-04T12:42:48ZRobbert KrebbersMore canonical mapsThis MR:
- Provides new implementations of `gmap`/`gset`, `Pmap`/`Pset`, `Nmap`/`Nset` and
`Zmap`/`Zset` based on the "canonical" version of binary tries by Appel and
Leroy (see https://inria.hal.science/hal-03372247) that avoid the...This MR:
- Provides new implementations of `gmap`/`gset`, `Pmap`/`Pset`, `Nmap`/`Nset` and
`Zmap`/`Zset` based on the "canonical" version of binary tries by Appel and
Leroy (see https://inria.hal.science/hal-03372247) that avoid the use of Sigma
types and enjoy:
+ More definitional equalities, because maps are no longer equipped with a
proof of canonicity. This means more equalities can be proved by
`reflexivity` or even by conversion as part of unification. For example,
`{[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]}` and `{[ 1 ]} ∖ {[ 1 ]} = ∅`
hold definitionally.
+ The use in nested recursive definitions. For example,
`Inductive gtest := GTest : gmap nat gtest → gtest`. (The old map types
would violate Coq's strict positivity condition due to the Sigma type.)
- Makes `map_fold` a primitive of the `FinMap`, and derive `map_to_list` from it.
(Before `map_fold` was derived from `map_to_list`.) This makes it possible to
use `map_fold` in nested-recursive definitions on maps. For example,
`Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts`.
This MR contains a bunch of tests:
- To show that we indeed have more definitional equalities that can be proved by `reflexivity`.
- We can use `gmap` and `pmap` in nested recursive definitions.
- Computations with `vm_compute` on "big" `pmap`/`gmap`s (size >100.000), which would only terminate if the complexity is n-log-n.
- Compared to the old versions, the computations with `vm_compute` are slightly faster.
- Computations with `reflexivity` on small `pmap`/`gmap`s (size 1000), showing that the even with Coq's naive reduction computation is reasonable (<1 second).
- More tests for `simpl`/`cbn` for `Pmap` (and a fix akin to `Opaque gmap_empty` to make those work). We also should have such tests for `Pset`, but I leave that for a future MR.
/cc @amintimany since we were chatting about this during the PKVM meeting in Aarhus.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/476Simplify definition of `mapset_dom_with`.2023-05-04T19:01:45ZRobbert KrebbersSimplify definition of `mapset_dom_with`.This fixes issue #183
It is not clear that it fixes similar issues. But regardless, I would say that the simplification of the definition of `dom` is a sensible change.This fixes issue #183
It is not clear that it fixes similar issues. But regardless, I would say that the simplification of the definition of `dom` is a sensible change.