stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-04-16T14:00:35Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/146Add `ProofIrrel ()`2020-04-16T14:00:35ZPaolo G. GiarrussoAdd `ProofIrrel ()`This instance might seem odd, but `ProofIrrel` takes a `Type` and not a `Prop`,
and stdpp already has instances for products.This instance might seem odd, but `ProofIrrel` takes a `Type` and not a `Prop`,
and stdpp already has instances for products.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/145Add `encode_Z` function to encode element of countable type as `Z`.2020-04-11T10:35:24ZRobbert KrebbersAdd `encode_Z` function to encode element of countable type as `Z`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/144Another try at removing strings.length2020-04-11T09:32:46ZMichael SammlerAnother try at removing strings.lengthSee discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/129
The idea of this version is to have two notations, one which shadows the bad definition `Strings.length` and the other which shadows the bad Notation `List.len...See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/129
The idea of this version is to have two notations, one which shadows the bad definition `Strings.length` and the other which shadows the bad Notation `List.length`, which is bad because it is parsing only.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/143Add tests for equiv notation2020-04-10T05:58:08ZPaolo G. GiarrussoAdd tests for equiv notationExtracted from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/409.Extracted from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/409.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/142Added select and select_revert tactics2021-01-20T11:02:05ZMichael SammlerAdded select and select_revert tacticsAs discussed with @robbertkrebbers
open points:
- [x] Names of the tactics (What are the names in Mtac? @janno )
- [x] Changelog entry?As discussed with @robbertkrebbers
open points:
- [x] Names of the tactics (What are the names in Mtac? @janno )
- [x] Changelog entry?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/141Extracted list_numbers.v with seq, seqZ, sum_list and max_list2020-04-15T10:44:28ZMichael SammlerExtracted list_numbers.v with seq, seqZ, sum_list and max_listThis is in preparation for adding the `rotate` functions.This is in preparation for adding the `rotate` functions.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/140Add notation `wn` of weakly normalizing terms; and prove some common theorems...2020-04-07T21:20:36ZRobbert KrebbersAdd notation `wn` of weakly normalizing terms; and prove some common theorems about it.Most important common theorem: strongly normalizing → weakly normalizing.Most important common theorem: strongly normalizing → weakly normalizing.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/138Revise uses of inj as discussed2020-04-05T18:50:44ZPaolo G. GiarrussoRevise uses of inj as discussedFollowup to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/412.
Quoting last commit:
> However, I'm unsure this is an improvement: in lots of cases here, the function
didn't need to be guessed, but could be deduced by "simple" hi...Followup to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/412.
Quoting last commit:
> However, I'm unsure this is an improvement: in lots of cases here, the function
didn't need to be guessed, but could be deduced by "simple" higher-order
unification, the one where unifying `?f ?a` against `g args last_arg` sets `?f =
g args`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/137Rename `fin_maps.singleton_proper` into `singletonM_proper`.2020-04-04T06:45:40ZRobbert KrebbersRename `fin_maps.singleton_proper` into `singletonM_proper`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/136Rotate everything2020-05-12T17:46:34ZMichael SammlerRotate everythingThis MR adds rotate_nat_add, rotate_nat_sub, rotate and rotate_take functions, which allow dealing with wraparound of lists. I don't know where these functions should go so I created a new file for them. But I can also move them somewher...This MR adds rotate_nat_add, rotate_nat_sub, rotate and rotate_take functions, which allow dealing with wraparound of lists. I don't know where these functions should go so I created a new file for them. But I can also move them somewhere else.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/135Fix typo in CHANGELOG2020-04-01T06:39:08ZTej Chajedtchajed@mit.eduFix typo in CHANGELOGRename performed in !131 was on `drop_insert`, not `drop_length`Rename performed in !131 was on `drop_insert`, not `drop_length`https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/134Lemmas for `list_find` in combination with `app` and `insert`.2020-05-12T17:00:22ZRobbert KrebbersLemmas for `list_find` in combination with `app` and `insert`.This MR proposes an alternative to the lemmas for `list_find` by @msammler in #131 (but that he removed later).
All lemmas are stated using a bi-implication, and they are strong enough to prove @msammler's original lemmas:
```coq
Lemma...This MR proposes an alternative to the lemmas for `list_find` by @msammler in #131 (but that he removed later).
All lemmas are stated using a bi-implication, and they are strong enough to prove @msammler's original lemmas:
```coq
Lemma list_find_insert_Some_ne1 l i i' x x':
list_find P l = Some (i', x') → ¬ P x → i ≠ i' →
list_find P (<[i:=x]> l) = Some (i', x').
Proof.
rewrite list_find_insert_Some, !list_find_Some.
destruct (decide (i < i')); naive_solver eauto with lia.
Qed.
Lemma list_find_insert_Some_ne_change2 l i i' x x':
list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x' → i < i' →
list_find P l = Some (i, x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver eauto with lia. Qed.
Lemma list_find_insert_Some_ne_same2 l i i' x x' x'':
list_find P (<[i:=x]>l) = Some (i', x') →
¬ P x → l !! i = Some x'' → (i < i' → ¬ P x'') →
list_find P l = Some (i', x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver. Qed.
Lemma list_find_insert_Some_ne2 l i i' x x' x'':
list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x'' → (x'' = x' ∨ ¬ P x'') →
∃ i'', list_find P l = Some (i'', x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver eauto with lia. Qed.
```
I very much dislike the statement of `list_find_insert_Some`, but I cannot come up with anything better that is true.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/133Remove trailing whitespace2020-03-31T08:07:03ZMichael SammlerRemove trailing whitespaceThis was done using `sed --in-place 's/[[:space:]]\+$//' theories/*.v`.This was done using `sed --in-place 's/[[:space:]]\+$//' theories/*.v`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/132Replace explicit use of Inj instances by inj2020-03-31T13:36:25ZPaolo G. GiarrussoReplace explicit use of Inj instances by injThis was inconsistent and not explained before. And I noticed when talking with Herbelin about view inference.This was inconsistent and not explained before. And I noticed when talking with Herbelin about view inference.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/131random collection of lemmas2020-04-08T07:26:43ZMichael Sammlerrandom collection of lemmasThese are some lemmas which I need in my development. @robbertkrebbers and I talked about some of them today. I will make another MR with the `rotate` function. Let me know what you think and which lemmas seem useful. Also better proofs ...These are some lemmas which I need in my development. @robbertkrebbers and I talked about some of them today. I will make another MR with the `rotate` function. Let me know what you think and which lemmas seem useful. Also better proofs are always appreciated.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/129Fix `Export` order for `length`. Remove `length` hack in strings.2020-04-11T10:35:00ZRobbert KrebbersFix `Export` order for `length`. Remove `length` hack in strings.The notation in `strings` was a hack to shadow the `length` function on strings with those on lists.
@msammler and I figured out how to change the imports to fix this problem without the hack. Basically, `stdpp.base` exports `Coq.Stri...The notation in `strings` was a hack to shadow the `length` function on strings with those on lists.
@msammler and I figured out how to change the imports to fix this problem without the hack. Basically, `stdpp.base` exports `Coq.Strings` and `Coq.List` in the right order, so the shadowing is done right. As a consequence `Coq.Strings` should never be exported by hand.
This approach seems to work among all supported Coq versions.
We also added a test.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/128add sed script for 1.3.02020-04-02T09:31:03ZRalf Jungjung@mpi-sws.orgadd sed script for 1.3.0Original sed script by @tchajed. I added `s/\bdom_map_filter\b/dom_map_filter_subseteq/g` and `s/\bseqZ_fmap\b/fmap_add_seqZ/g`.Original sed script by @tchajed. I added `s/\bdom_map_filter\b/dom_map_filter_subseteq/g` and `s/\bseqZ_fmap\b/fmap_add_seqZ/g`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/127Update CHANGELOG for 1.3 release.2020-03-18T09:20:57ZRobbert KrebbersUpdate CHANGELOG for 1.3 release.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/126Make lemmas for `seq` and `seqZ` consistent.2020-03-18T15:51:22ZRobbert KrebbersMake lemmas for `seq` and `seqZ` consistent.This closes issue #57This closes issue #57https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/125Lookup total lemmas2020-03-17T20:45:23ZRobbert KrebbersLookup total lemmasThis closes issue #50 and is a more complete alternative to !109.
This MR includes all lemmas that I think make sense. See also the discussion there.This closes issue #50 and is a more complete alternative to !109.
This MR includes all lemmas that I think make sense. See also the discussion there.