stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-10-26T09:46:19Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/183Swap import of Peano and Utf8 to ensure that Utf8 notations are preferred.2020-10-26T09:46:19ZHugo HerbelinSwap import of Peano and Utf8 to ensure that Utf8 notations are preferred.Coq PR [#12950](https://github.com/coq/coq/pull/12950), among others changes, gives to import the effect of reactivating the imported notations.
This has an impact for stdpp, e.g. on printing `le n m` as either `m <= n` or `m ≤ n`, due ...Coq PR [#12950](https://github.com/coq/coq/pull/12950), among others changes, gives to import the effect of reactivating the imported notations.
This has an impact for stdpp, e.g. on printing `le n m` as either `m <= n` or `m ≤ n`, due to the order of imports between `Utf8.v` and `Peano.v` in `base.v`.
The Coq PR is still at the beginning of a process of discussion but the change to stdpp is backward compatible (as far as I can judge) and it should be safe to merge it anyway.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/179Add lemmas and max for Qp2020-10-27T13:54:55ZSimon Friis VindumAdd lemmas and max for QpAdd a few extra lemmas for `Qp` and adds a `max` operation for `Qp`. The lemmas for `max` are not exhaustive. The names of the lemmas are consistent with those in [GenericMinMax](https://coq.inria.fr/library/Coq.Structures.GenericMinMax....Add a few extra lemmas for `Qp` and adds a `max` operation for `Qp`. The lemmas for `max` are not exhaustive. The names of the lemmas are consistent with those in [GenericMinMax](https://coq.inria.fr/library/Coq.Structures.GenericMinMax.html).
The library `GenericMinMax` contains a way to implement `max` (see for instance [how it's used with `Q`](https://coq.inria.fr/library/Coq.QArith.Qminmax.html)). I'm not sure if that's the better way to do it. But, modules aren't used in this way anywhere in stdpp so I opted to not use it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/197Remove dead type classes and notations.2020-10-28T19:00:01ZRobbert KrebbersRemove dead type classes and notations.These were very specific, there were no lemmas about them. They were used back in the days for some specific things in my C semantics.
Thanks to @blaisorblade for pointing out.These were very specific, there were no lemmas about them. They were used back in the days for some specific things in my C semantics.
Thanks to @blaisorblade for pointing out.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/195add dom_insert_lookup2020-10-28T19:21:46ZRalf Jungjung@mpi-sws.orgadd dom_insert_lookupI was just looking for this lemma and couldn't find it, so I figured it might be good to add. :)I was just looking for this lemma and couldn't find it, so I figured it might be good to add. :)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/196add a function to obtain a set with all elements of a finite type2020-10-29T09:20:15ZRalf Jungjung@mpi-sws.orgadd a function to obtain a set with all elements of a finite typeThis lets us use the existing nice `gmap`/`gset` infrastructure even for total functions when the domain type is finite.This lets us use the existing nice `gmap`/`gset` infrastructure even for total functions when the domain type is finite.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/149Add a way to disable typeclass search in `Program` obligations2020-11-03T12:13:26ZPaolo G. GiarrussoAdd a way to disable typeclass search in `Program` obligationsFrom the coqdoc of the new feature:
```coq
(** When using [Program], you can use [notc_hole] in place of [_] to create
an obligation that does not trigger typeclass search. That is useful if the
search fails slowly, for instance for [Pro...From the coqdoc of the new feature:
```coq
(** When using [Program], you can use [notc_hole] in place of [_] to create
an obligation that does not trigger typeclass search. That is useful if the
search fails slowly, for instance for [Proper] obligations.
Should https://github.com/coq/coq/issues/12147 be fixed, this can be
deprecated or replaced by the new syntax. *)
```
#### Rationale for inclusion
I think https://github.com/coq/coq/issues/12147 is potentially bad enough that it could belong in stdpp. I haven't found very compelling usecases in iris: in part, you already avoid writing `Program Definition foo ...: A -n> B`, at the cost of more boilerplate.
See also: discussion from https://mattermost.mpi-sws.org/iris/pl/r885z6apefr9bjpuctczruogrr onwards.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/198WIP: Pretty-print 0 as "0" for N, Z, and nat2020-11-10T10:29:06ZTej Chajedtchajed@gmail.comWIP: Pretty-print 0 as "0" for N, Z, and natFormerly printed as an empty string.Formerly printed as an empty string.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/199Add lemmas about `list_to_map`2020-11-10T11:51:29ZSimon Friis VindumAdd lemmas about `list_to_map`Adds two lemmas about `list_to_map` that seem generally useful.Adds two lemmas about `list_to_map` that seem generally useful.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/200Pretty-print 0 as "0" for N, Z, and nat2020-11-11T16:03:15ZRobbert KrebbersPretty-print 0 as "0" for N, Z, and natAlternative to #198 that is correct. This MR also:
- Adds test cases.
- Proves injectivity of `pretty` for `Z`.
- Refactored the code a bit by turning some results into lemmas.Alternative to #198 that is correct. This MR also:
- Adds test cases.
- Proves injectivity of `pretty` for `Z`.
- Refactored the code a bit by turning some results into lemmas.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/201Set `Hint Mode` for `pretty`.2020-11-12T12:17:24ZRobbert KrebbersSet `Hint Mode` for `pretty`.Title says it all.Title says it all.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/203Replace unused pattern variables with underscore2020-11-26T10:24:52ZTej Chajedtchajed@gmail.comReplace unused pattern variables with underscoreAddresses new unused-pattern-matching-variable warning on Coq master (see https://github.com/coq/coq/pull/12768).
I'm pretty sure the `hlist.v` warning is a bug in Coq's heuristics for this, since those variables are used as implicit ar...Addresses new unused-pattern-matching-variable warning on Coq master (see https://github.com/coq/coq/pull/12768).
I'm pretty sure the `hlist.v` warning is a bug in Coq's heuristics for this, since those variables are used as implicit arguments and I don't see why the pattern matches more than one case (the warning is also printed twice for the same definition). Maybe there's something in the elaborated term I'm missing, which Coq doesn't even print back?
Regardless of what's going on in Coq, it's much easier for us to suppress the warning than to try to fix this upstream.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/202Add explicit Global to hints at top level2020-12-03T17:17:30ZTej Chajedtchajed@gmail.comAdd explicit Global to hints at top levelFixes new Coq master warning deprecated-hint-without-locality: https://github.com/coq/coq/pull/13384.
I created this largely automatically based on the assumption that hints in sections would be indented. If some aren't, this MR will ch...Fixes new Coq master warning deprecated-hint-without-locality: https://github.com/coq/coq/pull/13384.
I created this largely automatically based on the assumption that hints in sections would be indented. If some aren't, this MR will change them to global when they should be left alone (implicitly as local). I haven't carefully audited that this didn't happen.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/204add insert_subseteq_l2020-12-04T18:57:23ZRalf Jungjung@mpi-sws.orgadd insert_subseteq_lA useful little lemma to iteratively build up map inclusion (just needed this in Perennial).A useful little lemma to iteratively build up map inclusion (just needed this in Perennial).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/205Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename...2021-01-07T08:30:19ZRobbert KrebbersRemove duplicate `map_fmap_empty` of `fmap_empty`, and rename...Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/207explicit Local/Global for all Instance, Arguments, Hint2021-01-07T12:44:21ZRalf Jungjung@mpi-sws.orgexplicit Local/Global for all Instance, Arguments, HintThis applies the script from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/609 to std++. I slightly extended the script to also handle `Arguments` and `Hint`:
```python
#!/usr/bin/env python3
# Add Local or Global to any unqual...This applies the script from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/609 to std++. I slightly extended the script to also handle `Arguments` and `Hint`:
```python
#!/usr/bin/env python3
# Add Local or Global to any unqualified Instance declarations. Tracks whether
# a section is open and adds Global outside any section and Local inside one.
import sys
import re
SECTION_RE = re.compile("""\s*Section\s+(?P<name>\w*).*\..*""")
END_RE = re.compile("""\s*End\s+(?P<name>\w*).*\..*""")
# Do not adjust `Hint Rewrite`, it does not support visibility.
ADJUST_VERNAC_RE = re.compile("""(?P<indent>\s*)(?P<vernac>(Instance|Arguments|Hint (Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold))\s.*)""")
def qualify_lines(lines):
"""Qualify instances in text given as a list of lines."""
# tracks the list of sections open
section_stack = []
out = []
for line in lines:
m = SECTION_RE.match(line)
if m:
name = m.group("name")
section_stack.append(name)
m = END_RE.match(line)
if m:
name = m.group("name")
# close a section if it's open (name may not match because End is
# for a module instead)
if len(section_stack) > 0 and section_stack[-1] == name:
section_stack.pop()
m = ADJUST_VERNAC_RE.match(line)
if m:
indent = m.group("indent")
modifier = "Local" if section_stack else "Global"
vernac = m.group("vernac")
line = f"{indent}{modifier} {vernac}\n"
out.append(line)
if section_stack:
print(f"oops {section_stack} remaining", file=sys.stderr)
sys.exit(1)
return out
for fname in sys.argv[1:]:
print(f"processing {fname}")
with open(fname) as f:
lines = f.readlines()
with open(fname, "w") as f:
lines = qualify_lines(lines)
f.writelines(lines)
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/209prove take_02021-01-11T17:18:29ZRalf Jungjung@mpi-sws.orgprove take_0This is taken from Perennial.This is taken from Perennial.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/211upstream some list_numbers lemmas from Perennial2021-01-11T19:10:10ZRalf Jungjung@mpi-sws.orgupstream some list_numbers lemmas from PerennialAlso rename `seq_S_end_app` to `seq_S_snoc`, which I think better matches our usual name for lemmas involving `_ ++ [_]`.
The proofs are by @tchajed.Also rename `seq_S_end_app` to `seq_S_snoc`, which I think better matches our usual name for lemmas involving `_ ++ [_]`.
The proofs are by @tchajed.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/212Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib2021-01-11T19:42:41ZRobbert KrebbersRename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlibThe lemma `seq_S` is present in Coq's stdlib since Coq 8.12, and is the same as our lemma `seq_S_snoc`.
MR !211 accidentally used the lemma `seq_S` from the stdlib, and hence CI failed with Coq 8.10 and Coq 8.11.
This MR adds a copy of...The lemma `seq_S` is present in Coq's stdlib since Coq 8.12, and is the same as our lemma `seq_S_snoc`.
MR !211 accidentally used the lemma `seq_S` from the stdlib, and hence CI failed with Coq 8.10 and Coq 8.11.
This MR adds a copy of the lemma from the stdlib, which we can remove once we drop support for Coq 8.10 and Coq 8.11.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/208prove map_size_delete, map_size_insert_Some, map_to_list_delete2021-01-11T19:43:38ZRalf Jungjung@mpi-sws.orgprove map_size_delete, map_size_insert_Some, map_to_list_delete`map_size_insert_Some` exists in Perennial as map_size_insert_overwrite, but with a very different proof.`map_size_insert_Some` exists in Perennial as map_size_insert_overwrite, but with a very different proof.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/213add set_map_union, set_map_singleton2021-01-15T10:36:34ZRalf Jungjung@mpi-sws.orgadd set_map_union, set_map_singleton