Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-02-05T19:04:27Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/282Undesired simplification behaviour of big_sepM22020-02-05T19:04:27ZMichael SammlerUndesired simplification behaviour of big_sepM2Iris version: dev.2019-11-22.2.a979391c
`simpl` unfolds the definition of `big_sepM2` which makes it basically unusable.
Example:
```coq
From iris.program_logic Require Import weakestpre.
Example big_sepM2_simpl Σ (xs ys : gmap nat na...Iris version: dev.2019-11-22.2.a979391c
`simpl` unfolds the definition of `big_sepM2` which makes it basically unusable.
Example:
```coq
From iris.program_logic Require Import weakestpre.
Example big_sepM2_simpl Σ (xs ys : gmap nat nat):
([∗ map] x;y ∈ xs;ys, ⌜x=y⌝ : iProp Σ)%I.
Proof. simpl. Abort.
(* => uPred_and ⌜∀ k : nat, is_Some (xs !! k) ↔ is_Some (ys !! k)⌝
([∗ map] xy ∈ map_zip xs ys, ⌜xy.1 = xy.2⌝%I) *)
```
I am currently using the following workaround (`big_sepM2` does not seem to have an `Arguments` command at the moment):
```coq
Arguments big_sepM2 {PROP K _ _ A B} _ !_ !_ /.
Example big_sepM2_simpl Σ (xs ys : gmap nat nat):
([∗ map] x;y ∈ xs;ys, ⌜x=y⌝ : iProp Σ)%I.
Proof. simpl. Abort.
(* => ([∗ map] x;y ∈ xs;ys, ⌜x = y⌝)%I *)
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/281proof_mode.md documentation has a broken link2019-12-19T19:14:39ZJules Jacobsproof_mode.md documentation has a broken linkproofmode.md's link to the heaplang tactics file is broken.
Also, the example of iIntros seems to show deprecated !# instead of !>, and Hx instead of x.proofmode.md's link to the heaplang tactics file is broken.
Also, the example of iIntros seems to show deprecated !# instead of !>, and Hx instead of x.https://gitlab.mpi-sws.org/iris/iris/-/issues/279Editor bindings for Emacs and m17n are inconsistent2020-02-11T08:40:22ZTej Chajedtchajed@mit.eduEditor bindings for Emacs and m17n are inconsistentThe list of bindings for Emacs in [editor.md](docs/editor.md) is missing a bunch of useful bindings for superscripts/subscripts and a rule for ö (for typing Löb) that are in the config for m17n. We should make both lists consistent by ta...The list of bindings for Emacs in [editor.md](docs/editor.md) is missing a bunch of useful bindings for superscripts/subscripts and a rule for ö (for typing Löb) that are in the config for m17n. We should make both lists consistent by taking the union of the bindings.https://gitlab.mpi-sws.org/iris/iris/-/issues/274Regression after !329 on recursive proofs2019-12-02T14:10:16ZPaolo G. GiarrussoRegression after !329 on recursive proofsHere's a self-contained testcase:
```coq
From iris.proofmode Require Import tactics.
Section testcase.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Fixpoint test_fixpoint (n : nat) {struct n} : emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝%I.
...Here's a self-contained testcase:
```coq
From iris.proofmode Require Import tactics.
Section testcase.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Fixpoint test_fixpoint (n : nat) {struct n} : emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝%I.
Proof.
case: n => [|n] /=.
- iIntros "_ !%". reflexivity.
- iIntros "_".
(* Works *)
(* by iDestruct (test_fixpoint n with "[//]") as %->. *)
(* Fails *)
by iDestruct (test_fixpoint with "[//]") as %->.
Qed.
```
This testcase is silly, but recursive proofs for mutually recursive lemmas can make sense, especially when the proof uses a custom induction scheme that is only used once: proving it by hand has advantages, especially for automation, but can create more boilerplate than a recursive proof.
I tried out a suggestion from @robbertkrebbers, got it to work and will send a MR shortly, but I expect the result should be achieved otherwise.https://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/270non-Unicode Iris notations2020-04-07T13:59:09ZRalf Jungjung@mpi-sws.orgnon-Unicode Iris notationsSome people askedd about a non-Unicode variant of our notation. @jihgfee @gmalecha have such a file I think, maybe we could contribute that upstream?Some people askedd about a non-Unicode variant of our notation. @jihgfee @gmalecha have such a file I think, maybe we could contribute that upstream?https://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/266`iDestruct 1` does not work when `Z_scope` is open2019-09-20T12:30:26ZJacques-Henri Jourdan`iDestruct 1` does not work when `Z_scope` is openIn this case, we have to write `iDestruct 1%nat`. It would be perfect to add the tactic notation for Z, too.In this case, we have to write `iDestruct 1%nat`. It would be perfect to add the tactic notation for Z, too.https://gitlab.mpi-sws.org/iris/iris/-/issues/265Add an "iStopProof" tactic2019-09-11T14:48:57ZJonas KastbergAdd an "iStopProof" tacticThere is currently no tactic to escape the IPM.
This make it so that pre-existing tactics that have been developed for the logic can no longer be used, once you are in the proof mode.
This is applicable assuming that someone migrates to ...There is currently no tactic to escape the IPM.
This make it so that pre-existing tactics that have been developed for the logic can no longer be used, once you are in the proof mode.
This is applicable assuming that someone migrates to IPM from an existing development, and want to keep being able to use their tactics, in-between progress made with IPM.
A WIP solution is as follows:
```
Lemma stop_proof {PROP : bi} c (P : PROP) :
P ->
environments.envs_entails
{|
environments.env_intuitionistic := environments.Enil;
environments.env_spatial := environments.Enil;
environments.env_counter := c |} P.
Proof. rewrite environments.envs_entails_eq. iIntros. iApply H. Qed.
Ltac iStopProof := apply stop_proof.
Ltac iStopProof' := iRevert "#∗"; iStopProof.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/263IPM/MoSeL nested disjunction syntax2019-11-01T13:02:01ZDan FruminIPM/MoSeL nested disjunction syntaxWould it be possible to support the following syntax for nested disjunctions:
`iDestruct H as (H|H|H)`? Similarly to the `(H1&H2&H3)` syntax for nested separating conjunctions.Would it be possible to support the following syntax for nested disjunctions:
`iDestruct H as (H|H|H)`? Similarly to the `(H1&H2&H3)` syntax for nested separating conjunctions.https://gitlab.mpi-sws.org/iris/iris/-/issues/260Confusing error message if iLoeb is not available (non-step indexed BI)2019-08-13T11:22:50ZDan FruminConfusing error message if iLoeb is not available (non-step indexed BI)Example code:
```
From iris.proofmode Require Import tactics.
Lemma test `{PROP : bi} (k : nat) (Φ : nat → PROP) :
Φ k -∗ Φ (S k).
Proof.
iLöb as "IH".
```
(PROP should have type `sbi`)
Error message:
```
In nested Ltac calls to...Example code:
```
From iris.proofmode Require Import tactics.
Lemma test `{PROP : bi} (k : nat) (Φ : nat → PROP) :
Φ k -∗ Φ (S k).
Proof.
iLöb as "IH".
```
(PROP should have type `sbi`)
Error message:
```
In nested Ltac calls to "iLöb as (constr)", "iLöbRevert (constr) with (tactic3)",
"iRevertIntros (constr) with (tactic3)", "go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
"∗" with tac), "iRevertIntros (constr) with (tactic3)",
"go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iLöbCore as IH), "tac" (bound to iLöbCore as IH),
"iLöbCore as (constr)" and "notypeclasses refine (uconstr)", last call failed.
In environment
PROP : bi
k : nat
Φ : nat → PROP
The term "coq_tactics.tac_löb ?Δ "IH" ?Q ?e ?y" has type
"environments.envs_entails ?Δ ?Q" while it is expected to have type
"--------------------------------------∗
Φ k -∗ Φ (S k)
".
```
I don't know if it is even possible, but it would be nice to detect this error and emit a nicer message.https://gitlab.mpi-sws.org/iris/iris/-/issues/259Confusing error message from iLoeb: `Variable x should be bound to a term but...2019-08-13T11:07:52ZDan FruminConfusing error message from iLoeb: `Variable x should be bound to a term but is bound to a ident.`Example code:
```
From iris.proofmode Require Import tactics.
Lemma test `{PROP : sbi} (k : nat) (Φ : nat → PROP) :
Φ k -∗ Φ (S k).
Proof.
iLöb as "IH" forall (k1).
```
(notice that `k1` should be `k` in the `forall` clause)
It fa...Example code:
```
From iris.proofmode Require Import tactics.
Lemma test `{PROP : sbi} (k : nat) (Φ : nat → PROP) :
Φ k -∗ Φ (S k).
Proof.
iLöb as "IH" forall (k1).
```
(notice that `k1` should be `k` in the `forall` clause)
It fails with a cryptic message:
```
Error:
In nested Ltac calls to "iLöb as (constr) forall ( (ident) )",
"iLöbRevert (constr) with (tactic3)", "iRevertIntros (constr) with (tactic3)",
"go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
"∗" with tac), "iRevertIntros (constr) with (tactic3)",
"go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as IH),
"tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as IH),
"iRevertIntros ( (ident) ) (constr) with (tactic3)",
"iRevertIntros (constr) with (tactic3)", "go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )),
"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )), "iRevert ( (ident) )",
"iForallRevert (ident)" and "x" (with IH:="IH", Hs:=""), last term evaluation
failed.
Variable x should be bound to a term but is bound to a ident.
```
What's bit strange is that the identifier `x` is not used in the code.https://gitlab.mpi-sws.org/iris/iris/-/issues/258Stronger `list_core_id`2020-03-18T15:00:32ZDmitry KhalanskiyStronger `list_core_id`Hi!
I needed a stronger version of `list_core_id` that could depend on the structure of a particular list, similarly to `pair_core_id`. I came up with this:
```
Global Instance list_core_id l : (forall x, x ∈ l -> CoreId x) -> CoreId ...Hi!
I needed a stronger version of `list_core_id` that could depend on the structure of a particular list, similarly to `pair_core_id`. I came up with this:
```
Global Instance list_core_id l : (forall x, x ∈ l -> CoreId x) -> CoreId l.
Proof.
intros Hyp. constructor. apply list_equiv_lookup=> i.
rewrite list_lookup_core.
destruct (l !! i) eqn:E.
2: done.
apply Hyp.
eapply elem_of_list_lookup; by eauto.
Qed.
```
It probably could serve as a drop-in replacement for the old one.https://gitlab.mpi-sws.org/iris/iris/-/issues/257Auth as Views2020-10-01T19:57:53ZRalf Jungjung@mpi-sws.orgAuth as ViewsGregory [suggested](https://lists.mpi-sws.org/pipermail/iris-club/2019-July/000198.html) a generalization of "Auth" that, in hindsight, seems blatantly obvious: make the authoritative and the fragment not the same type, and let the user ...Gregory [suggested](https://lists.mpi-sws.org/pipermail/iris-club/2019-July/000198.html) a generalization of "Auth" that, in hindsight, seems blatantly obvious: make the authoritative and the fragment not the same type, and let the user pick some relation between them. I think it can truly be any (Coq-level) relation for discrete types; for the CMRA variant we likely need a step-indexed relation. The existing "auth" is then the special case of using the same type, and equality as the relation.
This subsumes https://gitlab.mpi-sws.org/iris/iris/merge_requests/91 by making the relation also require bijectivity. And this also could be useful for situations where we have a very right CMRA for the fragments, which often means lots of "junk" data (such as `to_agree`, of `ExclBot`). So instead of the pattern where we do `exists heap, own (● to_auth heap)`, we could have this `to_auth` in the relation.
An open question is what would happen with all our theory about local updates.
Things to do:
* [ ] Implement a generalized "auth as view" library
* [ ] Implement monotone partial bijections (https://gitlab.mpi-sws.org/iris/iris/merge_requests/91) in terms of that.https://gitlab.mpi-sws.org/iris/iris/-/issues/256Consisent direction for `CMRA_NAME_op` lemmas.2019-08-13T16:01:57ZDan FruminConsisent direction for `CMRA_NAME_op` lemmas.I've noticed something which can be seen as a discrepancy in the lemmas.
These ones follow the pattern "constructor of the multiplication is equal to the multiplication of constructors".
```
Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ ...I've noticed something which can be seen as a discrepancy in the lemmas.
These ones follow the pattern "constructor of the multiplication is equal to the multiplication of constructors".
```
Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl.
```
These ones go the other way around: "multiplication of constructors is equal to the constructor of multiplications":
```
Lemma Cinl_op a a' : Cinl a ⋅ Cinl a' = Cinl (a ⋅ a').
Lemma Cinr_op b b' : Cinr b ⋅ Cinr b' = Cinr (b ⋅ b').
Lemma pair_op (a a' : A) (b b' : B) : (a, b) ⋅ (a', b') = (a ⋅ a', b ⋅ b').
```
Should this be changed or am I nitpicking and the (breaking) change will be too invasive?https://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/254Reliance on `Export` bug2019-11-01T12:48:48ZMaxime DénèsReliance on `Export` bugDear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is...Dear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is an easy way to observe the problem on Coq master: take `algebra.ufrac_auth`, and change the first line:
```coq
From iris.algebra Require Export auth frac.
```
into:
```coq
From iris.algebra Require Export auth.
From iris.algebra Require Export frac.
```
it will make the proof of `ufrac_auth_agreeN` fail because a view starts applying in the wrong direction...
Could you provide some guidance on how to make the file pass with the two separate `Export`s? It will probably make it compatible with the fix of the bug I mentioned above.
Thanks!https://gitlab.mpi-sws.org/iris/iris/-/issues/253Constructing CMRAs by giving isomorphism to CMRAs2020-11-06T14:41:47ZPaolo G. GiarrussoConstructing CMRAs by giving isomorphism to CMRAsIris has such a construction for OFEs, and @jung asked for one on CMRAs on chat (https://mattermost.mpi-sws.org/iris/pl/h9q6eeu3ojnxfcwr1w59z76jcr).Iris has such a construction for OFEs, and @jung asked for one on CMRAs on chat (https://mattermost.mpi-sws.org/iris/pl/h9q6eeu3ojnxfcwr1w59z76jcr).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/249Better solvers for properness/contractiveness2020-02-13T22:39:23ZPaolo G. GiarrussoBetter solvers for properness/contractivenesssolve_proper doesn't deal well with higher-order functions. Here's my home-grown variant:
```coq
(** An ad-hoc variant of solve_proper that seems to work better when defining
proper higher-order functions. In particular, using int...solve_proper doesn't deal well with higher-order functions. Here's my home-grown variant:
```coq
(** An ad-hoc variant of solve_proper that seems to work better when defining
proper higher-order functions. In particular, using intro allows showing that a
lambda abstraction is proper if its body is proper.
Its implementation can also prove [f1 x ≡ f2 x] from [H : f1 ≡ f2]:
neither f_equiv nor rewrite deal with that, but [apply H] does. *)
Ltac solve_proper_ho_core tac :=
solve [repeat (tac (); cbn); cbn in *;
repeat match goal with H : _ ≡{_}≡ _|- _ => apply H end].
Ltac solve_proper_ho := solve_proper_ho_core
ltac:(fun _ => f_equiv || intro).
Ltac solve_contractive_ho := solve_proper_ho_core
ltac:(fun _ => f_contractive || f_equiv || intro).
```
Should we have something like this in Iris/stdpp? There's some heuristic tuning involved, but I use this rather happily...