Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-09-17T17:50:33Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/346Typeclass inference fails to trigger.2020-09-17T17:50:33ZArthur Azevedo de AmorimTypeclass inference fails to trigger.I am trying to use `auth_acc`, but typeclass inference misses an apparently obvious instance that I have to provide by hand. Am I doing something wrong?
```
From stdpp Require Import base gmap.
From iris.algebra Require Import gmap numbers.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import auth invariants.
Section Test.
Context `{!invG Σ, !authG Σ (gmapUR nat natR)}.
Implicit Types m : gmap nat nat.
Definition my_inv m : iProp Σ := True.
Goal ∀ γ, auth_ctx γ nroot id my_inv ={⊤}=∗ False.
iIntros (γ) "Hctx".
iMod (auth_empty γ) as "#Hinit".
iMod (auth_acc _ _ _ _ _ ε with "[Hctx Hinit]") as "Hinv"; try by eauto.
(* Inhabited (gmap nat nat) is now shelved... *)
Abort.
End Test.
```I am trying to use `auth_acc`, but typeclass inference misses an apparently obvious instance that I have to provide by hand. Am I doing something wrong?
```
From stdpp Require Import base gmap.
From iris.algebra Require Import gmap numbers.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import auth invariants.
Section Test.
Context `{!invG Σ, !authG Σ (gmapUR nat natR)}.
Implicit Types m : gmap nat nat.
Definition my_inv m : iProp Σ := True.
Goal ∀ γ, auth_ctx γ nroot id my_inv ={⊤}=∗ False.
iIntros (γ) "Hctx".
iMod (auth_empty γ) as "#Hinit".
iMod (auth_acc _ _ _ _ _ ε with "[Hctx Hinit]") as "Hinv"; try by eauto.
(* Inhabited (gmap nat nat) is now shelved... *)
Abort.
End Test.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/344Set Default Goal Selector2020-09-15T02:34:25ZRalf Jungjung@mpi-sws.orgSet Default Goal SelectorAs a follow-up to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/491, @tchajed suggested to add
```
Set Default Goal Selector "!".
```
To enforce that we properly use goal selectors.As a follow-up to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/491, @tchajed suggested to add
```
Set Default Goal Selector "!".
```
To enforce that we properly use goal selectors.https://gitlab.mpi-sws.org/iris/iris/-/issues/343Make CI fail when proofs depend on auto-generated names2020-09-08T09:52:18ZRalf Jungjung@mpi-sws.orgMake CI fail when proofs depend on auto-generated namesWe already did it in std++, now [that this is fixed](https://github.com/coq/coq/issues/12944) it is time to do the same in Iris: make CI ensure that we do not use auto-generated names.
I plan to work on this when I find some time, but if someone beats me to it and fixes some proof scripts, that is not a problem at all. ;)We already did it in std++, now [that this is fixed](https://github.com/coq/coq/issues/12944) it is time to do the same in Iris: make CI ensure that we do not use auto-generated names.
I plan to work on this when I find some time, but if someone beats me to it and fixes some proof scripts, that is not a problem at all. ;)https://gitlab.mpi-sws.org/iris/iris/-/issues/341Coecisting fractional and persistent read-only ownership2020-08-25T09:34:48ZRalf Jungjung@mpi-sws.orgCoecisting fractional and persistent read-only ownershipAs part of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486, @tchajed and @simonfv raised the point that sometimes it would be useful to convert ownership of *some fraction* of a map element to persistent read-only ownership. Right now, our encoding through `frac * agree T + agree T` (or equivalently `(frac + ()) * agree T`) requires ownership of the full fraction for that move.
I think such a construction is possible, but it requires https://gitlab.mpi-sws.org/iris/iris/-/issues/257. Then we could relate an authoritative map to a fragment that's more like `option (frac * agree T) * option (agree T)`, and ensure that the second `option` is `None` unless the sum of all fraction fragments is less than 1.As part of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486, @tchajed and @simonfv raised the point that sometimes it would be useful to convert ownership of *some fraction* of a map element to persistent read-only ownership. Right now, our encoding through `frac * agree T + agree T` (or equivalently `(frac + ()) * agree T`) requires ownership of the full fraction for that move.
I think such a construction is possible, but it requires https://gitlab.mpi-sws.org/iris/iris/-/issues/257. Then we could relate an authoritative map to a fragment that's more like `option (frac * agree T) * option (agree T)`, and ensure that the second `option` is `None` unless the sum of all fraction fragments is less than 1.https://gitlab.mpi-sws.org/iris/iris/-/issues/340Polymorphic equality for HeapLang2020-08-22T19:06:03ZDan FruminPolymorphic equality for HeapLangIt would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.It would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.https://gitlab.mpi-sws.org/iris/iris/-/issues/339Add "reservation map" CMRA2020-09-09T12:29:51ZRalf Jungjung@mpi-sws.orgAdd "reservation map" CMRAFor the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an infinite amount of names in a first frame-preserving update.
2. Next you can use that infinite set to reserve a particular name in some other abstraction, with the usual "strong allocation" lemma that picks the new name from any infinite set.
3. Finally you can take that one name you got, and since it is in the infinite set you reserved, you may now own that name in the reservation map after a second frame-preserving update.
The code for this is at https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/theories/typing/lib/gsingleton.v. @pythonsq do you think you will have time to clean this up and make it into an MR?For the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an infinite amount of names in a first frame-preserving update.
2. Next you can use that infinite set to reserve a particular name in some other abstraction, with the usual "strong allocation" lemma that picks the new name from any infinite set.
3. Finally you can take that one name you got, and since it is in the infinite set you reserved, you may now own that name in the reservation map after a second frame-preserving update.
The code for this is at https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/theories/typing/lib/gsingleton.v. @pythonsq do you think you will have time to clean this up and make it into an MR?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_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.
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/335iris.sty incompatible with acmart2020-07-15T12:25:40ZRalf Jungjung@mpi-sws.orgiris.sty incompatible with acmartThe `\nequiv` macro in `iris.sty` clashes with something that is import by the `acm` template. In our own papers, we work around this by undefining `\nequiv` locally, but that's not great.
We should either always overwrite whatever the existing `\nequiv` is, or else change the name of our macro.The `\nequiv` macro in `iris.sty` clashes with something that is import by the `acm` template. In our own papers, we work around this by undefining `\nequiv` locally, but that's not great.
We should either always overwrite whatever the existing `\nequiv` is, or else change the name of our macro.https://gitlab.mpi-sws.org/iris/iris/-/issues/334Expand test coverage of proofmode2020-07-14T07:13:05ZTej Chajedtchajed@mit.eduExpand test coverage of proofmodeThe proof mode tests don't cover the following:
- [ ] `iRename`
- [ ] `iTypeOf`
- [ ] `iInduction`'s ability to freshen the inductive hypothesis
I have tests for the first two on my [bytes-ident](https://gitlab.mpi-sws.org/tchajed/iris-coq/-/tree/bytes-ident) branch.The proof mode tests don't cover the following:
- [ ] `iRename`
- [ ] `iTypeOf`
- [ ] `iInduction`'s ability to freshen the inductive hypothesis
I have tests for the first two on my [bytes-ident](https://gitlab.mpi-sws.org/tchajed/iris-coq/-/tree/bytes-ident) branch.https://gitlab.mpi-sws.org/iris/iris/-/issues/332Become part of Coq Platform?2020-07-21T18:01:10ZRalf Jungjung@mpi-sws.orgBecome part of Coq Platform?We should consider making iris part of the [Coq Platform](https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md).
Quoting Michael Soegtrop:
> So if IRIS becomes part of the platform, the platform takes care that there is a reliable, fast and fool proof way to install Coq including IRIS on Windows, OSX and - maybe a bit less fool proof - Linux. This should make it easier for teachers and interested explorers to install IRIS. On the other hand you agree to do your best to deliver a working release of IRIS for any major Coq release (like 8.12, 8.13) within at most 3 months, better 1 month.We should consider making iris part of the [Coq Platform](https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md).
Quoting Michael Soegtrop:
> So if IRIS becomes part of the platform, the platform takes care that there is a reliable, fast and fool proof way to install Coq including IRIS on Windows, OSX and - maybe a bit less fool proof - Linux. This should make it easier for teachers and interested explorers to install IRIS. On the other hand you agree to do your best to deliver a working release of IRIS for any major Coq release (like 8.12, 8.13) within at most 3 months, better 1 month.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 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.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 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?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/329Iris Website Reform2020-06-25T21:39:26ZRalf Jungjung@mpi-sws.orgIris Website ReformWe had a long discussion on Mattermost today discussing potential improvements to the website. Some of the take-aways include:
* We'd like to move to a static site generator (Jekyll, or something else if someone makes a good pitch).
* We'd like to split the website into sub-pages, as the list of papers is getting too long.
* We'd like to have the website repo public for contributors. I think it would make sense to have it in the Iris organization here on MPI's GitLab.
* In terms of content, the concern that triggered this discussion was along the lines of "(some) people think Iris is just for academic/toy/ML-like languages". We should probably put the fact that Iris is very flexible front and center, maybe by picking a few papers to display on the front page that use Iris for various models of real-world definitely-not-toy languages (RustBelt for Rust, runST for Haskell, DOT for Scala, "Non-Determinism in C Expressions" for C, Goose for Go, and once that paper exists RefinedC for C).
* We could also highlight the different kinds of properties people verify in Iris (type system soundness, refinement, verification of concurrent algorithms, non-interference, ...).
I expect I will take the lead on setting up the infrastructure for wiring up GitLab with Jekyll and GH pages, and @robbertkrebbers offered to take the lead on the content side of things.We had a long discussion on Mattermost today discussing potential improvements to the website. Some of the take-aways include:
* We'd like to move to a static site generator (Jekyll, or something else if someone makes a good pitch).
* We'd like to split the website into sub-pages, as the list of papers is getting too long.
* We'd like to have the website repo public for contributors. I think it would make sense to have it in the Iris organization here on MPI's GitLab.
* In terms of content, the concern that triggered this discussion was along the lines of "(some) people think Iris is just for academic/toy/ML-like languages". We should probably put the fact that Iris is very flexible front and center, maybe by picking a few papers to display on the front page that use Iris for various models of real-world definitely-not-toy languages (RustBelt for Rust, runST for Haskell, DOT for Scala, "Non-Determinism in C Expressions" for C, Goose for Go, and once that paper exists RefinedC for C).
* We could also highlight the different kinds of properties people verify in Iris (type system soundness, refinement, verification of concurrent algorithms, non-interference, ...).
I expect I will take the lead on setting up the infrastructure for wiring up GitLab with Jekyll and GH pages, and @robbertkrebbers offered to take the lead on the content side of things.https://gitlab.mpi-sws.org/iris/iris/-/issues/328Add RA for auth of a heap2020-08-07T18:02:31ZRalf Jungjung@mpi-sws.orgAdd RA for auth of a heap`auth (gmap X Y)` is a very frequently reoccurring RA, and finding all the right lemmas to compose for it can be challenging. After I saw people use `gen_heap` when really they want this RA, I am now convinced that we should have it in Iris. ;)
The only open question for me is, what is `Y`? (`X` is any countable type.)
* We probably should have fractions, so that would be `Y := frac * agree T`. Even if you don't need fractions, just making it always "1" should not be hard to use (we should just make sure to have a lemma that from owning the "1" fraction twice, derives `False`).
* @tchajed mentioned they also need something with agreement in a few places. So we could either also have a version with `Y := agree T`, or we could do the strictly more powerful thing (subsuming both of the above) and do `Y := (frac * agree T) + agree T`. I *think* with the right surface-level definitions, this is actually not harder to use than either of the two more specialized heaps.`auth (gmap X Y)` is a very frequently reoccurring RA, and finding all the right lemmas to compose for it can be challenging. After I saw people use `gen_heap` when really they want this RA, I am now convinced that we should have it in Iris. ;)
The only open question for me is, what is `Y`? (`X` is any countable type.)
* We probably should have fractions, so that would be `Y := frac * agree T`. Even if you don't need fractions, just making it always "1" should not be hard to use (we should just make sure to have a lemma that from owning the "1" fraction twice, derives `False`).
* @tchajed mentioned they also need something with agreement in a few places. So we could either also have a version with `Y := agree T`, or we could do the strictly more powerful thing (subsuming both of the above) and do `Y := (frac * agree T) + agree T`. I *think* with the right surface-level definitions, this is actually not harder to use than either of the two more specialized heaps.https://gitlab.mpi-sws.org/iris/iris/-/issues/327Add RA for auth max_nat2020-08-05T18:22:40ZRobbertAdd RA for auth max_natAs @tchajed pointed out, this RA is quite commonly used. While porting developments as a consequence of !461 I noticed it's also used in ReLoC.
So, concretely, there are the following uses:
- Iris: https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/heap_lang/lib/counter.v#L16
- ReLoC: https://gitlab.mpi-sws.org/iris/reloc/-/blob/7dca8f9472290626ac5174d5789512234ce115e9/theories/examples/symbol.v#L49
- Perennial: https://github.com/mit-pdos/perennial/blob/master/src/algebra/fmcounter.v
Would be good to add it to `algebra/lib` so people don't reprove the same stuff all the time.As @tchajed pointed out, this RA is quite commonly used. While porting developments as a consequence of !461 I noticed it's also used in ReLoC.
So, concretely, there are the following uses:
- Iris: https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/heap_lang/lib/counter.v#L16
- ReLoC: https://gitlab.mpi-sws.org/iris/reloc/-/blob/7dca8f9472290626ac5174d5789512234ce115e9/theories/examples/symbol.v#L49
- Perennial: https://github.com/mit-pdos/perennial/blob/master/src/algebra/fmcounter.v
Would be good to add it to `algebra/lib` so people don't reprove the same stuff all the time.https://gitlab.mpi-sws.org/iris/iris/-/issues/321Make `contractive_proper` into a lemma, or control other instances that make ...2020-07-14T08:20:29ZPaolo G. GiarrussoMake `contractive_proper` into a lemma, or control other instances that make it costly.Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that `proper_reflexive` is tried first, and then search diverges. Finding a way to blacklist certain instances for `Reflexive (equiv ==> equiv)%signature` would be useful — maybe removing them and replacing them with `Hint Extern`?Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that `proper_reflexive` is tried first, and then search diverges. Finding a way to blacklist certain instances for `Reflexive (equiv ==> equiv)%signature` would be useful — maybe removing them and replacing them with `Hint Extern`?https://gitlab.mpi-sws.org/iris/iris/-/issues/320λne should use %I for body — or add a variant using `%I`.2020-07-14T08:20:05ZPaolo G. Giarrussoλne should use %I for body — or add a variant using `%I`.For unbundled functions, I've used for a while a lambda notation that places the body automatically in `bi_scope`:
```coq
(** * Notation for functions in the Iris scope. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : function_scope.
```
Similarly, needing both `λne` and `%I` is annoying, what about:
```coq
Notation "'λneI' x .. y , t" :=
(@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t)%I _) ..) _)
(at level 200, x binder, y binder, right associativity).
```
I'd even consider placing that annotation in `λne` itself – `algebra.ofe` could import `bi.notation`; but many non-expansive functions aren't predicates :-).For unbundled functions, I've used for a while a lambda notation that places the body automatically in `bi_scope`:
```coq
(** * Notation for functions in the Iris scope. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : function_scope.
```
Similarly, needing both `λne` and `%I` is annoying, what about:
```coq
Notation "'λneI' x .. y , t" :=
(@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t)%I _) ..) _)
(at level 200, x binder, y binder, right associativity).
```
I'd even consider placing that annotation in `λne` itself – `algebra.ofe` could import `bi.notation`; but many non-expansive functions aren't predicates :-).Paolo G. GiarrussoPaolo G. Giarrussohttps://gitlab.mpi-sws.org/iris/iris/-/issues/317Use `byte` based strings for proof mode2020-05-16T19:16:11ZRobbertUse `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 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".
```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/316Explore use of `#[local]`/`Local` definitions2020-08-07T17:57:53ZRalf Jungjung@mpi-sws.orgExplore use of `#[local]`/`Local` definitionsI recently learned that in Coq, we can [mark a definition as not being imported with `Import`/`Export`](https://github.com/coq/coq/pull/12162#issuecomment-625186261). I think we should explore the option of using this to mark definitions that are internal to a module and should not be used by clients -- those then don't need the C-style namespacing of prefixing everything.
As a random example for such definitions, [consider these](https://gitlab.mpi-sws.org/iris/iris/-/blob/701b533c8be530a69e605ee5443a089146d5701f/theories/base_logic/lib/gen_heap.v#L136-164).
`Local Definition` is supported in Coq 8.9 (and maybe older) so we can start using it any time.I recently learned that in Coq, we can [mark a definition as not being imported with `Import`/`Export`](https://github.com/coq/coq/pull/12162#issuecomment-625186261). I think we should explore the option of using this to mark definitions that are internal to a module and should not be used by clients -- those then don't need the C-style namespacing of prefixing everything.
As a random example for such definitions, [consider these](https://gitlab.mpi-sws.org/iris/iris/-/blob/701b533c8be530a69e605ee5443a089146d5701f/theories/base_logic/lib/gen_heap.v#L136-164).
`Local Definition` is supported in Coq 8.9 (and maybe older) so we can start using it any time.https://gitlab.mpi-sws.org/iris/iris/-/issues/312Fix setoid rewriting for function application in Iris2020-04-22T22:59:30ZPaolo G. GiarrussoFix setoid rewriting for function application in IrisSome of you (me included) might have struggled rewriting into f a using H : f ≡ g. Today, a user called [Yannick Zakowski](https://coq.discourse.group/t/confused-with-a-failure-of-a-generalized-rewrite/783?u=blaisorblade) discovered a fix by reading rewrite's error message, and I adapted this to Iris:
```coq
From iris.algebra Require Import ofe.
Instance equiv_ext_discrete_fun {A B} :
subrelation (≡@{A -d> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance equiv_ext_ofe_mor {A B} :
subrelation (≡@{A -n> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance dist_ext_discrete_fun {A B n} :
subrelation (dist n (A := A -d> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
Instance dist_ext_ofe_mor {A B n} :
subrelation (dist n (A := A -n> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
```
I'm going to test this in my project first, to verify the performance implication and robustness, and to find again good testcases, but I thought I'd record this here in an issue.Some of you (me included) might have struggled rewriting into f a using H : f ≡ g. Today, a user called [Yannick Zakowski](https://coq.discourse.group/t/confused-with-a-failure-of-a-generalized-rewrite/783?u=blaisorblade) discovered a fix by reading rewrite's error message, and I adapted this to Iris:
```coq
From iris.algebra Require Import ofe.
Instance equiv_ext_discrete_fun {A B} :
subrelation (≡@{A -d> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance equiv_ext_ofe_mor {A B} :
subrelation (≡@{A -n> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance dist_ext_discrete_fun {A B n} :
subrelation (dist n (A := A -d> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
Instance dist_ext_ofe_mor {A B n} :
subrelation (dist n (A := A -n> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
```
I'm going to test this in my project first, to verify the performance implication and robustness, and to find again good testcases, but I thought I'd record this here in an issue.