Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-02-10T15:44:56Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/269Editor config should explain how to configure CoqIDE 8.10 unicode input2020-02-10T15:44:56ZTej Chajedtchajed@mit.eduEditor config should explain how to configure CoqIDE 8.10 unicode inputCoqIDE 8.10 has a new feature for inputting unicode symbols with LaTeX-to-unicode conversion (triggered by typing shift-space). It's possible to configure the supported bindings (see https://coq.github.io/doc/master/refman/practical-tool...CoqIDE 8.10 has a new feature for inputting unicode symbols with LaTeX-to-unicode conversion (triggered by typing shift-space). It's possible to configure the supported bindings (see https://coq.github.io/doc/master/refman/practical-tools/coqide.html#coqide-unicode), so [editor.md](docs/editor.md) should give a configuration file with the Iris LaTeX bindings.https://gitlab.mpi-sws.org/iris/iris/-/issues/250equivI lemma for sigT2019-06-25T10:41:37ZPaolo G. GiarrussoequivI lemma for sigTTo use the new `sigT` construction, it helps to have an `equivI` lemma such as:
```coq
Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
x ≡ y ⊣⊢
∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y : iProp Σ.
...To use the new `sigT` construction, it helps to have an `equivI` lemma such as:
```coq
Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
x ≡ y ⊣⊢
∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y : iProp Σ.
Proof. by unseal. Qed.
```
@robbertkrebbers asks: should we have this just for iProp, or for any `sbi`?https://gitlab.mpi-sws.org/iris/iris/-/issues/14Evaluation-context language2016-03-29T18:01:52ZRalf Jungjung@mpi-sws.orgEvaluation-context languageWe should have a typeclass for an evaluation-context based language, and an instance to convert these into a general Iris language, and some specialized lifting lemmas for such languages.We should have a typeclass for an evaluation-context based language, and an instance to convert these into a general Iris language, and some specialized lifting lemmas for such languages.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/334Expand test coverage of proofmode2021-12-16T22:21:12ZTej Chajedtchajed@mit.eduExpand test coverage of proofmodeThe proof mode tests don't cover the following:
- [x] `iRename`
- [x] `iTypeOf`
- [x] `iInduction`'s ability to freshen the inductive hypothesis
I have tests for the first two on my [bytes-ident](https://gitlab.mpi-sws.org/tchajed/iris...The proof mode tests don't cover the following:
- [x] `iRename`
- [x] `iTypeOf`
- [x] `iInduction`'s ability to freshen the inductive hypothesis
I have tests for the first two on my [bytes-ident](https://gitlab.mpi-sws.org/tchajed/iris-coq/-/tree/bytes-ident) branch.https://gitlab.mpi-sws.org/iris/iris/-/issues/215Explore getting rid of implication2019-11-01T11:07:41ZRalf Jungjung@mpi-sws.orgExplore getting rid of implicationIt seems possible that we don't actually need implication and could work without it (so we'd work in intuitionistic linear logic instead of the more general separation logic/BI). Seems at least interesting to figure out of that's true. ...It seems possible that we don't actually need implication and could work without it (so we'd work in intuitionistic linear logic instead of the more general separation logic/BI). Seems at least interesting to figure out of that's true. We could remove implication from the MoSeL interface and see what happens.
For Iris itself I mostly expect this to work, but the general linear case might make this harder. Or not.https://gitlab.mpi-sws.org/iris/iris/-/issues/153Exponential slowdown in `iFrame` and the number of laters2018-02-20T00:50:15ZRobbert KrebbersExponential slowdown in `iFrame` and the number of laters```coq
From iris Require Import proofmode.tactics.
Lemma test2 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 0.141s *) Admitted.
Lemma test4 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R)...```coq
From iris Require Import proofmode.tactics.
Lemma test2 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 0.141s *) Admitted.
Lemma test4 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 0.7s *) Admitted.
Lemma test8 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ ▷ ▷ ▷ ▷ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 6.796s *) Admitted.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/255Failure to find a proof of persistence2020-03-18T20:54:41ZDmitry KhalanskiyFailure to find a proof of persistenceVersion of Iris: dev.2019-07-01.1.6e79f000
Typeclass search fails when trying to prove that a particular statement is persistent.
In resource algebra
```
authR (prodUR
(prodUR
(optionUR (exclR unitO))
(optio...Version of Iris: dev.2019-07-01.1.6e79f000
Typeclass search fails when trying to prove that a particular statement is persistent.
In resource algebra
```
authR (prodUR
(prodUR
(optionUR (exclR unitO))
(optionUR (exclR unitO)))
(optionUR (agreeR (boolO))))
```
proof of
```
Persistent (own γ (◯((None, None), Some (to_agree true))))
```
fails with
```
Proof search failed without reaching its limit.
```
if performed with `typeclasses eauto 10`. It similarly doesn't work with `apply _`.
The statement is actually persistent, as shown by Jonas Kastberg:
```
Proof.
apply own_core_persistent.
apply auth_frag_core_id.
apply pair_core_id; typeclasses eauto.
Qed.
```
Minimal (non-)working example: https://pastebin.com/T7zhm9Zuhttps://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/103Find a better name for iMod2017-11-24T15:57:13ZRalf Jungjung@mpi-sws.orgFind a better name for iModWe do have at least one more badly named item: iMod. The name is both uninformative (what does it do with the modality?) and wrong (the tactic does nothing with the persistent and plain modalities).
Proposed alternatives: `iRun`, `iUpd`...We do have at least one more badly named item: iMod. The name is both uninformative (what does it do with the modality?) and wrong (the tactic does nothing with the persistent and plain modalities).
Proposed alternatives: `iRun`, `iUpd`. `iUpd` is my personal favorite. I know that the tactic supports other modalities, but 99,9% of the time it is used to eliminate some form of an update. The name is more informative than `iMod`, and not more wrong.
`iRun` is slightly less informative, but also less wrong: The tactic does bind in a monad, which can be seen as "running the computation".
Cc @robbertkrebbers @jjourdan
EDIT: All right, I stand corrected on the "wrong" part. Sorry for that. It is still uninformative.https://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/24Find nice syntax for our "CPS" WP specifications2016-10-27T09:23:29ZRalf Jungjung@mpi-sws.orgFind nice syntax for our "CPS" WP specificationsIt would be nice to have "something" that makes our specs more readable to someone not familiar with our "CPS" style of writing specs with an arbitrary postcondition (Φ).
I believe @janno has been working on something like that... wha...It would be nice to have "something" that makes our specs more readable to someone not familiar with our "CPS" style of writing specs with an arbitrary postcondition (Φ).
I believe @janno has been working on something like that... what was the status of that again?https://gitlab.mpi-sws.org/iris/iris/-/issues/319Fix "omega is deprecated" warnings by switching to lia2020-05-16T17:14:49ZTej Chajedtchajed@mit.eduFix "omega is deprecated" warnings by switching to liaOn Coq v8.12+alpha there are a few new warnings from uses of `omega`, which should be replaced with `lia`. This might be a little annoying to make compatible with Coq v8.9, since `lia` has gotten progressively more powerful.On Coq v8.12+alpha there are a few new warnings from uses of `omega`, which should be replaced with `lia`. This might be a little annoying to make compatible with Coq v8.9, since `lia` has gotten progressively more powerful.https://gitlab.mpi-sws.org/iris/iris/-/issues/309Fix name duplication `elem_of_list_singleton` in Iris and std++2020-07-15T09:36:22ZRobbert KrebbersFix name duplication `elem_of_list_singleton` in Iris and std++See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47923See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47923Iris 3.3https://gitlab.mpi-sws.org/iris/iris/-/issues/271Follow-up from "Lang lemmas": intuitive explanation of mixin_step_by_val2020-05-13T09:53:35ZRalf Jungjung@mpi-sws.orgFollow-up from "Lang lemmas": intuitive explanation of mixin_step_by_valIn !324 I started a [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/324#note_41125) to find an intuitive explanation of "mixin_step_by_val". I propose this, and I still think it's good:
"Let \[fill K e1\] and \[fill K' ...In !324 I started a [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/324#note_41125) to find an intuitive explanation of "mixin_step_by_val". I propose this, and I still think it's good:
"Let \[fill K e1\] and \[fill K' e1'\] be two decompositions of the same expression such that \[e1'\] is reducible. Then either \[K\] is a prefix of \[K'\] (so \[e1\] actually contains \[e1'\] as its head redex), or \[e1\] is a value. In other words, there cannot be two entirely unrelated head redexes that actually reduce."
@amintimany had an objection that I did not understand:
> This does not really say anything about there not being redxes!
My response:
> Of course it does? If there are redexes, the contexts are related; thus if there are unrelated contexts, there are no redexes.
@amintimany @robbertkrebbers let's discuss here.Iris 3.3Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/9Formalize a realistic language2016-01-18T16:58:07ZRalf Jungjung@mpi-sws.orgFormalize a realistic languageTo gain confidence in the axioms we use for abstracting away the language, and in our lifting lemmas, it'd be great if we could have a formalization of the lambda-calculus we used in the paper (or maybe one with a heap, I don't care stro...To gain confidence in the axioms we use for abstracting away the language, and in our lifting lemmas, it'd be great if we could have a formalization of the lambda-calculus we used in the paper (or maybe one with a heap, I don't care strongly either way).
@swasey I think you're the one who did most work in this direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/132Formalize example that impredicative invariants and linearity are incompatible2020-02-07T15:22:45ZRobbert KrebbersFormalize example that impredicative invariants and linearity are incompatibleRalf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://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/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/145Framing should succeed when a disjunct is exactly the framed hypothesis2018-02-08T21:00:00ZRobbert KrebbersFraming should succeed when a disjunct is exactly the framed hypothesisFor example, framing `P` in `(P ∨ Q) ∗ R` should succeed and turn the goal into `R`.
In general, framing of non-persistent hypotheses in just one disjunct of a disjunction leads to information loss, so should fail. However, if framing i...For example, framing `P` in `(P ∨ Q) ∗ R` should succeed and turn the goal into `R`.
In general, framing of non-persistent hypotheses in just one disjunct of a disjunction leads to information loss, so should fail. However, if framing in one disjunct turns it into `True`, framing should succeed.Robbert KrebbersRobbert Krebbershttps://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.