stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-02-15T08:40:42Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/226Add several simple lemmas (mostly about list and map filter).2021-02-15T08:40:42ZPaulo Emílio de VilhenaAdd several simple lemmas (mostly about list and map filter).Some simple lemmas about lists and maps. The lemma `map_filter_lookup_eq'` generalises `map_filter_lookup_eq` and can be used to shorten the proof of `map_filter_iff`.Some simple lemmas about lists and maps. The lemma `map_filter_lookup_eq'` generalises `map_filter_lookup_eq` and can be used to shorten the proof of `map_filter_iff`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/225add pred_infinite_surj2021-03-22T11:56:18ZRalf Jungjung@mpi-sws.orgadd pred_infinite_surjI wondered when `pred_infinite (P ∘ f)` holds. This is the best lemma I could come up with so far. It's not the lemma I hoped for, but I realized the lemma I hoped for is wrong.^^ However, now that I did this proof, I figured it'd be a w...I wondered when `pred_infinite (P ∘ f)` holds. This is the best lemma I could come up with so far. It's not the lemma I hoped for, but I realized the lemma I hoped for is wrong.^^ However, now that I did this proof, I figured it'd be a waste to throw it away.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/224Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`2021-01-29T16:09:15ZRobbert KrebbersAdd `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/223Rename `Forall_Forall2` → `Forall_Forall2_diag`2021-01-28T11:49:19ZRobbert KrebbersRename `Forall_Forall2` → `Forall_Forall2_diag`This is to be consistent with the names for big operators in Iris.This is to be consistent with the names for big operators in Iris.https://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)
```