Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-01T13:46:23Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/130Make iApply "with" specialization lazier2019-11-01T13:46:23ZRobbert KrebbersMake iApply "with" specialization lazierFor example, the `[$]` specialization pattern for frame inference is too eager. In the example below, it would like to be able to prove the premises of `swap_spec` by framing. However, this does not quite work because `wp_apply` first tr...For example, the `[$]` specialization pattern for frame inference is too eager. In the example below, it would like to be able to prove the premises of `swap_spec` by framing. However, this does not quite work because `wp_apply` first tries to prove the premises of the lemma by framing, and then tries to match the goal. Since framing is performed first, it instantiates evars in the wrong way. If it would first try to match the goal, and then frame, the evars would already be instantiated when framing is performed.
```coq
From iris.heap_lang Require Import proofmode notation.
Parameter swap : val.
Definition rotate_r : val := λ: "x" "y" "z",
swap "y" "z";; swap "x" "y".
Section proof.
Context `{!heapG Σ}.
Lemma swap_spec x y v1 v2 :
{{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
Proof. Admitted.
Lemma rotate_r_spec x y z v1 v2 v3 :
{{{ x ↦ v1 ∗ y ↦ v2 ∗ z ↦ v3 }}}
rotate_r #x #y #z
{{{ RET #(); x ↦ v3 ∗ y ↦ v1 ∗ z ↦ v2 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". do 3 wp_lam.
Fail wp_apply (swap_spec with "[$]").
wp_apply (swap_spec y z with "[$]").
Admitted.
End proof.
```
It's probably easy to come up with a simpler example, but I ran into this one while preparing the Iris tutorial.
Another example:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/112Make invariants and slices closed under equivalence2018-02-08T10:43:12ZRalf Jungjung@mpi-sws.orgMake invariants and slices closed under equivalenceThis has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the followi...This has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the following holds:
```coq
Lemma inv_iff P Q :
later persistently (P <-> Q) -> inv P -> inv Q.
```
I think this may be worth it, *if* it means we can simplify the definition of the lifetime logic a little bit. However, that will only be the case if we manage to also get this law for `slice`, which requires either a separate closure in `slice` (so the one in `inv` does not help), or doing the same kind of closure in `saved_prop_own` (but then, do we also want the equivalent law for `saved_pred_own`?).
Also, I am not sure if we should do this before or after Iris 3.1. Either way, it is backwards-compatible.https://gitlab.mpi-sws.org/iris/iris/-/issues/101Make Iris run in jsCoq2017-11-30T09:53:53ZRalf Jungjung@mpi-sws.orgMake Iris run in jsCoqCurrent status according to @janno:
> I think I got all Iris dependencies to work. The only problem I encountered was the lack of vm_compute. However, that seems to be only necessary for generating fresh names for hypotheses. Robbert al...Current status according to @janno:
> I think I got all Iris dependencies to work. The only problem I encountered was the lack of vm_compute. However, that seems to be only necessary for generating fresh names for hypotheses. Robbert already mentioned that he wanted to look into that.https://gitlab.mpi-sws.org/iris/iris/-/issues/79Make iSplit work below existentials?2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgMake iSplit work below existentials?I have a goal of the form
```
∃ x : vec val m, ⌜#l = #l⌝ ∗ ▷ l ↦∗ x
```
and all my assumptions are only available later. I cannot do `iNext` because not everything is below a later, but I can do `rewrite -uPred.sep_exist_l. iSplit; f...I have a goal of the form
```
∃ x : vec val m, ⌜#l = #l⌝ ∗ ▷ l ↦∗ x
```
and all my assumptions are only available later. I cannot do `iNext` because not everything is below a later, but I can do `rewrite -uPred.sep_exist_l. iSplit; first done.`. This works because some part of what is below the existential does not depend on the witness.
Now I wonder, would it make sense for `iSplit` to work in this case (giving me ` ⌜#l = #l⌝` and `∃ x : vec val m, ▷ l ↦∗ x` as goals)? The rewrite I did above is not very discoverable, but neither is the `iSplit`. What do you think? @jjourdan @robbertkrebbers
(You may wonder why I have things under the existential that do not depend on the witness. The reason is that lemmas of the form `∃ x y z, P` work much better with the proofmode, because I an do a single `iDestruct ... as (x y z) ...`. If I pushed the existential down, destructing things would become much more annoying.)https://gitlab.mpi-sws.org/iris/iris/-/issues/205Make notation for pure and plainly affine2021-07-18T09:46:52ZRalf Jungjung@mpi-sws.orgMake notation for pure and plainly affineI think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use `*` and `-*` even when working in linear Iris.I think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use `*` and `-*` even when working in linear Iris.https://gitlab.mpi-sws.org/iris/iris/-/issues/379Make sealing consistent and document it2020-11-10T13:15:28ZRalf Jungjung@mpi-sws.orgMake sealing consistent and document itWe should document the "sealing" pattern that we use throughout Iris, and make sure that we use it in a consistent way. Things to take care of:
* Avoid eta-expanding the sealed definition; that means that the write lemma only applies to ...We should document the "sealing" pattern that we use throughout Iris, and make sure that we use it in a consistent way. Things to take care of:
* Avoid eta-expanding the sealed definition; that means that the write lemma only applies to the eta-expanded term. This immediately implies that sealing should be done outside of sections.
* Add an `unseal` tactic, either as `Local Ltac` or in a module to avoid polluting the global namespace.
* There is no need to make sealed definitions `Typeclasses Opaque`.
- no eta, ergo no sections
- unseal tactic
- no TC opaque
For example, here is how sealing of a logic-level RA wrapper could look like:
```
Definition mnat_own_auth_def `{!mnatG Σ} (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
own γ (mnat_auth_auth q n).
Definition mnat_own_auth_aux : seal (@mnat_own_auth_def). Proof. by eexists. Qed.
Definition mnat_own_auth := mnat_own_auth_aux.(unseal).
Definition mnat_own_auth_eq : @mnat_own_auth = @mnat_own_auth_def := mnat_own_auth_aux.(seal_eq).
Arguments mnat_own_auth {Σ _} γ q n.
Definition mnat_own_lb_def `{!mnatG Σ} (γ : gname) (n : nat): iProp Σ :=
own γ (mnat_auth_frag n).
Definition mnat_own_lb_aux : seal (@mnat_own_lb_def). Proof. by eexists. Qed.
Definition mnat_own_lb := mnat_own_lb_aux.(unseal).
Definition mnat_own_lb_eq : @mnat_own_lb = @mnat_own_lb_def := mnat_own_lb_aux.(seal_eq).
Arguments mnat_own_lb {Σ _} γ n.
Local Ltac unseal := rewrite
?mnat_own_auth_eq /mnat_own_auth_def
?mnat_own_lb_eq /mnat_own_lb_def.
```
When there are operational typeclasses involved, the `_eq` lemma should also account for those to avoid having to rewrite twice:
```
Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
MonPred (λ i, |==> P i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
Definition monPred_bupd := monPred_bupd_aux.(unseal).
Arguments monPred_bupd {_}.
Lemma monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/117Make some of the `wp_` tactics language independent2019-11-01T13:23:45ZRobbert KrebbersMake some of the `wp_` tactics language independentA large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.A large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.https://gitlab.mpi-sws.org/iris/iris/-/issues/404Make string-ident a standard part of Iris2021-03-24T11:03:52ZLennard GäherMake string-ident a standard part of IrisSince support for Coq 8.10 has been dropped for a while now and 8.11 is required, the `string-ident` plugin could be integrated into Iris master so that the named `%H` intro pattern becomes available in the IPM by default.
Mainly, this w...Since support for Coq 8.10 has been dropped for a while now and 8.11 is required, the `string-ident` plugin could be integrated into Iris master so that the named `%H` intro pattern becomes available in the IPM by default.
Mainly, this would have the benefits of
* not having to explicitly require the user to install the plugin in developments using Iris,
* and thus be beneficial to overall code quality of developments using Iris (since there would be a clear argument for using the new intro pattern instead of using auto-generated names).
@jung suggested I create an issue for this.https://gitlab.mpi-sws.org/iris/iris/-/issues/381Make sure we have Hint Mode for every typeclass2021-06-17T13:19:41ZRalf Jungjung@mpi-sws.orgMake sure we have Hint Mode for every typeclassWe should have `Hint Mode` for all our `Class`es. We could detect this with some kind of shell script that greps for `Class`, extracts the name, and then greps for `Hint Mode`.
Currently known missing `Mode`s:
* [ ] `IntoVal`
* [ ] `Wp`...We should have `Hint Mode` for all our `Class`es. We could detect this with some kind of shell script that greps for `Class`, extracts the name, and then greps for `Hint Mode`.
Currently known missing `Mode`s:
* [ ] `IntoVal`
* [ ] `Wp`
* [ ] `Twp`https://gitlab.mpi-sws.org/iris/iris/-/issues/211Masks are coPsets in the Coq development, not arbitrary subsets of natural nu...2020-03-18T15:29:30ZJoseph TassarottiMasks are coPsets in the Coq development, not arbitrary subsets of natural numbersThe appendix suggests that masks for updates and weakest preconditions may be arbitrary sets (it does not say so explicitly when defining fancy updates, but on p. 29 the camera used for "enabled" invariants is said to be P(N)). However, ...The appendix suggests that masks for updates and weakest preconditions may be arbitrary sets (it does not say so explicitly when defining fancy updates, but on p. 29 the camera used for "enabled" invariants is said to be P(N)). However, in the Coq code, the representation used for masks is `coPset`. @robbertkrebbers says that `coPsets` are used so that the representation has extensional equality, but that in principle the constructions all could work with arbitrary sets.
It seems like either the discussion in the appendix should be changed to `coPset` as well (in order to stick to the claim that everything is verified), or an explanatory note should be given. Unfortunately, it is not so easy to concisely describe `coPsets`: they contain all finite and cofinite sets, and are closed under various set operations. However, as @jung points out, the namespace "suffix" construction is not so clearly derivable just from the closure properties.https://gitlab.mpi-sws.org/iris/iris/-/issues/392Masks in step-taking fupd notation2020-12-10T13:37:03ZRalf Jungjung@mpi-sws.orgMasks in step-taking fupd notationEarlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gi...Earlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595 finally making the more-than-1-step case actually useful in Iris proper.
The current notation is
```coq
(** * Step-taking fancy updates. *)
(** These have two masks, but they are different than the two masks of a
mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
mask") holds at the beginning and the end; the second mask [Ei] ("inner
mask") holds around each ▷. This is also why we use a different notation
than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=> ▷ |={Ei,Eo}=> Q)%I : bi_scope.
Notation "|={ E }▷=> Q" := (|={E}[E]▷=> Q)%I : bi_scope.
(** For the iterated version, in principle there are 4 masks: "outer" and
"inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
that could potentially differ from [Eo]. The latter can be obtained from
this notation by adding normal mask-changing update modalities: [
|={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
Notation "|={ E }▷=>^ n Q" := (|={E}[E]▷=>^n Q)%I : bi_scope.
```
Now it turns out that an n-step update that opens and closes things at each step is basically never useful (or at least that is what things look like so far). So the iterated step-taking update should really open some masks once, then do a bunch of steps with updates, and then close some masks again: [rj1]
```coq
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
For `n=1` this is equivalent, but for larger `n` it is not (unless `Ei=Eo`). Since this is not just strictly iterating the single-step update any more, maybe the notation should be slightly different to reflect this, such as [rj1']
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
And then, to make things even stranger, @jjourdan started using this kind of update in !595:
```coq
|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P
```
I thought quite a bit about this update the last few days... the empty set makes it look like no invariants can be used "while counting down the steps", but that is not so: when considering masks as resources/tokens (which under the hood they are), this update lets us grab the tokens for `E1\E2` in the beginning, use them throughout the update in any way we please, and give them back in the end. We don't have good proof rules for this general case though. We do have rules for the easier case where `E2=∅`: then one can use `mask_fupd_intro'` to introduce the `|={E1,∅}=>` modality while obtaining `|={∅,E1}=> emp` that can be kept around, and can be used when the goal starts with `|={∅}=>`. In other words:
```coq
|={E1,∅}=> |={∅}▷=>^n |={∅,E1}=> P
----------------------------------
|={E1}=> |={E1}▷=>^n |={E1}=> P
```
So from this it looks like maybe we want to define the iterated step-taking update as [jh]
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
But we need to come up with better proof rules to actually make this conveniently usable, so maybe it's not worth it having such a flexible notation, and we should just have [rj2] (basically the special case of [rj1] where the inner mask is empty, which coincides with [jh] where the inner mask is empty)
```coq
Notation "|={ Eo }▷^ n => Q" := (|={Eo,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,Eo}=> Q)))%I : bi_scope.
```
or maybe we take inspiration from some recent work by @simonspies and go for [simon]
```coq
Notation "|={ E1 , E2 }▷^ n => Q" := (|={E1,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,E2}=> Q)))%I : bi_scope.
```
There's just too many variants that could make sense.^^ (We could also have variants of some earlier notations where the pre- and post-masks are different, but having a notation with three masks seems a bit unwieldy...)
My current thinking is that it's not worth to expose the full power of @jjourdan's theorem (we have no known user that requires it, I think, but we should check in RustBelt), so we can go with one of the last two and exploit that `|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P` is implied by the easier-to-use `|={E1\E2,∅}=> |={∅}▷=>^n |={∅,E1\E2}=> P` (I am just a bit worried about how well `solve_nidjs` will be able to handle these masks).
The one thing that is clear is that the current multi-mask multi-step notation is not useful enough to justify its existence -- since there is no way to use it to state the new lemma in !595. That is the one design constraint I have identified so far: have a notation such that we can use it to state a many-step-fupd-lemma that is actually useful (and by this I mean use *just* this notation, not composing it with some pre- and post-updates like @jjourdan did). All of the above fit this condition to some extend, but [rj1] results in a very weak statement that we probably do not want. [jh] will be hard to write good rules for I think (but maybe I am wrong about this), which pushes me towards [rj2]; generalizing that to [simon] means we can even use this notation to define WP (even the WP in !595, where `={∅}▷=∗^(S $ steps_per_step stepcnt) |={∅,E}=>` could become `={∅,E}▷^(S $ steps_per_step stepcnt)=∗`).
That was lots of rambling... any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/27mathpartir.sty is missing2016-08-09T13:09:45ZJeehoon Kangjeehoon.kang@kaist.ac.krmathpartir.sty is missingI believe the intention of `\usepackage{\basedir mathpartir}` in `iris.tex` is using the local `mathpartir.sty` file in the same directory. But it is missing in the repository.I believe the intention of `\usepackage{\basedir mathpartir}` in `iris.tex` is using the local `mathpartir.sty` file in the same directory. But it is missing in the repository.https://gitlab.mpi-sws.org/iris/iris/-/issues/206Missing error message with `iDestruct ... as "#..."`2019-01-23T09:20:00ZRalf Jungjung@mpi-sws.orgMissing error message with `iDestruct ... as "#..."`Testcase:
```coq
Lemma test {PROP: bi} {P Q : PROP} `{!Persistent P}:
Q ∗ (Q -∗ P) -∗ Q ∗ P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP".
```
Prints
```
No matching clauses for match.
```
That's never an acceptable ...Testcase:
```coq
Lemma test {PROP: bi} {P Q : PROP} `{!Persistent P}:
Q ∗ (Q -∗ P) -∗ Q ∗ P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP".
```
Prints
```
No matching clauses for match.
```
That's never an acceptable error message, obviously.https://gitlab.mpi-sws.org/iris/iris/-/issues/338Missing unseal tactic for siProp2020-08-30T07:04:36ZPaolo G. GiarrussoMissing unseal tactic for siProp
Here's what I've used:
```coq
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_affinely, bi_...
Here's what I've used:
```coq
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
monPred_upclosed, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
bi_persistently, bi_affinely, bi_later;
simpl.
(* Should be siProp.unseal. *)
Ltac siProp_unseal := unseal_prepare; siProp_primitive.unseal.
```
The second part is easy, but the first not (tho it was worse before the bi-sbi merge), and deserves to be abstracted.https://gitlab.mpi-sws.org/iris/iris/-/issues/342Missing {u,}rFunctors and conversions2020-09-10T17:45:28ZPaolo G. GiarrussoMissing {u,}rFunctors and conversionsSome missing utilities I noticed:
- there's no conversion function from `urFunctor` (COFE -> uCMRA) to an `rFunctor` (COFE -> CMRA), and an `rFunctor` to an `oFunctor` (COFE -> OFE)
- `gmapRF` does not exist and should be definable throu...Some missing utilities I noticed:
- there's no conversion function from `urFunctor` (COFE -> uCMRA) to an `rFunctor` (COFE -> CMRA), and an `rFunctor` to an `oFunctor` (COFE -> OFE)
- `gmapRF` does not exist and should be definable through the above conversion, and @jung suggests that's an oversight; OTOH, that alerted me to a bug; I only needed it because I tried writing `GFunctor (gmapRF ...)`, which does not seem useful
- `listRF` does not exist (which I noticed while grepping)https://gitlab.mpi-sws.org/iris/iris/-/issues/410Modality for `Timeless`2021-04-19T07:51:21ZRalf Jungjung@mpi-sws.orgModality for `Timeless`We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ ...We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ P
```
Unlike prior attempts, this is a *monadic* modality, i.e. it is easy to introduce but hard to eliminate. That makes it less useful -- I was hoping that `<timeless> P` would be *stronger* than `P` and basically say that the proof only requires timeless resources (restriction of the context, and thus comonadic); instead, here `<timeless> P` is *weaker* than `P`, it basically says "I have a proof of `P` at step-index 0".
The existing `later_false_em` can now be written as `▷ P ⊢ ▷ False ∨ <timeless> P` (or `▷ P ⊢ ◇ <timeless> P`).
But this could still be interesting and useful in other situations we have not considered yet, so it is worth exploring. One open question is which primitive laws we need to derive all the properties of `Timeless` that we currently have. For the record, this is the current definition of `Timeless`:
```
Timeless' P := ▷ P ⊢ ▷ False ∨ P
(* or *)
Timeless' P := ▷ P ⊢ ◇ P
```
By `later_false_em`, we have `Timeless P → Timeless' P` (so the new class is at least as strong). I am not sure about the other direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/8Modular global monoid2016-03-17T16:06:26ZRalf Jungjung@mpi-sws.orgModular global monoidRight now, Iris is instantiated with a single global monoid. As described in the appendix, we can easily use the product monoid to have multiple different monoids available in Iris, but this still requires knowing the exact set of all mo...Right now, Iris is instantiated with a single global monoid. As described in the appendix, we can easily use the product monoid to have multiple different monoids available in Iris, but this still requires knowing the exact set of all monoids we will need up-front, before instantiating the logic. That's not nice.
I see two possible solutions.
### The "any" monoid
We could have a monoid of the form "\Sigma (A: Type) {RA A}. A". This is a monoid that can be "any" monoid. However, doing that in Coq would get very hairy. We would have to require equality of the types and RAs in the composition, and somehow transport the actual data in A over that equality to even compose the pieces. I think FCSL is doing something like this, but they assume all sorts of classical axioms. We would probably want at least function extensionality and Axiom K.
### The "all" monoid
When I was visiting @robbertkrebbers , we talked about indexed products a lot as they impose some interesting challenges when done in Coq, where we don't want to assume the axiom of choice. We agreed that for example, it would be nice to have he set of all STS graphs + token assignments in the index set, so that we could actually have *all* STS monoids at once, rather than having to add every single STS monoid to the global monoid individually.
That had me thinking, could it be possible to index the product by monoids? Essentially, replace the \Sigma above by a \Pi. That would be the monoid of all monoids, with the index defining the monoid structure at that position. We just do everything pointwise, so there should be no trouble with inhomogenous equality or anything like that. As long as we make sure that a module always uses the *same* index, and nobody reasons about equality of indices, we should be good - right? Or did I miss anything here?
@janno, @swasey, we also talked about this problem at some point, so you're probably also interested in this.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/88More convenient destruct of pure hypotheses2020-04-07T07:01:25ZRalf Jungjung@mpi-sws.orgMore convenient destruct of pure hypothesesIt is currently pretty annoying to destruct things into the pure (Coq) context, because the assertions cannot be named. This should be fixed.
One somewhat hack-ish option would be to do this the ssreflect style. So `iDestruct ... as "...It is currently pretty annoying to destruct things into the pure (Coq) context, because the assertions cannot be named. This should be fixed.
One somewhat hack-ish option would be to do this the ssreflect style. So `iDestruct ... as "[% %]"` would put two things onto the goal stack, and one would follow this tactic by `=>H1 H2` to give them names. This is somewhat non-local, but OTOH it lets us use the full power of ssreflect intro patterns.
Another option would be to somehow solve the "cannot convert string to ident"-problem, and then support patterns of the form `%H`. This will require a plugin to work in Coq 8.6, which makes it really hard to support Windows (as far as I can tell). Also, I suppose currently `%H` is parsed just like `% H`? So there would be a backwards compatibility problem when `%` starts to behave like `#` (i.e., being a modifier on the following name). We could mitigate that by detecting uses of `%H` right now and warning about them (or erroring immediately?).https://gitlab.mpi-sws.org/iris/iris/-/issues/80More precise error message on missing hypothesis2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgMore precise error message on missing hypothesisCurrently, when I say e.g. `iSplit "H1 H2 H3 H4"` and one of the hypotheses does not exist, the error is `hypotheses ["H1"; "H2"; "H3"; "H4"] not found in the context.`. This is confusing because it indicates that none of them was found ...Currently, when I say e.g. `iSplit "H1 H2 H3 H4"` and one of the hypotheses does not exist, the error is `hypotheses ["H1"; "H2"; "H3"; "H4"] not found in the context.`. This is confusing because it indicates that none of them was found (while actually, only some of them have not been found). It is also not as useful as the error would be if it would name which hypothesis has not been found.
I assume spec patterns have the same issue.