Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-08-13T11:19:53Zhttps://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/243Avoid type-level aliases for overloading of canonical structures2019-11-01T13:05:35ZRobbert KrebbersAvoid type-level aliases for overloading of canonical structuresIn https://gitlab.mpi-sws.org/iris/iris/merge_requests/187#note_36185 @jjourdan expressed his dissatisfaction with the current means of overloading canonical structures:
> I have to say that I really don't like the idea of overloading a...In https://gitlab.mpi-sws.org/iris/iris/merge_requests/187#note_36185 @jjourdan expressed his dissatisfaction with the current means of overloading canonical structures:
> I have to say that I really don't like the idea of overloading a canonical structure for a type... Why cannot we define `ufrac` as something like: `Record ufrac := uf_qp { qp_uf : Qp }.`? Sure, this will require some boilerplate for projecting and boxing fractions, but hoping that such hack will keep a stable behaviors seems rather optimistic!
This applies to `ufrac` (introduced in !195) and `mnat` (introduced a long time ago).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/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/228"expression validity" in WP2019-11-01T13:59:44ZJonas Kastberg"expression validity" in WPI propose updating the weakest precondition with a predicate over expressions,
mainly for the purpose of establishing a notion of ```well formed``` expressions.
General idea:
The idea is that some expressions might be outright invalid i...I propose updating the weakest precondition with a predicate over expressions,
mainly for the purpose of establishing a notion of ```well formed``` expressions.
General idea:
The idea is that some expressions might be outright invalid in the absence of certain properties on the state. A predicate on expression, that are preserved under step reduction, could be used to differentiate such expressions.
Furthermore, being able to derive certain properties about expressions when opening the weakest precondition might allow for some automation in regards to "pure" reductions that depend on the state while not changing it.
Specific Case:
My Iris instantation is a "language" over processes, where ```pstate := gmap pid (state)``` and ```pexpr := pid * expr```, where ```pid``` is a process identifier.
For modularity I have separate reduction layers, with the top-layer looking up the state of the process in the state map ```step ((p,e), <[p := σh]>σp) -> ((p,e'), <[p := σh']>σp), efs)```.
This means that every single reduction requires the process id of the expression to be in the map, even if it does not change (in case the underlying reduction is pure).
The presence of the necessary mapping is then expressed as a logical fragment, which is required by every single of my weakest precondition rules. Furthermore, I cannot do "Pure" reductions, as conceptualised with the existing ```PureExec``` class.
Proposed Solution:
Update the language instantiation to include a predicate over expressions (here named ```well_formed```), and use it in the weakest precondition.
The predicate should uphold certain properties, such as being preserved under step reduction and contexts.
```
Definition wp_pre `{irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => ∀ σ1 κ κs n,
state_interp σ1 (κ ++ κs) n ∗ well_formed e1 ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs (length efs + n) ∗
well_formed e2 ∗
wp E e2 Φ ∗
[∗ list] i ↦ ef ∈ efs, well_formed ef ∗ wp ⊤ ef fork_post
end%I.
```
Define a lifted ```PureExecState```, which defines expressions that are reducible and "pure" assuming that the state interpretation and well-formedness predicates hold:
```
Record pure_step_state (e1 e2 : expr Λ) := {
pure_exec_val_state : to_val e1 = None;
pure_step_safe_state σ1 κ n : state_interp σ1 κ n -∗ well_formed e1 -∗ ⌜reducible_no_obs e1 σ1⌝;
pure_step_det_state σ1 κ κs e2' σ2 efs n :
state_interp σ1 (κ++κs) n -∗ well_formed e1 -∗ ⌜prim_step e1 σ1 κ e2' σ2 efs⌝ → ⌜κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []⌝
}.
```
An important property of the proposed change is that original Iris instances remain unchanged when given ```True``` as the well_formed predicate.
Points of discussion:
- It has earlier been suggested to introduce closedness of expression in a [similar manner](https://gitlab.mpi-sws.org/iris/iris/merge_requests/58). Note however that the closedness condition on expressions has been phased out of the current iteration of Iris.
- The change would mean that any WP holds trivially true for invalid expressions, which must then suddenly be considered in many places.https://gitlab.mpi-sws.org/iris/iris/-/issues/227Provide a convenient way to define non-recursive ghost state2020-12-07T10:18:54ZRalf Jungjung@mpi-sws.orgProvide a convenient way to define non-recursive ghost stateIt is somewhat annoying, in particular from a teaching perspective, that we have to use incantations like the following each time we want to use some ghost state:
```
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definitio...It is somewhat annoying, in particular from a teaching perspective, that we have to use incantations like the following each time we want to use some ghost state:
```
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
```
To make things worse, if you forget the `lockΣ`, your proof will still work. You might just have assumed false, accidentally.
Can we do better than that, at least for the simple and common case of non-recursive ghost state?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
```