stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2018-11-08T09:53:58Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/41Consistently block `simpl` on all `Z` operations2018-11-08T09:53:58ZRobbert KrebbersConsistently block `simpl` on all `Z` operationsWe used to do this some operations (`Z.add`, `Z.mul`), but not for others (`Z.sub`, `Z.of_nat`); this MR blocks `simpl` consistently for all operations involving `Z` that I could think of.
The rationale for blocking everything is that...We used to do this some operations (`Z.add`, `Z.mul`), but not for others (`Z.sub`, `Z.of_nat`); this MR blocks `simpl` consistently for all operations involving `Z` that I could think of.
The rationale for blocking everything is that `simpl` produces very bad results, e.g. try:
```coq
Require Import ZArith.
Eval simpl in (fun n y => Z.of_nat (S n) + y)%Z.
(*
Yields:
fun (n : nat) (y : Z) =>
match y with
| 0%Z => Z.pos (Pos.of_succ_nat n)
| Z.pos y' => Z.pos (Pos.of_succ_nat n + y')
| Z.neg y' => Z.pos_sub (Pos.of_succ_nat n) y'
end
*)
```
Note that blocking `simpl` for `Z.of_nat` used to break `lia` and `omega` in the past, see https://github.com/coq/coq/issues/5039. For `lia` this has been fixed, but for `omega` not yet. However, in !37 we decided to use `lia` everywhere in both std++ and Iris because it's faster, and moreover, I believe the Coq devs intend to deprecate `omega` in favor of `lia` in the future. So, I don't think we should care about `omega` anymore.
I also updated the item "Side-effects" in the README to document that we block `simpl` on `Z` operations.
@jjourdan @jung Any objections to this MR?
I have fixes for Iris, iris-examples, Iron, lambdaRust (which are mostly a couple of one-liners). I thus would like to merge this ASAP (so I don't get merge conflicts on my fixes).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/40Add `Countable` instance for `gset`.2018-06-29T11:25:47ZJannoAdd `Countable` instance for `gset`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/39begin a test suite2018-06-25T12:31:27ZRalf Jungjung@mpi-sws.orgbegin a test suiteTest that https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38 doesn't regress, and also add some tests for `solve_proper` because I remember being annoyed at some point that I had to go all the way to Iris to test even...Test that https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38 doesn't regress, and also add some tests for `solve_proper` because I remember being annoyed at some point that I had to go all the way to Iris to test even the most basic functionality.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/38decrease priority for rtc_reflexive instance2018-06-25T12:12:27ZRalf Jungjung@mpi-sws.orgdecrease priority for rtc_reflexive instanceWe give this instance a lower-than-usual priority because when it is applied to `Reflexive ?`, it leads to a new evar being created for `R`. Unfortunately, we cannot set `Hint Mode` for `Reflexive` in a way that just rules out `Reflexive...We give this instance a lower-than-usual priority because when it is applied to `Reflexive ?`, it leads to a new evar being created for `R`. Unfortunately, we cannot set `Hint Mode` for `Reflexive` in a way that just rules out `Reflexive ?` [1], but we can at least stop TC search from using this instance. This helps performance because it gives TC search less freedom in the remainder of the search. It doesn't seem like backtracking is happening here.
Also see the discussion below https://gitlab.mpi-sws.org/FP/iris-coq/commit/8e8c722870b36c23032d9bc10019e40e6eb6be62. I think this is useful even if we decide to roll back the `IntoVal` change as there may be other places where `rtc_reflexive` inadvertently gets chosen.
[1] That would break https://gitlab.mpi-sws.org/FP/iris-coq/blob/38ba379fae88865ed3a06ba44bf22938b6524610/theories/algebra/list.v#L213https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/22Reserve more notation in `integers.v`.2018-06-20T20:57:26ZDavid SwaseyReserve more notation in `integers.v`.Avoid duplicating details like `at level 35`.
This is a bit of a slippery slope. (I reserved just the notation that
I overload elsewhere.)Avoid duplicating details like `at level 35`.
This is a bit of a slippery slope. (I reserved just the notation that
I overload elsewhere.)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/36add lemma about chained difference2018-06-18T19:52:18ZRalf Jungjung@mpi-sws.orgadd lemma about chained differencehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/35solve_ndisj: try harder2018-06-14T20:24:20ZRalf Jungjung@mpi-sws.orgsolve_ndisj: try harderIn my logically atomic stack, the following goal fails to be solved currently but is solved after this patch:
```
⊤ ∖ ↑stackN ⊆ ⊤ ∖ ↑offerN ∖ ↑protoN
```
where
```
Definition stackN : namespace := nroot .@ "logatom_stack".
Definit...In my logically atomic stack, the following goal fails to be solved currently but is solved after this patch:
```
⊤ ∖ ↑stackN ⊆ ⊤ ∖ ↑offerN ∖ ↑protoN
```
where
```
Definition stackN : namespace := nroot .@ "logatom_stack".
Definition offerN : namespace := nroot .@ "logatom_stack" .@ "offer".
Definition protoN : namespace := nroot .@ "logatom_stack" .@ "protocol".
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/34add telescopic versions of the Coq quantifiers2018-06-09T09:47:09ZRalf Jungjung@mpi-sws.orgadd telescopic versions of the Coq quantifiershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/33add telescopes and a bit of theory about them2018-06-06T21:28:48ZRalf Jungjung@mpi-sws.orgadd telescopes and a bit of theory about themI think the basic definitions are pretty solid by now, though I am still fighting with making high-level telescope-based definitions that have nice pretty-printing.
Open question: Telescopes generalize hlists to the dependent case. Shou...I think the basic definitions are pretty solid by now, though I am still fighting with making high-level telescope-based definitions that have nice pretty-printing.
Open question: Telescopes generalize hlists to the dependent case. Should we get rid of hlists? Does anyone want to attempt porting hlist users over to telescopes? Restricting the dependency can actually be useful because it makes them easier to use.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/32introduce [default] as abbreviation for [from_option id], and use it2018-05-29T13:56:27ZRalf Jungjung@mpi-sws.orgintroduce [default] as abbreviation for [from_option id], and use itThere's some more uses in Iris, so this seems worth it. Over std++ and Iris together, the new default will actually be used *more often* than the old one I removed in !31.There's some more uses in Iris, so this seems worth it. Over std++ and Iris together, the new default will actually be used *more often* than the old one I removed in !31.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/31Remove the `default` notation for options2018-05-28T17:09:06ZRalf Jungjung@mpi-sws.orgRemove the `default` notation for optionsThe notation was parsing-only and all it did was reorder the arguments for
from_option. This creates just a needless divergence between what is written
and what is printed. Also, removing it frees the name for maybe introducing a
funct...The notation was parsing-only and all it did was reorder the arguments for
from_option. This creates just a needless divergence between what is written
and what is printed. Also, removing it frees the name for maybe introducing a
function or notation `default` with a type like `T -> option T -> T`.
I volunteer to fix all reverse deps that we know about.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/30Notations for relations with explicit type arguments2018-04-06T12:27:13ZRobbert KrebbersNotations for relations with explicit type argumentsWe discussed this already here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/134
The consensus was that `@{A}` would be a good fit, and would not cause conflicts. I implemented it here for hopefully all relations in std++: `=`,...We discussed this already here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/134
The consensus was that `@{A}` would be a good fit, and would not cause conflicts. I implemented it here for hopefully all relations in std++: `=`, `≡`, `⊆`, `⊂`, `⊑`, `##`, `∈`, `≡ₚ`, and adopted the code at many places to make use of these notations.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/28add exact_vm_cast2018-03-01T15:57:30ZRalf Jungjung@mpi-sws.orgadd exact_vm_castThis generalizes https://gitlab.mpi-sws.org/FP/LambdaRust-coq/merge_requests/10 into a reusable tactic.This generalizes https://gitlab.mpi-sws.org/FP/LambdaRust-coq/merge_requests/10 into a reusable tactic.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/27Add a `NoBackTrack` type class.2018-02-09T08:57:26ZRobbert KrebbersAdd a `NoBackTrack` type class.`NoBackTrack P` requires `P` but will never backtrack on it
once a result for `P` has been found.
See also https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112`NoBackTrack P` requires `P` but will never backtrack on it
once a result for `P` has been found.
See also https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/26A simple type class based canceler for natural numbers.2018-02-08T15:27:18ZRobbert KrebbersA simple type class based canceler for natural numbers.See also https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/109
Main question: where to put this? In `numbers.v` or in a separate file (as in this MR).See also https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/109
Main question: where to put this? In `numbers.v` or in a separate file (as in this MR).Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/25Add a Notation for `sn`: strongly normalizing.2018-01-13T22:46:59ZRobbert KrebbersAdd a Notation for `sn`: strongly normalizing.As requested by @jung in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/65
I made this a notation to avoid unfolding issues.As requested by @jung in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/65
I made this a notation to avoid unfolding issues.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/23Lattices notation for order, join, meet, top and bot.2017-12-05T19:14:14ZJacques-Henri JourdanLattices notation for order, join, meet, top and bot.They are needed both for `monPred` and the weak memory lifetime logic.They are needed both for `monPred` and the weak memory lifetime logic.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/24typeclass comments2017-12-05T19:13:59ZRalf Jungjung@mpi-sws.orgtypeclass commentsI only now understood why `Equiv` is called the way it is. Let's document that.I only now understood why `Equiv` is called the way it is. Let's document that.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/15Provide a pretty-printer for [nat].2017-11-29T17:44:35ZGhost UserProvide a pretty-printer for [nat].Pretty-print nat; this simply reduced to the N pretty printer.Pretty-print nat; this simply reduced to the N pretty printer.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/21Make x.1, x.2 notation compatible with ssrfun.2017-11-29T15:10:24ZDavid SwaseyMake x.1, x.2 notation compatible with ssrfun.Enable one to import both stdpp's base and ssrfun.
Note that (f x.1) now parses as (f (fst x)) rather than (fst (f x)).
(This change affects one proof in Iris.)Enable one to import both stdpp's base and ssrfun.
Note that (f x.1) now parses as (f (fst x)) rather than (fst (f x)).
(This change affects one proof in Iris.)