Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2017-05-19T15:20:29Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/72Support `iCombine "H1 H2 ..." as "Hx"`2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgSupport `iCombine "H1 H2 ..." as "Hx"`It'd be nice if `iCombine` supported passing a single string of space-separated hypothesis instead of insisting on two strings, each being a single name. Combining more than two hypothesis would be done by folding.It'd be nice if `iCombine` supported passing a single string of space-separated hypothesis instead of insisting on two strings, each being a single name. Combining more than two hypothesis would be done by folding.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/71Framing in Disjunctions2019-11-01T13:20:31ZJannoFraming in Disjunctions@haidang and I used to have two Instances for Frame that would let us frame out things from only one side of a disjunction. We currently do not have that instance anymore – apparently, it got lost somehow – but we miss it. I do realize t...@haidang and I used to have two Instances for Frame that would let us frame out things from only one side of a disjunction. We currently do not have that instance anymore – apparently, it got lost somehow – but we miss it. I do realize that such an instance potentially leads to unsolvable goals more often than any of the existing framing instances. So this should probably not be the default behavior of `iFrame`. Nonetheless, the functionality was extremely convenient in some places. Often, disjunctive goals could easily be closed by framing out a bunch of resources and closing the goal with a `by` prefix or a separate `done`. No `iLeft` or `iRight` was needed.
I wonder if Iris could still benefit from such rules by adding a marker in the syntax for `iFrame`, e.g. `iFrame "!H"`, which applies the more reckless disjunction framing rules. The same could be applied for specialization patterns with something like `$!H`.
What do you think?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/70`wp_apply` cannot deal with curried lemmas2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.org`wp_apply` cannot deal with curried lemmasThe `wp_apply` tactic was written in a time when all our lemmas were uncurried. It always distributes all the resources of the current context to one of the goals that it creates, not leaving any control to the user. I think we need some...The `wp_apply` tactic was written in a time when all our lemmas were uncurried. It always distributes all the resources of the current context to one of the goals that it creates, not leaving any control to the user. I think we need something like `wp_apply with "<spec pattern>"` to accommodate curried lemmas.
See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/6d36b8cfbe2e7dbeda13889b17ef4b168d6953cf/theories/lang/spawn.v#L77> and <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/6d36b8cfbe2e7dbeda13889b17ef4b168d6953cf/theories/typing/unsafe/cell.v#L165> for some examples.https://gitlab.mpi-sws.org/iris/iris/-/issues/69Make `done` solve the goal when one of the Iris hypothesis is `False`2017-05-19T15:20:29ZJacques-Henri JourdanMake `done` solve the goal when one of the Iris hypothesis is `False`As in Coq, this should work even if the hypothesis is not syntacticaly `False`, but only convertible to it.As in Coq, this should work even if the hypothesis is not syntacticaly `False`, but only convertible to it.https://gitlab.mpi-sws.org/iris/iris/-/issues/68iSpecialize should work even if the wand is under a later.2017-05-19T15:20:29ZJacques-Henri JourdaniSpecialize should work even if the wand is under a later.In the proofmode, if I have, say, the hypothesis `"H1" : ▷ (A -* B)`, then `iSpecialize ("H1" with "[]")` does not work. Is there any good reason for this ?In the proofmode, if I have, say, the hypothesis `"H1" : ▷ (A -* B)`, then `iSpecialize ("H1" with "[]")` does not work. Is there any good reason for this ?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/67iAssert does not support destructing existentials2017-05-19T15:20:29ZJacques-Henri JourdaniAssert does not support destructing existentialsIt seems like I cannot use something like:
```
iAssert (∃ a, P a) with "[]" as (a) "H".
```It seems like I cannot use something like:
```
iAssert (∃ a, P a) with "[]" as (a) "H".
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/66Use a "settings" file for setting options within the project2020-09-10T17:37:08ZRalf Jungjung@mpi-sws.orgUse a "settings" file for setting options within the projectFollowing a suggestion of PMP, we should add a file setting our options (Default Proof Using, Bullet Mode, ...) and import this everywhere. That makes it much easier to change such options in the future.
I think the only point left to d...Following a suggestion of PMP, we should add a file setting our options (Default Proof Using, Bullet Mode, ...) and import this everywhere. That makes it much easier to change such options in the future.
I think the only point left to discuss is the name of that file... I suggest putting it into the root, i.e. sth. like `theories/options.v`.https://gitlab.mpi-sws.org/iris/iris/-/issues/65Wish: Prelude support for currying (and other operations) on gmap.2017-05-19T15:20:29ZJannoWish: Prelude support for currying (and other operations) on gmap.The following operations would (or could) be quite useful in my planned clean-up of iGPS:
1. Converting `gmap A (gmap B C)` to `gmap (A* B) (C)` and vice versa.
1. Converting `gmap A B` to `gmap A (A * B)` by copying the argument.
1. C...The following operations would (or could) be quite useful in my planned clean-up of iGPS:
1. Converting `gmap A (gmap B C)` to `gmap (A* B) (C)` and vice versa.
1. Converting `gmap A B` to `gmap A (A * B)` by copying the argument.
1. Converting `gmap A B` as a `gset (A * B)` (possibly by simply adding a ElemOf instance and corresponding lemma).
As Robbert already mentioned to me, these things probably should be generalized. I think there is a general map-filter function lurking in there somewhere. One that gives access to both the key and the value and returns and optional results which is used for the new gmap. I might be wrong though.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/64Destruct patterns: Support -> and <- (at least) for pure Coq equalities, and ...2017-10-27T13:17:57ZRalf Jungjung@mpi-sws.orgDestruct patterns: Support -> and <- (at least) for pure Coq equalities, and maybe injection patternsIn lambdaRust, we sometimes write something like `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %->`. It would be nice if we could write `iDestruct "H" as "[? ->]"`.
As a bonus: We also even more often write `iDestruct "H" as "[? EQ]"; i...In lambdaRust, we sometimes write something like `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %->`. It would be nice if we could write `iDestruct "H" as "[? ->]"`.
As a bonus: We also even more often write `iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %[= ->]`, i.e., there is an additional injection applied. Any way we could also get that in the proof mode? Maybe even using the "injective" typeclass so that it doesn't have to be the constructor of an inductive type (however, of course it'd also have to support all constructors, so it can't rely just on that typeclass).Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/63gmultiset.gmultiset_eq_dec applied too eagerly?2017-05-19T15:20:29ZJannogmultiset.gmultiset_eq_dec applied too eagerly?I don't have time to debug this in more detail so I am just going to dump a representative trace here. Without exception, all my diverging type class searches (of which I have a few per hour) eventually look like this one:
[trace.txt](/...I don't have time to debug this in more detail so I am just going to dump a representative trace here. Without exception, all my diverging type class searches (of which I have a few per hour) eventually look like this one:
[trace.txt](/uploads/1fad04b1b2cb32d92e41f976f8853f1f/trace.txt)
(Just in case somebody actually looks at it: the piece of code you can see in line 1 doesn't actually make any sense, I think.)https://gitlab.mpi-sws.org/iris/iris/-/issues/62Specialization (iApply/iMod) often diverges on missing *2017-11-16T09:36:42ZRalf Jungjung@mpi-sws.orgSpecialization (iApply/iMod) often diverges on missing *When specializing a lemma that contains Iris-level universal quantifiers, if I forget to add the `*` to the pattern, the tactic frequently diverges. This is very frustrating as it is not even clear what's wrong, or where the `*` has to b...When specializing a lemma that contains Iris-level universal quantifiers, if I forget to add the `*` to the pattern, the tactic frequently diverges. This is very frustrating as it is not even clear what's wrong, or where the `*` has to be added.
If you want, I can create a minimal example. Right now, one way to see this is to remove the `*` from the `iMod` in `weakestpre.wp_atomic`, line 172.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/61iLöb doesn't work in the empty context.2017-05-19T15:20:29ZJannoiLöb doesn't work in the empty context.As witnessed by the following example.
```
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Se...As witnessed by the following example.
```
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*".
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
Proof.
Fail (iLöb as "IH" forall (e Closed0)).
iAssert (True)%I as "T"; [by admit|].
(iLöb as "IH" forall (e Closed0)).
Abort.
```
I guess with the new unified handling of reverting hypotheses this probably applies to other tactics as well.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/60Consider the destruct pattern "_" as being persistent2017-01-01T19:10:30ZJacques-Henri JourdanConsider the destruct pattern "_" as being persistentIf I do:
```
iDestruct ("A" with "B") as "[#X #Y]".
```
Then "B" is not consumed because the destruct pattern only produce persistent hypotheses. So far so good.
But if I do:
```
iDestruct ("A" with "B") as "[#X _]".
```
That's not th...If I do:
```
iDestruct ("A" with "B") as "[#X #Y]".
```
Then "B" is not consumed because the destruct pattern only produce persistent hypotheses. So far so good.
But if I do:
```
iDestruct ("A" with "B") as "[#X _]".
```
That's not the case.https://gitlab.mpi-sws.org/iris/iris/-/issues/59Stronger Invariant Allocation Rules2017-01-11T09:49:16ZJannoStronger Invariant Allocation RulesAllocating Iris invariants currently combines allocating and closing the invariant. I see no reason to do that other than it being somewhat convenient for 80% of the use cases. Here's a stronger invariant allocation rule that we need for...Allocating Iris invariants currently combines allocating and closing the invariant. I see no reason to do that other than it being somewhat convenient for 80% of the use cases. Here's a stronger invariant allocation rule that we need for our GPS work. This is not (yet) a pull request for - just a copy of my local file. But I wanted to dump this here so that you guys can discuss if you want it in Iris.
```
From iris.base_logic.lib Require Export own wsat.
From iris.prelude Require Export coPset.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export fancy_updates namespaces.
From iris.base_logic.lib Require Import wsat invariants.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics coq_tactics intro_patterns.
Section wsat.
Import invG.
Context `{invG Σ}.
Implicit Types P : iProp Σ.
Lemma ownI_alloc_strong φ P :
(∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
wsat ==∗ ∃ i, ⌜φ i⌝ ∗ (ownE {[i]} -∗ wsat) ∗ ownI i P ∗ ownD {[i]}.
Proof.
iIntros (Hfresh) "Hw". iDestruct "Hw" as (I) "[? HI]".
iMod (own_empty (gset_disjUR positive) disabled_name) as "HD".
iMod (own_updateP with "HD") as "HD".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
intros E. destruct (Hfresh (E ∪ dom _ I))
as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
iMod (own_update with "Hw") as "[Hw HiP]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ i (invariant_unfold P)); last done.
by rewrite /= lookup_fmap HIi. }
iModIntro; iExists i; iSplit; [done|]. rewrite /ownI; iFrame "HiP".
rewrite -/(ownD _). iFrame "HD".
iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
{ by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
iApply (big_sepM_insert _ I); first done.
iFrame "HI". by iRight.
Qed.
End wsat.
Section invariants.
Import uPred.
Context `{invG Σ}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Σ.
Lemma ownE_proper : Proper ((≡) ==> (≡)) ownE.
Proof.
rewrite /ownE => ? ? Eq. f_equiv. f_equiv. by apply leibniz_equiv.
Qed.
Lemma inv_alloc_strong N E P : ↑N ⊆ E → True ={E, E∖↑N}=∗ inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def.
iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_strong (∈ ↑ N) P with "Hw") as (i) "(% & Hw & #Hi & HD)".
- intros Ef. exists (coPpick (↑ N ∖ coPset.of_gset Ef)).
rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
apply coPpick_elem_of=> Hfin.
eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
apply of_gset_finite.
- iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I with "[HE]" as "(HEi & HEN\i & HE\N)".
{ rewrite -?ownE_op; [|set_solver|set_solver]. rewrite ownE_proper; [done|].
rewrite assoc. rewrite <-!union_difference; set_solver. }
iModIntro. rewrite /uPred_except_0. iRight. iFrame.
iSplitL "Hw HEi".
+ by iApply "Hw".
+ iSplitL "Hi"; [eauto|].
iIntros "HP [Hw HE\N]".
iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[? HEi]".
iModIntro. iRight. iFrame. iSplitL; [|done].
iCombine "HEi" "HEN\i" as "HEN".
iCombine "HEN" "HE\N" as "HE".
rewrite -?ownE_op; [|set_solver|set_solver].
rewrite ownE_proper; [done|].
rewrite <-!union_difference; set_solver.
Qed.
End invariants.
```Iris 3.0Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/58Proofmode with Coq binders, and without strings2019-11-01T11:15:16ZRalf Jungjung@mpi-sws.orgProofmode with Coq binders, and without strings@janno mentioned to me some ideas for how one could make a proofmode that uses Coq names and syntax instead of strings. Just imagine, we could have nested Coq- and Iris-level intro patterns... that would cut many proofs in lambdaRust sig...@janno mentioned to me some ideas for how one could make a proofmode that uses Coq names and syntax instead of strings. Just imagine, we could have nested Coq- and Iris-level intro patterns... that would cut many proofs in lambdaRust significantly. We could also not use strings, which may even help with speed. (Well, strings are not very efficient in Coq -- but I kind of doubt that's out bottleneck currently.)
I'll leave it to Janno to explain the idea, because I would totally screw that up.
I any case, even if we want to go for this, this is a long-term thing... definitely post-3.0, and definitely breaking everybody using Iris horribly (if we don't just keep the string-based stuff around).https://gitlab.mpi-sws.org/iris/iris/-/issues/57Support clear patterns in more places2017-02-01T10:58:47ZRalf Jungjung@mpi-sws.orgSupport clear patterns in more placesRight now, one can write `iIntros "{Hfoo} [Hfoo Hbar]"`, but if I do `iMod ... as "{Hshr} [Hshr $]"`, I get
```
Tactic failure: invalid intro_pat "{Hshr} [Hshr $]".
```
(See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theor...Right now, one can write `iIntros "{Hfoo} [Hfoo Hbar]"`, but if I do `iMod ... as "{Hshr} [Hshr $]"`, I get
```
Tactic failure: invalid intro_pat "{Hshr} [Hshr $]".
```
(See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/typing/own.v#L134>)https://gitlab.mpi-sws.org/iris/iris/-/issues/56iAssert ... as %X should get all assumptions2017-01-03T13:28:17ZRalf Jungjung@mpi-sws.orgiAssert ... as %X should get all assumptionsWhen I write `iAssert ... as %X`, it is syntactically clear that I am proving sth. persistent (even pure). Still, I have to add `with [#]` to be allowed to use all assumptions. Wouldn't it make sense to do that automatically? IIRC we ar...When I write `iAssert ... as %X`, it is syntactically clear that I am proving sth. persistent (even pure). Still, I have to add `with [#]` to be allowed to use all assumptions. Wouldn't it make sense to do that automatically? IIRC we are doing sth. like that with ´iDestruct ... as %X`.Iris 3.0Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/55iNext unfolds things (more than simpl) even when there is no later to strip2018-02-20T00:50:15ZRalf Jungjung@mpi-sws.orgiNext unfolds things (more than simpl) even when there is no later to stripSee <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/02ef8176f01f8de0563a2f5a8e1444bb9ee01b6d/theories/typing/cont.v#L40>: The context goas from
```
"HC" : elctx_interp E qE -∗ cctx_interp tid C
"HE" : elctx_interp E qE
"HL" ...See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/02ef8176f01f8de0563a2f5a8e1444bb9ee01b6d/theories/typing/cont.v#L40>: The context goas from
```
"HC" : elctx_interp E qE -∗ cctx_interp tid C
"HE" : elctx_interp E qE
"HL" : llctx_interp L1 1
"HT" : tctx_interp tid (T' args)
```
to
```
"HC" : elctx_interp E qE -∗ cctx_interp tid C
"HE" : [∗ list] k↦x ∈ E, (λ (_ : nat) (x0 : elctx_elt), elctx_elt_interp x0 qE) k x
"HL" : [∗ list] k↦x ∈ L1, (λ (_ : nat) (x0 : llctx_elt), llctx_elt_interp x0 1) k x
"HT" : [∗ list] k↦x ∈ T' args, (λ (_ : nat) (x0 : tctx_elt), tctx_elt_interp tid x0) k x
```
but no later is removed. Not even simpl unfolds these definitions.Iris 3.0Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/54iIntros fails to introduce Coq-level and Iris-level universal quantifiers at ...2016-12-21T19:01:39ZRalf Jungjung@mpi-sws.orgiIntros fails to introduce Coq-level and Iris-level universal quantifiers at onceSee for example <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/ca917d76e1318fb3a6e0aa0c61f777a2e62ac8d0#51956c642cbeef54a2f1728f704193c7e23720f3_97_98>: `iIntros (HTsat HEsat). iIntros (tid qE) "#LFT HE HL HC".` works but `iIntros ...See for example <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/ca917d76e1318fb3a6e0aa0c61f777a2e62ac8d0#51956c642cbeef54a2f1728f704193c7e23720f3_97_98>: `iIntros (HTsat HEsat). iIntros (tid qE) "#LFT HE HL HC".` works but `iIntros (HTsat HEsat tid qE) "#LFT HE HL HC".` does not.Iris 3.0Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/53Improve solve_ndisj2017-02-16T14:07:06ZRalf Jungjung@mpi-sws.orgImprove solve_ndisj<https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c72bfec9e38531b7dc70f05c2415ed1e3f806899> demonstrates some cases that `solve_ndisj` cannot handle, and it'd be great if it could. Most of them could be handled if we added
```
Hint Ex...<https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c72bfec9e38531b7dc70f05c2415ed1e3f806899> demonstrates some cases that `solve_ndisj` cannot handle, and it'd be great if it could. Most of them could be handled if we added
```
Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
```
The one remaining case is more subtle. It is solved by `assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. set_solver.`, but is there a way we can plug solve_ndisj and set_solver together so that we don't have to say in advance which inclusions we need?
Cc @robbertkrebbers @jjourdan