stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-12-08T16:36:56Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/250WIP: bitvector library2021-12-08T16:36:56ZMichael SammlerWIP: bitvector libraryhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/249Add list_to_map_app2021-04-20T08:41:11ZMichael SammlerAdd list_to_map_appSee discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244#note_65864See discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244#note_65864https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/248Add lemmas about testbit on bounded integers2021-04-19T10:13:23ZMichael SammlerAdd lemmas about testbit on bounded integersThese proofs are originally by @paulzhu, which is why I put him as the author of this commit. This is a part of !244.These proofs are originally by @paulzhu, which is why I put him as the author of this commit. This is a part of !244.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/247Add tactic `learn_hyp`, fixes #732021-04-19T12:30:59ZMichael SammlerAdd tactic `learn_hyp`, fixes #73This is another part of !244 and fixes #73.This is another part of !244 and fixes #73.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/246Add more typeclasses2021-04-15T08:03:48ZMichael SammlerAdd more typeclassesThis adds the typeclasses from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244. See also the discussion here: https://mattermost.mpi-sws.org/iris/pl/37b8m6pmdfr3pfwwjssre3oqjcThis adds the typeclasses from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244. See also the discussion here: https://mattermost.mpi-sws.org/iris/pl/37b8m6pmdfr3pfwwjssre3oqjchttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/245Add more lemmas for FinMaps (for union, filter, difference)2021-07-28T14:24:18ZHai DangAdd more lemmas for FinMaps (for union, filter, difference)Some lemmas that I believe worth upstreaming.Some lemmas that I believe worth upstreaming.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244Random collection of lemmas from RefinedC2021-04-15T13:18:41ZMichael SammlerRandom collection of lemmas from RefinedCThese are some things from RefinedC that I would like to upstream to stdpp. There are still some open questions, see the comments for them. Please let me know which of these changes make sense in stdpp.These are some things from RefinedC that I would like to upstream to stdpp. There are still some open questions, see the comments for them. Please let me know which of these changes make sense in stdpp.https://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.