stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2022-01-14T15:31:17Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/363Add lemmas `app_cons_eq_inv_{l,r}`.2022-01-14T15:31:17ZRobbert KrebbersAdd lemmas `app_cons_eq_inv_{l,r}`.This MR contains two commits: One with the actual lemmas, and one to perform some rearrangements. To prove the `_r` variant, I needed properties of `reverse`. I thus moved the `reverse` lemmas above the `elem_of` lemmas.
The lemmas in t...This MR contains two commits: One with the actual lemmas, and one to perform some rearrangements. To prove the `_r` variant, I needed properties of `reverse`. I thus moved the `reverse` lemmas above the `elem_of` lemmas.
The lemmas in this MR generalize the ones in !356. They also allow proving a variant for `suffix_of`, which is missing in that MR.
/cc @jihgfeehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/362Set the priority of the rewrite relation for sqsubseteq to not take precedence over...2022-01-14T10:59:45ZMatthieu SozeauSet the priority of the rewrite relation for sqsubseteq to not take precedence over...Set the priority of the rewrite relation for sqsubseteq to not take precedence over the eq instance from Coq or equiv.Set the priority of the rewrite relation for sqsubseteq to not take precedence over the eq instance from Coq or equiv.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/361Add `last_cons_Some_ne` lemma for the `last` function2022-01-14T11:58:54ZJonas KastbergAdd `last_cons_Some_ne` lemma for the `last` functionA useful lemma for the [last] function, to reduce `last (x::l) = Some y` to `last l = Some y` whenever `x ≠ y`.
This is useful since using `last_cons` leaves us with
```{coq}
match last l with
| Some y0 => Some y0
| None => Some x
end = ...A useful lemma for the [last] function, to reduce `last (x::l) = Some y` to `last l = Some y` whenever `x ≠ y`.
This is useful since using `last_cons` leaves us with
```{coq}
match last l with
| Some y0 => Some y0
| None => Some x
end = Some y
```
which only reduces through a subgoal.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/360Set the priority of the rewrite relation for equiv to not take precedence over...2022-01-13T16:37:57ZMatthieu SozeauSet the priority of the rewrite relation for equiv to not take precedence over...Set the priority of the rewrite relation for equiv to not take precedence over the eq instance from Coq.
This is more backwards compatible performance-wise with the old resolution where `eq` was favored (otherwise we get a 70% slowdown i...Set the priority of the rewrite relation for equiv to not take precedence over the eq instance from Coq.
This is more backwards compatible performance-wise with the old resolution where `eq` was favored (otherwise we get a 70% slowdown in perennial).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/359Added some useful lemmas about [list_subseteq]2022-01-14T11:03:41ZJonas KastbergAdded some useful lemmas about [list_subseteq]Added some generally useful lemmas about the [list_subseteq] functionAdded some generally useful lemmas about the [list_subseteq] functionhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/358Add lemmas about empty `filter` on list, map, and set2022-08-08T13:37:43ZJonas KastbergAdd lemmas about empty `filter` on list, map, and setAdded an advanced lemma about [filter] on lists.
Whenever a filter with a proposition [P] on a list [l] results in an empty list,
we can derive that `x ∉ l` for any [x] where `P x`.Added an advanced lemma about [filter] on lists.
Whenever a filter with a proposition [P] on a list [l] results in an empty list,
we can derive that `x ∉ l` for any [x] where `P x`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/356Renamed `app_cons_eq_inv_{l,r}`, and added derived versions for `prefix/suffix`2022-01-19T16:49:29ZJonas KastbergRenamed `app_cons_eq_inv_{l,r}`, and added derived versions for `prefix/suffix`Renamed the lemmas `app_cons_eq_inv_{l,r}`, to `elem_of_app_cons_inv_{l,r}`, to be more descriptive and consistent with existing lemmas.
Additionally, derived versions for `prefix/suffix`, as they recall some non-immediate properties of...Renamed the lemmas `app_cons_eq_inv_{l,r}`, to `elem_of_app_cons_inv_{l,r}`, to be more descriptive and consistent with existing lemmas.
Additionally, derived versions for `prefix/suffix`, as they recall some non-immediate properties of the relations on similar list structures.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/355Added some useful lemmas for the [last] function2022-01-12T15:13:03ZJonas KastbergAdded some useful lemmas for the [last] functionAdded some utility lemmas for the [last] function.
(precursor to the !353 MR)Added some utility lemmas for the [last] function.
(precursor to the !353 MR)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/354Add lemmas `elem_of_prefix` and `elem_of_suffix`2022-01-12T15:13:39ZJonas KastbergAdd lemmas `elem_of_prefix` and `elem_of_suffix`Added a lemma that captures that any element [x] that is in a prefix [l1] is also in the full list [l2].
The property is only trivial from the definition of `l1 prefix_of l2` (i.e. `∃ l, l2 = l1 ++ l2`).
Adding the lemma thus avoids brea...Added a lemma that captures that any element [x] that is in a prefix [l1] is also in the full list [l2].
The property is only trivial from the definition of `l1 prefix_of l2` (i.e. `∃ l, l2 = l1 ++ l2`).
Adding the lemma thus avoids breaking abstraction.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/353Add `filter_reverse`, `head_filter_Some`, `last_filter_Some` lemmas2022-01-19T09:39:46ZJonas KastbergAdd `filter_reverse`, `head_filter_Some`, `last_filter_Some` lemmasAdded the lemma:
```coq
Lemma last_filter_postfix P `{!∀ x : A, Decision (P x)} l x
last (filter P l) = Some x →
∃ l1 l2, l = l1 ++ [x] ++ l2 ∧ Forall (λ z, ¬ (P z)) l2.
```
(and its counterpart for `head`)
The lemmas seem useful an...Added the lemma:
```coq
Lemma last_filter_postfix P `{!∀ x : A, Decision (P x)} l x
last (filter P l) = Some x →
∃ l1 l2, l = l1 ++ [x] ++ l2 ∧ Forall (λ z, ¬ (P z)) l2.
```
(and its counterpart for `head`)
The lemmas seem useful and general enough to fit in stdpp.
The `last` lemma derives the property `Forall (λ z, ¬ (P z)) l2` of the postfix of a split `l1 ++ [x] ++ l2` for a list `l` whenever `last (filter P l) = Some x`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/352Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.2021-12-16T17:29:42ZRobbert KrebbersAdd tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.These tactics are consistent with existing tactics like `revert select` and `rename select`.These tactics are consistent with existing tactics like `revert select` and `rename select`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/351add some lemmas about `Finite` and `pred_finite`2021-12-22T21:06:21ZGlen Méveladd some lemmas about `Finite` and `pred_finite`Merge it if you like it. Feel free to suggest better naming and placement.Merge it if you like it. Feel free to suggest better naming and placement.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/350remove a Global Arguments Pos.of_nat from the middle of a proof2021-12-13T19:13:40ZRalf Jungjung@mpi-sws.orgremove a Global Arguments Pos.of_nat from the middle of a proofThis doesn't seem to actually be required, at least not in this file...This doesn't seem to actually be required, at least not in this file...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/349Fix list_fmap_inj_12021-12-08T19:49:25ZMichael SammlerFix list_fmap_inj_1`list_fmap_inj_1` introduced by https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/344 accidentally has a superfluous `(?A → ?B)` due to `Set Default Proof Using "Type*".` :
```
Check list_fmap_inj_1.
=> list_fmap_inj_1
: (?A →...`list_fmap_inj_1` introduced by https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/344 accidentally has a superfluous `(?A → ?B)` due to `Set Default Proof Using "Type*".` :
```
Check list_fmap_inj_1.
=> list_fmap_inj_1
: (?A → ?B)
→ ∀ (f1 f2 : ?A → ?B) (l : list ?A) (x : ?A),
f1 <$> l = f2 <$> l → x ∈ l → f1 x = f2 x
```
This MR fixes this such that `list_fmap_inj_1` has the intended type:
```
Check list_fmap_inj_1.
=> list_fmap_inj_1
: ∀ (f f' : ?A → ?B) (l : list ?A) (x : ?A),
f <$> l = f' <$> l → x ∈ l → f x = f' x
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/348Homomorphism properties for `bool_decide` + rename (bool_)decide_iff.2021-12-09T12:03:11ZRobbert KrebbersHomomorphism properties for `bool_decide` + rename (bool_)decide_iff.- Add homomorphism properties for bool_decide and True, False, →, ↔
- Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext` because `_iff` is now used for the above property for `↔`. This is also more consistent wi...- Add homomorphism properties for bool_decide and True, False, →, ↔
- Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext` because `_iff` is now used for the above property for `↔`. This is also more consistent with other extensionality properties.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/347add bool_decide_negb2021-12-09T20:51:27ZRalf Jungjung@mpi-sws.orgadd bool_decide_negbI had to move up all the `Decision` stuff since the new lemma needs the `not_dec` instance.
Proof by Yun-Sheng.I had to move up all the `Decision` stuff since the new lemma needs the `not_dec` instance.
Proof by Yun-Sheng.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/346Avoid using Arith libraries deprecated in v8.162021-12-07T09:38:50ZTej Chajedtchajed@gmail.comAvoid using Arith libraries deprecated in v8.16Coq v8.16 will deprecate several libraries in `Arith` (see https://github.com/coq/coq/pull/14736). This results in warnings like:
```
File "./theories/numbers.v", line 1374, characters 13-23:
Warning: Notation plus_assoc is deprecated ...Coq v8.16 will deprecate several libraries in `Arith` (see https://github.com/coq/coq/pull/14736). This results in warnings like:
```
File "./theories/numbers.v", line 1374, characters 13-23:
Warning: Notation plus_assoc is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_assoc instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/list.v", line 1207, characters 29-47:
Warning: Notation Min.min_idempotent is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_id instead.
[deprecated-syntactic-definition,deprecated]
```
These changes seem to be backwards-compatible to Coq 8.11 so we might as well fix them now. In several cases the recommended fix is incorrect because it isn't the same lemma (for example, `minus_plus` has no replacement lemma, at least with the current imports); in those cases I changed the proof script to use `replace` and `lia` rather than introduce a lemma identical to the old one to continue using `rewrite`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/345Add is_closed_term tactic2021-12-08T06:53:44ZMichael SammlerAdd is_closed_term tacticThis MR adds a tactic that has been proven quite useful in RefinedC. An example usecase can be found here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/4168f736be2fd735dc9680fda0a3b3a6af2b1b5e/theories/bitvector.v#L294 (There it is still...This MR adds a tactic that has been proven quite useful in RefinedC. An example usecase can be found here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/4168f736be2fd735dc9680fda0a3b3a6af2b1b5e/theories/bitvector.v#L294 (There it is still called checked_closed).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/344Add list_fmap_inj1, Z_to_little_endian_lookup_Some and little_endian_to_Z_spec2021-12-08T07:39:26ZMichael SammlerAdd list_fmap_inj1, Z_to_little_endian_lookup_Some and little_endian_to_Z_specSome more lemmas...Some more lemmas...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/343some more lemmas about list folding2021-12-01T17:04:08ZRalf Jungjung@mpi-sws.orgsome more lemmas about list folding