Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2023-02-02T17:27:43Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/507Non-fresh identifiers in intro patterns sometimes turn the goal unprovable in...2023-02-02T17:27:43ZLennard Gähergaeher@mpi-sws.orgNon-fresh identifiers in intro patterns sometimes turn the goal unprovable instead of generating an error messageOn latest Iris master (Coq 8.16.1), I am encountering the following error:
```
From iris Require Import base.
From iris.heap_lang Require Import proofmode.
Local Lemma bla `{!heapGS Σ} :
(True : iProp Σ) -∗
(True ∗ True) -∗ True.
...On latest Iris master (Coq 8.16.1), I am encountering the following error:
```
From iris Require Import base.
From iris.heap_lang Require Import proofmode.
Local Lemma bla `{!heapGS Σ} :
(True : iProp Σ) -∗
(True ∗ True) -∗ True.
Proof.
iIntros "Ha Hc".
iDestruct "Hc" as "(%Ha & Ha)".
(* goal becomes False *)
Abort.
```
It seems like the check for freshness sometimes fails to generate an error message.
Changing the second line of the proof script to `iDestruct "Hc" as "(Hd & Ha)".` correctly generates an error message.https://gitlab.mpi-sws.org/iris/iris/-/issues/462iRewrite with a Coq-level equality gives bad error message2022-05-20T17:14:58ZRalf Jungjung@mpi-sws.orgiRewrite with a Coq-level equality gives bad error messageIn a lambdaRust proof, I tried `iRewrite tctx_hasty_val in "Ha''".`. I had forgotten that `iRewrite` is for internal equalities only. That shows this error:
```
Error: No matching clauses for match.
```
This error is always a bug, at le...In a lambdaRust proof, I tried `iRewrite tctx_hasty_val in "Ha''".`. I had forgotten that `iRewrite` is for internal equalities only. That shows this error:
```
Error: No matching clauses for match.
```
This error is always a bug, at least the tactic should tell me what is wrong. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/458Inconsistency in weakening of modalities in `iApply`2022-05-01T11:54:32ZRobbert KrebbersInconsistency in weakening of modalities in `iApply````coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens...```coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens is that the first (and failing) `iApply` directly attempts to find an `IntoWand` instance to match the conclusion of the wand with the goal. This fails because the only applicable `IntoWand` instance is:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
There is no `FromAssumption` for `Q`, so no weakening of the conclusion is performed.
In the second attempt, `iApply` will first `iSpecialize` with the wand. As such, it tries to find an `IntoWand` instance where the conclusion can be unified with an evar. Then after that, it will use `iAssumption`, which uses `FromAssumption` to weaken the modality.
## Solution
We probably should add `FromAssumption` to instances like `into_wand_wand`. I do not know if this was just an omission, or there's a reason for that. Should try.https://gitlab.mpi-sws.org/iris/iris/-/issues/413Better errors when tactic fails to automatically resolve some side-condition2021-07-22T12:54:29ZRalf Jungjung@mpi-sws.orgBetter errors when tactic fails to automatically resolve some side-condition@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as `iMod` with mismatching masks:
1. `ElimModal` already has support for a pure side-conditio...@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as `iMod` with mismatching masks:
1. `ElimModal` already has support for a pure side-condition; we could introduce something like
```
Definition pm_error (s : string) := False
```
and add instances with `error "foo"` as their side-condition; together with some support in `iSolveSideCondition` this could be used to then show better, instance-specific error messages when `iMod` fails.
2. We could add a new typeclass like `ElimModalError` that is used to compute an error message when `ElimModal` failed to find an instance.
Since this is used for diagnostics only, there are no backwards compatibility concerns -- so I feel like we should start with the first approach, since it is easy to implement; we can always switch to something more principled later.https://gitlab.mpi-sws.org/iris/iris/-/issues/411Taking ∃ out of ▷ without Inhabited, more easily2021-04-29T09:25:44ZYusuke MatsushitaTaking ∃ out of ▷ without Inhabited, more easilyIn Iris Proof Mode, destruction of `▷ (∃ (x: A), Φ a)` into `(x) "H"` (where `"H"` will assert `▷ Φ x`) always requires `Inhabited A`, because it uses the lemma `later_exist`.
In some situations, `Inhabited A` is not known a priori.
If w...In Iris Proof Mode, destruction of `▷ (∃ (x: A), Φ a)` into `(x) "H"` (where `"H"` will assert `▷ Φ x`) always requires `Inhabited A`, because it uses the lemma `later_exist`.
In some situations, `Inhabited A` is not known a priori.
If we use the lemma `later_exist_except_0` instead, we get `▷ Φ x` without having `Inhabited A`, under the `◇` modality.
In Iris we are often under the `◇` modality because the update modality `|=>` contains `◇`.
I hope the operation of taking `∃x` out of `▷` without `Inhabited` becomes easier to use.
One possibility is to let Iris Proof Mode apply `later_exist_except_0` when the goal is under the `◇` modality.https://gitlab.mpi-sws.org/iris/iris/-/issues/402iFrame performance issues2022-05-06T12:56:32ZRalf Jungjung@mpi-sws.orgiFrame performance issuesThere are some situations where iFrame is rather slow.
- For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into ...There are some situations where iFrame is rather slow.
- For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into disjunctions at all by default?
- Also, @tchajed noticed that `iFrame` is doing a lot of `AsFractional` everywhere, which might also be a too expensive default -- this is tracked separately in https://gitlab.mpi-sws.org/iris/iris/-/issues/351.
- Cc https://gitlab.mpi-sws.org/iris/iris/-/issues/183 for the general "power vs performance" tradeoff in `iFrame`.
- https://gitlab.mpi-sws.org/iris/iris/-/issues/434 for diverging iFrame because Hint Mode is accidentally being circumvented.https://gitlab.mpi-sws.org/iris/iris/-/issues/397`iRename` fails with bad error message when not in proof mode2021-02-17T08:48:22ZRobbert Krebbers`iRename` fails with bad error message when not in proof mode```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
wit...```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
with "True".
```
The tactic probably does not call `iStartProof` at the beginning.https://gitlab.mpi-sws.org/iris/iris/-/issues/396Intro pattern `>` has wrong behavior with side-conditions of `iMod`2021-04-29T09:25:46ZRobbert KrebbersIntro pattern `>` has wrong behavior with side-conditions of `iMod````coq
Section atomic.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
(* These tests check if a side-condition for [Atomic] is generated *)
Check "wp_iMod_fupd_atomic".
Lemma wp_iMod_fupd_atomic E1 E2 P :
(|={E1,E2}=> ...```coq
Section atomic.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
(* These tests check if a side-condition for [Atomic] is generated *)
Check "wp_iMod_fupd_atomic".
Lemma wp_iMod_fupd_atomic E1 E2 P :
(|={E1,E2}=> P) -∗ WP #() #() @ E1 {{ _, True }}.
Proof.
iIntros ">H".
```
fails with
```
In environment
Σ : gFunctors
heapG0 : heapG Σ
E1, E2 : coPset
P : iProp Σ
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11809)
(environments.env_spatial ?M11809) ?M11814"
with
"∀ (σ : language.state heap_lang) (e' : language.expr heap_lang) (κ :
list
(language.observation
heap_lang))
(σ' : language.state heap_lang) (efs : list (language.expr heap_lang)),
language.prim_step (#() #()) σ κ e' σ' efs
→ match stuckness_to_atomicity NotStuck with
| StronglyAtomic => is_Some (language.to_val e')
| WeaklyAtomic => irreducible e' σ'
end".
```
See also https://mattermost.mpi-sws.org/iris/pl/r47q3gcq4fddxnhpddj91yb1wyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/380iDestruct does not handle some patterns that it probably could2020-11-11T16:57:53ZTej Chajedtchajed@gmail.comiDestruct does not handle some patterns that it probably couldThe pattern match in `iDestructHypGo` misses a handful of patterns that perhaps it could process. For example `IDone` could probably be given a sensible interpretation.
Similarly `iDestructHypFindPat` complains about `H //` even though ...The pattern match in `iDestructHypGo` misses a handful of patterns that perhaps it could process. For example `IDone` could probably be given a sensible interpretation.
Similarly `iDestructHypFindPat` complains about `H //` even though that could be processed as `iDestruct ... as H; done`. It does handle `H /=` (by running `simpl` after the destruct).https://gitlab.mpi-sws.org/iris/iris/-/issues/359Use the IPM to prove some example IPM extension theorems2020-10-21T11:00:32ZTej Chajedtchajed@gmail.comUse the IPM to prove some example IPM extension theoremsThe current proofs for some HeapLang tactics use a bunch of separation logic theorems manually, like this proof:
```coq
Lemma tac_wp_free Δ Δ' s E i K l v Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
...The current proofs for some HeapLang tactics use a bunch of separation logic theorems manually, like this proof:
```coq
Lemma tac_wp_free Δ Δ' s E i K l v Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
(let Δ'' := envs_delete false i false Δ' in
envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})) →
envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ? Hlk Hfin.
rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
apply later_mono, sep_mono_r, wand_intro_r. rewrite right_id //.
Qed.
```
It would be much nicer to use the proof mode to do these proofs, which is also nicely circular because we're extending the proof mode using the proof mode. For example, the above proof can be written:
```coq
rewrite envs_entails_eq=> ? Hlk Hfin.
rewrite into_laterN_env_sound.
iIntros "HΔ'".
iApply wp_bind.
pose proof (envs_lookup_sound' _ false _ _ _ Hlk) as HΔ'split.
set (Δ'':=envs_delete false i false Δ') in *.
iDestruct (HΔ'split with "HΔ'") as "[Hl HΔ'']".
iApply (wp_free with "Hl").
iNext. iIntros "_".
iApply (Hfin with "HΔ''").
```
This proof isn't shorter but you can figure out how to write such a proof using only the proof mode rather than convoluted uses of theorems like `sep_mono_r` and `wand_intro_r`. This particular case become slightly messier because if you do `iDestruct envs_lookup_sound with "HΔ'"` then the proof mode reduces `envs_delete` and the result is horrendous.
I don't think we need to re-do all of the proofs; I'm thinking having a few such examples would go a long way as examples that demonstrate how to extend the IPM in a nice way. We couldn't port all of the theorems anyway since of course some of these theorems are actually used to implement the IPM.https://gitlab.mpi-sws.org/iris/iris/-/issues/331simpl breaks error checking of `iNext (S i)`2020-07-14T08:21:09ZPaolo G. Giarrussosimpl breaks error checking of `iNext (S i)`I'd expect `iNext (S i)` to introduce exactly `S i` later, and fail otherwise. However, after e.g. `simpl` turns `▷^(S i) P` into `▷ ▷^i P`, that will sometimes introduce _one_ later, as shown below.
```coq
From iris.proofmode Require I...I'd expect `iNext (S i)` to introduce exactly `S i` later, and fail otherwise. However, after e.g. `simpl` turns `▷^(S i) P` into `▷ ▷^i P`, that will sometimes introduce _one_ later, as shown below.
```coq
From iris.proofmode Require Import tactics.
Lemma foo i {PROP} P : P ⊢@{PROP} ▷^(S i) P.
Proof.
iIntros "H".
Fail iNext 2.
iNext (S i).
Fail iNext i.
Fail iNext.
iExact "H".
Restart.
iIntros "H /=".
Fail iNext 2.
iNext (S i).
iNext i. (* !!! *)
Abort.
```
### Iris version
```
$ opam show coq-iris -f version
dev.2020-05-24.2.af5e50e7
```
with Coq 8.11.1.https://gitlab.mpi-sws.org/iris/iris/-/issues/330Consider adding `iEnough` variants of `iAssert` ?2020-06-26T07:35:15ZPaolo G. GiarrussoConsider adding `iEnough` variants of `iAssert` ?Something like:
```coq
Tactic Notation "iEnough" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssert Q with Hs as pat; first last.
Tactic Notation "iEnough" open_constr(Q) "as" constr(pat) :=
iAssert Q as pat; first ...Something like:
```coq
Tactic Notation "iEnough" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssert Q with Hs as pat; first last.
Tactic Notation "iEnough" open_constr(Q) "as" constr(pat) :=
iAssert Q as pat; first last.
```
The point is just readability, and adding all the overloads is probably not worth it, but maybe this would change with an Ltac2 proofmode?https://gitlab.mpi-sws.org/iris/iris/-/issues/317Use `byte` based strings for proof mode2020-05-16T19:16:11ZRobbert KrebbersUse `byte` based strings for proof modeNewer versions of Coq have a type `byte` with 256 constructors. We could use strings based on `byte` in the proofmode. Maybe that gives a significant speed up compared to the current `ascii` based strings.
@tchajed said the construction...Newer versions of Coq have a type `byte` with 256 constructors. We could use strings based on `byte` in the proofmode. Maybe that gives a significant speed up compared to the current `ascii` based strings.
@tchajed said the construction of `byte` based strings does not exist in the Coq stdlib but can be defined as:
```
From Coq Require Import Init.Byte.
Record bytes := bytes_from_list { bytes_to_list : list byte }.
Declare Scope bytestring_scope.
Open Scope bytestring_scope.
String Notation bytes bytes_from_list bytes_to_list : bytestring_scope.
Definition foo : bytes := "foo".
```https://gitlab.mpi-sws.org/iris/iris/-/issues/295Have iApply introduce equalities for subterms that cannot be unified directly2020-08-08T21:57:49ZArmaël GuéneauHave iApply introduce equalities for subterms that cannot be unified directlyThe initial motivation is to be able to go from a proof-mode goal of the form:
```
"H" : r ↦ (x, x0, x1, x2, x4)
--------------------------------------∗
r ↦ (x, x0, x1, x2, z)
```
to
```
--------------------------------------∗
⌜x4 ...The initial motivation is to be able to go from a proof-mode goal of the form:
```
"H" : r ↦ (x, x0, x1, x2, x4)
--------------------------------------∗
r ↦ (x, x0, x1, x2, z)
```
to
```
--------------------------------------∗
⌜x4 = z⌝
```
without relying explicitly on the names `x4` and `z`.
I'm not sure what would be the most general form of such a tactic, or what its user interface would be, though. I think it would be nice to have it as an instance of `iApply`, if that's possible. (having it in `iFrame` as well is perhaps possible but risky, for instance in the case of mapsto it should at least be restricted to mapsto with the same syntactic location...).https://gitlab.mpi-sws.org/iris/iris/-/issues/290Possible redesign of handling of persistent/intuitionistic propositions in in...2020-02-11T17:35:16ZRalf Jungjung@mpi-sws.orgPossible redesign of handling of persistent/intuitionistic propositions in intro patternsAt https://gitlab.mpi-sws.org/iris/iris/merge_requests/370#note_43784 we had some discussion about possible re-designs of the handling of persistent/intuitionistic propositions (when `#` is needed and when not) with the goal of being mor...At https://gitlab.mpi-sws.org/iris/iris/merge_requests/370#note_43784 we had some discussion about possible re-designs of the handling of persistent/intuitionistic propositions (when `#` is needed and when not) with the goal of being more consistent. That was put on hold for now due to being too much work and likely also breaking many things; the issue here tracks possibly doing at least some of that in the future if we want to improve the situation around the `#` pattern (and its opt-out version, whatever that will be).https://gitlab.mpi-sws.org/iris/iris/-/issues/287iApply strips some modalities, but not monotonically2020-02-01T13:06:32ZPaolo G. GiarrussoiApply strips some modalities, but not monotonicallyHere's a minimized inconsistent behavior and a possible fix via an instance. I suspect *that* instance is missing by design, but I can't tell what the design is, even tho I can read `Hint Mode` — see #139.
(I also realize that such insta...Here's a minimized inconsistent behavior and a possible fix via an instance. I suspect *that* instance is missing by design, but I can't tell what the design is, even tho I can read `Hint Mode` — see #139.
(I also realize that such instances must appear for either all or none of the monotonic modalities).
```coq
From iris.proofmode Require Import tactics.
From iris.bi Require Import bi.
Import bi.
Section sbi_instances.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
(* Here [iApply] works. *)
Lemma foo0 P : □ P -∗ P.
Proof. iIntros "H". iApply "H". Qed.
(* But here it fails! *)
Lemma foo1 P : ▷ □ P -∗ ▷ P.
Proof. iIntros "H". Fail iApply "H". iNext. iApply "H". Qed.
(* Here's a possible fix, but I'm unsure whether it respects the interplay of
FromAssumption, KnownLFromAssumption and KnownRFromAssumption,
as it is not fully documented.
Should I add this for both KnownLFromAssumption and KnownRFromAssumption? *)
Global Instance from_assumption_later_later p P Q :
FromAssumption p P Q → FromAssumption p (▷ P) (▷ Q)%I.
Proof.
rewrite /KnownRFromAssumption /FromAssumption
later_intuitionistically_if_2 => ->. exact: later_mono.
Qed.
Lemma foo P : ▷ □ P -∗ ▷ P.
Proof. iIntros "H". iApply "H". Qed.
End sbi_instances.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/275use implicit arguments for lemmas in coq_tactics.v2019-11-22T16:30:29ZPaolo G. Giarrussouse implicit arguments for lemmas in coq_tactics.v- [ ] The following [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/338#note_42171) from !338 should be addressed:
> > I was tempted to use implicit arguments instead of (some of) these underscores to make the `refi...- [ ] The following [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/338#note_42171) from !338 should be addressed:
> > I was tempted to use implicit arguments instead of (some of) these underscores to make the `refine` more readable... does that cause problems? [@Blaisorblade]
> I have been thinking about this many times. However, we should not just do it locally here, but should do it globally for all proof mode tactics. First let's get #135 fixed and then do what you suggest. [@robbertkrebbers]https://gitlab.mpi-sws.org/iris/iris/-/issues/268`iInv`: support tokens that are "framed" around the accessor2020-03-18T15:01:32ZDan Frumin`iInv`: support tokens that are "framed" around the accessorI have cancellable invariant and `cinv_own` token in a proposition "Hp", then usually I don't want to touch "Hp" when opening an invariant. However, if I use `iInv` I have to explicitly name "Hp" again:
```
iInv N with "Hp" as "[H Hp]" ...I have cancellable invariant and `cinv_own` token in a proposition "Hp", then usually I don't want to touch "Hp" when opening an invariant. However, if I use `iInv` I have to explicitly name "Hp" again:
```
iInv N with "Hp" as "[H Hp]" "Hcl"
```
This also prevents me from using the `(x1 x2) "..."` introduction pattern. E.g. instead of
```
iInv N with "Hp" as (x) "[H1 H2]" "Hcl"
```
one has to write
```
iInv N with "Hp" as "[H Hp]" "Hcl";
iDestruct "H" as (x) "[H1 H2]"
```
It is not immediately obvious how to modify the tactics, because in general the `selpat` in `iInv N with selpat` can be an arbitrary selection pattern and not just one identifier.https://gitlab.mpi-sws.org/iris/iris/-/issues/241"Flattened" introduction patterns for intuitionistic conjunction elimination.2019-11-01T13:07:29ZDan Frumin"Flattened" introduction patterns for intuitionistic conjunction elimination.The "flattened" introduction patterns (I don't know the official terminology, but I meant the patterns like `(H1 & H2 & H3 &H4)`) interact in a weird way with intuitionistic conjunction:
In particular, I would expect to get a `P` from `...The "flattened" introduction patterns (I don't know the official terminology, but I meant the patterns like `(H1 & H2 & H3 &H4)`) interact in a weird way with intuitionistic conjunction:
In particular, I would expect to get a `P` from `P ∧ Q ∧ R` by `iDestruct "H" as "(H&_&_)"`, but it doesn't work this way.
```
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic.
Section base_logic_tests.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
Lemma test P Q R : (P ∧ Q ∧ R) -∗ P.
Proof.
iIntros "H".
(* This works fine *)
iDestruct "H" as "(_ & _ & H)".
Undo.
iDestruct "H" as "(_ & H & _)".
Undo.
(* This results in an error *)
Fail iDestruct "H" as "(H & _ & _)".
(* "Proper" way of doing it *)
iDestruct "H" as "(H & _)".
done.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/216Replace most occurences of `.. || ..` by `first [..|..]`2021-02-02T16:14:57ZRobbert KrebbersReplace most occurences of `.. || ..` by `first [..|..]`Today I found out, as described [in the Coq documentation](https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html#left-biased-branching), that the behavior of `e1 || e2` in Ltac is not what I expected. It will execute `e2` no...Today I found out, as described [in the Coq documentation](https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html#left-biased-branching), that the behavior of `e1 || e2` in Ltac is not what I expected. It will execute `e2` not just when `e1` fails, but also when it does not make any progress.
This problem came up when debugging an issue reported by YoungJu Song on Mattermost. He noticed that the `wp_bind` tactic does not work when one tries to bind the top-level term. The code of `wp_bind` contains:
```coq
reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
|| fail "wp_bind: cannot find" efoc "in" e
```
`wp_bind_core` is special casing the context `[]`, and then performs just an `idtac` instead of actually using the bind rule for WP.