Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-07-13T08:40:31Zhttps://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/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/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/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/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 Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/176Reconsider normalizing `/\ emp` into `<affine>`2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgReconsider normalizing `/\ emp` into `<affine>`I was rather surprised when running `iFrame` added an `<affine>` modality in front of a goal. @robbertkrebbers explained:
> To understand what's happening, first note that when you frame something in a general BI, it will turn it into `...I was rather surprised when running `iFrame` added an `<affine>` modality in front of a goal. @robbertkrebbers explained:
> To understand what's happening, first note that when you frame something in a general BI, it will turn it into `emp`, not `True`. So, framing let's say `P` in `P ∗ Q` turns it into `emp ∗ Q`, which then get beautified into `Q`.
> In this case, you are framing `P` in `<pers> Q ∧ P`, which will turn it into `<pers> Q ∧ emp`. This is then beautified into `<affine> <pers> Q`
I think we should not perform this normalization, and just keep it as `<pers> Q /\ emp`.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/174Confusing result by `wp_op`2018-04-22T18:08:36ZRobbert KrebbersConfusing result by `wp_op`As reported in private by @birkedal:
```coq
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition test `{heapG Σ} (n : nat) (v : val) :
(W...As reported in private by @birkedal:
```coq
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition test `{heapG Σ} (n : nat) (v : val) :
(WP if: #n = v then #true else #false {{ _, True }})%I.
Proof.
wp_op.
```
This gives
```coq
bin_op_eval EqOp #n v = Some ?Goal0
______________________________________(2/2)
--------------------------------------∗
WP if: ?Goal0 then #true else #false {{ _, True }}
```
Pre !97 this used to work because `bin_op_eval` used to match first on the operations and then on the operand. Right now, it first matches on the operands, and only then on the operation.https://gitlab.mpi-sws.org/iris/iris/-/issues/173Ambiguous reference to eqb in coq_tactics.v2018-03-12T13:17:31ZGhost UserAmbiguous reference to eqb in coq_tactics.vWhile preparing [Coq PR #6948](https://github.com/coq/coq/pull/6948), we noticed a little issue with `Bool.eqb` in your development. Indeed, after this PR introducing `Ascii.eqb` and `String.eqb` in the standard library, your file `theor...While preparing [Coq PR #6948](https://github.com/coq/coq/pull/6948), we noticed a little issue with `Bool.eqb` in your development. Indeed, after this PR introducing `Ascii.eqb` and `String.eqb` in the standard library, your file `theories/proofmode/coq_tactics.v` fails to compile due to 2 unqualified references to `eqb` not been seen as `Bool.eqb` anymore.
This issue can be fixed in a straightforward (and backward-compatible) way : replace the two occurrence of `eqb` in this file (lines 95 and 288) by `Bool.eqb` (or alternatively, add an `Import Bool` at the end of this file's header).
Sorry for not proposing a pull request directly, but apparently I do not have enough permission to fork on your gitlab.
For this fix to be correctly taken in account by our travis testing infrastructure, could you please update the `opam` file of repository `LambdaRust-coq.git` to mention a fixed version of `iris-coq` ? Currently it points to `iris-coq` version `dev.2018-02-23.0`, leading to commit `db735a4558ad`.
Thanks!
Pierre Letouzeyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/171Split derived_laws.v2018-03-21T15:05:46ZRalf Jungjung@mpi-sws.orgSplit derived_laws.v`derived_laws.v` is a very-hard-to-navigate monster. Can we find a good way to split it?
One fairly obvious thing to do is to split the `Sbi` stuff into a separate file. Then the `Bi` file will still be huge, probably... what could be a...`derived_laws.v` is a very-hard-to-navigate monster. Can we find a good way to split it?
One fairly obvious thing to do is to split the `Sbi` stuff into a separate file. Then the `Bi` file will still be huge, probably... what could be a good criterion to separate that?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/170iFresh should reserve fresh names2018-07-13T08:51:26ZJoseph TassarottiiFresh should reserve fresh namesRight now `iFresh` just generates a name that is fresh with respect to the current context, but doesn't ensure that the generated name will not be returned again by subsequent calls to `iFresh`. As a result, the following pattern fails:
...Right now `iFresh` just generates a name that is fresh with respect to the current context, but doesn't ensure that the generated name will not be returned again by subsequent calls to `iFresh`. As a result, the following pattern fails:
```
let H1 := iFresh in
let H2 := eval vm_compute in (match H1 with
| IAnon x => IAnon (1 + x)
| INamed x => IAnon 1
end) in
let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
iDestruct "H" as pat.
```
because `iDestruct` will also use `iFresh` and gets a name that conflicts with `H1`.
One solution would be to add a counter to the `envs` record which is incremented each time `iFresh` is called. This would actually also probably make `iFresh` more efficient anyway.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/164Take a closer look at the interaction of fancy updates and plainly2018-10-31T14:44:29ZRalf Jungjung@mpi-sws.orgTake a closer look at the interaction of fancy updates and plainlyCurrently we have these two laws:
```
fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
E1 ⊆ E2 →
(Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
later_fupd_plain E (P : PROP) `{!Plain P} :
(▷ |={E}=> ...Currently we have these two laws:
```
fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
E1 ⊆ E2 →
(Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
later_fupd_plain E (P : PROP) `{!Plain P} :
(▷ |={E}=> P) ={E}=∗ ▷ ◇ P;
```
First, I find it surprising that we need two laws. Second, the first law looks really unwieldy.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/162Have `iFrame` smartly instantiate existentials2018-03-03T19:06:32ZJacques-Henri JourdanHave `iFrame` smartly instantiate existentialsIn the case the goal is e.g., of the form `P * ?Q`, where `?Q` is an existential, and we want to frame some assertion `R` that does not appear, we may want to instantiate `?Q` with `R * ?Q'`. Therefore, the meta-variable serves as a "buf...In the case the goal is e.g., of the form `P * ?Q`, where `?Q` is an existential, and we want to frame some assertion `R` that does not appear, we may want to instantiate `?Q` with `R * ?Q'`. Therefore, the meta-variable serves as a "buffer" where we put everything which we frame and fail to put anywhere else.
This is usefull in CFML, so I think I will implement this anyway in CFML. The reason it is usefull is that the typical CFML workflow implies working with an evar as a post-condition, which is instantiated by whatever is remaining.
Would you think this might be worth having in the general IPM?https://gitlab.mpi-sws.org/iris/iris/-/issues/161Use `plainly_alt` as an axiom and replace most of the current ones2020-03-18T15:08:43ZJacques-Henri JourdanUse `plainly_alt` as an axiom and replace most of the current onesIn the interface for plainly, we could have `plainly_alt` as an axiom. Here are the reasons this is not a completely absurd idea:
1- Most of the axioms can be removed. Namely, the only ones remaining are:
* `bi_persistently_impl_plainly...In the interface for plainly, we could have `plainly_alt` as an axiom. Here are the reasons this is not a completely absurd idea:
1- Most of the axioms can be removed. Namely, the only ones remaining are:
* `bi_persistently_impl_plainly`, `bi_plainly_impl_plainly` (which I find kind of arbitrary anyway),
* `sbi_mixin_prop_ext` (which is actually one of the few current axioms of `plainly` that actually /says/ something about the BI. So this is expected that it stays.
* The axioms about the updates, but I would say these are rather about the update than about `bi_plainly`
* `sbi_mixin_later_plainly_2`, which somehow I am not able to prove. But perhaps I am missing something.
Note that for some of these axioms (except `bi_plainly_impl_plainly`, `sbi_mixin_prop_ext` and the update axioms), we could
replace "for all plain assertion P" by "for all equality", which make them understandable even without understanding what is plainly.
2- I would say the definition of `plainly_alt` is quite intuitive. Indeed, `P /\ emp = emp` is a way of internally saying `emp |- P`, which exactly means that `P` is valid. So this definition can directly be interpreted as the "internal validity".https://gitlab.mpi-sws.org/iris/iris/-/issues/160Figure out the best place for the plainly modality2018-03-03T16:56:51ZRalf Jungjung@mpi-sws.orgFigure out the best place for the plainly modalityRight now, `plainly` is part of the BI interface, so *every* logic has to have this modality. Given that this modality is not at all needed for the proof mode to function, I think that's a bad choice. We already have some rather arbitra...Right now, `plainly` is part of the BI interface, so *every* logic has to have this modality. Given that this modality is not at all needed for the proof mode to function, I think that's a bad choice. We already have some rather arbitrary-looking axioms for `bi_persistently`; let's try to minimize the amount of "strange modalities" in the interface(s) as much as possible.
The following proposals are on the table:
1. Follow !98 and treat `plainly` like `fupd` and `bupd`: As "standardized extensions" that come with their own separate interface, but once instantiated with proofs of the basic laws are automatically integrated into the proofmode (because a bunch of instances based on this interface already exist).
1. Put `plainly` into `Sbi`.
1. Have a new "IrisLikeLogic", extending `Sbi`, which contains `plainly` as well as the update modalities.
My own comments:
1. This is the most general and, absent technical concerns, "best" solution -- but handling the resulting hierarchie(s) could become annoying. We'd also have to decide which approach to use for these (bundled/unbundled, typeclasses/canonical structures). (I somehow thought @robbertkrebbers was able to solve all hierarchy problems in Coq as that's what you did so far; hearing even you say that this is getting too complicated is quite unsettling to be honest ;)
1. I see no motivation for doing this, it seems rather arbitrary.
1. seems okay to me -- a little sad, but given the state of affairs probably a reasonable compromise for the time being. We have no example of a logic that would benefit from `plainly` that doesn't also have the updates.
Ideally I'd prefer 1., but given that if @robbertkrebbers can't get the hierarchy to work, neither will I -- that makes 3. look appealing enough. ;) I don't like 2. at all.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/159Find better name for "emp |- P"2018-07-13T08:51:26ZRalf Jungjung@mpi-sws.orgFind better name for "emp |- P"Currently, `emp |- P` is called `bi_valid P` and is used as a coercion from `PROP` to `Prop`. This turns out to be the right definition for the coercion (i.e., `(l |-> v -* l |->{0.5} v * l |->{0.5} v)%I` is provable), but the name is d...Currently, `emp |- P` is called `bi_valid P` and is used as a coercion from `PROP` to `Prop`. This turns out to be the right definition for the coercion (i.e., `(l |-> v -* l |->{0.5} v * l |->{0.5} v)%I` is provable), but the name is dubious: Usually, validity is defined as `True |- P`. Let's try to find a better name.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/158Make clear which arguments of tactics are optional in `ProofMode.md`2020-12-19T17:43:20ZRobbert KrebbersMake clear which arguments of tactics are optional in `ProofMode.md`See the discussion in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/116#note_25050See the discussion in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/116#note_25050https://gitlab.mpi-sws.org/iris/iris/-/issues/157`done` loops in proofmode2018-03-07T18:16:58ZRobbert Krebbers`done` loops in proofmode```coq
Lemma test : ∃ R, R ⊢ ∀ P, P.
Proof. eexists. iIntros "?" (P). done.
``````coq
Lemma test : ∃ R, R ⊢ ∀ P, P.
Proof. eexists. iIntros "?" (P). done.
```Generalized Proofmode MergerRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/156How to deal with `emp`, `True`, and friends when the BI is ambigious2018-07-13T08:40:32ZRobbert KrebbersHow to deal with `emp`, `True`, and friends when the BI is ambigiousThe following discussion from !115 should be addressed:
We often write `emp : PROP`. However, since coercions are explicit term constructors in Coq, this apparently leads to unification problems here and there.
The alternative is to wr...The following discussion from !115 should be addressed:
We often write `emp : PROP`. However, since coercions are explicit term constructors in Coq, this apparently leads to unification problems here and there.
The alternative is to write `bi_emp (PROP:=PROP)`, which is ugly.
Maybe we should have special notations to force the type arguments of `emp`, `True`, and friends.
I think ssr is also doing something like that. Depending on the outcome of this issue, we should not just address the occurrence in !115, but also fix other occurrences.Generalized Proofmode Merger