Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-07-01T14:46:59Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/248Comparison with `=` and with CAS is not the same2019-07-01T14:46:59ZRalf Jungjung@mpi-sws.orgComparison with `=` and with CAS is not the sameCurrently, `heap_lang` allows more things to be compared with `=` than with `CAS`: for the latter, one of the two values-to-be-compared has to be "unboxed", meaning that it is a literal or inl/inr of a literal. If this condition is not m...Currently, `heap_lang` allows more things to be compared with `=` than with `CAS`: for the latter, one of the two values-to-be-compared has to be "unboxed", meaning that it is a literal or inl/inr of a literal. If this condition is not met, the program is stuck.
@robbertkrebbers proposes that we should restrict `=` in a similar way. On the other hand, it is nice that `=` is a total operation currently.https://gitlab.mpi-sws.org/iris/iris/-/issues/247iInv does not behave as intended when the goal is an accessor2019-11-01T12:32:42ZRalf Jungjung@mpi-sws.orgiInv does not behave as intended when the goal is an accessorWhen the goal is of the form
```
|={⊤,∅}=> ∃ ..., P ∗ (Q ={∅,⊤}=∗ Φ )
```
I would hope `iInv N` where the invariant assertion is `I` to turn it into something like
```
|={N,∅}=> ∃ ..., P ∗ (I * Q ={∅,⊤}=∗ Φ )
```
but currently we have no...When the goal is of the form
```
|={⊤,∅}=> ∃ ..., P ∗ (Q ={∅,⊤}=∗ Φ )
```
I would hope `iInv N` where the invariant assertion is `I` to turn it into something like
```
|={N,∅}=> ∃ ..., P ∗ (I * Q ={∅,⊤}=∗ Φ )
```
but currently we have no good way to even detect the goal as an accessor, so none of this can happen.https://gitlab.mpi-sws.org/iris/iris/-/issues/246iEval (eauto) "corrupts" goal2019-06-15T11:43:47ZPaolo G. GiarrussoiEval (eauto) "corrupts" goalWhile I ran into !269, I also ended up learning that `iEval (eauto)` can "corrupt" the goal by calling `iStartProof` again:
```
1 subgoal
Σ : gFunctors
H : heapG Σ
c1, c2 : val
A1, A2, B1, B2 : lty Σ
v1, v2 : val
w2, w1 : ...While I ran into !269, I also ended up learning that `iEval (eauto)` can "corrupt" the goal by calling `iStartProof` again:
```
1 subgoal
Σ : gFunctors
H : heapG Σ
c1, c2 : val
A1, A2, B1, B2 : lty Σ
v1, v2 : val
w2, w1 : language.val heap_lang
============================
"HwB2" : B2 w2
"HwB1" : B1 w1
--------------------------------------∗
⌜--------------------------------------∗
(B1 * B2)%lty (w1, w2)%V
⌝
```
(from https://gitlab.mpi-sws.org/Blaisorblade/examples/commit/e9851f6#16adf89a84c96614a153a2ca8db8a92215d85db3_244_297).
Minimized version:
```
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
Lemma foo {Σ}: True ⊢ True : iProp Σ.
Proof.
iIntros.
iEval (info_eauto).
Show.
(*Equal to: *)
(* iEval (iStartProof; iPureIntro). *)
```
gives:
```
1 subgoal
Σ : gFunctors
a : True
============================
--------------------------------------∗
⌜?P⌝
```https://gitlab.mpi-sws.org/iris/iris/-/issues/245Add IntoAnd instance (and more) for array2019-08-13T11:19:53ZRodolphe LepigreAdd IntoAnd instance (and more) for arrayWe should add `IntoAnd` instances (and friends) for `array`.
This has been discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/267#note_37037).We should add `IntoAnd` instances (and friends) for `array`.
This has been discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/267#note_37037).Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/242Planning the Iris 3.2 release2019-11-01T12:31:44ZRalf Jungjung@mpi-sws.orgPlanning the Iris 3.2 releaseI have finally gotten around to update the documentation for the Iris 3.2 changes. Turns out that wasn't actually that much work as heap_lang is not part of the formal documentation.
That removes the last blocker for a new release! So I...I have finally gotten around to update the documentation for the Iris 3.2 changes. Turns out that wasn't actually that much work as heap_lang is not part of the formal documentation.
That removes the last blocker for a new release! So I think we should make that release soon-ish. Are there any issues or MRs that you think should be included? Let's collect them in [this milestone](https://gitlab.mpi-sws.org/iris/iris/milestones/4).
We might consider doing the release after the POPL deadline so that our Iris-using POPL submissions (if any) can claim to be compatible with Iris 3.2. But honestly I don't think that is a big factor, the artifacts should anyway bundle the right version of Iris -- and I'd rather avoid extra coordination overhead if possible.
After the release:
* [ ] Drop support for Coq 8.7, and enable the `sigT`-functor notation (at the bottom of `ofe.v`).Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/240We have ambiguous coercion paths2020-04-02T09:08:16ZRalf Jungjung@mpi-sws.orgWe have ambiguous coercion pathsWhen compiling with Coq master, we see lots of these:
```
[constRF; rFunctor_diag] : cmraT >-> Funclass
[ucmra_cmraR; constRF; rFunctor_diag] : ucmraT >-> Funclass
```
Also see e.g. [this build log](https://gitlab.mpi-sws.org/iris/iris/-...When compiling with Coq master, we see lots of these:
```
[constRF; rFunctor_diag] : cmraT >-> Funclass
[ucmra_cmraR; constRF; rFunctor_diag] : ucmraT >-> Funclass
```
Also see e.g. [this build log](https://gitlab.mpi-sws.org/iris/iris/-/jobs/31380).
Is this a problem? Can we do anything about it?https://gitlab.mpi-sws.org/iris/iris/-/issues/239Iris logo2021-02-05T12:43:21ZRobbert KrebbersIris logoWe need a logo for the project. The issue collects proposals so far:
By @janno:
![Janno](https://robbertkrebbers.nl/iris_logos/janno.jpg)
By @lgg:
![Janno](https://robbertkrebbers.nl/iris_logos/leon.jpg)
As @dreyer said: I think if ...We need a logo for the project. The issue collects proposals so far:
By @janno:
![Janno](https://robbertkrebbers.nl/iris_logos/janno.jpg)
By @lgg:
![Janno](https://robbertkrebbers.nl/iris_logos/leon.jpg)
As @dreyer said: I think if we all start singing I-R-I-S to the tune of YMCA, we'll really be getting somewherehttps://gitlab.mpi-sws.org/iris/iris/-/issues/238Wish: iSimpl on multiple hypothesis2019-05-22T22:53:15ZDan FruminWish: iSimpl on multiple hypothesis**A wish**: it would be nice if we could run `iSimpl` on several hypothesis: `iSimpl in "H1 H2"`.**A wish**: it would be nice if we could run `iSimpl` on several hypothesis: `iSimpl in "H1 H2"`.https://gitlab.mpi-sws.org/iris/iris/-/issues/237Stripping laterN from pure propositions when proving laterN *without except-0*2019-11-01T11:09:51ZPaolo G. GiarrussoStripping laterN from pure propositions when proving laterN *without except-0*I just proved that, for uniform predicates, when proving `▷^i Q`, you can strip `▷^i` from `"Hfoo": ▷^i ⌜ P ⌝`, for arbitrary uniform predicates. Statements:
`(⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.`
`(⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).`
I ...I just proved that, for uniform predicates, when proving `▷^i Q`, you can strip `▷^i` from `"Hfoo": ▷^i ⌜ P ⌝`, for arbitrary uniform predicates. Statements:
`(⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.`
`(⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).`
I needed this in my proof; could we add support for this in Iris? I'm not sending a MR because the code is far from ready for that.
Was this already possible? I didn't find how, and thought this would need some new variant of except-0 (an except-i modality).
- IPM suggested that wouldn't work — `iDestruct "Hfoo" as "%"` complains that `Hfoo` is not pure, even when the conclusion starts with `▷^i`.
- The proof is by case distinction on the world: in worlds `n < i`, the conclusion is trivial, while in worlds `n >= i`, we have that `▷^i ⌜ P ⌝ → P`. This must be done in the model.
My proof is easy for later, but laterN was trickier; I'm also not sure where this proof would go (since laterN is a derived connective, but the proof for laterN goes in the model).
I expect one could lift this lemma to wand as well (since `▷^i ⌜ P ⌝` is persistent, this shouldn't need going to the model).
- These lemmas are also a bit inconvenient to use; it's not clear that `IntoPure` supports such conditional tactics. A typical example, for hypothesis "Hlclw": ▷^i ⌜ nclosed_vl w 0 ⌝, is:
```
iApply (strip_pure_laterN i with "[] Hlclw").
iIntros (Hclw).
```
`iRevert "Hlclw"; iApply strip_pure_wand_laterN; iIntros (Hclw)` might also work, given a version for wand.
My proof script is:
```coq
From iris.base_logic Require Import base_logic lib.iprop.
Import uPred.
Section uPred_later_extra.
Context `{M: ucmraT}.
Implicit Types (Q: uPred M) (x: M).
Lemma laterN_pure_id i n P x: i <= n →
(▷^i uPred_pure_def P)%I n x → P.
Proof.
move => Hle H; induction i => //=.
apply IHi; first lia.
elim: i n Hle H {IHi} => [|i IHi] [|n] Hle;
unseal => // H; first lia.
apply IHi; first lia. by unseal.
Qed.
Lemma laterN_trivial i n Q x: i > n →
(▷^i Q)%I n x.
Proof.
move: i => [|i] Hle. by lia.
apply uPred_mono with i x; eauto with lia.
elim: i {Hle}; by unseal.
Qed.
Lemma strip_pure_later P Q:
(⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).
Proof.
unseal; constructor => n x Hvx Hyp [|n'] // ?????.
by apply Hyp.
Qed.
Lemma strip_pure_laterN i P Q:
(⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.
Proof.
unseal; constructor => n x Hvx Hyp n' //= x' ?? Hvx' H.
destruct (decide (i <= n')) as [Hle|Hge].
- by eapply Hyp, laterN_pure_id.
- by apply laterN_trivial; lia.
Qed.
End uPred_later_extra.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/236Non-expansiveness for big ops2020-03-19T11:07:23ZDan FruminNon-expansiveness for big opsA wish:
non-expansiveness for the big_op operations, e.g.
```
[∗ map] k ↦ x ∈ m, Φ k x
```
is non-expansive in `m`, if `m` is a gmap into an OFEA wish:
non-expansiveness for the big_op operations, e.g.
```
[∗ map] k ↦ x ∈ m, Φ k x
```
is non-expansive in `m`, if `m` is a gmap into an OFEhttps://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/233Can't install on Coq 8.8.12019-03-20T08:40:16ZMaximilian WuttkeCan't install on Coq 8.8.1Hi,
I want to try out Iris, but `opam install coq-iris` yields this this:
```
#=== ERROR while compiling coq-iris.dev.2019-03-14.3.2d1c8352 ================#
# context 2.0.0~beta5 | linux/x86_64 | coq.8.8.1 | git+https://gitlab.mp...Hi,
I want to try out Iris, but `opam install coq-iris` yields this this:
```
#=== ERROR while compiling coq-iris.dev.2019-03-14.3.2d1c8352 ================#
# context 2.0.0~beta5 | linux/x86_64 | coq.8.8.1 | git+https://gitlab.mpi-sws.org/iris/opam.git
# path ~/.opam/coq88/.opam-switch/build/coq-iris.dev.2019-03-14.3.2d1c8352
# command /usr/bin/make -j7
# exit-code 2
# env-file ~/.opam/log/coq-iris-30223-f0f09f.env
# output-file ~/.opam/log/coq-iris-30223-f0f09f.out
### output ###
# [...]
# -Closed under the global context
# +Axioms:
# +iProp_unfold : ∀ Σ : gFunctors, iProp Σ -n> iPreProp Σ
# +iProp_fold_unfold : ∀ (Σ : gFunctors) (P : iProp Σ),
# +iProp_fold (iProp_unfold P) ≡ P
# +iProp_fold : ∀ Σ : gFunctors, iPreProp Σ -n> iProp Σ
# +iPreProp : gFunctors → ofeT
# make[2]: *** [Makefile.coq.local:20: tests/one_shot.vo] Error 1
# make[2]: *** Waiting for unfinished jobs....
# make[1]: *** [Makefile.coq:318: all] Error 2
# make[1]: Leaving directory '/home/maxi/.opam/coq88/.opam-switch/build/coq-iris.dev.2019-03-14.3.2d1c8352'
# make: *** [Makefile:6: all] Error 2
```
However, these definitions like `iProp_unfold` etc are not axioms (are they?). Is this a known bug of Coq `8.8.1`?
I will try out the newest Coq version, but compilation takes some time...https://gitlab.mpi-sws.org/iris/iris/-/issues/232Investigate slowdown caused by gset change2019-04-24T08:26:43ZRalf Jungjung@mpi-sws.orgInvestigate slowdown caused by gset change[This std++ diff](https://gitlab.mpi-sws.org/iris/stdpp/compare/b938e033...e2eb2948) caused an [80% slowdown in `algebra/gset.v`](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1552558727491&to=1552560733442&var-metric=...[This std++ diff](https://gitlab.mpi-sws.org/iris/stdpp/compare/b938e033...e2eb2948) caused an [80% slowdown in `algebra/gset.v`](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1552558727491&to=1552560733442&var-metric=instructions&var-project=iris&var-branch=master&var-config=coq-8.9.0&var-group=(.*)). We should find a way to fix that regression, or at least understand what causes it.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/231Allow swapping later^i and forall, later, etc.2019-11-01T11:12:12ZPaolo G. GiarrussoAllow swapping later^i and forall, later, etc.For swapping later^i and forall, an instance suffices: https://gist.github.com/Blaisorblade/3f9e41b7f044617fd5789b0d3554a2d7 (I suppose this isn't good enough for a PR).
For swapping later^i and later, I'm not sure what's the typeclass, ...For swapping later^i and forall, an instance suffices: https://gist.github.com/Blaisorblade/3f9e41b7f044617fd5789b0d3554a2d7 (I suppose this isn't good enough for a PR).
For swapping later^i and later, I'm not sure what's the typeclass, but it should be possible — I do the swaps through complicated proofs, applied inline.
Generally, I suspect all the instances for later could be lifted (by induction) to later^i, and I suspect I'd be willing to do that work (once I move).https://gitlab.mpi-sws.org/iris/iris/-/issues/230"Generalizable All Variables" considered harmful2019-02-27T11:21:27ZRalf Jungjung@mpi-sws.org"Generalizable All Variables" considered harmfulOver the last few days, when reflecting the way we introduce assumptions in our proofs, I came to the conclusion that I am somewhat uneasy with globally setting `Generalizable All Variables`. Imagine we had a type `spropC`, an OFE, and ...Over the last few days, when reflecting the way we introduce assumptions in our proofs, I came to the conclusion that I am somewhat uneasy with globally setting `Generalizable All Variables`. Imagine we had a type `spropC`, an OFE, and then consider the following preamble:
```
Section something_about_sprop.
Conext `{authG Σ (exR spropC)}.
```
Can you spot what's wrong with this? Well, we just assumed that SProp is discrete, which it is not. Ouch.
From my experiments, we can avoid over-eager generalization by adding a `!`. I have not found conclusive documentation for `!`, but it seems the least we should do is (a) add `!` basically everywhere, and (b) treat the *absence* of `!` as a big fat warning bell during code review. The latter will be hard.
But really, while `Generalizable All Variables` is very useful for some things (like the general fin map libraries in std++), I think for most code the benefits are slim. I have [ported a few files](https://gitlab.mpi-sws.org/iris/iris/commit/f5bceb45532b5c9dff9124589b93eccee722be8f) to `Generalizable No Variables`, and the additional declarations required are negligible IMO. So I think what we should aim for (but that might take a while) is for std++ to no longer set `Generalizable All Variables` (to avoid inflicting this subtle issue onto unsuspecting users), and to locally set that flag in the (few) files that really benefit.
Or maybe I am overreacting, and things are not that bad. But the thought of accidentally assuming things I don't want to assume makes me nervous. What do you think?https://gitlab.mpi-sws.org/iris/iris/-/issues/229Odd Behavior for Substitution2020-03-12T21:08:39ZDaniel GratzerOdd Behavior for SubstitutionHello,
Simon noticed a somewhat odd occurrence with substitution today. Apparently values are no longer required to be closed (?) but defining a value which is open seems to break substitution in a confusing way?
```
Definition tryset ...Hello,
Simon noticed a somewhat odd occurrence with substitution today. Apparently values are no longer required to be closed (?) but defining a value which is open seems to break substitution in a confusing way?
```
Definition tryset : val :=
λ: "n",
CAS "x" NONE (SOME "n").
Definition check : val :=
λ: <>,
let: "y" := !"x" in λ: <>,
match: "y" with
NONE => #()
| SOME "n" =>
match: !"x" with
NONE => assert: #false
| SOME "m" => assert: "n" = "m"
end
end.
Definition mk_oneshot : val := λ: <>,
let: "x" := ref NONE in (tryset, check).
```
With this example program we have separated out `tryset` and `check` even though they both depend on `"x"`. However, when proving some properties about `mk_oneshot` substituting `"x"` for a new location `#l` does not replace `"x` in either.
This behavior is demonstrated by the attached file: [oneshot.v](/uploads/cc01dea007082db718057bb66ad87c88/oneshot.v). Am I missing something obvious here?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/225`is_closed_expr` is stronger than stability under `subst`2019-01-06T17:04:41ZDan Frumin`is_closed_expr` is stronger than stability under `subst`I think there is a discrepancy between the substitution and `is_closed_expr` for heap_lang
According to [subst](https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lang.v#L400),
`subst x v' (of_val v) = of_val v`.
How...I think there is a discrepancy between the substitution and `is_closed_expr` for heap_lang
According to [subst](https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lang.v#L400),
`subst x v' (of_val v) = of_val v`.
However, `is_closed_expr (of_val v) = is_closed_val v` (<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/metatheory.v#L22>) which is not always true.
That means, IIUC, that there are expressions that are not closed, but which are idempotent under the substitution.https://gitlab.mpi-sws.org/iris/iris/-/issues/223Module `iris.algebra.big_op` exports unqualified `foo`2018-12-20T21:06:52ZPaolo G. GiarrussoModule `iris.algebra.big_op` exports unqualified `foo`Minor issue — `iris.algebra.big_op` uses `foo` for the name of an instance. A more unique name might be better.
```
From iris.program_logic Require Import ectx_lifting.
About foo.
foo : ∀ (A : Type) (R : relation A), RewriteRelation R
...Minor issue — `iris.algebra.big_op` uses `foo` for the name of an instance. A more unique name might be better.
```
From iris.program_logic Require Import ectx_lifting.
About foo.
foo : ∀ (A : Type) (R : relation A), RewriteRelation R
Argument A is implicit and maximally inserted
Argument scopes are [type_scope _]
foo is transparent
Expands to: Constant iris.algebra.big_op.foo
```https://gitlab.mpi-sws.org/iris/iris/-/issues/222Can't iSpecialize/iDestruct with (("A" with "B") with "C")2018-12-03T07:17:44ZPaolo G. GiarrussoCan't iSpecialize/iDestruct with (("A" with "B") with "C")`iSpecialize (("HLT" with "Hg") with "HL").` fails with
```
Error:
In nested Ltac calls to "iSpecialize (open_constr)", "iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)" and
"iSpecializeCore (open_c...`iSpecialize (("HLT" with "Hg") with "HL").` fails with
```
Error:
In nested Ltac calls to "iSpecialize (open_constr)", "iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)" and
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)", last call failed.
Tactic failure: iSpecialize: ("HLT" with "Hg") should be a hypothesis, use iPoseProof instead.
```
While that's technically true, it seems unfortunate, and forces me to call two tactics for the job. I end up writing
`iSpecialize ("HLT" with "Hg"); iDestruct ("HLT" with "HL") as "#HLT1"; auto.`
instead of `iDestruct (("HLT" with "Hg") with "HL") as "#HLT1"; auto.`, which fails with
```
Error:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)", "iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)", "iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>" and "<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call
failed.
No applicable tactic.
```
FWIW here's my context. Things are persistent as I'm not yet using mutable state (only persistent ghost state).
```
1 subgoal (ID 3041)
Σ : gFunctors
HdotG : dotG Σ
Γ : list ty
T, L, U : ty
γ : gname
ρ : vls
l : label
v : vl
============================
"Hv" : γ ⤇ (λ ρ0 : leibnizC vls, ⟦ T ⟧ ρ0)
"Hg" : ⟦ Γ ⟧* ρ
"HLU" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ⟦ L ⟧ ρ0 v0 → ⟦ U ⟧ ρ0 v0
"HTU" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ▷ ⟦ T ⟧ ρ0 v0 → ▷ ⟦ U ⟧ ρ0 v0
"HLT" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ▷ ⟦ L ⟧ ρ0 v0 → ▷ ⟦ T ⟧ ρ0 v0
"HL" : ▷ ⟦ L ⟧ ρ v
--------------------------------------□
▷ □ ⟦ T ⟧ ρ v
```