stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-03-22T13:24:11Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/238surjective_finite2021-03-22T13:24:11ZAlix Trieusurjective_finiteProve that `Finite B` knowing that `Finite A` and there exists a surjection `f` from `A` to `B`.Prove that `Finite B` knowing that `Finite A` and there exists a surjection `f` from `A` to `B`.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/237Fix finite map notations for Coq < 8.132021-03-19T14:10:52ZLennard Gähergaeher@mpi-sws.orgFix finite map notations for Coq < 8.13As discussed, this fixes the notations introduced by !236 by using parentheses for resolving the notations instead of `$`.
I also added a `TODO` comment to change it back when support for Coq 8.12 is dropped.
I have tested against Coq ...As discussed, this fixes the notations introduced by !236 by using parentheses for resolving the notations instead of `$`.
I also added a `TODO` comment to change it back when support for Coq 8.12 is dropped.
I have tested against Coq 8.13 and Coq 8.12.1 this time around.
Updated script for generating it:
```
#!/bin/python3
n = 13
# indent by two spaces
indent = " "
def generate(n):
# Header
out = "Notation \"{[ "
# notation itself
for i in range(1, n+1):
if i > 1:
out += " ; "
out += "k" + str(i) + " := a" + str(i)
out += " ]}\" := \n"
# translation of notation
line = indent + "("
for i in range(1, n):
if i > 1:
line += " ( "
if len(line) > 70:
out += line + "\n"
line = indent + indent
line += "<[ k" + str(i) + " := a" + str(i) + " ]>"
# singleton element
line += "{[ k" + str(n) + " := a" + str(n) + " ]}"
for i in range(1, n):
line += ")"
out += line + "\n"
out += indent + "(at level 1, format\n"
# format printing
line = indent + "\"{[ '[hv' "
for i in range(1, n+1):
if i > 1:
# extra space for printing
line += " ; ']' '/' "
# if len(line) > 70:
# out += line + "\"\n"
# line = indent + indent + "\""
line += "'[' k" + str(i) + " := a" + str(i)
line += " ']' ']' ]}\")"
out += line
out += " : stdpp_scope."
return out
for i in range(2, n+1):
print(generate(i))
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/236Finite map notations2021-03-19T11:16:53ZLennard Gähergaeher@mpi-sws.orgFinite map notationsThis adds some ad-hoc notations for maps up to size 13, e.g.
`{[ k1 := a1 ; k2 := a2 ]}`
for
`(<[k2 := a2]>{[k1 := a1]})`.
13 seems to be enough for many useful cases.
For future reference if notations for larger sets are needed, this...This adds some ad-hoc notations for maps up to size 13, e.g.
`{[ k1 := a1 ; k2 := a2 ]}`
for
`(<[k2 := a2]>{[k1 := a1]})`.
13 seems to be enough for many useful cases.
For future reference if notations for larger sets are needed, this is the script I used:
```
#!/bin/python3
n = 13
# indent by two spaces
indent = " "
def generate(n):
# Header
out = "Notation \"{[ "
# notation itself
for i in range(1, n+1):
if i > 1:
out += " ; "
out += "k" + str(i) + " := a" + str(i)
out += " ]}\" := \n"
# translation of notation
line = indent + "("
for i in range(1, n):
if i > 1:
line += " $ "
if len(line) > 70:
out += line + "\n"
line = indent + indent
line += "<[ k" + str(i) + " := a" + str(i) + " ]>"
# singleton element
line += "{[ k" + str(n) + " := a" + str(n) + " ]}"
line += ")\n"
out += line
out += indent + "(at level 1, format\n"
# format printing
line = indent + "\"{[ '[hv' "
for i in range(1, n+1):
if i > 1:
# extra space for printing
line += " ; ']' '/' "
# if len(line) > 70:
# out += line + "\"\n"
# line = indent + indent + "\""
line += "'[' k" + str(i) + " := a" + str(i)
line += " ']' ']' ]}\")"
out += line
out += " : stdpp_scope."
return out
for i in range(2, n+1):
print(generate(i))
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/235Add more underscores to f_equiv2021-03-15T16:15:32ZMichael SammlerAdd more underscores to f_equivhttps://gitlab.mpi-sws.org/iris/lambda-rust/-/merge_requests/21#note_64914 requires a version of f_equiv with 5 underscores instead of 4. This is the minimal patch to fulfil this usecase, but we could add even more underscores while we a...https://gitlab.mpi-sws.org/iris/lambda-rust/-/merge_requests/21#note_64914 requires a version of f_equiv with 5 underscores instead of 4. This is the minimal patch to fulfil this usecase, but we could add even more underscores while we are at it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/234some map lemmas2021-03-14T14:22:00ZRalf Jungjung@mpi-sws.orgsome map lemmasThis upstreams some lemmas from Perennial (so I assume the proofs are by @tchajed; I ported them to the non-ssreflect world of std++).This upstreams some lemmas from Perennial (so I assume the proofs are by @tchajed; I ported them to the non-ssreflect world of std++).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/231Many improvements to `multiset_solver`2021-03-13T07:24:13ZRobbert KrebbersMany improvements to `multiset_solver`1. Support `∈`
2. Support `⊂`
3. Support case splitting on `multiplicity x {[ y ]}`, but only do this when there's no other way.
With the improved `multiset_solver` I am able to solve pretty much all lemmas in the `gmultiset` file autom...1. Support `∈`
2. Support `⊂`
3. Support case splitting on `multiplicity x {[ y ]}`, but only do this when there's no other way.
With the improved `multiset_solver` I am able to solve pretty much all lemmas in the `gmultiset` file automatically (apart from those that involve `elements`, `size`, and other connectives that are out of scope).
The new version also handles @fpottier's test case `x ∈ X → {[x]} ⊆ X` from #86.
In addition, I added a bunch of other test cases.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/233Remove singleton notations for tuples2021-03-12T06:14:55ZRobbert KrebbersRemove singleton notations for tuplesRemove singleton notations `{[ x,y ]}` and `{[ x,y,z ]}` for `{[ (x,y) ]}` and `{[ (x,y,z) ]}`. They date back to the time we used the `singleton` class with a product for maps (there's now the `singletonM` class).Remove singleton notations `{[ x,y ]}` and `{[ x,y,z ]}` for `{[ (x,y) ]}` and `{[ (x,y,z) ]}`. They date back to the time we used the `singleton` class with a product for maps (there's now the `singletonM` class).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/57Rename multiset "union" into "disjoint union"2021-03-10T16:41:16ZRobbert KrebbersRename multiset "union" into "disjoint union"This fixes #13. Now `∪` and `∩` are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas `⊎` is the "sum" (i.e. adding the multiplicities).
Some questions/remarks:
- `⊎` and `∪` have different heig...This fixes #13. Now `∪` and `∩` are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas `⊎` is the "sum" (i.e. adding the multiplicities).
Some questions/remarks:
- `⊎` and `∪` have different heights in my font (see `⊎∪`). Is there maybe a better disjoint union symbol in unicode?
- There are probably all kinds of laws about the interaction between `∪`, `∩`, and `⊎`, like distributivity. I did not attempt to prove a comprehensive set of such laws.
- `∖` is still the operation that subtracts multiplicity. I think that's fine, since there is no sensible difference operator for multisets that matches up with the union operator.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/230coPset: some lemmas about infinity2021-03-05T21:02:23ZRalf Jungjung@mpi-sws.orgcoPset: some lemmas about infinityProofs by Joshua YanowskiProofs by Joshua Yanowskihttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/229clarify Pmap_raw comment2021-02-17T13:15:51ZRalf Jungjung@mpi-sws.orgclarify Pmap_raw commentMaking this an MR so @robbertkrebbers can check if it makes sense.Making this an MR so @robbertkrebbers can check if it makes sense.https://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/228Avoid relying on buggy simpl never behavior2021-02-12T13:33:42ZTej Chajedtchajed@gmail.comAvoid relying on buggy simpl never behaviorWhat's going on in this proof is that `simpl` is unfolding both `decode_nat` _and_ `decode`, even though `decode` is marked `simpl never`. This is a bug in Coq and std++ should not rely on it.
Alternate take on
https://gitlab.inria.fr/b...What's going on in this proof is that `simpl` is unfolding both `decode_nat` _and_ `decode`, even though `decode` is marked `simpl never`. This is a bug in Coq and std++ should not rely on it.
Alternate take on
https://gitlab.inria.fr/bertot/stdpp/-/commit/895121f919c6f1332f41f658ce7f850e391eb49e,
which is used as an overlay in Coq for
https://github.com/coq/coq/pull/13448.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/227add Nat_iter_mul2021-02-09T11:15:11ZRalf Jungjung@mpi-sws.orgadd Nat_iter_mulOriginal proof by Joshua YanovskiOriginal proof by Joshua Yanovskihttps://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/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/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`.