Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-09-20T12:30:26Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/266`iDestruct 1` does not work when `Z_scope` is open2019-09-20T12:30:26ZJacques-Henri Jourdan`iDestruct 1` does not work when `Z_scope` is openIn this case, we have to write `iDestruct 1%nat`. It would be perfect to add the tactic notation for Z, too.In this case, we have to write `iDestruct 1%nat`. It would be perfect to add the tactic notation for Z, too.https://gitlab.mpi-sws.org/iris/iris/-/issues/76`iDestruct` for big ops2017-05-19T15:20:29ZRobbert Krebbers`iDestruct` for big opsTogether with @jung and @jjourdan we discussed that it would be useful if `iDestruct` (and tactics like `iSplit` and `iFrame`) would have better support for big ops, in particular, that when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ ...Together with @jung and @jjourdan we discussed that it would be useful if `iDestruct` (and tactics like `iSplit` and `iFrame`) would have better support for big ops, in particular, that when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ k x
we could use `iDestruct "H" as "[H1 H2]"` to turn it into:
H1 : Φ 0 y
H2 : [∗ list] k ↦ x ∈ l, Φ (S k) x
Although this is not particularly difficult to implement (it just requires one to declare suitable `IntoAnd` instances), it gives rise to some potential ambiguity, namely, what is going to happen when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ k x ∗ Ψ k x
Will it split through the cons, or through the star inside of the predicate in the big op?
Currently, it will split through the ∗ due to the instance `into_and_big_sepL`. Declaring yet another `IntoAnd` instance for the `cons` case is a bad idea, as it will give rise to the ambiguity above, and we end up with tactics that will behave unpredictably.
However, I think that the `cons` instance would be much more useful than the `∗` instance, hence I propose to drop the current `∗` instance, and instead declare instances for `cons` (and possibly `app`, which does not lead to ambiguity).https://gitlab.mpi-sws.org/iris/iris/-/issues/301`iExists` ignores `Opaque`2020-03-30T11:52:39ZPaolo G. Giarrusso`iExists` ignores `Opaque`Probably a WONTFIX, but this is new (presumably from !372), and Robbert asked for an example.
```coq
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import iprop.
Section foo.
Context `(Σ : gFunctors).
Defi...Probably a WONTFIX, but this is new (presumably from !372), and Robbert asked for an example.
```coq
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import iprop.
Section foo.
Context `(Σ : gFunctors).
Definition foo : iProp Σ := ∃ (x : nat), x ≡ 0.
End foo.
Opaque foo.
Lemma bar Σ : ⊢ foo Σ .
Proof.
by iExists 0. Restart.
iStartProof.
eapply coq_tactics.tac_exist.
Fail apply (class_instances_bi.from_exist_exist _).
(* The Hint Extern from !372: *)
notypeclasses refine (class_instances_bi.from_exist_exist _).
(* apply: (class_instances_bi.from_exist_exist _). (* Also works *) *)
by eexists 0.
Qed.
```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/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/537`iInduction ... forall (xs)` does not revert persistent hypotheses containing...2023-08-04T08:15:01ZRobbert Krebbers`iInduction ... forall (xs)` does not revert persistent hypotheses containing `xs````coq
From iris.algebra Require Export big_op.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Lemma big_sepL_impl' {PROP : bi} {A B} (l1 : list A) (l2 : list B) :
⊢@{PROP} □ (∀ k x2, ⌜l2 !! k = Some x2⌝ ...```coq
From iris.algebra Require Export big_op.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Lemma big_sepL_impl' {PROP : bi} {A B} (l1 : list A) (l2 : list B) :
⊢@{PROP} □ (∀ k x2, ⌜l2 !! k = Some x2⌝ -∗ True) -∗
True.
Proof. iIntros "#Himpl". iInduction l1 as [|x1 l1] "IH" forall (l2).
```
Example taken from https://gitlab.mpi-sws.org/iris/iris/-/issues/534https://gitlab.mpi-sws.org/iris/iris/-/issues/140`iIntoValid` failing in an unexpected way2019-12-03T12:34:58ZJacques-Henri Jourdan`iIntoValid` failing in an unexpected waySee e181f737.
I have no idea why these changes are needed to make the test pass. It seems like iIntoValid is failing in an unexpected way.See e181f737.
I have no idea why these changes are needed to make the test pass. It seems like iIntoValid is failing in an unexpected way.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/307`iIntros "%"` no longer works with universal quantification2020-04-07T15:39:37ZRalf Jungjung@mpi-sws.org`iIntros "%"` no longer works with universal quantificationThis test used to pass until yesterday, but got broken by !400:
```
Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_iIntros_forall_pure P :
⊢ ∀ x : nat, P.
Proof. iIntros "%". Abort.
```
Cc @robbertkrebber...This test used to pass until yesterday, but got broken by !400:
```
Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_iIntros_forall_pure P :
⊢ ∀ x : nat, P.
Proof. iIntros "%". Abort.
```
Cc @robbertkrebbers @tchajedhttps://gitlab.mpi-sws.org/iris/iris/-/issues/536`iIntros (?%lemma) "H"` fails if the lemma opens side-conditions2023-08-04T07:57:15ZRalf Jungjung@mpi-sws.org`iIntros (?%lemma) "H"` fails if the lemma opens side-conditionsTest case:
```
Lemma test_iIntros_subgoals (m : gmap nat nat) i x :
⊢@{PROP} ⌜kmap (M2 :=gmap nat) id m !! i = Some x⌝ → True → True.
Proof. iStartProof. iIntros (?%lookup_kmap_Some) "H".
```
If we fix this we should be able to revert...Test case:
```
Lemma test_iIntros_subgoals (m : gmap nat nat) i x :
⊢@{PROP} ⌜kmap (M2 :=gmap nat) id m !! i = Some x⌝ → True → True.
Proof. iStartProof. iIntros (?%lookup_kmap_Some) "H".
```
If we fix this we should be able to revert the hack from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/964.
As @robbertkrebbers says the fix is probably to put `first` in the right places, but the annoying thing is that `first` fails when there are 0 goals, and 0 goals is also a real possibility (when destructing `False`, for instance). We want to run our remaining tactics on "the first goal, but only if any goal exists" -- I don't know how to do that.
Also `_iIntros_go` has a `startproof` variable that is set to `false` in a bunch of random places without any comment that would explain why, so refactoring that code is very hard. I think we should be able to just do `iStartProof` once upfront instead of all of that mess, but that is blocked on https://gitlab.mpi-sws.org/iris/iris/-/issues/535, and even then maybe it breaks whatever logic that `startproof` variable is supposed to capture.https://gitlab.mpi-sws.org/iris/iris/-/issues/98`iIntros.` fails to introduce `True`2017-09-27T08:45:17ZRalf Jungjung@mpi-sws.org`iIntros.` fails to introduce `True````
Lemma push_atomic_spec (s: loc) (x: val) :
True -∗ (WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros "?".
```
shows an error:
```
Tactic failure: iIntro: nothing to introduce.
``````
Lemma push_atomic_spec (s: loc) (x: val) :
True -∗ (WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros "?".
```
shows an error:
```
Tactic failure: iIntro: nothing to introduce.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/97`iIntros.` should always enter proof mode2017-09-27T08:45:18ZRalf Jungjung@mpi-sws.org`iIntros.` should always enter proof mode```
Lemma test (s: loc) (x: val) :
(WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros.
(* Now I should be in proof mode, but I am not. *)
``````
Lemma test (s: loc) (x: val) :
(WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros.
(* Now I should be in proof mode, but I am not. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/268`iInv`: support tokens that are "framed" around the accessor2020-03-18T15:01:32ZDan Frumin`iInv`: support tokens that are "framed" around the accessorI have cancellable invariant and `cinv_own` token in a proposition "Hp", then usually I don't want to touch "Hp" when opening an invariant. However, if I use `iInv` I have to explicitly name "Hp" again:
```
iInv N with "Hp" as "[H Hp]" ...I have cancellable invariant and `cinv_own` token in a proposition "Hp", then usually I don't want to touch "Hp" when opening an invariant. However, if I use `iInv` I have to explicitly name "Hp" again:
```
iInv N with "Hp" as "[H Hp]" "Hcl"
```
This also prevents me from using the `(x1 x2) "..."` introduction pattern. E.g. instead of
```
iInv N with "Hp" as (x) "[H1 H2]" "Hcl"
```
one has to write
```
iInv N with "Hp" as "[H Hp]" "Hcl";
iDestruct "H" as (x) "[H1 H2]"
```
It is not immediately obvious how to modify the tactics, because in general the `selpat` in `iInv N with selpat` can be an arbitrary selection pattern and not just one identifier.https://gitlab.mpi-sws.org/iris/iris/-/issues/397`iRename` fails with bad error message when not in proof mode2021-02-17T08:48:22ZRobbert Krebbers`iRename` fails with bad error message when not in proof mode```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
wit...```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
with "True".
```
The tactic probably does not call `iStartProof` at the beginning.https://gitlab.mpi-sws.org/iris/iris/-/issues/225`is_closed_expr` is stronger than stability under `subst`2019-01-06T17:04:41ZDan Frumin`is_closed_expr` is stronger than stability under `subst`I think there is a discrepancy between the substitution and `is_closed_expr` for heap_lang
According to [subst](https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lang.v#L400),
`subst x v' (of_val v) = of_val v`.
How...I think there is a discrepancy between the substitution and `is_closed_expr` for heap_lang
According to [subst](https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lang.v#L400),
`subst x v' (of_val v) = of_val v`.
However, `is_closed_expr (of_val v) = is_closed_val v` (<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/metatheory.v#L22>) which is not always true.
That means, IIUC, that there are expressions that are not closed, but which are idempotent under the substitution.https://gitlab.mpi-sws.org/iris/iris/-/issues/547`IsOp` classes are poorly named, fulfill two functions, yet they will be used...2023-11-10T12:26:10ZIke Mulder`IsOp` classes are poorly named, fulfill two functions, yet they will be used differently after !930We noticed in !1004 that the `IsOp`, `IsOp'` and `IsOpLR` classes are somewhat problematic.
Firstly, their names are somewhat confusing (something like `IntoOp` is imo more descriptive of what `IsOpLR` does).
Secondly, `IsOp` is used b...We noticed in !1004 that the `IsOp`, `IsOp'` and `IsOpLR` classes are somewhat problematic.
Firstly, their names are somewhat confusing (something like `IntoOp` is imo more descriptive of what `IsOpLR` does).
Secondly, `IsOp` is used both for merging (`iCombine`ing owns) and splitting (`iSplit`/`iDestruct`ing owns) ops.
This usually saves some lines of code for clients, but complicates things in other cases.
This could be fixed, but these classes will also be used somewhat differently once !930 lands.
After !930, there will be an `IsValidOp` class responsible for `iCombine`ing.
The current proposal for !930 would still rely on `IsOp`---but only for some `cmra`s (those with trivial validity),
and only for `cmra`s that occur as 'leaves' in a term (so not for `cmra`s constructed with combinators).https://gitlab.mpi-sws.org/iris/iris/-/issues/551`iSpecialize` fails on `bi_forall` without eta expansion2024-02-16T16:30:51ZRobbert Krebbers`iSpecialize` fails on `bi_forall` without eta expansion```coq
From iris Require Import proofmode.tactics.
(* works --- with eta expansion *)
Lemma foo {PROP : bi} {A} (P : A → PROP) x :
bi_forall (λ x, P x) ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
done.
Qed.
(* fails -- wit...```coq
From iris Require Import proofmode.tactics.
(* works --- with eta expansion *)
Lemma foo {PROP : bi} {A} (P : A → PROP) x :
bi_forall (λ x, P x) ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
done.
Qed.
(* fails -- without eta expansion *)
Lemma bar {PROP : bi} {A} (P : A → PROP) x :
bi_forall P ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
(* Tactic failure: iSpecialize: cannot instantiate (∀ y, P y)%I with x. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/535`iStartProof` does not preserve names of quantified variables2023-08-04T07:57:15ZRalf Jungjung@mpi-sws.org`iStartProof` does not preserve names of quantified variables```
Lemma test_iStartProof_variable_names (Φ: nat → PROP) :
∀ y, Φ y -∗ ∃ x, Φ x.
Proof. iStartProof.
```
Now the goal is `∀ x : nat, Φ x -∗ ∃ x0 : nat, Φ x0`: `iStartProof` does not preserve the name `y` properly.```
Lemma test_iStartProof_variable_names (Φ: nat → PROP) :
∀ y, Φ y -∗ ∃ x, Φ x.
Proof. iStartProof.
```
Now the goal is `∀ x : nat, Φ x -∗ ∃ x0 : nat, Φ x0`: `iStartProof` does not preserve the name `y` properly.https://gitlab.mpi-sws.org/iris/iris/-/issues/299`leibnizO` finds convoluted proof for definitions2020-03-12T21:15:28ZRobbert Krebbers`leibnizO` finds convoluted proof for definitions```coq
Require Import iris.algebra.ofe.
Definition tag := nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. rewrite /tagO /natO /tag. reflexivity.
(* Why doesn't this hold? *)
``````coq
Require Import iris.algebra.ofe.
Definition tag := nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. rewrite /tagO /natO /tag. reflexivity.
(* Why doesn't this hold? *)
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/178`MIEnvIsEmpty` and `MIEnvTransform` have inconsistent behaviors2019-11-01T12:50:05ZJacques-Henri Jourdan`MIEnvIsEmpty` and `MIEnvTransform` have inconsistent behaviorsIn an affine logic, `MIEnvTransform` will clear the hypotheses that fail to be transformed, while `MIEnvIsEmpty` would fail if the environment is not empty. This is inconsistent.
The same remark applies to `MIEnvForall`.In an affine logic, `MIEnvTransform` will clear the hypotheses that fail to be transformed, while `MIEnvIsEmpty` would fail if the environment is not empty. This is inconsistent.
The same remark applies to `MIEnvForall`.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/102`solve_proper` having troubles proving non-expansiveness2017-10-10T11:50:17ZDan Frumin`solve_proper` having troubles proving non-expansivenessIn the snippet below`solve_proper` is not able to prove non-expansiveness of a higher-order predicate.
`solve_proper` is defined as `solve_proper_core ltac:(fun _ => f_equiv)`.
However, one can use `solve_proper_core ltac:(fun _ => simp...In the snippet below`solve_proper` is not able to prove non-expansiveness of a higher-order predicate.
`solve_proper` is defined as `solve_proper_core ltac:(fun _ => f_equiv)`.
However, one can use `solve_proper_core ltac:(fun _ => simpl; f_equiv)` to automatically discharge the obligations.
Is there a reason why this simplification is not happening in `solve_proper_core`?
Is it for the performance reasons?
```coq
From iris.heap_lang Require Import lang proofmode tactics notation.
Section linkedlist.
Context `{heapG Σ}.
Program Definition pre_isLinkedList : (valC -n> iProp Σ) -n> (valC -n> iProp Σ) :=
λne P v, (⌜v = InjLV #()⌝
∨ ∃ (h t : val) (l : loc),
⌜v = InjRV (PairV h #l)⌝
∗ l ↦ t
∗ ▷ (P t))%I.
Solve Obligations with solve_proper_core ltac:(fun _ => simpl; f_equiv).
End linkedlist.
```