Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2017-11-13T18:13:54Zhttps://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/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/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 https://gitlab.mpi-sws.org/iris/iris/-/issues/28docs: the universe $\cal U$ is used without definition2016-08-16T17:40:06ZJeehoon Kangjeehoon.kang@kaist.ac.krdocs: the universe $\cal U$ is used without definitionHere: https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/model.tex#L155
Without saying that $\cal U$ is the universe (in whatever sense), the sentence seems confusing to me..Here: https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/model.tex#L155
Without saying that $\cal U$ is the universe (in whatever sense), the sentence seems confusing to me..https://gitlab.mpi-sws.org/iris/iris/-/issues/27mathpartir.sty is missing2016-08-09T13:09:45ZJeehoon Kangjeehoon.kang@kaist.ac.krmathpartir.sty is missingI believe the intention of `\usepackage{\basedir mathpartir}` in `iris.tex` is using the local `mathpartir.sty` file in the same directory. But it is missing in the repository.I believe the intention of `\usepackage{\basedir mathpartir}` in `iris.tex` is using the local `mathpartir.sty` file in the same directory. But it is missing in the repository.https://gitlab.mpi-sws.org/iris/iris/-/issues/26heap-lang CAS capability2016-10-21T20:08:42ZGhost Userheap-lang CAS capabilityCurrently, CAS can be performed on all value type, including pair. But this is not normally what real machine can do.
(However this is prevalent in a lot of simplified models?)
cc @jung Currently, CAS can be performed on all value type, including pair. But this is not normally what real machine can do.
(However this is prevalent in a lot of simplified models?)
cc @jung