stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-04-28T17:36:44Zhttps://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/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/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/466Add lemmas about the union and intersection of filters on maps2023-07-29T12:51:37ZMarijn van Wezelmarijn.vanwezel@ru.nlAdd lemmas about the union and intersection of filters on mapsWhen merged, this merge request adds two new lemmas about the intersection and the union of filters on maps, as well as a supporting lemma about the intersection of lookups (such a supporting lemma already existed for unions, `lookup_uni...When merged, this merge request adds two new lemmas about the intersection and the union of filters on maps, as well as a supporting lemma about the intersection of lookups (such a supporting lemma already existed for unions, `lookup_union`). The proofs for the two primary lemmas were in part made with the help of Robbert.
To support the intersection of lookups, I had to create an instance of `Intersection` for the `option` type. This instance has the following behaviour:
* `None ∩ None` → `None`
* `Some a ∩ None` → `None`
* `None ∩ Some b` → `None`
* `Some a ∩ Some b` → `Some a`
This means that the intersection of `option` does not have a left identity. I am not sure if this is a problem.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/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/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/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/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/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/459Finite map composition2023-09-28T14:01:30ZDorian LesbreFinite map composition- Add a `map_compose` operator for finite map composition
- Add notation `m ∘ₘ n` for `map_compose m n`
- Add various lemmas to manipulate map composition
This is arguably a niche operator we might not want to include.
If you think that...- Add a `map_compose` operator for finite map composition
- Add notation `m ∘ₘ n` for `map_compose m n`
- Add various lemmas to manipulate map composition
This is arguably a niche operator we might not want to include.
If you think that is the case feel free to close without merging.
I'm submitting in case someone else would have a use for it, since this
is now fairly complete (although it could use some compatibility lemmas with `insert`).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/457Add `by` parameter to `multiset_solver`2023-03-20T11:12:29ZRobbert KrebbersAdd `by` parameter to `multiset_solver`The tactics `naive_solver` and `set_solver` have a `by` parameter to specify the tactic that is used on the leafs. This MR adds such a parameter to `multiset_solver` too, and similar to `naive_solver`/`set_solver` lets it default to `eau...The tactics `naive_solver` and `set_solver` have a `by` parameter to specify the tactic that is used on the leafs. This MR adds such a parameter to `multiset_solver` too, and similar to `naive_solver`/`set_solver` lets it default to `eauto`.
I cannot easily come up with useful test cases where we need the full power of `eauto`. Either just `fast_done` is sufficient (e.g., if the goal is an equality, see `test_goal_{1,2}` and `gmultiset_singleton_subseteq`) or you need `eauto` with some hints (see `test_goal_3`). Nonetheless, I think it makes sense to be consistent with `naive_solver`/`set_solver` to avoid issues such as !420.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/455Various tweaks to lists, maps, sets2023-03-21T16:36:03ZRobbert KrebbersVarious tweaks to lists, maps, setsWhile reviewing !442 and !441 I ran into a bunch of stuff that should be improved:
- Add `subset_proper`.
- Add `list_eq_prefix_length` and `list_eq_suffix_length`. **The version for `prefix` is also part of !441, but the version for `s...While reviewing !442 and !441 I ran into a bunch of stuff that should be improved:
- Add `subset_proper`.
- Add `list_eq_prefix_length` and `list_eq_suffix_length`. **The version for `prefix` is also part of !441, but the version for `suffix` was missing there.**
- Add `set_equiv_subseteq_size` and `set_eq_subseteq_size`. **Similar to the prior lemmas, but now for set equality. These are not part of !441 and !442.**
- Add `dom_subseteq_size`, `dom_subset_size`, `map_eq_subseteq_dom`. **The last lemma is part of !442, but the version in this MR is stronger since it requires `Set_` instead of `FinSet`)**
- Add `map_eq_subseteq_size`, `map_subseteq_size`, `map_subset_size`. **These lemmas are also part of !442, but the statement and naming are made consistent with similar lemmas for sets, and the proof have been shortened.**
- Add `Permutation_submseteq_length` to replace `Permutation_alt`, `submseteq_Permutation_length_le` and `submseteq_Permutation_length_eq`. **This makes the statement and naming consistent with the new lemmas for prefix/suffix/sets/maps**
- Simplify proofs of map induction principles; remove `map_to_list_length`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/454Rename `map_preimage` into `map_preimg` (to be consistent with `dom`).2023-03-19T19:47:33ZRobbert KrebbersRename `map_preimage` into `map_preimg` (to be consistent with `dom`).For the domain of a map we use `dom`, not `domain`.
So it makes sense to also use `img` instead of `image`. In !444 we already do that for the proper image, so let's do too for the pre-image.For the domain of a map we use `dom`, not `domain`.
So it makes sense to also use `img` instead of `image`. In !444 we already do that for the proper image, so let's do too for the pre-image.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/453Improve `bijective_finite`.2023-03-19T18:21:39ZRobbert KrebbersImprove `bijective_finite`.Make the statement stronger by no longer requiring an inverse.
Make the implementation more efficient by not filtering duplicates.Make the statement stronger by no longer requiring an inverse.
Make the implementation more efficient by not filtering duplicates.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/452Add scalar multiplication for multisets.2023-03-19T20:27:14ZRobbert KrebbersAdd scalar multiplication for multisets.The operation `n *: X` multiplies the multiplicity of each element `x ∈ X` with `n`
This MR:
- Introduces a type class `ScalarMul N A := N → A → A` with associated notations for scalar multiplication. The notation `*:` is taken from ss...The operation `n *: X` multiplies the multiplicity of each element `x ∈ X` with `n`
This MR:
- Introduces a type class `ScalarMul N A := N → A → A` with associated notations for scalar multiplication. The notation `*:` is taken from ssreflect, see https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnotations.v
- Provides an instance `ScalarMul nat (gmultiset A)`.
- Provides a bunch of lemmas for `*:` on multisets
- Extends `multiset_solver` and adds a couple of tests.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`?