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/204Support `iInduction .. using ...`2018-08-29T09:48:58ZRobbert KrebbersSupport `iInduction .. using ...`Like `induction ... using ...`; so one can more easily use custom induction principle like `map_ind`.
Requested by @dfruminLike `induction ... using ...`; so one can more easily use custom induction principle like `map_ind`.
Requested by @dfruminRobbert KrebbersRobbert Krebbershttps://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/129Support COQBIN2018-01-23T16:16:54ZRalf Jungjung@mpi-sws.orgSupport COQBINI just got the second request to support a COQBIN environment variable, so maybe we should just do that. I imagine something like what [this Makefile](https://github.com/ppedrot/coq-string-ident/blob/master/Makefile) does, so that not se...I just got the second request to support a COQBIN environment variable, so maybe we should just do that. I imagine something like what [this Makefile](https://github.com/ppedrot/coq-string-ident/blob/master/Makefile) does, so that not setting COQBIN follows the PATH.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://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/32Support framing pure/Coq hypotheses2016-09-19T19:18:18ZJacques-Henri JourdanSupport framing pure/Coq hypothesesIn the following, iFrame does not have the expected behavior:
Lemma L `{irisG Λ Σ} : ∀ P:iProp Σ, □ P ⊢ P ★ True.
iIntros (P) "#HP". iFrame.In the following, iFrame does not have the expected behavior:
Lemma L `{irisG Λ Σ} : ∀ P:iProp Σ, □ P ⊢ P ★ True.
iIntros (P) "#HP". iFrame.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/7Support stored propositions2016-01-20T13:26:21ZRalf Jungjung@mpi-sws.orgSupport stored propositionsIt would be nice to have support for "Stored propositions" as described in <http://www-users.cs.york.ac.uk/~miked/publications/verifying_custom_sync_constructs.pdf>.
@kaspersv suggested they could be hacked into Iris without changing ...It would be nice to have support for "Stored propositions" as described in <http://www-users.cs.york.ac.uk/~miked/publications/verifying_custom_sync_constructs.pdf>.
@kaspersv suggested they could be hacked into Iris without changing in the model. Let me quote his mail (with some parts of my mail also being inline):
>> And finally, of course, there's the question whether this could be done
>> in Iris. I am sure we could have the following proof rule:
>>
>> \inv^i (P) * \inv^i (Q) => \later (P <=> Q)
>
>Indeed, we can even strengthen it to inv^j (P) * inv^j (Q) => later (P = Q)
>because the interpretation of inv is slightly stronger in Iris than rintrp is
>in iCAP. In particular, inv^j (P) asserts that the invariant is n-equal to P,
>while iCAP only asserts that the region interpretation is n-equal to
>the given predicate when applied to any future world of the current
>world.
>
>> but we can't easily use the trick you did, with the 2-state STS, in
>> order to not actually store a P in the invariant. Did you think about this?
>
>Yes, we did think about an encoding, using two mutually exclusive
>ghost resources gh(0) and gh(1). The idea would be to create an
>invariant (P * gh(0)) \/ gh(1) and transfer gh(1) to the region. Then
>the question boils down to:
>
>(P * gh(0)) \/ gh(1) = (Q * gh(0)) \/ gh(1) |- P = Q
>
>I don’t think it is possible to prove this internally and we weren’t
>sufficiently motivated to check if it holds in the semantics, but it
>seems like it should.
As an alternative, @janno and me tossed around the idea of letting the user chose an arbitrary, locally non-expansive functor to construct the ghost monoid. That would allow the user to make use of my agreement construction, with "Ag(\later Prop)" being in the ghost monoid. This would then let the user do stored propositions without hacks like the above. @robbertkrebbers also seemed to like that. However, we would lose the axiom that ghost ownership is timeless, and I see no easy way to regain it for the part of the functor that has a discrete metric. So, probably, we would want to keep both a discrete monoid (where ownership is timeless) and a functor (where crazy things can happen) in the interface, and pair them together ourselves - which raises the question if that's worth it. The model would end up with a 4-tuple-monoid instead of the three-tuples is has currently (invariants, ghost, physical). Right now, I cannot imagine using any other monoid with propositions embedded. Of course it would be nice to have, for example, STSs with states indexed by propositions, but actually doing that would require making this STS a functor, and showing all the functorial properties and local non-expansiveness and so on - probably it would be much easier to go with stored propositions and index the STS by the name instead. For that reason, right now, I'd prefer the solution suggested by @kaspersv if it works.
@jtassaro: I mentioned this yesterday during our conversation.https://gitlab.mpi-sws.org/iris/iris/-/issues/234Syntactic type system for heap_lang2020-10-01T11:28:21ZRobbert KrebbersSyntactic type system for heap_lang@dfrumin defined a syntactic type system for heap_lang in the reloc repo:
https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v
I would like to use his type system to state the fundamental theorem for the unary lo...@dfrumin defined a syntactic type system for heap_lang in the reloc repo:
https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v
I would like to use his type system to state the fundamental theorem for the unary logical relation of heap_lang in iris-examples (https://gitlab.mpi-sws.org/iris/examples/tree/master/theories/logrel_heaplang), as right now that formalization only has semantic types and the semantic typing rules.
How about adding @dfrumin's syntactic type system to the heap_lang folder of the Iris repo?
Some things to discuss:
- [ ] It currently relies on autosubst. Using strings for binding in types will be horrible, since there we actually have to deal with capture. Do we mind having a dependency of Iris on Autosubst, or would it be better to write a manual version with De Bruijn indexes?
- [ ] It uses some fun encodings for pack and unpack (of existential types) and type abstraction and application, see https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v#L80 Are we happy with that, or are there more elegant ways of doing that?https://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/115Test2017-12-08T15:54:33ZRalf Jungjung@mpi-sws.orgTestThis is an issue to test the mattermost integration. Please ignore.This is an issue to test the mattermost integration. Please ignore.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/149The current axioms of BI imply emp ≡ True2018-02-26T13:43:07ZAleš Bizjakales@alesb.comThe current axioms of BI imply emp ≡ TrueAs the subject states, the current axiomatization of the plainly modality implies emp ≡ True.
In particular, the guilty parties are the axioms `prop_ext` and `plainly_emp_intro`.
I am not sure whose axioms they are, but I hope either @r...As the subject states, the current axiomatization of the plainly modality implies emp ≡ True.
In particular, the guilty parties are the axioms `prop_ext` and `plainly_emp_intro`.
I am not sure whose axioms they are, but I hope either @robbertkrebbers or @jjourdan knows the history.
I believe this must be an error, since otherwise there is no point in having `emp`.
```coq
From iris.bi Require Import interface.
Import bi.
Section bi_emp.
Context {PROP : bi}.
Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).
Lemma bar: emp ⊢ (True → emp) ∧ (emp → True).
Proof.
apply and_intro.
- apply impl_intro_r, and_elim_l.
- apply impl_intro_r, pure_intro; exact I.
Qed.
Lemma baz: True ⊢ ((True : PROP) ≡ emp).
Proof.
transitivity (bi_plainly (emp : PROP))%I; first apply plainly_emp_intro.
transitivity (bi_plainly ((True → emp : PROP) ∧ (emp → True))%I).
{ apply plainly_mono, bar. }
apply prop_ext.
Qed.
End bi_emp.
```Generalized Proofmode MergerJacques-Henri JourdanJacques-Henri Jourdanhttps://gitlab.mpi-sws.org/iris/iris/-/issues/1Thread-local state, user-controlled fork2016-08-23T14:34:02ZRalf Jungjung@mpi-sws.orgThread-local state, user-controlled forkChange `core_lang` to get rid of evaluation contexts and let the user control what fork does. This will invalidate the Bind rule, I will create another issue for that.Change `core_lang` to get rid of evaluation contexts and let the user control what fork does. This will invalidate the Bind rule, I will create another issue for that.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/22Ticket lock proof2016-08-02T11:52:30ZGhost UserTicket lock proofJust finished [here](https://gitlab.mpi-sws.org/zhangz/iris-coq/tree/ticket-lock). Would it be good to merge into master?Just finished [here](https://gitlab.mpi-sws.org/zhangz/iris-coq/tree/ticket-lock). Would it be good to merge into master?https://gitlab.mpi-sws.org/iris/iris/-/issues/415Tracking issue for append-only list RA2021-11-22T17:58:29ZRalf Jungjung@mpi-sws.orgTracking issue for append-only list RAThis is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Op...This is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Do we really want notation for the mono_list algebra elements? The main "pro" reason here is that `dfrac` otherwise becomes somewhat painful. OTOH, mono_nat and gset_bij algebras do not have notation either. It'd be safe to start without notation
and add them on-demand.
* On the logic layer, should `mono_list_auth` take `Qp` or `dfrac`? Eventually we want to move everything to `dfrac` but again the concern is that (without good notation), this will make the library more annoying to use. This is discussed in more generality at https://gitlab.mpi-sws.org/iris/iris/-/issues/412.
* Do a solid review of the API surface.https://gitlab.mpi-sws.org/iris/iris/-/issues/144Turn Coq quantifiers into proofmode quantifiers on `iStartProof`2018-01-30T14:17:25ZRobbert KrebbersTurn Coq quantifiers into proofmode quantifiers on `iStartProof`For example, it should turn the Coq goal `forall x, P ⊢ Q` into a proof mode goal `∀ x, P → Q`. (And likewise for let-bindings).
Since issue came up in d7db5250ad0214ef4be5f634f81fe35caf6ad0d8, which changes the behavior of `iStartProof...For example, it should turn the Coq goal `forall x, P ⊢ Q` into a proof mode goal `∀ x, P → Q`. (And likewise for let-bindings).
Since issue came up in d7db5250ad0214ef4be5f634f81fe35caf6ad0d8, which changes the behavior of `iStartProof PROP`, to just introduce all quantifiers. @jjourdan introduced that because in iGPS they were often doing:
```coq
intros; iStartProof (uPred _); iIntros (V) "..."
```
The proposal in this issue fixes this problem in a nicer way.Jacques-Henri JourdanJacques-Henri Jourdanhttps://gitlab.mpi-sws.org/iris/iris/-/issues/346Typeclass inference fails to trigger.2020-09-21T18:08:44ZArthur Azevedo de AmorimTypeclass inference fails to trigger.I am trying to use `auth_acc`, but typeclass inference misses an apparently obvious instance that I have to provide by hand. Am I doing something wrong?
```
From stdpp Require Import base gmap.
From iris.algebra Require Import gmap num...I am trying to use `auth_acc`, but typeclass inference misses an apparently obvious instance that I have to provide by hand. Am I doing something wrong?
```
From stdpp Require Import base gmap.
From iris.algebra Require Import gmap numbers.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import auth invariants.
Section Test.
Context `{!invG Σ, !authG Σ (gmapUR nat natR)}.
Implicit Types m : gmap nat nat.
Definition my_inv m : iProp Σ := True.
Goal ∀ γ, auth_ctx γ nroot id my_inv ={⊤}=∗ False.
iIntros (γ) "Hctx".
iMod (auth_empty γ) as "#Hinit".
iMod (auth_acc _ _ _ _ _ ε with "[Hctx Hinit]") as "Hinv"; try by eauto.
(* Inhabited (gmap nat nat) is now shelved... *)
Abort.
End Test.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/226Typeclass interference does not work for Timeless (□ P)2019-02-12T20:55:26ZMichael SammlerTypeclass interference does not work for Timeless (□ P)In the following code I would expect the first `apply _` to work. Instead `affinely_timeless` has to be applied explicitly before `apply _` works.
```
Instance timeless (P : iProp Σ) `{!Timeless P} : Timeless (□ (P)).
Proof.
F...In the following code I would expect the first `apply _` to work. Instead `affinely_timeless` has to be applied explicitly before `apply _` works.
```
Instance timeless (P : iProp Σ) `{!Timeless P} : Timeless (□ (P)).
Proof.
Fail apply _.
eapply affinely_timeless; by apply _. (* this goes through *)
Qed.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/136Typeclass search loops in gen_proofmode2018-01-22T17:22:52ZJannoTypeclass search loops in gen_proofmodeThe cycle is
```
simple apply @as_valid' on
simple apply @as_valid_embed on
simple apply @sbi_embed_bi_embed on
simple eapply @as_valid_monPred_at_equiv on
simple apply @as_valid' on
simple eapply @as_valid_monPred_at_wand on
simp...The cycle is
```
simple apply @as_valid' on
simple apply @as_valid_embed on
simple apply @sbi_embed_bi_embed on
simple eapply @as_valid_monPred_at_equiv on
simple apply @as_valid' on
simple eapply @as_valid_monPred_at_wand on
simple apply @as_valid' on
```
and can be witnessed in
https://gitlab.mpi-sws.org/FP/sra-gps/blob/4514e8fdd515772c09e5a5797327651b4e6f49d4/theories/examples/tstack.v#L112Jacques-Henri JourdanJacques-Henri Jourdanhttps://gitlab.mpi-sws.org/iris/iris/-/issues/437Typo in documentation2021-10-26T19:12:53ZAlexandre MoineTypo in documentationHi,
There is a typo here: https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html#lab34, which shows:
![2021-10-19_09-35](/uploads/a590aa61f3327bb234d97e50b29cd31a/2021-10-19_09-35.png)
It comes from a section title spitted in two l...Hi,
There is a typo here: https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html#lab34, which shows:
![2021-10-19_09-35](/uploads/a590aa61f3327bb234d97e50b29cd31a/2021-10-19_09-35.png)
It comes from a section title spitted in two lines. This seems to be the only occurrence