stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-06-18T19:17:26Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/164Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)2020-06-18T19:17:26ZsarahzrfAdded sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)I've added an instance `sig_finite` along with a couple of minor things used to define/prove it. This is a `Finite` instance for `sig`s over `Finite` types whose predicates are decidable and proof irrelevant:
```coq
(* Not a direct excer...I've added an instance `sig_finite` along with a couple of minor things used to define/prove it. This is a `Finite` instance for `sig`s over `Finite` types whose predicates are decidable and proof irrelevant:
```coq
(* Not a direct excerpt. *)
Context `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)} `{∀ x, ProofIrrel (P x)}.
Global Instance sig_finite : Finite (sig P).
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/165Adapt w.r.t. coq/coq#12512.2020-06-17T18:54:51ZGhost UserAdapt w.r.t. coq/coq#12512.This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.
https://github.com/coq/coq/pull/12512This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.
https://github.com/coq/coq/pull/12512https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/166Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #125122020-06-17T08:54:53ZRobbert KrebbersAvoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512This MR provides an alternative to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/165, but avoids the `epose` horribleness. Instead, it just spells out some proofs, which IMHO makes things easier to maintain.This MR provides an alternative to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/165, but avoids the `epose` horribleness. Instead, it just spells out some proofs, which IMHO makes things easier to maintain.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/163Remove type scope from forall notation2020-05-27T22:12:37ZTej Chajedtchajed@gmail.comRemove type scope from forall notationFixes #67.Fixes #67.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/152notation for forall2020-05-27T21:51:21ZGregory Malechanotation for forallhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/106Opaquify proofs in gmap_partial_alter (fix #46)2020-05-20T14:58:06ZPaolo G. GiarrussoOpaquify proofs in gmap_partial_alter (fix #46)- Ensure gmap well-formedness proofs are fully opaque.
- Use pattern-matching lambdas over lets.- Ensure gmap well-formedness proofs are fully opaque.
- Use pattern-matching lambdas over lets.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/161rename Z2Nat_inj_div and Z2Nat_inj_mod2020-05-12T21:43:31ZMichael Sammlerrename Z2Nat_inj_div and Z2Nat_inj_modThis MR renames `Z2Nat_inj_div`, `Z2Nat_inj_mod`, `Nat2Z_inj_div` and `Nat2Z_inj_mod` to follow the naming conventions of `Z2Nat` and `Nat2Z`. See https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/136#note_49866
Should I mention ir...This MR renames `Z2Nat_inj_div`, `Z2Nat_inj_mod`, `Nat2Z_inj_div` and `Nat2Z_inj_mod` to follow the naming conventions of `Z2Nat` and `Nat2Z`. See https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/136#note_49866
Should I mention iris-users here already or only if the MR is merged?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/155Add Countable instances for byte2020-05-12T17:53:49ZTej Chajedtchajed@gmail.comAdd Countable instances for bytehttps://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/160Revert "Merge branch 'byte-countable' into 'master'"2020-05-12T17:33:24ZRobbert KrebbersRevert "Merge branch 'byte-countable' into 'master'"This reverts merge request !155 because it's incompatible with Coq ≤8.9.This reverts merge request !155 because it's incompatible with Coq ≤8.9.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/159alternative overlay for coq/coq#121622020-05-08T09:42:13ZOlivier Laurentalternative overlay for coq/coq#12162This is an alternative to !153 which follows the spirit of !156.
It is adapted to the last version of [coq/coq#12162](https://github.com/coq/coq/pull/12162) which takes into account the introduction of `Bool.lt`.This is an alternative to !153 which follows the spirit of !156.
It is adapted to the last version of [coq/coq#12162](https://github.com/coq/coq/pull/12162) which takes into account the introduction of `Bool.lt`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/158add map_Forall_lookup2020-05-07T14:13:20ZRalf Jungjung@mpi-sws.orgadd map_Forall_lookupI was just searching for this lemma for at least 5 minutes until I realized that this is the definition of `map_Forall` -- usually our definitions are such that just `Print`ing stuff doesn't actually get me anywhere useful.
I think it w...I was just searching for this lemma for at least 5 minutes until I realized that this is the definition of `map_Forall` -- usually our definitions are such that just `Print`ing stuff doesn't actually get me anywhere useful.
I think it would be good for a lemma like this to show up in `Search` results.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/153overlay for coq/coq#121622020-05-07T11:20:25ZOlivier Laurentoverlay for coq/coq#12162The PR [coq/coq#12162](https://github.com/coq/coq/pull/12162) renames `Bool.leb` into `Bool.le` which is more coherent with the rest of the standard library since it has type `bool -> bool -> Prop`.
This generates possible clashes with `...The PR [coq/coq#12162](https://github.com/coq/coq/pull/12162) renames `Bool.leb` into `Bool.le` which is more coherent with the rest of the standard library since it has type `bool -> bool -> Prop`.
This generates possible clashes with `Nat.le` or `Peano.le` so that additional qualification is required.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/156Alternative take on #153: fix `le` in future versions of Coq2020-05-07T11:20:16ZRobbert KrebbersAlternative take on #153: fix `le` in future versions of CoqThis should provide compatibility for https://github.com/coq/coq/pull/12162
Other changes:
- Use `Arith` instead of `NPeano`, since the latter is deprecated. While it may also be possible to import `NPeano`, numbers export `PArith NAri...This should provide compatibility for https://github.com/coq/coq/pull/12162
Other changes:
- Use `Arith` instead of `NPeano`, since the latter is deprecated. While it may also be possible to import `NPeano`, numbers export `PArith NArith ZArith`, so it seemed logical to also export `Arith`.
- Add test to check for correct version of `le`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/157tactics.v: Fix parsing precedence for `select` tactic2020-05-06T20:04:57ZPaolo G. Giarrussotactics.v: Fix parsing precedence for `select` tactichttps://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/154Add Countable instance for Ascii.ascii2020-05-01T15:01:36ZTej Chajedtchajed@gmail.comAdd Countable instance for Ascii.asciihttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/151fix imap_seq and imap_seq0 to make them useful2020-04-23T12:57:45ZMichael Sammlerfix imap_seq and imap_seq0 to make them usefulI think I made a mistake when I originally upstreamed these lemmas. Now they are more generic and thus actually useful.I think I made a mistake when I originally upstreamed these lemmas. Now they are more generic and thus actually useful.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.