Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-03-12T13:17:31Zhttps://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/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/151Naming : Absolute, absolutely, relatively2018-03-04T19:19:42ZJacques-Henri JourdanNaming : Absolute, absolutely, relativelyThis issue is here just to make sure that everyone agrees with the new names and notations (and to choose other ones, as I am sure you will not agree).
So:
- `monPred_all` becomes `monPred_absolutely`, written `∀ᵢ P`
- `monPred_ex` beco...This issue is here just to make sure that everyone agrees with the new names and notations (and to choose other ones, as I am sure you will not agree).
So:
- `monPred_all` becomes `monPred_absolutely`, written `∀ᵢ P`
- `monPred_ex` becomes `monPred_relatively`, written `∃ᵢ P`
- `Objective` becomes `Absolute`
Just to be clear: it took these names because something had to be chosen to make progress, and because there was objections about the previous names. No decision is taken, and anyone should feel free to contest.Generalized Proofmode Mergerhttps://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/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/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/148Make `iNext` smarter for mixed `▷` and `▷^(n+m)`2018-02-20T15:29:40ZLéon GondelmanMake `iNext` smarter for mixed `▷` and `▷^(n+m)`Following the (fixed) issue (https://gitlab.mpi-sws.org/FP/iris-coq/issues/141), there is still an error w.r.t. addition in the laterN modality:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n m : ▷ ▷^...Following the (fixed) issue (https://gitlab.mpi-sws.org/FP/iris-coq/issues/141), there is still an error w.r.t. addition in the laterN modality:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n m : ▷ ▷^(n+m) P ⊢ ▷^n ▷ P.
Proof. iIntros "H". iNext.
```
```coq
(* Gives
"H" : ▷ ▷^(n + m) P
--------------------------------------∗
▷ P
*)
```
forgetting erroneously to cancel `n` in the premise `"H"`.Robbert 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/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/155Make `iPureIntro` able to introduce affine pure assertions when the context i...2018-02-15T16:08:05ZJacques-Henri JourdanMake `iPureIntro` able to introduce affine pure assertions when the context is emtpy.The current lemma behind `iPureIntro` is:
```coq
Lemma tac_pure_intro Δ Q φ : FromPure false Q φ → φ → envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure _ Q). by apply pure_intro. Qed.
```
Could we change it a bit, ...The current lemma behind `iPureIntro` is:
```coq
Lemma tac_pure_intro Δ Q φ : FromPure false Q φ → φ → envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure _ Q). by apply pure_intro. Qed.
```
Could we change it a bit, so that we ask for `FromPure true Q φ` when the context is empty? That way, we could introduce CFML's affine pure assertions transparently when the context is empty.Robbert KrebbersRobbert Krebbershttps://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/112Make invariants and slices closed under equivalence2018-02-08T10:43:12ZRalf Jungjung@mpi-sws.orgMake invariants and slices closed under equivalenceThis has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the followi...This has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the following holds:
```coq
Lemma inv_iff P Q :
later persistently (P <-> Q) -> inv P -> inv Q.
```
I think this may be worth it, *if* it means we can simplify the definition of the lifetime logic a little bit. However, that will only be the case if we manage to also get this law for `slice`, which requires either a separate closure in `slice` (so the one in `inv` does not help), or doing the same kind of closure in `saved_prop_own` (but then, do we also want the equivalent law for `saved_pred_own`?).
Also, I am not sure if we should do this before or after Iris 3.1. Either way, it is backwards-compatible.https://gitlab.mpi-sws.org/iris/iris/-/issues/143Gen_proofmode: move internal eq into SBI2018-02-05T15:16:38ZJacques-Henri JourdanGen_proofmode: move internal eq into SBIIf the Bi is not step-indexed, then there is no reason not to use the pure embedding.If the Bi is not step-indexed, then there is no reason not to use the pure embedding.https://gitlab.mpi-sws.org/iris/iris/-/issues/13Bring back unsafe triples2018-02-02T19:07:29ZRalf Jungjung@mpi-sws.orgBring back unsafe triplesThey were lost in the transition from Iris 1.1 to Iris 2.0. @swasey needs them.They were lost in the transition from Iris 1.1 to Iris 2.0. @swasey needs them.https://gitlab.mpi-sws.org/iris/iris/-/issues/82Consider adding a "strong" always modality2018-01-31T09:21:27ZRalf Jungjung@mpi-sws.orgConsider adding a "strong" always modalityThe idea of a stronger always modality keeps coming up, so let's collect the arguments somewhere.
IMHO the main argument against it is that it would increase the number of modalities of the base logic by 33%. In other words, the default...The idea of a stronger always modality keeps coming up, so let's collect the arguments somewhere.
IMHO the main argument against it is that it would increase the number of modalities of the base logic by 33%. In other words, the default should be not to add anything unless we really need it -- and we got pretty far without the strong always.
So what do we have that this would enable? (I am writing "SB" for the strong box below.)
* Propositional extensionality. Not sure how useful that would be though.
* `(|=> SB P) -> SB P`, i.e. basic updates can be removed around the strong box. That seems pretty powerful, but the only application we have so far is to make the adequacy lemma nicer to state (no more "nested laters and basic updates", but just "nested laters").
* It would be possible to have the "core of a proposition" in a clean way, defined as `∀ Q, SB (Q -> □Q) -> SB (P -> Q) → □ Q`. This works because `SB P -> □ Q` is persistent.
@robbertkrebbers I seem to remember you saying that one of the Iris-based papers added the strong box. Why again did they need it?
I am not convinced that the above is enough of a reason to add the box to the core. In particular, I feel like it would be non-trivial to explain to people why we have two box-like modalities.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/141Make `iNext` smarter for mixed `▷` and `▷^n`2018-01-27T16:11:56ZRobbert KrebbersMake `iNext` smarter for mixed `▷` and `▷^n`See below:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n : ▷ ▷^n P ⊢ ▷^n ▷ P.
Proof. iIntros "H". iNext.
(* Gives
"H" : ▷ ▷^n P
--------------------------------------∗
▷ P
*)
```See below:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n : ▷ ▷^n P ⊢ ▷^n ▷ P.
Proof. iIntros "H". iNext.
(* Gives
"H" : ▷ ▷^n P
--------------------------------------∗
▷ P
*)
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/116A tactical for applying tactics to individual proof mode hypotheses2018-01-24T15:27:28ZRobbert KrebbersA tactical for applying tactics to individual proof mode hypothesesFor example, so that you can perform a `rewrite` or `simpl` in just one proof mode hypothesis.
Ssreflect also has such a tactical.For example, so that you can perform a `rewrite` or `simpl` in just one proof mode hypothesis.
Ssreflect also has such a tactical.Robbert KrebbersRobbert Krebbershttps://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/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 Jourdan