stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-01-28T09:18:33Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/222Rename `_11` and `_12` suffixes into `_1_1` and `_1_2`2021-01-28T09:18:33ZRobbert KrebbersRename `_11` and `_12` suffixes into `_1_1` and `_1_2`Rename `_11` and `_12` into `_1_1` and `_1_2`, respectively. These suffixes are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas.
The previous suffixes looked like lemma number 11 and 12, respectively.Rename `_11` and `_12` into `_1_1` and `_1_2`, respectively. These suffixes are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas.
The previous suffixes looked like lemma number 11 and 12, respectively.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/221Fix documentation of `select` to state that it selects the "last" hypothesis.2021-01-27T17:30:44ZRobbert KrebbersFix documentation of `select` to state that it selects the "last" hypothesis.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/220Rename instance `finmap_lookup_total` → `map_lookup_total`.2021-01-20T12:58:57ZRobbert KrebbersRename instance `finmap_lookup_total` → `map_lookup_total`.This this is an instance, not a definition, it _should_ not affect anyone.This this is an instance, not a definition, it _should_ not affect anyone.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/219remove unused find_pat tactic2021-01-20T11:44:26ZRalf Jungjung@mpi-sws.orgremove unused find_pat tacticCloses https://gitlab.mpi-sws.org/iris/stdpp/-/issues/93Closes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/93https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/218add rename-by-pattern tactic2021-01-20T11:31:14ZRalf Jungjung@mpi-sws.orgadd rename-by-pattern tactic`rename_pat` would be a shorter name, but OTOH this is more consistent with the existing `select`-style tactics so maybe that's the better choice.`rename_pat` would be a shorter name, but OTOH this is more consistent with the existing `select`-style tactics so maybe that's the better choice.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/217add map_zip_diag and the lemmas required for that2021-01-20T12:58:41ZRalf Jungjung@mpi-sws.orgadd map_zip_diag and the lemmas required for thatIs `map_fmap_omap` truly new? I was surprised to not find an existing lemma like that.Is `map_fmap_omap` truly new? I was surprised to not find an existing lemma like that.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/216Remove hint db and import of omega, since omega will be removed from Coq.2021-01-19T11:33:34ZRobbert KrebbersRemove hint db and import of omega, since omega will be removed from Coq.See https://github.com/coq/coq/pull/13741#issuecomment-762761112See https://github.com/coq/coq/pull/13741#issuecomment-762761112https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/215add zip_with_diag and zip_diag2021-01-19T10:57:10ZRalf Jungjung@mpi-sws.orgadd zip_with_diag and zip_diaghttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/214fix and reject warnings on Coq 8.132021-01-19T10:57:59ZRalf Jungjung@mpi-sws.orgfix and reject warnings on Coq 8.13https://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_singletonhttps://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.