stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-01-11T17:18:29Zhttps://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/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/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/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/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/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/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/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/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/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/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/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/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.