stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-05-04T10:05:59Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/256`_True`/`_False` lemmas for `decide` and `mguard`2021-05-04T10:05:59ZRobbert Krebbers`_True`/`_False` lemmas for `decide` and `mguard`For `decide` we currently have the following lemmas:
```coq
Lemma decide_True {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x.
Lemma decide_False {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y.
Lemm...For `decide` we currently have the following lemmas:
```coq
Lemma decide_True {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x.
Lemma decide_False {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y.
Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
```
The first two are most commonly used, whereas the last two are also applicable if you do a `match` on `decide` and use the proof of `P` or `¬P`.
For `guard` we have similar lemmas that correspond to the first two lemmas for `decide`.
```coq
Lemma option_guard_True {A} P `{Decision P} (mx : option A) : P → (guard P; mx) = mx.
Lemma option_guard_False {A} P `{Decision P} (mx : option A) : ¬P → (guard P; mx) = None.
```
However, these don't work for `guard P as HP; ... something containing HP ...`, so I wanted to have lemmas like the last two for `decide`. The one for `False` can be generalized trivially, but (like `decide`) the one for `True` only works if the proposition is proof irrelevant:
```coq
Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A) (HP : P) : mguard P f = f HP.
Lemma option_guard_False {A} P `{Decision P} (f : P → option A) : ¬P → mguard P f = None.
```
(Note that `guard P as HP; y` is notation for `mguard P (λ HP, y)`).
The main problem, as usual, is naming... The `_left` and `_right` suffixes for `decide` make no sense for `guard`. So instead, I propose the `_pi` suffix for proof irrelevant. Opinions about that?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/255add Countable instance for decidable Sigma types2021-05-06T07:05:11ZSimon Gregersenadd Countable instance for decidable Sigma typesThis instance became useful when working with, e.g., a type for elements of a set `{ a : A | a ∈ X }` and wanting to construct a `gmap` with this domain.This instance became useful when working with, e.g., a type for elements of a set `{ a : A | a ∈ X }` and wanting to construct a `gmap` with this domain.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/254Add little endian encoding of Z2021-05-17T20:30:33ZMichael SammlerAdd little endian encoding of Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/253Fix pretty printing of multset literals + add tests2021-04-21T07:03:32ZRobbert KrebbersFix pretty printing of multset literals + add testshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/252Fix inconsistent arguments of `subset_difference_elem_of`.2021-04-20T09:36:50ZRobbert KrebbersFix inconsistent arguments of `subset_difference_elem_of`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/251Introduce `SingletonMS` class for multiset singletons.2021-04-20T16:44:32ZRobbert KrebbersIntroduce `SingletonMS` class for multiset singletons.- Define set-like notation `{[+ x1; ..; xn ]}` for multisets in terms of the new
singleton class and disjoint union `⊎`.
- Remove `SemiSet` instance for multisets.
- Prove lemmas regarding `∈` and `∉` for multisets since we no longer g...- Define set-like notation `{[+ x1; ..; xn ]}` for multisets in terms of the new
singleton class and disjoint union `⊎`.
- Remove `SemiSet` instance for multisets.
- Prove lemmas regarding `∈` and `∉` for multisets since we no longer get the
generic versions for sets.
- Provide `SetUnfoldElemOf` instances for multisets since we no longer get the
generic versions for sets.
- Prove lemmas new regarding `∈` and `∉` for `∩`
Fixes #100, #98 and #87.
This MR is an alternative to !232.https://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))
```