stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-05-01T17:22:55Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/150WIP: rework of naive_solver after discussion with Robbert2020-05-01T17:22:55ZMichael SammlerWIP: rework of naive_solver after discussion with RobbertThis is a slightly reworked version of `naive_solver`, which hopefully fails faster. @robbertkrebbers What do you think? What would be other kinds of goals I should try this version on?This is a slightly reworked version of `naive_solver`, which hopefully fails faster. @robbertkrebbers What do you think? What would be other kinds of goals I should try this version on?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/149Add a way to disable typeclass search in `Program` obligations2020-11-03T12:13:26ZPaolo G. GiarrussoAdd a way to disable typeclass search in `Program` obligationsFrom the coqdoc of the new feature:
```coq
(** When using [Program], you can use [notc_hole] in place of [_] to create
an obligation that does not trigger typeclass search. That is useful if the
search fails slowly, for instance for [Pro...From the coqdoc of the new feature:
```coq
(** When using [Program], you can use [notc_hole] in place of [_] to create
an obligation that does not trigger typeclass search. That is useful if the
search fails slowly, for instance for [Proper] obligations.
Should https://github.com/coq/coq/issues/12147 be fixed, this can be
deprecated or replaced by the new syntax. *)
```
#### Rationale for inclusion
I think https://github.com/coq/coq/issues/12147 is potentially bad enough that it could belong in stdpp. I haven't found very compelling usecases in iris: in part, you already avoid writing `Program Definition foo ...: A -n> B`, at the cost of more boilerplate.
See also: discussion from https://mattermost.mpi-sws.org/iris/pl/r885z6apefr9bjpuctczruogrr onwards.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/148Create HintDBs with the discriminated option2020-04-23T09:16:19ZMichael SammlerCreate HintDBs with the discriminated optionAccording to the documentation
https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:cmd.create-hintdb,
when creating a hint database without discrimination, Coq uses the
legacy implementation, which only uses Discrim...According to the documentation
https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:cmd.create-hintdb,
when creating a hint database without discrimination, Coq uses the
legacy implementation, which only uses Discrimination Trees for goals
without evars and does not use opaqueness information. This commit
switches the hint databases of stdpp to the new implementation.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/147Add filter_app lemma2020-04-17T19:46:33ZTej Chajedtchajed@gmail.comAdd filter_app lemmahttps://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/139Added strings to prelude to fix printing of strings.length2020-04-08T07:28:27ZMichael SammlerAdded strings to prelude to fix printing of strings.lengthThis should hopefully fix `strings.length` showing up in random places. I tested it with iris and RefinedC. Both compile without changes and `length` is no more printed as `strings.length` in RefinedC. See the comment for the reasoning w...This should hopefully fix `strings.length` showing up in random places. I tested it with iris and RefinedC. Both compile without changes and `length` is no more printed as `strings.length` in RefinedC. See the comment for the reasoning why I think this works.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@gmail.comFix 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.