stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-03-21T16:45:56Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/449Rename `option_union_Some` → `union_Some`2023-03-21T16:45:56ZRobbert KrebbersRename `option_union_Some` → `union_Some`See discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/432#note_87085
This removes `option_` if there's already something else in the name to disambiguate, here that is `_Some`.
We could also prefix everything with `o...See discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/432#note_87085
This removes `option_` if there's already something else in the name to disambiguate, here that is `_Some`.
We could also prefix everything with `option_`, but that would require more changes. For better or worse, I think this MR matches the consensus we also have for lists, maps, sets (e.g., having `lookup_app_Some` instead of `list_lookup_app_Some`).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439add basic list functionality with Z-based indexing2023-03-23T22:10:13ZRalf Jungjung@mpi-sws.orgadd basic list functionality with Z-based indexingThis starts the work on https://gitlab.mpi-sws.org/iris/stdpp/-/issues/108 by implementing `insert` and `index` for `Z` as well as `lengthZ`, `takeZ`, `dropZ`, and porting much of the associated theory.
I have not ported everything, e.g...This starts the work on https://gitlab.mpi-sws.org/iris/stdpp/-/issues/108 by implementing `insert` and `index` for `Z` as well as `lengthZ`, `takeZ`, `dropZ`, and porting much of the associated theory.
I have not ported everything, e.g. the interactions with `Forall3`, `subseteq`, `submseteq`, `filter`, `mask` are missing. Also there are more operations that would need a Z-based version, such as `lookup_total`, `alter`, `delete`, `inserts`, `find`, `imap`, `imap2`, `resize`, `rotate`, `rotate_take`, `sublist_lookup`, `sublist_alter`. There are also some tactics that will not handle these new operations and so might need adjustments or Z-based tactics: `solve_length`, `simplify_list_eq`.
Still I think this is a useful start that can serve as a foundation for later extensions. :)
Blocked on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/441.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/442miscellaneous map lemmas2023-03-24T15:49:54ZRalf Jungjung@mpi-sws.orgmiscellaneous map lemmassome of these are from Perennialsome of these are from Perennialhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/441Add some list lemmas2023-03-24T15:54:25ZRalf Jungjung@mpi-sws.orgAdd some list lemmasThis fixes some inconsistencies and gaps that I noticed while working on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439, and ports some list lemmas from Perennial.This fixes some inconsistencies and gaps that I noticed while working on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439, and ports some list lemmas from Perennial.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/460Extend `set_solver` with support for `set_Forall` and `set_Exists`.2023-04-11T09:33:09ZRobbert KrebbersExtend `set_solver` with support for `set_Forall` and `set_Exists`.This closes issue #178This closes issue #178https://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...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...2023-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.)