stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-04-15T09:13:25Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/243Add lemma `lookup_app`, and derive other `lookup_app` lemmas from it.2021-04-15T09:13:25ZRobbert KrebbersAdd lemma `lookup_app`, and derive other `lookup_app` lemmas from it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/242Add lemma `lookup_map_seq`, derive other `lookup_map_seq` lemmas from that.2021-04-14T10:16:43ZRobbert KrebbersAdd lemma `lookup_map_seq`, derive other `lookup_map_seq` lemmas from that.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/241Hint Mode Equiv: update link to blocking Coq issue2021-04-11T18:06:52ZPaolo G. GiarrussoHint Mode Equiv: update link to blocking Coq issueBased on
https://github.com/coq/coq/issues/9058#issuecomment-496479506.
The goal is to track when this can be fixed.Based on
https://github.com/coq/coq/issues/9058#issuecomment-496479506.
The goal is to track when this can be fixed.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/240Future proof rotate_nat_add_add_mod2021-04-08T09:22:35ZAndrej DudenhefnerFuture proof rotate_nat_add_add_modThis prepares `rotate_nat_add_add_mod` for https://github.com/coq/coq/pull/14086 in a backwards compatible manner. Crucially, the design decision `n mod 0 = 0` could change to `n mod 0 = n` in future. This merge request makes `rotate_nat...This prepares `rotate_nat_add_add_mod` for https://github.com/coq/coq/pull/14086 in a backwards compatible manner. Crucially, the design decision `n mod 0 = 0` could change to `n mod 0 = n` in future. This merge request makes `rotate_nat_add_add_mod` agnostic of the particular design decision.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/239More lemmas for list's prefix_of and suffix_of2021-04-15T09:58:04ZHai DangMore lemmas for list's prefix_of and suffix_ofMore properties of `prefix_of` and `suffix_of`:
- they are partial orders, not just pre orders
- `prefix_nil_inv` and `prefix_of_down_total`.More properties of `prefix_of` and `suffix_of`:
- they are partial orders, not just pre orders
- `prefix_nil_inv` and `prefix_of_down_total`.https://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/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/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/232Multiset set notation2021-04-20T14:59:03ZRobbert KrebbersMultiset set notationThis MR adds a notation `{[ x1 ;+ .. ;+ xn ]}` for `{{ x1 ]} ⊎ .. ⊎ {{ xn ]}`.
Todo:
- [x] bikeshed about notation
- [x] port tests in !231 to new notation
Fixes #100This MR adds a notation `{[ x1 ;+ .. ;+ xn ]}` for `{{ x1 ]} ⊎ .. ⊎ {{ xn ]}`.
Todo:
- [x] bikeshed about notation
- [x] port tests in !231 to new notation
Fixes #100https://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/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/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/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`