stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-05-10T06:45:06Zhttps://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.152023-05-02T18:32:29ZRobbert 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-05-01T07:48:24ZRobbert 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-05-01T13:18:01ZMarijn 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/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.