stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-02-01T11:56:08Zhttps://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/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/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/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/192Draft: Drop misleading gmultiset_simple_set instance2020-10-12T09:51:39ZPaolo G. GiarrussoDraft: Drop misleading gmultiset_simple_set instanceThe problem is that `elem_of_subseteq_singleton` applies to multiset goals, but uses the wrong instance.
> [...] when my goal is a multiset elem-of, then `apply gmultiset_elem_of_singleton_subseteq.` and `apply elem_of_subseteq_singleton...The problem is that `elem_of_subseteq_singleton` applies to multiset goals, but uses the wrong instance.
> [...] when my goal is a multiset elem-of, then `apply gmultiset_elem_of_singleton_subseteq.` and `apply elem_of_subseteq_singleton.` result in different goals that print exactly the same (also btw note the inconsistent lemma name)
Based on a suggestion by Robbert (which I might have misunderstood); but I'm not sure this is the right fix.
This instance appears to not be used, and it allows applying lemmas like `elem_of_subseteq_singleton` which are inappropriate for gmultiset, as they use the `set_subseteq` instance for `SubsetEq`, instead of `gmultiset_subseteq : SubsetEq (gmultiset A)`.
However, the lemmas should be restated in terms of `gmultiset`, since they do hold, and they hold on sensible instances.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.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/190Drop support for Coq 8.8 and 8.92020-10-13T15:27:45ZRalf Jungjung@mpi-sws.orgDrop support for Coq 8.8 and 8.9This lets us clean up some little things (see this MR), and it enables some major improvements to `gmap` and `Qp` by relying on definitionally proof-irrelevant propositions.
I asked last evening on Mattermost if anyone still uses std++ ...This lets us clean up some little things (see this MR), and it enables some major improvements to `gmap` and `Qp` by relying on definitionally proof-irrelevant propositions.
I asked last evening on Mattermost if anyone still uses std++ with such old versions of Coq. So far, nobody responded, but it has been less than 24h. On the other hand, such users can just stick to std++ 1.4.0.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/189Draft: use SProp for well-formedness condition in Pmap and gmap2021-07-27T21:03:00ZTej Chajedtchajed@gmail.comDraft: use SProp for well-formedness condition in Pmap and gmapProof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only `simpl` (ordinarily you can get this to work with `vm_compute`, which breaks th...Proof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only `simpl` (ordinarily you can get this to work with `vm_compute`, which breaks the opacity of proofs).