Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-11-24T20:53:20Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/498Add support for more tactics in spec patterns2022-11-24T20:53:20ZRalf Jungjung@mpi-sws.orgAdd support for more tactics in spec patternsOur spec patterns support `//`, but sometimes one wants to use other tactics -- most frequently `eauto with iFrame`. Would be nice to have time way to support them.
Ssreflect itself has 10 numbered patterns (not entirely sure about the ...Our spec patterns support `//`, but sometimes one wants to use other tactics -- most frequently `eauto with iFrame`. Would be nice to have time way to support them.
Ssreflect itself has 10 numbered patterns (not entirely sure about the syntax for those -- @blaisorblade?) and `/[name]` for named patterns (not sure what the syntax is for declaring one).https://gitlab.mpi-sws.org/iris/iris/-/issues/497Hint Immediate plain_persistent affects type inference of unrelated variables2022-11-25T02:25:29ZPaolo G. GiarrussoHint Immediate plain_persistent affects type inference of unrelated variablesI reproduced the same issue as https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/424 / https://gitlab.mpi-sws.org/iris/stdpp/-/issues/160. Below, notice how evar `?T` is instantiated with `Plain P`, and how that stops once we replac...I reproduced the same issue as https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/424 / https://gitlab.mpi-sws.org/iris/stdpp/-/issues/160. Below, notice how evar `?T` is instantiated with `Plain P`, and how that stops once we replace the `Hint Immediate.
```coq
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Section foo.
Context (PROP : bi) `{BiPlainly PROP}.
Implicit Type (P : PROP).
Lemma test P `{!Affine P} `{!Plain P} :
∃ T : Type, T -> P ⊢ □ P.
Proof.
eexists.
Show.
(*
1 focused goal (shelved: 1)
PROP : bi
H : BiPlainly PROP
P : PROP
Affine0 : Affine P
Plain0 : Plain P
============================
?T → P -∗ □ P
*)
iIntros (X) "#?".
Show.
(*
1 goal
PROP : bi
H : BiPlainly PROP
P : PROP
Affine0 : Affine P
Plain0 : Plain P
X : Plain P
============================
_ : P
--------------------------------------□
□ P
*)
Abort.
Local Remove Hints plain_persistent : typeclass_instances.
(* An instance would be enough locally: *)
(* Local Existing Instance plain_persistent. *)
(* but we sketch the proper fix. *)
Ltac solve_tc_onestep :=
solve [once (typeclasses eauto 1)].
Local Hint Extern 1 (Persistent _) =>
notypeclasses refine (plain_persistent _ _); solve_tc_onestep : typeclass_instances.
Lemma test P `{!Affine P} `{!Plain P} :
∃ T : Type, T -> P ⊢ □ P.
Proof.
eexists.
Show.
(*
1 focused goal (shelved: 1)
PROP : bi
H : BiPlainly PROP
P : PROP
Affine0 : Affine P
Plain0 : Plain P
============================
?T → P -∗ □ P
*)
iIntros (X) "#?".
Show.
(*
1 focused goal (shelved: 1)
PROP : bi
H : BiPlainly PROP
P : PROP
Affine0 : Affine P
Plain0 : Plain P
X : ?T
============================
_ : P
--------------------------------------□
□ P
*)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/496Cannot iApply lemma with let-binder and bi_emp_valid2022-11-23T18:37:35ZRalf Jungjung@mpi-sws.orgCannot iApply lemma with let-binder and bi_emp_validThe following script fails:
```
Lemma test_iPoseProof_let2 P Q :
(let R := True%I in ⊢ R ∗ P -∗ Q) →
P ⊢ Q.
Proof.
iIntros (help) "HP".
iPoseProof (help with "[$HP]") as "?". done.
Qed.
```
It says (notation printing due to this ...The following script fails:
```
Lemma test_iPoseProof_let2 P Q :
(let R := True%I in ⊢ R ∗ P -∗ Q) →
P ⊢ Q.
Proof.
iIntros (help) "HP".
iPoseProof (help with "[$HP]") as "?". done.
Qed.
```
It says (notation printing due to this being in !791)
```
Error: Tactic failure: iPoseProof: (let R := True%I in R ∗ P -∗ Q) not a BI assertion.
```
If I move the ⊢ between `R ∗ P` and `Q`, it works, so this is related to bi_entails vs bi_emp_valid somehow.https://gitlab.mpi-sws.org/iris/iris/-/issues/494Support `%x` in selection patterns2022-11-03T15:11:41ZRobbert KrebbersSupport `%x` in selection patternsThen we can do things such as `iRevert "%x H"`.Then we can do things such as `iRevert "%x H"`.https://gitlab.mpi-sws.org/iris/iris/-/issues/493Using hypotheses / applying lemmas "up to equality"2022-11-02T18:24:00ZRalf Jungjung@mpi-sws.orgUsing hypotheses / applying lemmas "up to equality"Perennial has an `iExactEq` tactic that works as follows: if your goal is `G` and there is a hypothesis `H: P`, you can use `iExactEq "H"` and then have to prove that `P = G`. This can be useful when a hypothesis is equal to the goal but...Perennial has an `iExactEq` tactic that works as follows: if your goal is `G` and there is a hypothesis `H: P`, you can use `iExactEq "H"` and then have to prove that `P = G`. This can be useful when a hypothesis is equal to the goal but they don't unify -- now you can use `rewrite` and `f_equiv` without having to explicitly state the equality.
Similarly one could imagine an `iApplyEq` that is like `iApply` but in case of unification failure requires the user to prove an equality.https://gitlab.mpi-sws.org/iris/iris/-/issues/491Regression of iFrame (with BiAffine and <absorb> _)2022-11-29T17:13:08ZRodolphe LepigreRegression of iFrame (with BiAffine and <absorb> _)@janno and I noticed a change of behaviour of the `iFrame` tactic that is better illustrated by the following code.
```coq
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Goal forall (PROP : bi) (H_PROP : B...@janno and I noticed a change of behaviour of the `iFrame` tactic that is better illustrated by the following code.
```coq
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Goal forall (PROP : bi) (H_PROP : BiAffine PROP) (P Q : PROP),
<absorb> P ∗ Q ⊢ <absorb> (P ∗ Q).
Proof.
iIntros (?? P Q) "[P Q]".
Fail Fail iFrame "Q".
(* The following used to work. *)
Fail iFrame "Q"; iFrame "P".
Fail iFrame "Q P".
Fail Fail by iSplitR "Q".
Fail Fail by iSplitL "P".
Abort.
```
The failures were noticed using Iris version `dev.2022-09-29.0.b335afaf`, and they did not happen with version `dev.2022-05-04.0.10e843d9`. I suspect this is related to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/838 (cc @robbertkrebbers), but I did not bisect.https://gitlab.mpi-sws.org/iris/iris/-/issues/490Move heaplang.sty towards being a community standard2022-10-14T13:38:49ZJonas KastbergMove heaplang.sty towards being a community standardSimilarly to #488 I believe it is beneficial to more carefully curate the `heaplang.sty` file contained in this repository.
Some immediate considerations that might make sense to review are:
- The notion-style supported by the language ...Similarly to #488 I believe it is beneficial to more carefully curate the `heaplang.sty` file contained in this repository.
Some immediate considerations that might make sense to review are:
- The notion-style supported by the language macros - e.g. parentheses vs spaces for function arguments
- The naming of each macro, to avoid clashes with popular latex packages
- Discuss what similarities we want HeapLang to have with existing languages (formerly ML, but has since moved quite past it)
- Casing of constructs, both in Latex and notation. Currently we have discrepancies such as `ref` and `Alloc` even though they live on the same level. The latex macros are mostly consistent, with some outliers like `\poison` and `\fold` / `\unfold`
The MR's !852 and !853 are some initial steps in this direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/488Move iris.sty towards being a community standard2022-10-27T11:54:07ZJonas KastbergMove iris.sty towards being a community standardMy impression is that there a multiple people who take inspiration from the `iris.sty` file
when writing papers about Iris.
For one, we use (a variant of) it in the Iris Lecture Notes (Soon to be publicly available).
I find that it would...My impression is that there a multiple people who take inspiration from the `iris.sty` file
when writing papers about Iris.
For one, we use (a variant of) it in the Iris Lecture Notes (Soon to be publicly available).
I find that it would be beneficial to have a "community standard" for this collection of macros,
to guarantee that notation is uniform throughout Iris papers (while of course authors should be free to diverge from the standard as need be).
To achieve this the style-file should be kept up to date with changing notation, terminiology, etc.
While good effort has already been put towards this, I find that more improvements could be made,
e.g. by reviewing the current file on terms such as:
- Completeness of the macro set (For one there is currently no `\pointsto`)
- Names of the macros (For one `\always` seem outdated in terms of the current "persistently" terminology)
- Notation of the macros
- Formatting of macros (kerning, squashing, etc.)
The merge request !851 is an attempt at an initial step in this direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/487Adding pointer order comparison to HeapLang2022-10-14T19:33:59ZArthur Azevedo de AmorimAdding pointer order comparison to HeapLangAs the following file shows, HeapLang makes it possible to compare pointers for their relative ordering. Should we extend the primitive comparison operation on HeapLang to work on pointers as well?
[pointer_comparison.v](/uploads/f638e4...As the following file shows, HeapLang makes it possible to compare pointers for their relative ordering. Should we extend the primitive comparison operation on HeapLang to work on pointers as well?
[pointer_comparison.v](/uploads/f638e4e4e81b856b5be629e623fe608f/pointer_comparison.v)https://gitlab.mpi-sws.org/iris/iris/-/issues/479`if b then ... else ...` is never persistent2023-10-25T19:31:57ZRalf Jungjung@mpi-sws.org`if b then ... else ...` is never persistentIn some situations it is fairly natural to write a proposition as `if b then P else Q`, where `b: bool`. However, even if both `P` and `Q` are persistent, such a proposition cannot be moved into the persistent context, which can be somew...In some situations it is fairly natural to write a proposition as `if b then P else Q`, where `b: bool`. However, even if both `P` and `Q` are persistent, such a proposition cannot be moved into the persistent context, which can be somewhat annoying.
So I wonder, should we add instances for propositions defined via `if`? Which typeclasses should get such instances? Is there some way we can make this work for *all* typeclasses in one go?https://gitlab.mpi-sws.org/iris/iris/-/issues/478Adding satisfiable to Iris2022-08-17T05:24:37ZSimon SpiesAdding satisfiable to IrisSeveral Iris projects have structured their adequacy proofs using the notion of a "`satisfiable`-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notio...Several Iris projects have structured their adequacy proofs using the notion of a "`satisfiable`-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notion of `satisfiable` can be added to Iris in a meaningful way and whether it can enable more modular adequacy proofs in the future.https://gitlab.mpi-sws.org/iris/iris/-/issues/477`iFrame` peforms some surprising modality cleanup2023-07-25T16:00:13ZRalf Jungjung@mpi-sws.org`iFrame` peforms some surprising modality cleanupFraming `<affine> P` on goal `<affine> <affine> (P ∗ Q)` produces the result `<affine> Q`. I think that is rather srprising and would have expected `<affine> <affine> Q`. It seems like as it traverses the term, `iFrame` is a bit too quic...Framing `<affine> P` on goal `<affine> <affine> (P ∗ Q)` produces the result `<affine> Q`. I think that is rather srprising and would have expected `<affine> <affine> Q`. It seems like as it traverses the term, `iFrame` is a bit too quick to apply the `MakeAffine` class even when there was a literal affinely modality before that should IMO just be preserved.
For `<absorb>` and `<pers>`, `iFrame` just fails in the same situation. The same is true for `□`, but when one has `P` in the intuitionistic context, then one can frame into goal `□ □ (P ∗ Q)` and once https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/842 lands that will produce `□ Q`.https://gitlab.mpi-sws.org/iris/iris/-/issues/476Have `known_make_absorbingly` and `make_absorbingly_default` instances in the...2022-08-15T14:17:18ZRalf Jungjung@mpi-sws.orgHave `known_make_absorbingly` and `make_absorbingly_default` instances in the same fileThe following discussion from !842 should be addressed:
> This makes me think, it's a bit annoying that the default instance and `known_make_absorbingly` are not at the same place. Could we somehow refactor that? Move the default instan...The following discussion from !842 should be addressed:
> This makes me think, it's a bit annoying that the default instance and `known_make_absorbingly` are not at the same place. Could we somehow refactor that? Move the default instances to `classes_make`, or move the other one here?https://gitlab.mpi-sws.org/iris/iris/-/issues/475Provide some way to "seal" a BI2022-08-12T14:53:14ZRalf Jungjung@mpi-sws.orgProvide some way to "seal" a BIOne reason why GPFSL and Iron are slower might be that their BI is bigger -- it is constructed via a combinator on top of iProp. So whenever the proof mode needs to query some property of the BI, there is one extra step, and also terms i...One reason why GPFSL and Iron are slower might be that their BI is bigger -- it is constructed via a combinator on top of iProp. So whenever the proof mode needs to query some property of the BI, there is one extra step, and also terms in general are just bigger.
It might be worth investigating some nice way to seal a BI (but that would probably have to be a macro):
- either lightweight sealing by just making it TC opaque and forwarding all instances
- or a proper seal that makes terms no convertible any more, and a *lot* of forwarding of things
We *do* seal `iProp` pretty heavily (in fact even more proper than the "proper" seal, this is the one place where we use a module type for sealing to be *really sure*), so Iris itself doesn't have this problem.
@robbertkrebbers IIRC you did an experiment along the lines of doing that by hand once? What were the results of that again?https://gitlab.mpi-sws.org/iris/iris/-/issues/471Planning for dune support (draft)2023-07-04T13:26:00ZPaolo G. GiarrussoPlanning for dune support (draft)Supporting dune would let users benefit from the dune cache, composable builds, etc. OTOH, its Coq support still has rough edges; in particular, `make vos` and `make validate` have no analogue yet.
Ralf was open to supporting dune as lo...Supporting dune would let users benefit from the dune cache, composable builds, etc. OTOH, its Coq support still has rough edges; in particular, `make vos` and `make validate` have no analogue yet.
Ralf was open to supporting dune as long as somebody else volunteered to maintain suport for it: https://mattermost.mpi-sws.org/iris/pl/bjqieom1tjrqmck6ahh9zp5ipc. I volunteer to help; I'd like somebody else to do that as well.
Various increments are possible:
1. enable building stdpp without tests
2. enable building iris, without tests; here we must choose whether to assume stdpp is installed, or assume it is part of the dune workspace and use compositional builds;
3. enable using dune in CI
4. document how to take advantage of dune — adding pointers on external docs where possible
- either document work arounds to use with Proof General (add `_build/default` to `_CoqProject`), or get the issue fixed properly upstream
5. migrate tests to dune cram tests (and potentially migrate Makefile.coq.local to support the new syntax)
I have some ideas of the maintenance costs.
- Coq warning flags need be synchronized between coq_makefile and dune
- Tests need be formatted as cram testshttps://gitlab.mpi-sws.org/iris/iris/-/issues/463Rename "head step"?2022-06-10T18:13:39ZRalf Jungjung@mpi-sws.orgRename "head step"?At some point there was a discussion on Mattermost about people objecting to the term "head step" that we use in our HeapLang operational semantics. I think there were proposals for others names, but I forgot if there was any consensus.At some point there was a discussion on Mattermost about people objecting to the term "head step" that we use in our HeapLang operational semantics. I think there were proposals for others names, but I forgot if there was any consensus.https://gitlab.mpi-sws.org/iris/iris/-/issues/462iRewrite with a Coq-level equality gives bad error message2022-05-20T17:14:58ZRalf Jungjung@mpi-sws.orgiRewrite with a Coq-level equality gives bad error messageIn a lambdaRust proof, I tried `iRewrite tctx_hasty_val in "Ha''".`. I had forgotten that `iRewrite` is for internal equalities only. That shows this error:
```
Error: No matching clauses for match.
```
This error is always a bug, at le...In a lambdaRust proof, I tried `iRewrite tctx_hasty_val in "Ha''".`. I had forgotten that `iRewrite` is for internal equalities only. That shows this error:
```
Error: No matching clauses for match.
```
This error is always a bug, at least the tactic should tell me what is wrong. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/460Improve iCombine to derive validity properties of ghost state automatically2023-05-25T11:45:27ZIke MulderImprove iCombine to derive validity properties of ghost state automaticallyIt would be great if `iCombine` was also able to derive and provide validity properties of ghost state or mapsto connectives automatically. Currently, you have to search and apply such properties manually. This could be fixed if `iCombin...It would be great if `iCombine` was also able to derive and provide validity properties of ghost state or mapsto connectives automatically. Currently, you have to search and apply such properties manually. This could be fixed if `iCombine` takes an extra (optional) `gives` clause, which provides extra persistent facts (if those exist).
For example, consider the following environment:
```
"H1" : l ↦{#q1} v1
"H2" : l ↦{#q2} v2
```
executing `iCombine "H1 H2" as "H" gives %[Hq Hv]` should replace `"H1"` and `"H2"` with `"H": l ↦{#(q1 + q2)} v1` and introduces two new pure hypotheses `Hq : q1 + q2 ≤ 1` and `Hv : v1 = v2`.
The roadmap for implementing this would be split into two merge requests:
1. Change `FromSep` to only be used for `iSplit{L,R}`, change `iCombine` to rely on two new typeclasses `CombineSepAs` and `CombineSepGives`.
These would be defined as `CombineSepAs P1 P2 P := P1 ∗ P2 ⊢ P` where `P1 P2` are input, `P` output
and `CombineSepGives P1 P2 := P1 ∗ P2 ⊢ <pers> R` where `P1 P2` are input, `R` output.
This MR would provide some instances for stuff in `base_logic.lib`, `mapsto`.
The new syntax would be `iCombine "Hs" [as "H"] [gives "P"]`, where either the `as` clause or the `gives` clause must be present.
* If `as "H"` is present, all hypotheses `"Hs"` will be replaced by `"H"`, which can be an introduction pattern.
If not present, all `"Hs"` are kept as is
* If `gives "P"` is present, additionally learn persistent fact `"P"`, which can be an introduction pattern. Also supports `%?` introduction if this fact is pure.
* If more than two hypotheses are provided in `"Hs"`, repeatedly run `CombineSep` with the accumulated results
* There will be an additional boolean indicating whether `CombineSepAs` used the default instance.
2. Give general instance for `own` (= MR !771, addresses #251)
This is a summary of a discussion by @jung, @robbertkrebbers, @snyke7 and @gmalecha at the Iris Workshop. Let me know if I forgot something.https://gitlab.mpi-sws.org/iris/iris/-/issues/458Inconsistency in weakening of modalities in `iApply`2022-05-01T11:54:32ZRobbert KrebbersInconsistency in weakening of modalities in `iApply````coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens...```coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens is that the first (and failing) `iApply` directly attempts to find an `IntoWand` instance to match the conclusion of the wand with the goal. This fails because the only applicable `IntoWand` instance is:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
There is no `FromAssumption` for `Q`, so no weakening of the conclusion is performed.
In the second attempt, `iApply` will first `iSpecialize` with the wand. As such, it tries to find an `IntoWand` instance where the conclusion can be unified with an evar. Then after that, it will use `iAssumption`, which uses `FromAssumption` to weaken the modality.
## Solution
We probably should add `FromAssumption` to instances like `into_wand_wand`. I do not know if this was just an omission, or there's a reason for that. Should try.https://gitlab.mpi-sws.org/iris/iris/-/issues/457"-" in selection patterns2024-02-26T16:06:50ZRalf Jungjung@mpi-sws.org"-" in selection patternsIt would be really useful to support "-" in selection patterns, such that one can do `iClear "- H1 H2 H3"`, like one can with regular Coq `clear`.It would be really useful to support "-" in selection patterns, such that one can do `iClear "- H1 H2 H3"`, like one can with regular Coq `clear`.