Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2017-05-19T15:20:29Zhttps://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 @jjourdanhttps://gitlab.mpi-sws.org/iris/iris/-/issues/52iMod and evar instantiation2019-06-17T07:54:22ZRalf Jungjung@mpi-sws.orgiMod and evar instantiationSee <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/acddfae5355a5e7540010c7ea6f423a892f9e887#note_17391>: `iMod ... as [$ ?]` fails even though `iMod ... as [H ?]; iFrame "H"` works fine.
@jjourdan suggests it may be related to C...See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/acddfae5355a5e7540010c7ea6f423a892f9e887#note_17391>: `iMod ... as [$ ?]` fails even though `iMod ... as [H ?]; iFrame "H"` works fine.
@jjourdan suggests it may be related to Coq lazily propagating instantiated evars, and adding a magic tactic that does the propagation in the right point of executing the `iMod` could help.Iris 3.0Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/51iApply: Add sufficiently many [] spec patterns per default?2017-11-16T09:36:46ZRalf Jungjung@mpi-sws.orgiApply: Add sufficiently many [] spec patterns per default?I find my self repeatedly writing `iApply (foo with "[] [] []")` in lambdaRust proofs. Would it make sense to extend the automatic "adding a `[]` to the end of th spec pattern list" that `iApply` does, such that it will add as many `[]` ...I find my self repeatedly writing `iApply (foo with "[] [] []")` in lambdaRust proofs. Would it make sense to extend the automatic "adding a `[]` to the end of th spec pattern list" that `iApply` does, such that it will add as many `[]` as are needed to get the job done? Essentially, `iApply foo` would always succeed if the conclusion of foo matches the goal, and all assumptions will only get the persistent contect -- spec patterns are only needed if one wants to give more than that? IMHO that would also improve the general workflow of working with `iApply` since I don't need to look up in advance how many items I need to put into the spec pattern, I can just `iApply` and then see which of the goals I get need further resources.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/50`contains` is named the wrong way around2017-01-14T21:53:11ZRalf Jungjung@mpi-sws.org`contains` is named the wrong way around``l1 `contains` l2`` confusing expresses that `l2` contains `l1`. Either the order of arguments should be changed, or the notation should be changed to e.g. `contained`.``l1 `contains` l2`` confusing expresses that `l2` contains `l1`. Either the order of arguments should be changed, or the notation should be changed to e.g. `contained`.Iris 3.0https://gitlab.mpi-sws.org/iris/iris/-/issues/49Improve support of simplify_option_eq (and simplify_map_eq?) for setoids2017-11-13T18:13:54ZRalf Jungjung@mpi-sws.orgImprove support of simplify_option_eq (and simplify_map_eq?) for setoidsSome testcases:
* <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d#59b3a9376af7e8ce6a745e02cef554707e5c7419_585_585>
* in lambdaRust, lifetime/primitive.v, proof of `own_ilft_auth_agree`Some testcases:
* <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d#59b3a9376af7e8ce6a745e02cef554707e5c7419_585_585>
* in lambdaRust, lifetime/primitive.v, proof of `own_ilft_auth_agree`Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/48Unify `iNext` and `iModIntro` (and more?)2018-07-13T15:56:18ZRobbert KrebbersUnify `iNext` and `iModIntro` (and more?)These tactics are very similar. I would be nice to generalize `iModIntro` to also strip occurrences of the modality from all of the hypotheses.
Given that we have already generalized `iNext` to deal with the iterated later modality, I t...These tactics are very similar. I would be nice to generalize `iModIntro` to also strip occurrences of the modality from all of the hypotheses.
Given that we have already generalized `iNext` to deal with the iterated later modality, I think this should not be too difficult.
See also the discussion as part of commit 9ae19ed5.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/47Use opam-based CI2016-12-14T13:19:40ZRalf Jungjung@mpi-sws.orgUse opam-based CII'd like to use the same opam-based CI setup that we also use for lambdaRust. This will also make it trivial for us to run the CI with both Coq 8.5 and 8.6, and to change Coq versions in the future (no changes in the CI image needed for ...I'd like to use the same opam-based CI setup that we also use for lambdaRust. This will also make it trivial for us to run the CI with both Coq 8.5 and 8.6, and to change Coq versions in the future (no changes in the CI image needed for this any more, yay :D ).
However, to make that work, we have to stop importing `.` in `_CoqProject`. So like in lambdaRust, I'd like to move everything into a subfolder `theories/`.
This will break all merge requests, so we should get at least some of them in. !30 will hang around for a while, so whatever. But I'd like to wait until we get at least !25 or !22 in.Iris 3.0Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/46Use the correct setoid equality in algebra/gset and algebra/coPset2016-11-30T12:14:50ZHai DangUse the correct setoid equality in algebra/gset and algebra/coPsetcofe_equiv takes precedence over available equivalences, which prevents rewriting with those equivalences. I have to make explicit those instances.
@janno suggested that it is due to this hint?
https://gitlab.mpi-sws.org/FP/iris-co...cofe_equiv takes precedence over available equivalences, which prevents rewriting with those equivalences. I have to make explicit those instances.
@janno suggested that it is due to this hint?
https://gitlab.mpi-sws.org/FP/iris-coq/blob/75518c9a4c5278b44120212060c2faceb875de3f/algebra/ofe.v#L52Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/45iLöb with non-empty revert list2016-11-30T12:14:50ZJannoiLöb with non-empty revert listWhen iLöb is given a list of iris assumptions it does not automatically generalize over all spatial assumptions any more. Adding a ∗ to the list of assumptions solves that problem.
Proposal: always add ∗ to the list of Iris assumptions.When iLöb is given a list of iris assumptions it does not automatically generalize over all spatial assumptions any more. Adding a ∗ to the list of assumptions solves that problem.
Proposal: always add ∗ to the list of Iris assumptions.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/44Vague iRevert error messages2016-11-30T12:14:50ZJannoVague iRevert error messagesiRevert does not report why exactly it fails (e.g. because the variable is used in a spatial assumption). It should do that. :)
(Note: ltac's revert actually has somewhat useful error messages.)iRevert does not report why exactly it fails (e.g. because the variable is used in a spatial assumption). It should do that. :)
(Note: ltac's revert actually has somewhat useful error messages.)Robbert KrebbersRobbert Krebbers