stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-06-29T11:53:21Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/167Add solver `multiset_solver` for multisets2020-06-29T11:53:21ZRobbert KrebbersAdd solver `multiset_solver` for multisetsThe code contains some documentation how it works.
I added a number of tests, and used it to automate many existing lemmas in the `gmultiset` file.
Note that this required restructuring the file quite a bit, since I needed some bas...The code contains some documentation how it works.
I added a number of tests, and used it to automate many existing lemmas in the `gmultiset` file.
Note that this required restructuring the file quite a bit, since I needed some basic lemmas (now in section `basic_lemmas`) to define the tactic, and wanted to use the tactic subsequently to prove many of the existing lemmas (now in section `multiset_unfold`). None of the lemma statements changed, only many proofs are replaced by a mere call to `multiset_solver`.
/cc @msammlerhttps://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/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/163Remove type scope from forall notation2020-05-27T22:12:37ZTej Chajedtchajed@mit.eduRemove type scope from forall notationFixes #67.Fixes #67.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/162Prove theorem about delete of gset_to_gmap2020-06-23T21:33:04ZTej Chajedtchajed@mit.eduProve theorem about delete of gset_to_gmapBasically the opposite of `gset_to_gmap_union_singleton`.
I was going to call this `gset_to_gmap_delete` but I decided to follow the convention from the other lemma (which isn't called `gset_to_gmap_insert`).Basically the opposite of `gset_to_gmap_union_singleton`.
I was going to call this `gset_to_gmap_delete` but I decided to follow the convention from the other lemma (which isn't called `gset_to_gmap_insert`).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/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/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/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/155Add Countable instances for byte2020-05-12T17:53:49ZTej Chajedtchajed@mit.eduAdd Countable instances for bytehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/154Add Countable instance for Ascii.ascii2020-05-01T15:01:36ZTej Chajedtchajed@mit.eduAdd Countable instance for Ascii.asciihttps://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/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.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/147Add filter_app lemma2020-04-17T19:46:33ZTej Chajedtchajed@mit.eduAdd 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.