Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2017-01-14T21:53:11Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/50`contains` is named the wrong way around2017-01-14T21:53:11ZRalf Jungjung@mpi-sws.org`contains` is named the wrong way around``l1 `contains` l2`` confusing expresses that `l2` contains `l1`. Either the order of arguments should be changed, or the notation should be changed to e.g. `contained`.``l1 `contains` l2`` confusing expresses that `l2` contains `l1`. Either the order of arguments should be changed, or the notation should be changed to e.g. `contained`.Iris 3.0https://gitlab.mpi-sws.org/iris/iris/-/issues/49Improve support of simplify_option_eq (and simplify_map_eq?) for setoids2017-11-13T18:13:54ZRalf Jungjung@mpi-sws.orgImprove support of simplify_option_eq (and simplify_map_eq?) for setoidsSome testcases:
* <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d#59b3a9376af7e8ce6a745e02cef554707e5c7419_585_585>
* in lambdaRust, lifetime/primitive.v, proof of `own_ilft_auth_agree`Some testcases:
* <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d#59b3a9376af7e8ce6a745e02cef554707e5c7419_585_585>
* in lambdaRust, lifetime/primitive.v, proof of `own_ilft_auth_agree`Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/48Unify `iNext` and `iModIntro` (and more?)2018-07-13T15:56:18ZRobbert KrebbersUnify `iNext` and `iModIntro` (and more?)These tactics are very similar. I would be nice to generalize `iModIntro` to also strip occurrences of the modality from all of the hypotheses.
Given that we have already generalized `iNext` to deal with the iterated later modality, I t...These tactics are very similar. I would be nice to generalize `iModIntro` to also strip occurrences of the modality from all of the hypotheses.
Given that we have already generalized `iNext` to deal with the iterated later modality, I think this should not be too difficult.
See also the discussion as part of commit 9ae19ed5.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/47Use opam-based CI2016-12-14T13:19:40ZRalf Jungjung@mpi-sws.orgUse opam-based CII'd like to use the same opam-based CI setup that we also use for lambdaRust. This will also make it trivial for us to run the CI with both Coq 8.5 and 8.6, and to change Coq versions in the future (no changes in the CI image needed for ...I'd like to use the same opam-based CI setup that we also use for lambdaRust. This will also make it trivial for us to run the CI with both Coq 8.5 and 8.6, and to change Coq versions in the future (no changes in the CI image needed for this any more, yay :D ).
However, to make that work, we have to stop importing `.` in `_CoqProject`. So like in lambdaRust, I'd like to move everything into a subfolder `theories/`.
This will break all merge requests, so we should get at least some of them in. !30 will hang around for a while, so whatever. But I'd like to wait until we get at least !25 or !22 in.Iris 3.0Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/46Use the correct setoid equality in algebra/gset and algebra/coPset2016-11-30T12:14:50ZHai DangUse the correct setoid equality in algebra/gset and algebra/coPsetcofe_equiv takes precedence over available equivalences, which prevents rewriting with those equivalences. I have to make explicit those instances.
@janno suggested that it is due to this hint?
https://gitlab.mpi-sws.org/FP/iris-co...cofe_equiv takes precedence over available equivalences, which prevents rewriting with those equivalences. I have to make explicit those instances.
@janno suggested that it is due to this hint?
https://gitlab.mpi-sws.org/FP/iris-coq/blob/75518c9a4c5278b44120212060c2faceb875de3f/algebra/ofe.v#L52Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/45iLöb with non-empty revert list2016-11-30T12:14:50ZJannoiLöb with non-empty revert listWhen iLöb is given a list of iris assumptions it does not automatically generalize over all spatial assumptions any more. Adding a ∗ to the list of assumptions solves that problem.
Proposal: always add ∗ to the list of Iris assumptions.When iLöb is given a list of iris assumptions it does not automatically generalize over all spatial assumptions any more. Adding a ∗ to the list of assumptions solves that problem.
Proposal: always add ∗ to the list of Iris assumptions.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/44Vague iRevert error messages2016-11-30T12:14:50ZJannoVague iRevert error messagesiRevert does not report why exactly it fails (e.g. because the variable is used in a spatial assumption). It should do that. :)
(Note: ltac's revert actually has somewhat useful error messages.)iRevert does not report why exactly it fails (e.g. because the variable is used in a spatial assumption). It should do that. :)
(Note: ltac's revert actually has somewhat useful error messages.)Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/43Proof mode intro pattern lexer: _ should be allowed as part of varianme names2016-11-24T08:27:45ZRalf Jungjung@mpi-sws.orgProof mode intro pattern lexer: _ should be allowed as part of varianme names`A_B` is a fine variable name. It is parsed as `A _ B`.`A_B` is a fine variable name. It is parsed as `A _ B`.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/42Authoritative with fraction2019-06-06T11:07:12ZRalf Jungjung@mpi-sws.orgAuthoritative with fractionThe authoritative CMRA provides a CMRA with a single, authoritative state. Several times now (most recently when @janno asked me about sth. like this today), it seemed useful to allow *more than one* authoritative state, that all have to...The authoritative CMRA provides a CMRA with a single, authoritative state. Several times now (most recently when @janno asked me about sth. like this today), it seemed useful to allow *more than one* authoritative state, that all have to be brought together to change it. I just realized that this could be supported by a fairly small change in the authoritative CMRA, namely to replace `Ex(M)` by `Frac * Ag(M)`:
```
Auth(M) := { (x, a) \in (Frac * Ag(M))^? * M | ...}
```
The interface would then change to allow a fraction in the `●` notation (and once we have an infrastructure for "assertions that can be split at a fraction", it could be registered there). What do you think?
Cc @janno @robbertkrebbers @jjourdanRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/41Rewrite unexpectedly failing (Nested below |-, *, \later, -*)2016-10-28T09:07:53ZRalf Jungjung@mpi-sws.orgRewrite unexpectedly failing (Nested below |-, *, \later, -*)The rewrite at <https://gitlab.mpi-sws.org/FP/iris-coq/blob/ralf/broken-rewrite/heap_lang/lifting.v#L66> is unexpectedly failing.
The goal is of the shape
```
▷ ownP σ ★ ▷ (ownP σ -★ Φ v) ⊢ ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v)
```
and I am ...The rewrite at <https://gitlab.mpi-sws.org/FP/iris-coq/blob/ralf/broken-rewrite/heap_lang/lifting.v#L66> is unexpectedly failing.
The goal is of the shape
```
▷ ownP σ ★ ▷ (ownP σ -★ Φ v) ⊢ ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v)
```
and I am trying to rewrite backwards with `P ⊢ |={E}=> P` to remove the fancy update (behind the linear view shift notation).
Cc @robbertkrebbers could you have a look at this?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/40iRewrite and internal equality on predicates2016-10-27T14:34:24ZJannoiRewrite and internal equality on predicatesConsider the following example: (Ignore saved_prop_own, I only needed it to make Coq happy)
```
Lemma test {A} (P Q : A -c> iProp) a i φ :
saved_prop_own i φ ★ P ≡ Q ⊢ P a ≡ Q a.
Proof.
iIntros "[_ #E]".
Fail iR...Consider the following example: (Ignore saved_prop_own, I only needed it to make Coq happy)
```
Lemma test {A} (P Q : A -c> iProp) a i φ :
saved_prop_own i φ ★ P ≡ Q ⊢ P a ≡ Q a.
Proof.
iIntros "[_ #E]".
Fail iRewrite "E".
Abort.
```
It seems to me that iRewrite should succeed here. Is there a logical reason for it to fail? (As opposed to an engineering reason.)
(We are using commit 9c5a95d3b271f4e0d0c657964dfa386070d0b322 in case that matters.)https://gitlab.mpi-sws.org/iris/iris/-/issues/39iIntros: bad error when trying to use a name that's already used2016-10-26T20:07:46ZRalf Jungjung@mpi-sws.orgiIntros: bad error when trying to use a name that's already usedIf there already is a variable `x` in the context, running `iIntros (x)` yields "No applicable tactic". That's not a very useful error, and it just took me a while to realize the actual problem. Is there a way to make this show the error...If there already is a variable `x` in the context, running `iIntros (x)` yields "No applicable tactic". That's not a very useful error, and it just took me a while to realize the actual problem. Is there a way to make this show the error generated by the underlying `intros`?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/38Refactor bigops2017-04-01T19:10:03ZRalf Jungjung@mpi-sws.orgRefactor bigopsCurrently, bigops are tied to CMRAs. This is silly, because it means we have to show extension for e.g. uPred (which so far we can only do after picking a silly validity), and also because it restricts us to pick *one* operator to be use...Currently, bigops are tied to CMRAs. This is silly, because it means we have to show extension for e.g. uPred (which so far we can only do after picking a silly validity), and also because it restricts us to pick *one* operator to be used in bigops, whereas we may also want to use big conjunction.
Instead we should do sth. like ssreflect does, with a typeclass/canonical structure for this special purpose that's completely separate from the main algebraic hierarchy.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/37saved_prop for predicate2016-10-05T23:07:43ZGhost Usersaved_prop for predicateI have a `Q: val -> iProp`, now I want to save predicate `Q` just like the saved proposition. How to do that?I have a `Q: val -> iProp`, now I want to save predicate `Q` just like the saved proposition. How to do that?https://gitlab.mpi-sws.org/iris/iris/-/issues/36STSs: Consider changing the def. of frame-steps2019-11-01T13:16:11ZRalf Jungjung@mpi-sws.orgSTSs: Consider changing the def. of frame-stepsJeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification...Jeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification:
> $(\mathcal{L}(s') # T) /\ s \rightarrow s' .$
> This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus \mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).
We could change `frame_step` accordingly, maybe this simplifies some things a little.https://gitlab.mpi-sws.org/iris/iris/-/issues/35Renaming things2016-11-09T12:42:38ZRalf Jungjung@mpi-sws.orgRenaming thingsThere are some names some of us are not happy with. This issue is just meant to track the latest status in these discussions.
* `◇`: After a lot of discussion about `except_last` vs. `except_now`, we agreed that depending on whether y...There are some names some of us are not happy with. This issue is just meant to track the latest status in these discussions.
* `◇`: After a lot of discussion about `except_last` vs. `except_now`, we agreed that depending on whether you look at the adequacy theorem or the state at some point of the proof, either may make sense. We all agreed that `except_0` would be acceptable.
* `≡`: I still plan to rename this from `uPred_eq` to `uPred_internal_eq`.
* The lowest-level view shift... my latest suggestion was
```
|=u=> Q update modality
|={E1,E2}=> Q view modality
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
```
or
```
|=s=> Q state update (modality)
|={E1,E2}=> Q view update (modality)
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
```
I couldn't find JH's last proposal. Robbert expressed that he liked Derek's:
```
|=p=> Q primitive shift
|={E1,E2}=> Q primitive view shift
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
```
However, my concern here is that it becomes hard to say that we want a
"primitive non-view shift". Also, the "primitive view shift" is not
primitive...
* Filenames:
```
base_logic/upred [just the definition, metric space, functors]
base_logic/primitive [primitive connectives and proofs in the model]
base_logic/base_logic or base_logic/logic [upred + primitive + derived connectives/rules]
```Iris 3.0https://gitlab.mpi-sws.org/iris/iris/-/issues/34Coq induction support in proof mode2016-09-30T10:31:09ZJacques-Henri JourdanCoq induction support in proof modeThere is no "right" way to do induction when in proof mode.
The minimal feature would be to provide a tactic to revert a proof mode goal (with empty context ?) into a standard Coq goal.There is no "right" way to do induction when in proof mode.
The minimal feature would be to provide a tactic to revert a proof mode goal (with empty context ?) into a standard Coq goal.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/33Confusing error msg for `iTimeless`2016-10-27T14:36:30ZGhost UserConfusing error msg for `iTimeless`For example,
```
Section demo.
Context `{!heapG Σ} (N: namespace).
Lemma foo (P: iProp Σ): inv N P ⊢ WP ref #1 {{ _, True%I }}.
Proof.
iIntros "#?".
iInv N as ">H" "Hclose".
```
Here, the error info will be
...For example,
```
Section demo.
Context `{!heapG Σ} (N: namespace).
Lemma foo (P: iProp Σ): inv N P ⊢ WP ref #1 {{ _, True%I }}.
Proof.
iIntros "#?".
iInv N as ">H" "Hclose".
```
Here, the error info will be
```
Toplevel input, characters 21-44:
Ltac call to "iInv" failed.
Error: Tactic failure: iTimeless: (▷ P)%I not timeless.
```
But this is confusing, because the concern is that `P` is not timeless, not `▷ P`.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/32Support framing pure/Coq hypotheses2016-09-19T19:18:18ZJacques-Henri JourdanSupport framing pure/Coq hypothesesIn the following, iFrame does not have the expected behavior:
Lemma L `{irisG Λ Σ} : ∀ P:iProp Σ, □ P ⊢ P ★ True.
iIntros (P) "#HP". iFrame.In the following, iFrame does not have the expected behavior:
Lemma L `{irisG Λ Σ} : ∀ P:iProp Σ, □ P ⊢ P ★ True.
iIntros (P) "#HP". iFrame.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/30Make coqchk (make verify) work2016-08-19T10:00:16ZRalf Jungjung@mpi-sws.orgMake coqchk (make verify) workCurrently, `make verify` fails with a stack overflow while checking `iris.prelude.pretty.pretty_N_inj`. We had a similar issue with another lemma in the same file, and Guillaume found a work-around for it (see https://coq.inria.fr/bugs/s...Currently, `make verify` fails with a stack overflow while checking `iris.prelude.pretty.pretty_N_inj`. We had a similar issue with another lemma in the same file, and Guillaume found a work-around for it (see https://coq.inria.fr/bugs/show_bug.cgi?id=4788). Can we find a similar work-around here?
Cc @robbertkrebbers