stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-05-30T16:39:39Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/479Fix tests for coq#176482023-05-30T16:39:39ZMichael SammlerFix tests for coq#17648See https://github.com/coq/coq/pull/17648#issuecomment-1568700456 . This MR simply removes the offending test because the test has already caused problems previously (https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/421) and does n...See https://github.com/coq/coq/pull/17648#issuecomment-1568700456 . This MR simply removes the offending test because the test has already caused problems previously (https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/421) and does not seem that useful.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/478Add lemmas for commuting funcs with folds2023-08-03T13:22:40ZIsaac van Bakelisaac.vanbakel@inf.ethz.chAdd lemmas for commuting funcs with foldsThese lemmas were helpful to me in recent proofs (in particular, the multiset one is used for iris/iris#923.) They allow for moving a unitary function on a fold accumulator in and out of the fold as necessary, provided the function commu...These lemmas were helpful to me in recent proofs (in particular, the multiset one is used for iris/iris#923.) They allow for moving a unitary function on a fold accumulator in and out of the fold as necessary, provided the function commutes appropriately with the fold function.
~~The location of the multiset lemma in the file is not ideal, since it has to come after `gmultiset_ind`, which is well after all the other fold lemmas. However, proving it without `gmultiset_ind` is much harder, and moving `gmultiset_ind` further up the file is itself non-trivial, so I've opted not to try.~~ Fixed by Robbert's changes.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/477Revert "Merge branch 'ralf/mangled' into 'master'"2023-05-10T06:45:06ZRobbert KrebbersRevert "Merge branch 'ralf/mangled' into 'master'"This reverts commit 6a7d163ca1b3d7ebccbb089c39ff1cd69799451b, reversing
changes made to 40e5274f6235ddbea3a187da79bc4871aebb6688.
See https://gitlab.mpi-sws.org/iris/stdpp/-/issues/184This reverts commit 6a7d163ca1b3d7ebccbb089c39ff1cd69799451b, reversing
changes made to 40e5274f6235ddbea3a187da79bc4871aebb6688.
See https://gitlab.mpi-sws.org/iris/stdpp/-/issues/184https://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.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/475enable name-mangling-light2023-05-10T06:45:08ZRalf Jungjung@mpi-sws.orgenable name-mangling-lightFor instance, the proof state after the `intros.` in `lookup_total_app_l` now looks like
```
A : Type
__Inhabited : Inhabited A
l1, l2 : list A
i : nat
__H : i < length l1
============================
(l1 ++ l2) !!! i = l1 ...For instance, the proof state after the `intros.` in `lookup_total_app_l` now looks like
```
A : Type
__Inhabited : Inhabited A
l1, l2 : list A
i : nat
__H : i < length l1
============================
(l1 ++ l2) !!! i = l1 !!! i
```
I like it. :) I think we can just always enable this and not have anything extra on CI; we will hopefully notice when proof scripts contain such an identifier starting with `__`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/473Take advantage of new Coq features in Coq 8.152024-04-20T07:38:40ZRobbert KrebbersTake advantage of new Coq features in Coq 8.15* [#7725](https://github.com/coq/coq/issues/7725) (8.15): Allows overriding `intuition_solver` instead of shadowing [intuition], see also https://gitlab.mpi-sws.org/iris/stdpp/-/issues/143
* [#14513](https://github.com/coq/coq/issues/145...* [#7725](https://github.com/coq/coq/issues/7725) (8.15): Allows overriding `intuition_solver` instead of shadowing [intuition], see also https://gitlab.mpi-sws.org/iris/stdpp/-/issues/143
* [#14513](https://github.com/coq/coq/issues/14513) (8.15): Allow `Global` on `Typeclasses Opaque`/`Transparent` ~~and `Hint Mode`, inside sections.~~
* [#13952](https://github.com/coq/coq/pull/13952) (8.15): Use hint `!` for `Equiv` type class.
* 8.15: `#[projections(primitive=yes/no)]` for better primitive projection control.
Also I removed an obsolete comment about `omega`, which has been removed since Coq 8.14.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/471Add ssreflect file (from Iris).2023-07-26T15:57:53ZRobbert KrebbersAdd ssreflect file (from Iris).This closes issue #177.This closes issue #177.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/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/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.