stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-01-11T19:42:41Zhttps://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/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/210rename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteq2021-02-01T11:56:08ZRalf Jungjung@mpi-sws.orgrename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteqThis hopefully makes the lemmas easier to find.This hopefully makes the lemmas easier to find.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/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/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/206Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}`.2021-01-23T10:14:39ZRobbert KrebbersVarious `omap` lemmas for finite maps; generalize `map_size_{insert,delete}`.- Add lemma `map_omap_union`.
- Add lemmas `map_disjoint_fmap` and `map_disjoint_omap`.
- Add lemmas `fmap_merge` and `omap_merge`.
- Add lemma `omap_delete`.
- Generalize `omap_insert` and `omap_singleton` to cover both the `Some` and `...- Add lemma `map_omap_union`.
- Add lemmas `map_disjoint_fmap` and `map_disjoint_omap`.
- Add lemmas `fmap_merge` and `omap_merge`.
- Add lemma `omap_delete`.
- Generalize `omap_insert` and `omap_singleton` to cover both the `Some` and `None` case. Add `_Some` and `_None` versions of the lemmas for the specific cases.
- Generalize `map_size_insert` and `map_size_delete` in the same way.
- Add lemmas `lookup_fmap_Some`, `lookup_omap_Some`, and `lookup_omap_id_Some`.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/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/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/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/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/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/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/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/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/194Add map_fmap_union for FinMap2020-10-21T06:57:40ZTej Chajedtchajed@gmail.comAdd map_fmap_union for FinMaphttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/193Avoid relying on implicit instance generalization, and name some instances.2020-10-15T17:44:59ZRobbert KrebbersAvoid relying on implicit instance generalization, and name some instances.Fix in preparation for https://github.com/coq/coq/pull/13188
I didn't name the `Forall2` instances, since I could not come up with a good naming scheme. So, I just used the `∀`.
There are probably plenty of other unnamed instances, but...Fix in preparation for https://github.com/coq/coq/pull/13188
I didn't name the `Forall2` instances, since I could not come up with a good naming scheme. So, I just used the `∀`.
There are probably plenty of other unnamed instances, but I would prefer defer naming them.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/191update Makefile2020-10-06T15:03:28ZRalf Jungjung@mpi-sws.orgupdate MakefileJust using an MR to make sure this builds on CI.Just using an MR to make sure this builds on CI.