Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-07-13T08:51:27Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/200Framing: Make* classes lead to suboptimal results2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgFraming: Make* classes lead to suboptimal resultsFraming uses `Make*` classes to turn terms into a certain form, e.g. a leading `▷^n`. However, those classes require the original term to be *equivalent* with the converted one. This leads to situations such as
```
Lemma test_iFrame_la...Framing uses `Make*` classes to turn terms into a certain form, e.g. a leading `▷^n`. However, those classes require the original term to be *equivalent* with the converted one. This leads to situations such as
```
Lemma test_iFrame_later_rel (P : PROP) :
▷ P -∗ (▷ (P ∧ P)).
Proof. iIntros "?". iFrame.
(* Now the goal is [▷ emp] *)
```
I would expect the goal to become `emp` (and hence `iFrame` closing the goal), and indeed that would be sound (`emp` implies `▷ emp`) but it doesn't happen.https://gitlab.mpi-sws.org/iris/iris/-/issues/199iSplitL no longer checks if assumptions are spatial2018-06-10T20:13:10ZRalf Jungjung@mpi-sws.orgiSplitL no longer checks if assumptions are spatialThe following used to fail with an error saying that `"HP"` is not a spatial assumption, now it just succeeds but still puts `"HP"` on both sides:
```
Lemma iSplit_intuitionistic P :
□ P -∗ P ∗ P.
Proof. iIntros "#HP". iSplitL "HP".
```The following used to fail with an error saying that `"HP"` is not a spatial assumption, now it just succeeds but still puts `"HP"` on both sides:
```
Lemma iSplit_intuitionistic P :
□ P -∗ P ∗ P.
Proof. iIntros "#HP". iSplitL "HP".
```https://gitlab.mpi-sws.org/iris/iris/-/issues/198iAlways fails without a proper error message2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgiAlways fails without a proper error messageThe following script
```
Lemma test_iAlways_emp : emp ⊢@{PROP} □ emp.
Proof.
iIntros "H". iAlways. done.
Qed.
```
Fails at `iAlways` saying
```
Error:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last ca...The following script
```
Lemma test_iAlways_emp : emp ⊢@{PROP} □ emp.
Proof.
iIntros "H". iAlways. done.
Qed.
```
Fails at `iAlways` saying
```
Error:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last call failed.
No matching clauses for match.
```
It should either give a proper error or empty the spatial context.https://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/196Extend `iApply` to deal with pure goals2019-11-01T12:50:03ZGlen MévelExtend `iApply` to deal with pure goalsIf I have a pure Coq lemma `A → B`, I would like to be able to use it in the proof-mode to prove an Iris goal `⌜B⌝` (under an Iris context). Currently `iApply` does not support this. Here is an example.
```coq
Lemma test {Σ} (A B : Pr...If I have a pure Coq lemma `A → B`, I would like to be able to use it in the proof-mode to prove an Iris goal `⌜B⌝` (under an Iris context). Currently `iApply` does not support this. Here is an example.
```coq
Lemma test {Σ} (A B : Prop) (P : iProp Σ) :
(A → B) → (P -∗ ⌜A⌝) → (P -∗ ⌜B⌝).
Proof.
iIntros (ab pa) "p".
(* what I would like to write directly: *)
Fail iApply ab. (* Tactic failure: iPoseProof: not a uPred. *)
(* what I need to write instead: *)
iApply (uPred.pure_mono _ _ ab).
iApply pa.
iExact "p".
Qed.
```
(tested with coq-iris dev.2018-04-10.0)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 Gondelman Tests 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 iFrame2021-02-03T22:31:23ZRalf 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 Krebbers