Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-06-14T11:41:14Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/197iFrame sometimes needs to be called twice2018-06-14T11:41:14ZRalf Jungjung@mpi-sws.orgiFrame sometimes needs to be called twiceConsider the following proof (written in the context of `tests/proofmode_monpred.v`):
```
Program Definition monPred_id (R : monPred) : monPred :=
MonPred (λ V, R V) _.
Next Obligation. intros ? ???. eauto. Qed.
Lemma test_iFr...Consider the following proof (written in the context of `tests/proofmode_monpred.v`):
```
Program Definition monPred_id (R : monPred) : monPred :=
MonPred (λ V, R V) _.
Next Obligation. intros ? ???. eauto. Qed.
Lemma test_iFrame_monPred_id (P Q R : monPred) i :
(P i) ∗ (Q i) ∗ (R i) -∗ (P ∗ Q ∗ monPred_id R) i.
Proof.
iIntros "(? & ? & ?)". iFrame. iFrame.
Qed.
```
Notice that I need to call `iFrame` twice. That should not be necessary.
This lead to a bunch of additional rewrites being introduced when fixing the fallout from https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/154 because the `[$]` specialization pattern stopped working (it does `iFrame` just once, it seems).https://gitlab.mpi-sws.org/iris/iris/-/issues/195Always qualify Instance with Local or Global2021-01-07T13:58:38ZRalf Jungjung@mpi-sws.orgAlways qualify Instance with Local or GlobalSince you can't see whether you are inside a section, that's needed to even see whether this is a local or global instance.
The trouble is, we have 444 occurrences of unqualified `Instance`. Can we rely on all of them being `Global`? Fo...Since you can't see whether you are inside a section, that's needed to even see whether this is a local or global instance.
The trouble is, we have 444 occurrences of unqualified `Instance`. Can we rely on all of them being `Global`? For the same reason that we should always use qualifiers, `sed` cannot know whether we are inside a section.
I can do the `sed`, but I'm not sure how to do the review if any of these should be `Local`. Also, let's do this after merging some MRs because this will cause plenty of conflicts.https://gitlab.mpi-sws.org/iris/iris/-/issues/194coq-speed: Measure using performance counters2018-06-22T22:02:37ZRalf Jungjung@mpi-sws.orgcoq-speed: Measure using performance counters@janno suggested that instead/in addition to raw time, we could measure some performance counter statistics which should be less noisy.
@janno which counter did you suggest we measure, and how does one go about measuring that?@janno suggested that instead/in addition to raw time, we could measure some performance counter statistics which should be less noisy.
@janno which counter did you suggest we measure, and how does one go about measuring that?https://gitlab.mpi-sws.org/iris/iris/-/issues/193Remove or fix `base_logic/deprecated.v`2018-07-13T08:51:26ZRobbert KrebbersRemove or fix `base_logic/deprecated.v`It currently contains:
```
(*
FIXME
...
*)
```It currently contains:
```
(*
FIXME
...
*)
```Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/192Document `iRewrite -...` in `ProofMode.md`2019-01-11T10:13:31ZDan FruminDocument `iRewrite -...` in `ProofMode.md`I would like to be able to say something like `iRewrite <- "Heq"` so that it would transform the goal
```
"Heq": R ≡ Q
-------------*
Q
```
into
```
-------------*
R
```I would like to be able to say something like `iRewrite <- "Heq"` so that it would transform the goal
```
"Heq": R ≡ Q
-------------*
Q
```
into
```
-------------*
R
```https://gitlab.mpi-sws.org/iris/iris/-/issues/191Printing of the sequence operator `;;`2018-06-13T10:08:33ZMarianna RapoportPrinting of the sequence operator `;;`The [first](https://gitlab.mpi-sws.org/FP/iris-examples/blob/f9bee86a91025f7d727a1765a2d9ad98fbd10c9f/theories/lecture_notes/coq_intro_example_1.v) Coq example that comes with the Iris [lecture notes]() shows how to prove a lemma with th...The [first](https://gitlab.mpi-sws.org/FP/iris-examples/blob/f9bee86a91025f7d727a1765a2d9ad98fbd10c9f/theories/lecture_notes/coq_intro_example_1.v) Coq example that comes with the Iris [lecture notes]() shows how to prove a lemma with the following proof goal:
`{{{ ℓ ↦ #n }}} (incr ℓ) ||| (incr ℓ) ;; !#ℓ {{{m, RET #m; ⌜n ≤ m⌝ }}}`
However, in the interactive proof mode, the goal is displayed as
`{{{ ℓ ↦ #n }}} (Lam <> ! #ℓ) (incr ℓ ||| incr ℓ) {{{ (m : Z), RET #m; ⌜n ≤ m⌝}}}`
I.e. Coq automatically desugars the `;;` notation.https://gitlab.mpi-sws.org/iris/iris/-/issues/190Framing persistent hypotheses under a later in the goal2018-07-13T08:40:31ZHai DangFraming persistent hypotheses under a later in the goalI have
```
"H": P
-------------□
▷ P ∗ Q
```
`iFrame "H"` gives me back `▷ emp ∗ Q`. I was working with an affine BI.
@jtassaro suggests to generalize `make_sep_emp_l`.I have
```
"H": P
-------------□
▷ P ∗ Q
```
`iFrame "H"` gives me back `▷ emp ∗ Q`. I was working with an affine BI.
@jtassaro suggests to generalize `make_sep_emp_l`.https://gitlab.mpi-sws.org/iris/iris/-/issues/189Tests do not compile on MacOS2018-05-31T16:30:05ZLéon GondelmanTests do not compile on MacOSI've tried to compile iris 3bed085d035f199518707472be59d18e5bbf8342 on the branch gen_proofmode and the tests did not manage to compile.
```
COQC [test] tests/algebra.v
COQC [test] tests/heap_lang.v
COQC [test] tests/ipm_paper.v
COQC [...I've tried to compile iris 3bed085d035f199518707472be59d18e5bbf8342 on the branch gen_proofmode and the tests did not manage to compile.
```
COQC [test] tests/algebra.v
COQC [test] tests/heap_lang.v
COQC [test] tests/ipm_paper.v
COQC [test] tests/list_reverse.v
/bin/sh: tempfile: command not found
/bin/sh: tempfile: command not found
/bin/sh: tempfile: command not found
make[2]: *** [tests/heap_lang.vo] Error 127
make[2]: *** Waiting for unfinished jobs....
make[2]: *** [tests/ipm_paper.vo] Error 127
make[2]: *** [tests/algebra.vo] Error 127
/bin/sh: tempfile: command not found
make[2]: *** [tests/list_reverse.vo] Error 127
make[1]: *** [all] Error 2
make: *** [all] Error 2
```https://gitlab.mpi-sws.org/iris/iris/-/issues/188eauto very slow when there is a chain of Iris quantifiers2019-11-01T12:49:47ZRalf Jungjung@mpi-sws.orgeauto very slow when there is a chain of Iris quantifiersSteps to reproduce:
* Change the `iIntros` hints in `ltac_tactics.v` to `iIntros (?).` and `iIntros "?".`.
* Compile `ectx_lifting.v`
`wp_lift_atomic_head_step_no_fork` takes forever:
```
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e...Steps to reproduce:
* Change the `iIntros` hints in `ltac_tactics.v` to `iIntros (?).` and `iIntros "?".`.
* Compile `ectx_lifting.v`
`wp_lift_atomic_head_step_no_fork` takes forever:
```
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
to_val e1 = None →
(∀ σ1, state_interp σ1 ={E}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step. done.
(* now it gets slow *) eauto.
```
Something seems to be exponential in the number of quantifiers. We currently use `iIntros.` to introduce them all at once but that's more of a work-around. I can't even really figure out what is taking so long, but I can definitely see tons of `FromAssumption` in the trace.
Cc @robbertkrebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/187Support framing in `iCombine`.2018-07-13T08:40:31ZDan FruminSupport framing in `iCombine`.I wish that the `iCombine` tactic would support framing: `iCombine "H1 H2" as "$"`.I wish that the `iCombine` tactic would support framing: `iCombine "H1 H2" as "$"`.https://gitlab.mpi-sws.org/iris/iris/-/issues/186iAssert without any spatial assumptions should produce a persistent result2020-09-29T11:15:49ZRalf Jungjung@mpi-sws.orgiAssert without any spatial assumptions should produce a persistent resultThe following proof script should work:
```
Lemma test_persistent_assert `{!BiBUpd PROP} P :
□ P -∗ □ |==> P.
Proof.
iIntros "#HP".
iAssert (|==> P)%I as "#HPupd". (* FAIL! *)
{ iIntros "!> !> !>". done. }
iAssumption.
Qed.
```...The following proof script should work:
```
Lemma test_persistent_assert `{!BiBUpd PROP} P :
□ P -∗ □ |==> P.
Proof.
iIntros "#HP".
iAssert (|==> P)%I as "#HPupd". (* FAIL! *)
{ iIntros "!> !> !>". done. }
iAssumption.
Qed.
```
It currently fails because the update is not persistent -- however, this is an iAssert which is not provided any spatial assertions, so whatever it produces can always be put into the persistent context.https://gitlab.mpi-sws.org/iris/iris/-/issues/185"iApply ... with" unifies with assumptions before taking goal into account2019-11-01T13:45:51ZRalf Jungjung@mpi-sws.org"iApply ... with" unifies with assumptions before taking goal into accountThe following test case fails:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```
This is fairly an...The following test case fails:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```
This is fairly annoying when working with higher-order lemmas, for example it came up in the logically atomic context when trying to apply
```coq
Lemma astep_intro Eo Em α P β Φ x :
α x -∗
((α x ={Eo}=∗ P) ∧ (∀ y, β x y ={Eo}=∗ Φ x y)) -∗
atomic_step Eo Em α P β Φ.
```
where `α : A -> PROP`. Now `iApply (astep_intro with "foo")` fails to apply in most cases because it infers the wrong `α`.https://gitlab.mpi-sws.org/iris/iris/-/issues/184`wp_binop` is not very useful for comparing arbitrary values2018-05-03T13:06:04ZDan Frumin`wp_binop` is not very useful for comparing arbitrary valuesConsider the following piece of code:
```
From iris.heap_lang Require Export proofmode notation.
Lemma wut `{heapG Σ} (v1 v2 : val) :
(WP if: (v1 = v2) then #0 else #0 {{ _, True }})%I.
Proof.
wp_binop.
Abort.
```
The goal that I ...Consider the following piece of code:
```
From iris.heap_lang Require Export proofmode notation.
Lemma wut `{heapG Σ} (v1 v2 : val) :
(WP if: (v1 = v2) then #0 else #0 {{ _, True }})%I.
Proof.
wp_binop.
Abort.
```
The goal that I expected after executing `wp_binop`:
```
WP if: #(bool_decide (v1 = v2)) then #0 else #0 {{ _, True }}
```
Instead I got two goals:
- `bin_op_eval EqOp v1 v2 = Some ?Goal0`
- `WP if: ?Goal0 then #0 else #0 {{ _, True }}`
This is not very helpful, as it is pretty annoying to get a boolean value for ?Goal0.
I believe this is due to the way that `bin_op_eval` is defined:
it first matches `v1` and `v2` for specific types of values (integers or booleans), and only then considers the case of generalized equality checks.
Since we have generalized/dynamic equality checks in heap_lang, why not first match on the type of the operation, and only then match on the values in `bin_op_eval`?
Best
-Danhttps://gitlab.mpi-sws.org/iris/iris/-/issues/183Stronger/Weaker iFrame2022-05-06T12:54:55ZRalf Jungjung@mpi-sws.orgStronger/Weaker iFrameIn a situation like
```
H1: R
H2: P
----------------------*
R * (P /\ Q)
```
calling `iFrame` will turn the goal into
```
----------------------*
Q
```
This is too aggressive: Frequently, I will need `P` to prove `Q`.In a situation like
```
H1: R
H2: P
----------------------*
R * (P /\ Q)
```
calling `iFrame` will turn the goal into
```
----------------------*
Q
```
This is too aggressive: Frequently, I will need `P` to prove `Q`.https://gitlab.mpi-sws.org/iris/iris/-/issues/182done when goal is evar picks unnecessarily strong2018-07-13T08:40:31ZRalf Jungjung@mpi-sws.orgdone when goal is evar picks unnecessarily strongWhen the goal is an evar (and that evar does not appear otherwise in the current goal), like in
```
_ : inv nroot (∃ x' : Z, l ↦ #x')%I
--------------------------------------□
?P
```
then doing `done` will pick a persistent (or spa...When the goal is an evar (and that evar does not appear otherwise in the current goal), like in
```
_ : inv nroot (∃ x' : Z, l ↦ #x')%I
--------------------------------------□
?P
```
then doing `done` will pick a persistent (or spatial, I guess) hypothesis instead of just `True` or `emp`.
Maybe we should add `bi.True_intro` with high priority to the database?https://gitlab.mpi-sws.org/iris/iris/-/issues/181wp_apply instantiates evars too far2018-07-13T08:51:26ZRalf Jungjung@mpi-sws.orgwp_apply instantiates evars too far```coq
Lemma wp_apply_evar e :
(∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof.
iIntros "H". wp_apply "H".
```
The goal is now
```
============================
--------------------------------------∗
WP ?e @ ?s;...```coq
Lemma wp_apply_evar e :
(∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof.
iIntros "H". wp_apply "H".
```
The goal is now
```
============================
--------------------------------------∗
WP ?e @ ?s; ?E {{ v, ?Φ v }}
```
but it should be
```
============================
--------------------------------------∗
?Q
```
This is in the generalized proofmode branch.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/180Explore performance implications of gen_proofmode2019-11-01T12:49:47ZRalf Jungjung@mpi-sws.orgExplore performance implications of gen_proofmodea74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search) made lambdaRust noticeably slower.
Also see the conversation following <https://mattermost.mpi-sws.org/iris/pl/btp695ny3prqjdqzojw9sj5i9w>. In particular:
> y...a74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search) made lambdaRust noticeably slower.
Also see the conversation following <https://mattermost.mpi-sws.org/iris/pl/btp695ny3prqjdqzojw9sj5i9w>. In particular:
> yeah, the bottelneck is definitely notypeclasses refine: https://gitlab.mpi-sws.org/FP/LambdaRust-coq/-/jobs/9346 took 29:47 user time
> btw we also have a 1min regression in this range: https://gitlab.mpi-sws.org/FP/LambdaRust-coq/compare/8799209d9c00f825e9ac059b3b864119e34f9aec...00b0c7704278028c4a73c9f0686a9070e92d3a06
> and ~30sec over https://gitlab.mpi-sws.org/FP/LambdaRust-coq/compare/474f82283e423b03ccf0adeb367e36eb68346a29...8799209d9c00f825e9ac059b3b864119e34f9aec
Looking at the [performance graph](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-project=lambda-rust&var-branch=ci%2Fgen_proofmode&var-config=All&from=1516679125714&to=now), the two commit ranges with the most sustained impact are LambdaRust-coq@c2c2b874eea8...00b0c7704278 and LambdaRust-coq@00b0c7704278...158d46797c99. They correspond to iris-coq@aa5b93f6319b9cb2d17a1c9f61947233b4033484...1a092f96b1350896c3801edb90b453f5b4d2a4cf and iris-coq@1a092f96b1350896c3801edb90b453f5b4d2a4cf...a74b8077f199e2d21ff49e91b5af0dfdcee362ff in Iris. The latter is just a74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search), but the former is just a whole bunch of commits that, altogether, seem to have made things slower by 40sec in LambdaRust.
There is also some variation in [this part of the graph](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-project=lambda-rust&var-branch=ci%2Fgen_proofmode&var-config=All&from=1518563995005&to=1520160053680) but I am not sure if that's real or just noise.https://gitlab.mpi-sws.org/iris/iris/-/issues/179Strengthen strong allocation lemmas to work for any infinite set2019-02-17T18:14:30ZRalf Jungjung@mpi-sws.orgStrengthen strong allocation lemmas to work for any infinite setNow that std++ has https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/blob/master/theories/infinite.v, we should be able to provide stronger versions of `own_alloc_strong` and similar lemmas.Now that std++ has https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/blob/master/theories/infinite.v, we should be able to provide stronger versions of `own_alloc_strong` and similar lemmas.https://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/177Improve naming of lemmas about modalities2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgImprove naming of lemmas about modalitiesThe following discussion from !130 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/130#note_26050): (+7 comments)
We agreed on the following scheme
```
M1_M2: M1...The following discussion from !130 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/130#note_26050): (+7 comments)
We agreed on the following scheme
```
M1_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2_{swap,comm}: M1 (M2 P) ⊣⊢ M2 (M1 P)
```
However, @robbertkrebbers noted that we have plenty of lemmas of the last form. Optimizing for conciseness, we could also use
```
M1_{into,impl,entails}_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
```Generalized Proofmode Merger