From bc99b3c9e78a7aa9e3b75191af0807843977a7d1 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 5 Mar 2019 15:33:39 +0100
Subject: [PATCH 01/15] add documentation of the global RA pattern

IrisProofs.md  73 +++++++++++++++++++++++++++++++++++++++++++++++++++
README.md  13 +++++++
2 files changed, 84 insertions(+), 2 deletions()
create mode 100644 IrisProofs.md
diff git a/IrisProofs.md b/IrisProofs.md
new file mode 100644
index 000000000..510692fa7
 /dev/null
+++ b/IrisProofs.md
@@ 0,0 +1,73 @@
+# Iris Proof Guide
+
+This document serves to explain how Iris proofs are typically carried out in
+Coq: what are the common patterns, what are the common pitfalls. It is a
+workinprogress. Basically, if there is something Coqspecific that does not
+fit into the [proof mode documentation](ProofMode.md) or the
+[HeapLang documentation](HeapLang.md), then this document is the right place.
+
+## Resource algebra management
+
+When using ghost state in Iris, you have to make sure that the resource algebras
+you need are actually available. Every Iris proof is carried out using a
+universally quantified list `Σ: gFunctors` of functors defining which resource
+algebras are available. This is the *global* list of resources that the entire
+proof can use. We keep it universally quantified to enable composition of
+proofs.
+
+The assumptions that an Iris proof makes are collected the a typeclass called
+`somethingG`. The most common kind of assumptions is `inG`, which says that a
+particular resource algebra is available for ghost state. For example, in the
+[oneshot example](tests/one_shot.v):
+```
+Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
+```
+The `:>` means that the projection `one_shot_inG` is automatically registered as
+an instance for typeclass resolution. If you need several resource algebras,
+just add more `inG` fields. If you are using another library as part of yours,
+add a field like `one_shot_other :> otherG Σ`.
+
+Having defined the typeclass, we need to provide a way to instantiate it. This
+is an important step, as not every resource algebra can actually be used: if
+your resource algebra refers to `Σ`, the definition becomes recursive. That is
+actually legal under some conditions (which is why the global list `Σ` contains
+functors and not just resource algebras), but for the purpose of this guide we
+will ignore that case. We have to define a list that contains all the resource
+algebras we need:
+```
+Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
+```
+This time, there is no `Σ` in the context, so we cannot accidentally introduce a
+bad dependency. Now we can define the one and only instance that our typeclass
+will ever need:
+```
+Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
+Proof. solve_inG. Qed.
+```
+The `subG` assumption here says that the list `one_shotΣ` is a sublist of the
+global list `Σ`. Typically, this should be the only assumption your instance
+needs, showing that the assumptions of the library (and all the sublibraries it
+uses internally) can trivially be satisfied by picking the right `Σ`.
+
+Now you can add this assumption to all your library definitions and proofs. We
+typically use a section for this:
+```
+Section proof.
+Context `{!heapG Σ, !one_shotG Σ}.
+```
+Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
+which are assumptions that every HeapLang proof makes (they are related to
+defining the `↦` connective as well as the basic Iris infrastructure for
+invariants and WP). For this purpose, `heapG` contains not only assumptions
+about `Σ`, it also contains some ghost names to refer to particular ghost state.
+Hence it cannot be treated like a sublibrary that can be instantiated
+arbitrarily often; there can only be one global `heapG` instance that is
+propagated everywhere.
+
+The backtic (`` ` ``) is used to make anonymous assumptions and to automatically
+generalize the `Σ`. When adding assumptions with backtic, you should most of
+the time also add a `!` in front of every assumption. If you do not then Coq
+will also automatically generalize all indices of typeclasses that you are
+assuming. This can easily lead to making more assumptions than you are aware
+of, and often it leads to duplicate assumptions which breaks typeclass
+resolutions.
diff git a/README.md b/README.md
index 1d934d454..9c4cc7b56 100644
 a/README.md
+++ b/README.md
@@ 111,13 +111,17 @@ that should be compatible with this version:
## Further Resources
* Information on how to set up your editor for unicode input and output is
 collected in [Editor.md](Editor.md).
+Getting along with Iris in Coq:
+
+* Iris proof patterns are documented in [IrisProofs.md](IrisProofs.md).
* The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
* HeapLang (the Iris example language) and its tactics are documented at
[HeapLang.md](HeapLang.md).
* Naming conventions are documented at [Naming.md](Naming.md).
* The generated coqdoc is [available online](https://plv.mpisws.org/coqdoc/iris/).
+
+Contacting the developers:
+
* Discussion about the Iris Coq development happens on the mailing list
[irisclub@lists.mpisws.org](https://lists.mpisws.org/listinfo/irisclub)
and in the [Iris Chat](https://mattermost.mpisws.org/iris). This is also the
@@ 128,6 +132,11 @@ that should be compatible with this version:
[issue tracker](https://gitlab.mpisws.org/iris/iris/issues), which also
requires an MPISWS GitLab account.
* To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).
+
+Miscellaneous:
+
+* Information on how to set up your editor for unicode input and output is
+ collected in [Editor.md](Editor.md).
* If you are writing a paper that uses Iris in one way or another, you could use
the [Iris LaTeX macros](docs/iris.sty) for typesetting the various Iris
connectives.

GitLab
From bc3843764f7ec9ad77358fd5fa8c2de174820a2f Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 5 Mar 2019 16:05:52 +0100
Subject: [PATCH 02/15] be more explicit about savedAnythinG assuming F to be
contractive

theories/base_logic/lib/saved_prop.v  6 ++++
1 file changed, 4 insertions(+), 2 deletions()
diff git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index bc0a581d9..8b5e51cbf 100644
 a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ 8,8 +8,10 @@ Import uPred.
(* "Saved anything"  this can give you saved propositions, saved predicates,
saved whateveryoulike. *)
Class savedAnythingG (Σ : gFunctors) (F : cFunctor) :=
 saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ))).
+Class savedAnythingG (Σ : gFunctors) (F : cFunctor) := SavedAnythingG {
+ saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ)));
+ saved_anything_contractive : cFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
+}.
Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
#[ GFunctor (agreeRF F) ].

GitLab
From b50b07088f593fed72975b23494a7930bb1d9055 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 5 Mar 2019 16:06:02 +0100
Subject: [PATCH 03/15] more on global library assumptions

IrisProofs.md  65 +++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 61 insertions(+), 4 deletions()
diff git a/IrisProofs.md b/IrisProofs.md
index 510692fa7..1d390b40a 100644
 a/IrisProofs.md
+++ b/IrisProofs.md
@@ 59,10 +59,8 @@ Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
which are assumptions that every HeapLang proof makes (they are related to
defining the `↦` connective as well as the basic Iris infrastructure for
invariants and WP). For this purpose, `heapG` contains not only assumptions
about `Σ`, it also contains some ghost names to refer to particular ghost state.
Hence it cannot be treated like a sublibrary that can be instantiated
arbitrarily often; there can only be one global `heapG` instance that is
propagated everywhere.
+about `Σ`, it also contains some ghost names to refer to particular ghost state
+(see "global ghost state instances" below).
The backtic (`` ` ``) is used to make anonymous assumptions and to automatically
generalize the `Σ`. When adding assumptions with backtic, you should most of
@@ 71,3 +69,62 @@ will also automatically generalize all indices of typeclasses that you are
assuming. This can easily lead to making more assumptions than you are aware
of, and often it leads to duplicate assumptions which breaks typeclass
resolutions.
+
+### Advanced topic: Global ghost state instances
+
+Some Iris libraries involve a form of "global state". For example, defining the
+`↦` for HeapLang involves a piece of ghost state that matches the current
+physical heap. The `gname` of that ghost state must be picked once when the
+proof starts, and then globally known everywhere.
+
+Such libraries always need some kind of "initialization" to create an instance
+of their typeclass. For example, the initialization for `heapG` is happening as
+part of [`heap_adequacy`](theories/heap_lang/adequacy.v); the initialization
+lemma for the general heap construction it is using is
+[`gen_heap_init`](theories/base_logic/lib/gen_heap.v):
+```
+Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
+ (==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
+```
+These lemmas themselves only make assumptions the way normal libraries (those
+without global state) do, which are typically collected in a `somethingPreG`
+typeclass (such as `gen_heapPreG`). Just like in the normal case,
+`somethingPreG` typeclasses have an `Instance` showing that a `subG` is enough
+to instantiate them. The initialization lemma then shows that the
+`somethingPreG` typeclass is enough to create an instance of the main
+`somethingG` class *below a view shift*. This is written with an existential
+quantifier in the lemma because the statement after the view shift
+(`gen_heap_ctx σ` in this case) depends on having an instance of `gen_heapG` in
+the context.
+
+Given that these global ghost state instances are singletons, they must be
+assumed explicitly everywhere. Bundling `heapG` in a library typeclass like
+`one_shotG` would lose track of the fact that there exists just one `heapG`
+instance that is shared by everyone.
+
+### Advanced topic: Additional library assumptions
+
+Some libraries need additional assumptions. For example, the STS library is
+parameterized by an STS and assumes that the STS state space is inhabited:
+```
+Class stsG Σ (sts : stsT) := StsG {
+ sts_inG :> inG Σ (stsR sts);
+ sts_inhabited :> Inhabited (sts.state sts);
+}.
+```
+In this rather exceptional case, the `Instance` for this class has more than
+just a `subG` assumption:
+```
+Instance subG_stsΣ Σ sts :
+ subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
+```
+If users of this library follow the pattern described above, their own typeclass
+instance will check these additional assumption. But this is one more reason
+why it is important for every library to have an instance for its `somethingG`:
+to make sure that it does not accidentally make more assumptions than it intends
+to.
+
+Another subtle detail here is that the `subG` assumption comes first in
+`subG_stsΣ`, i.e., it appears before the `Inhabited`. This is important because
+otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes
+typeclass search diverge.

GitLab
From 1e329b25c286e87e926cc85cc169d191c4c0c9a7 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 5 Mar 2019 16:39:25 +0100
Subject: [PATCH 04/15] also explain how to obtain a closed proof

IrisProofs.md  27 +++++++++++++++++++++++++
tests/one_shot.v  3 +
2 files changed, 26 insertions(+), 4 deletions()
diff git a/IrisProofs.md b/IrisProofs.md
index 1d390b40a..8101848d7 100644
 a/IrisProofs.md
+++ b/IrisProofs.md
@@ 38,8 +38,9 @@ algebras we need:
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
```
This time, there is no `Σ` in the context, so we cannot accidentally introduce a
bad dependency. Now we can define the one and only instance that our typeclass
will ever need:
+bad dependency. If you are using another library as part of yours, add their
+`somethingΣ` to yours. Now we can define the one and only instance that our
+typeclass will ever need:
```
Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
Proof. solve_inG. Qed.
@@ 70,6 +71,28 @@ assuming. This can easily lead to making more assumptions than you are aware
of, and often it leads to duplicate assumptions which breaks typeclass
resolutions.
+### Obtaining a closed proof
+
+To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
+`inG`, you have to assemble a list of functors of all the involved libraries,
+and if your proof relies on some singleton (most do), you have to call the
+respective initialziation or adequacy lemma. [For example](tests/one_shot.v):
+```
+Section client.
+ Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
+
+ Lemma client_safe : WP client {{ _, True }}%I.
+ (* ... *)
+End client.
+
+(** Assemble all functors needed by the [client_safe] proof. *)
+Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
+
+(** Apply [heap_adequacy] with this list of all functors. *)
+Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
+Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
+```
+
### Advanced topic: Global ghost state instances
Some Iris libraries involve a form of "global state". For example, defining the
diff git a/tests/one_shot.v b/tests/one_shot.v
index a71159b6a..1b5ff38cf 100644
 a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ 103,11 +103,10 @@ Definition client : expr :=
(Fst "ff" #5  let: "check" := Snd "ff" #() in "check" #()).
Section client.
 Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
Lemma client_safe : WP client {{ _, True }}%I.
 Proof.
+ Proof using Type*.
rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]".
wp_let. wp_apply wp_par.
 wp_apply "Hf1".

GitLab
From 028531ed901941f78e1307141ef87a45963616c4 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 5 Mar 2019 17:34:17 +0100
Subject: [PATCH 05/15] typos

IrisProofs.md  4 ++
1 file changed, 2 insertions(+), 2 deletions()
diff git a/IrisProofs.md b/IrisProofs.md
index 8101848d7..3cfd359cb 100644
 a/IrisProofs.md
+++ b/IrisProofs.md
@@ 15,7 +15,7 @@ algebras are available. This is the *global* list of resources that the entire
proof can use. We keep it universally quantified to enable composition of
proofs.
The assumptions that an Iris proof makes are collected the a typeclass called
+The assumptions that an Iris proof makes are collected in a typeclass called
`somethingG`. The most common kind of assumptions is `inG`, which says that a
particular resource algebra is available for ghost state. For example, in the
[oneshot example](tests/one_shot.v):
@@ 76,7 +76,7 @@ resolutions.
To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
`inG`, you have to assemble a list of functors of all the involved libraries,
and if your proof relies on some singleton (most do), you have to call the
respective initialziation or adequacy lemma. [For example](tests/one_shot.v):
+respective initialization or adequacy lemma. [For example](tests/one_shot.v):
```
Section client.
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.

GitLab
From fa8f7be05a1afe2c414703035007d115a7962f4a Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 6 Mar 2019 10:29:41 +0100
Subject: [PATCH 06/15] refer to TID

IrisProofs.md  4 +++
1 file changed, 3 insertions(+), 1 deletion()
diff git a/IrisProofs.md b/IrisProofs.md
index 3cfd359cb..348ef2d01 100644
 a/IrisProofs.md
+++ b/IrisProofs.md
@@ 13,7 +13,9 @@ you need are actually available. Every Iris proof is carried out using a
universally quantified list `Σ: gFunctors` of functors defining which resource
algebras are available. This is the *global* list of resources that the entire
proof can use. We keep it universally quantified to enable composition of
proofs.
+proofs. The formal side of this is described in §7.4 of
+[The Iris Documentation](http://plv.mpisws.org/iris/appendix3.1.pdf); here we
+describe the Coq aspects of this approach.
The assumptions that an Iris proof makes are collected in a typeclass called
`somethingG`. The most common kind of assumptions is `inG`, which says that a

GitLab
From 701458c6bd96df26c3c3e979c8838ca425228230 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 6 Mar 2019 10:58:48 +0100
Subject: [PATCH 07/15] library > module

IrisProofs.md  26 +++++++++++++
1 file changed, 13 insertions(+), 13 deletions()
diff git a/IrisProofs.md b/IrisProofs.md
index 348ef2d01..366f758f2 100644
 a/IrisProofs.md
+++ b/IrisProofs.md
@@ 26,7 +26,7 @@ Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
```
The `:>` means that the projection `one_shot_inG` is automatically registered as
an instance for typeclass resolution. If you need several resource algebras,
just add more `inG` fields. If you are using another library as part of yours,
+just add more `inG` fields. If you are using another module as part of yours,
add a field like `one_shot_other :> otherG Σ`.
Having defined the typeclass, we need to provide a way to instantiate it. This
@@ 40,7 +40,7 @@ algebras we need:
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
```
This time, there is no `Σ` in the context, so we cannot accidentally introduce a
bad dependency. If you are using another library as part of yours, add their
+bad dependency. If you are using another module as part of yours, add their
`somethingΣ` to yours. Now we can define the one and only instance that our
typeclass will ever need:
```
@@ 49,10 +49,10 @@ Proof. solve_inG. Qed.
```
The `subG` assumption here says that the list `one_shotΣ` is a sublist of the
global list `Σ`. Typically, this should be the only assumption your instance
needs, showing that the assumptions of the library (and all the sublibraries it
+needs, showing that the assumptions of the module (and all the modules it
uses internally) can trivially be satisfied by picking the right `Σ`.
Now you can add this assumption to all your library definitions and proofs. We
+Now you can add this assumption to all your module definitions and proofs. We
typically use a section for this:
```
Section proof.
@@ 76,7 +76,7 @@ resolutions.
### Obtaining a closed proof
To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
`inG`, you have to assemble a list of functors of all the involved libraries,
+`inG`, you have to assemble a list of functors of all the involved modules,
and if your proof relies on some singleton (most do), you have to call the
respective initialization or adequacy lemma. [For example](tests/one_shot.v):
```
@@ 97,12 +97,12 @@ Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
### Advanced topic: Global ghost state instances
Some Iris libraries involve a form of "global state". For example, defining the
+Some Iris modules involve a form of "global state". For example, defining the
`↦` for HeapLang involves a piece of ghost state that matches the current
physical heap. The `gname` of that ghost state must be picked once when the
proof starts, and then globally known everywhere.
Such libraries always need some kind of "initialization" to create an instance
+Such modules always need some kind of "initialization" to create an instance
of their typeclass. For example, the initialization for `heapG` is happening as
part of [`heap_adequacy`](theories/heap_lang/adequacy.v); the initialization
lemma for the general heap construction it is using is
@@ 111,7 +111,7 @@ lemma for the general heap construction it is using is
Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
(==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
```
These lemmas themselves only make assumptions the way normal libraries (those
+These lemmas themselves only make assumptions the way normal modules (those
without global state) do, which are typically collected in a `somethingPreG`
typeclass (such as `gen_heapPreG`). Just like in the normal case,
`somethingPreG` typeclasses have an `Instance` showing that a `subG` is enough
@@ 123,13 +123,13 @@ quantifier in the lemma because the statement after the view shift
the context.
Given that these global ghost state instances are singletons, they must be
assumed explicitly everywhere. Bundling `heapG` in a library typeclass like
+assumed explicitly everywhere. Bundling `heapG` in a module typeclass like
`one_shotG` would lose track of the fact that there exists just one `heapG`
instance that is shared by everyone.
### Advanced topic: Additional library assumptions
+### Advanced topic: Additional module assumptions
Some libraries need additional assumptions. For example, the STS library is
+Some modules need additional assumptions. For example, the STS module is
parameterized by an STS and assumes that the STS state space is inhabited:
```
Class stsG Σ (sts : stsT) := StsG {
@@ 143,9 +143,9 @@ just a `subG` assumption:
Instance subG_stsΣ Σ sts :
subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
```
If users of this library follow the pattern described above, their own typeclass
+If users of this module follow the pattern described above, their own typeclass
instance will check these additional assumption. But this is one more reason
why it is important for every library to have an instance for its `somethingG`:
+why it is important for every module to have an instance for its `somethingG`:
to make sure that it does not accidentally make more assumptions than it intends
to.

GitLab
From ef3d9111ef1f704e196ec1e7e57a65a194ba031d Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 6 Mar 2019 10:59:59 +0100
Subject: [PATCH 08/15] add a forward ref

IrisProofs.md  7 ++++
1 file changed, 4 insertions(+), 3 deletions()
diff git a/IrisProofs.md b/IrisProofs.md
index 366f758f2..23a4c03ae 100644
 a/IrisProofs.md
+++ b/IrisProofs.md
@@ 77,8 +77,9 @@ resolutions.
To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
`inG`, you have to assemble a list of functors of all the involved modules,
and if your proof relies on some singleton (most do), you have to call the
respective initialization or adequacy lemma. [For example](tests/one_shot.v):
+and if your proof relies on some singleton (most do, at least indirectly; also
+see the next section), you have to call the respective initialization or
+adequacy lemma. [For example](tests/one_shot.v):
```
Section client.
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
@@ 95,7 +96,7 @@ Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
```
### Advanced topic: Global ghost state instances
+### Advanced topic: Ghost state singletons
Some Iris modules involve a form of "global state". For example, defining the
`↦` for HeapLang involves a piece of ghost state that matches the current

GitLab
From 8679b07fe84243cd88c988470da0e19de900e5ea Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 6 Mar 2019 11:15:05 +0100
Subject: [PATCH 09/15] rename things a bit

IrisProofs.md => ProofGuide.md  6 +
README.md  10 ++
StyleGuide.md  98 ++++++++++++++++++++++++++++++++++
3 files changed, 106 insertions(+), 8 deletions()
rename IrisProofs.md => ProofGuide.md (97%)
create mode 100644 StyleGuide.md
diff git a/IrisProofs.md b/ProofGuide.md
similarity index 97%
rename from IrisProofs.md
rename to ProofGuide.md
index 23a4c03ae..5e6070145 100644
 a/IrisProofs.md
+++ b/ProofGuide.md
@@ 2,9 +2,9 @@
This document serves to explain how Iris proofs are typically carried out in
Coq: what are the common patterns, what are the common pitfalls. It is a
workinprogress. Basically, if there is something Coqspecific that does not
fit into the [proof mode documentation](ProofMode.md) or the
[HeapLang documentation](HeapLang.md), then this document is the right place.
+workinprogress. This complements the tactic documentation for the
+[proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as well as the
+documentation of syntactic conventions in the [style guide](StyleGuide.md).
## Resource algebra management
diff git a/README.md b/README.md
index 9c4cc7b56..4312f7b6f 100644
 a/README.md
+++ b/README.md
@@ 113,11 +113,11 @@ that should be compatible with this version:
Getting along with Iris in Coq:
* Iris proof patterns are documented in [IrisProofs.md](IrisProofs.md).
* The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
* HeapLang (the Iris example language) and its tactics are documented at
 [HeapLang.md](HeapLang.md).
* Naming conventions are documented at [Naming.md](Naming.md).
+* Iris proof patterns are documented in the [proof guide](ProofGuide.md).
+* Syntactic conventions are described in the [style guide](StyleGuide.md).
+* The Iris tactics are described in the
+ [the Iris Proof Mode (IPM) / MoSeL documentation](ProofMode.md) as well as the
+ [HeapLang documentation](HeapLang.md).
* The generated coqdoc is [available online](https://plv.mpisws.org/coqdoc/iris/).
Contacting the developers:
diff git a/StyleGuide.md b/StyleGuide.md
new file mode 100644
index 000000000..66857f16f
 /dev/null
+++ b/StyleGuide.md
@@ 0,0 +1,98 @@
+# Iris Style Guide
+
+This document lays down syntactic conventions about how we usually write our Iris proofs in Coq.
+It is a workinprogress.
+This complements the tactic documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as well as the [proof guide](ProofGuide.md).
+
+## Implicit generalization
+
+We often use the implicit generalization feature of Coq, triggered by a backtic: `` `{!term A B}`` means that an implicit argument of type `term A B` is added, and if any of the identifiers that are used here is not yet bound, it gets added as well.
+Usually, `term` will be some existing typeclass or similar, and we use this syntax to also generalize over `A` and `B`; then the above is equivalent to `{A B} {Hterm: term A B}`.
+The `!` in front of the term disables an even stronger form of generalization, where if `term` is a typeclass then all missing arguments get implicitly generalized as well.
+This is sometimes useful, e.g. we can write `` `{Countable C}`` instead of `` `{!EqDecision C, !Countable C}``.
+However, generally it is more important to be aware of the assumptions you are making, so implicit generalization without `!` should be avoided.
+
+## Naming conventions for variables/arguments/hypotheses
+
+### small letters
+
+* a : A = cmraT or cofeT
+* b : B = cmraT or cofeT
+* c
+* d
+* e : expr = expressions
+* f = some generic function
+* g = some generic function
+* h : heap
+* i
+* j
+* k
+* l
+* m : iGst = ghost state
+* m* = prefix for option
+* n
+* o
+* p
+* q
+* r : iRes = resources
+* s = state (STSs)
+* s = stuckness bits
+* t
+* u
+* v : val = values of language
+* w
+* x
+* y
+* z
+
+### capital letters
+
+* A : Type, cmraT or cofeT
+* B : Type, cmraT or cofeT
+* C
+* D
+* E : coPset = Viewshift masks
+* F = a functor
+* G
+* H = hypotheses
+* I = indexing sets
+* J
+* K : ectx = evaluation contexts
+* K = keys of a map
+* L
+* M = maps / global CMRA
+* N : namespace
+* O
+* P : uPred, iProp or Prop
+* Q : uPred, iProp or Prop
+* R : uPred, iProp or Prop
+* S : set state = state sets in STSs
+* T : set token = token sets in STSs
+* U
+* V : abstraction of value type in frame shift assertions
+* W
+* X : sets
+* Y : sets
+* Z : sets
+
+### small greek letters
+
+* γ : gname
+* σ : state = state of language
+* φ : interpretation of STS/Auth
+
+### capital greek letters
+
+* Φ : general predicate (over uPred, iProp or Prop)
+* Ψ : general predicate (over uPred, iProp or Prop)
+
+## Naming conventions for algebraic classes
+
+### Suffixes
+
+* C: OFEs
+* R: cameras
+* UR: unital cameras or resources algebras
+* F: functors (can be combined with all of the above, e.g. CF is an OFE functor)
+* G: global camera functor management
+* T: canonical structurs for algebraic classes (for example ofeT for OFEs, cmraT for cameras)

GitLab
From 0fd1aeab87af72ad4bf05ef52fb43a48ff4bbcd4 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 6 Mar 2019 11:23:53 +0100
Subject: [PATCH 10/15] short reference to material about canonical structures
and type classes

ProofGuide.md  38 ++++++++++++++++++++++
StyleGuide.md  4 ++
2 files changed, 24 insertions(+), 18 deletions()
diff git a/ProofGuide.md b/ProofGuide.md
index 5e6070145..4e87f2b80 100644
 a/ProofGuide.md
+++ b/ProofGuide.md
@@ 1,10 +1,8 @@
# Iris Proof Guide
This document serves to explain how Iris proofs are typically carried out in
Coq: what are the common patterns, what are the common pitfalls. It is a
workinprogress. This complements the tactic documentation for the
[proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as well as the
documentation of syntactic conventions in the [style guide](StyleGuide.md).
+This document serves to explain how Iris proofs are typically carried out in Coq: what are the common patterns, what are the common pitfalls.
+It is a workinprogress.
+This complements the tactic documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in the [style guide](StyleGuide.md).
## Resource algebra management
@@ 17,7 +15,7 @@ proofs. The formal side of this is described in §7.4 of
[The Iris Documentation](http://plv.mpisws.org/iris/appendix3.1.pdf); here we
describe the Coq aspects of this approach.
The assumptions that an Iris proof makes are collected in a typeclass called
+The assumptions that an Iris proof makes are collected in a type class called
`somethingG`. The most common kind of assumptions is `inG`, which says that a
particular resource algebra is available for ghost state. For example, in the
[oneshot example](tests/one_shot.v):
@@ 29,7 +27,7 @@ an instance for typeclass resolution. If you need several resource algebras,
just add more `inG` fields. If you are using another module as part of yours,
add a field like `one_shot_other :> otherG Σ`.
Having defined the typeclass, we need to provide a way to instantiate it. This
+Having defined the type class, we need to provide a way to instantiate it. This
is an important step, as not every resource algebra can actually be used: if
your resource algebra refers to `Σ`, the definition becomes recursive. That is
actually legal under some conditions (which is why the global list `Σ` contains
@@ 42,7 +40,7 @@ Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
This time, there is no `Σ` in the context, so we cannot accidentally introduce a
bad dependency. If you are using another module as part of yours, add their
`somethingΣ` to yours. Now we can define the one and only instance that our
typeclass will ever need:
+type class will ever need:
```
Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
Proof. solve_inG. Qed.
@@ 70,7 +68,7 @@ generalize the `Σ`. When adding assumptions with backtic, you should most of
the time also add a `!` in front of every assumption. If you do not then Coq
will also automatically generalize all indices of typeclasses that you are
assuming. This can easily lead to making more assumptions than you are aware
of, and often it leads to duplicate assumptions which breaks typeclass
+of, and often it leads to duplicate assumptions which breaks type class
resolutions.
### Obtaining a closed proof
@@ 104,7 +102,7 @@ physical heap. The `gname` of that ghost state must be picked once when the
proof starts, and then globally known everywhere.
Such modules always need some kind of "initialization" to create an instance
of their typeclass. For example, the initialization for `heapG` is happening as
+of their type class. For example, the initialization for `heapG` is happening as
part of [`heap_adequacy`](theories/heap_lang/adequacy.v); the initialization
lemma for the general heap construction it is using is
[`gen_heap_init`](theories/base_logic/lib/gen_heap.v):
@@ 114,17 +112,17 @@ Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
```
These lemmas themselves only make assumptions the way normal modules (those
without global state) do, which are typically collected in a `somethingPreG`
typeclass (such as `gen_heapPreG`). Just like in the normal case,
`somethingPreG` typeclasses have an `Instance` showing that a `subG` is enough
+type class (such as `gen_heapPreG`). Just like in the normal case,
+`somethingPreG` type classes have an `Instance` showing that a `subG` is enough
to instantiate them. The initialization lemma then shows that the
`somethingPreG` typeclass is enough to create an instance of the main
+`somethingPreG` type class is enough to create an instance of the main
`somethingG` class *below a view shift*. This is written with an existential
quantifier in the lemma because the statement after the view shift
(`gen_heap_ctx σ` in this case) depends on having an instance of `gen_heapG` in
the context.
Given that these global ghost state instances are singletons, they must be
assumed explicitly everywhere. Bundling `heapG` in a module typeclass like
+assumed explicitly everywhere. Bundling `heapG` in a module type class like
`one_shotG` would lose track of the fact that there exists just one `heapG`
instance that is shared by everyone.
@@ 144,7 +142,7 @@ just a `subG` assumption:
Instance subG_stsΣ Σ sts :
subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
```
If users of this module follow the pattern described above, their own typeclass
+If users of this module follow the pattern described above, their own type class
instance will check these additional assumption. But this is one more reason
why it is important for every module to have an instance for its `somethingG`:
to make sure that it does not accidentally make more assumptions than it intends
@@ 153,4 +151,12 @@ to.
Another subtle detail here is that the `subG` assumption comes first in
`subG_stsΣ`, i.e., it appears before the `Inhabited`. This is important because
otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes
typeclass search diverge.
+type class search diverge.
+
+## Canonical structures and type classes
+
+In Iris, we use both canonical structures and type classes, and some careful tweaking is necessary to make the two work together properly.
+The details of this still need to be written up properly, but here is some background material:
+
+* [Type Classes for Mathematics in Type Theory](http://www.eelis.net/research/mathclasses/mscs.pdf)
+* [Canonical Structures for the working Coq user](https://hal.inria.fr/hal00816703v1/document)
diff git a/StyleGuide.md b/StyleGuide.md
index 66857f16f..b8e5819af 100644
 a/StyleGuide.md
+++ b/StyleGuide.md
@@ 7,8 +7,8 @@ This complements the tactic documentation for the [proof mode](ProofMode.md) and
## Implicit generalization
We often use the implicit generalization feature of Coq, triggered by a backtic: `` `{!term A B}`` means that an implicit argument of type `term A B` is added, and if any of the identifiers that are used here is not yet bound, it gets added as well.
Usually, `term` will be some existing typeclass or similar, and we use this syntax to also generalize over `A` and `B`; then the above is equivalent to `{A B} {Hterm: term A B}`.
The `!` in front of the term disables an even stronger form of generalization, where if `term` is a typeclass then all missing arguments get implicitly generalized as well.
+Usually, `term` will be some existing type class or similar, and we use this syntax to also generalize over `A` and `B`; then the above is equivalent to `{A B} {Hterm: term A B}`.
+The `!` in front of the term disables an even stronger form of generalization, where if `term` is a type class then all missing arguments get implicitly generalized as well.
This is sometimes useful, e.g. we can write `` `{Countable C}`` instead of `` `{!EqDecision C, !Countable C}``.
However, generally it is more important to be aware of the assumptions you are making, so implicit generalization without `!` should be avoided.

GitLab
From 899e4fb1fb075780927804ff0964a3feb83c9a75 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 6 Mar 2019 12:09:49 +0100
Subject: [PATCH 11/15] mention Typeclasses Opaque

StyleGuide.md  8 ++++++++
1 file changed, 8 insertions(+)
diff git a/StyleGuide.md b/StyleGuide.md
index b8e5819af..c71e25d86 100644
 a/StyleGuide.md
+++ b/StyleGuide.md
@@ 12,6 +12,14 @@ The `!` in front of the term disables an even stronger form of generalization, w
This is sometimes useful, e.g. we can write `` `{Countable C}`` instead of `` `{!EqDecision C, !Countable C}``.
However, generally it is more important to be aware of the assumptions you are making, so implicit generalization without `!` should be avoided.
+## Type class resolution control
+
+When you are writing a module that exports some Iris term for others to use (e.g., `join_handle` in the [spawn module](theories/heap_lang/lib/spawn.v)), be sure to mark these terms as opaque for type class search at the *end* of your module (and outside any section):
+```
+Typeclasses Opaque join_handle.
+```
+This makes sure that the proof mode does not "look into" your definition when it is used by clients.
+
## Naming conventions for variables/arguments/hypotheses
### small letters

GitLab
From a416acbd518ed66d1c05ae95228de883642f8762 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 6 Mar 2019 13:39:44 +0100
Subject: [PATCH 12/15] forgot to remove this

Naming.md  84 
1 file changed, 84 deletions()
delete mode 100644 Naming.md
diff git a/Naming.md b/Naming.md
deleted file mode 100644
index b330260a8..000000000
 a/Naming.md
+++ /dev/null
@@ 1,84 +0,0 @@
# Naming conventions for variables/arguments/hypotheses in the Coq development

## small letters

* a : A = cmraT or cofeT
* b : B = cmraT or cofeT
* c
* d
* e : expr = expressions
* f = some generic function
* g = some generic function
* h : heap
* i
* j
* k
* l
* m : iGst = ghost state
* m* = prefix for option
* n
* o
* p
* q
* r : iRes = resources
* s = state (STSs)
* s = stuckness bits
* t
* u
* v : val = values of language
* w
* x
* y
* z

## capital letters

* A : Type, cmraT or cofeT
* B : Type, cmraT or cofeT
* C
* D
* E : coPset = Viewshift masks
* F = a functor
* G
* H = hypotheses
* I = indexing sets
* J
* K : ectx = evaluation contexts
* K = keys of a map
* L
* M = maps / global CMRA
* N : namespace
* O
* P : uPred, iProp or Prop
* Q : uPred, iProp or Prop
* R : uPred, iProp or Prop
* S : set state = state sets in STSs
* T : set token = token sets in STSs
* U
* V : abstraction of value type in frame shift assertions
* W
* X : sets
* Y : sets
* Z : sets

## small greek letters

* γ : gname
* σ : state = state of language
* φ : interpretation of STS/Auth

## capital greek letters

* Φ : general predicate (over uPred, iProp or Prop)
* Ψ : general predicate (over uPred, iProp or Prop)

# Naming conventions for algebraic classes in the Coq development

## Suffixes

* C: OFEs
* R: cameras
* UR: unital cameras or resources algebras
* F: functors (can be combined with all of the above, e.g. CF is an OFE functor)
* G: global camera functor management
* T: canonical structurs for algebraic classes (for example ofeT for OFEs, cmraT for cameras)

GitLab
From 27276f03f99bf21a2038f82fdcc1a9668ce88ed8 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Thu, 7 Mar 2019 16:14:40 +0100
Subject: [PATCH 13/15] tweak and expand

ProofGuide.md  60 +++++++++++++++++++++++++++++++++
1 file changed, 39 insertions(+), 21 deletions()
diff git a/ProofGuide.md b/ProofGuide.md
index 4e87f2b80..766777d7a 100644
 a/ProofGuide.md
+++ b/ProofGuide.md
@@ 1,17 +1,18 @@
# Iris Proof Guide
This document serves to explain how Iris proofs are typically carried out in Coq: what are the common patterns, what are the common pitfalls.
It is a workinprogress.
+This workinprogress document serves to explain how Iris proofs are typically carried out in Coq: what are the common patterns, what are the common pitfalls.
This complements the tactic documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in the [style guide](StyleGuide.md).
## Resource algebra management
When using ghost state in Iris, you have to make sure that the resource algebras
you need are actually available. Every Iris proof is carried out using a
universally quantified list `Σ: gFunctors` of functors defining which resource
algebras are available. This is the *global* list of resources that the entire
proof can use. We keep it universally quantified to enable composition of
proofs. The formal side of this is described in §7.4 of
+universally quantified list `Σ: gFunctors` defining which resource algebras are
+available. You can think of this as a list of resource algebras, though in
+reality it is a list of functors from OFEs to Cameras (where Cameras are a
+stepindexed generalization of resource algebras). This is the *global* list of
+resources that the entire proof can use. We keep it universally quantified to
+enable composition of proofs. The formal side of this is described in §7.4 of
[The Iris Documentation](http://plv.mpisws.org/iris/appendix3.1.pdf); here we
describe the Coq aspects of this approach.
@@ 50,8 +51,8 @@ global list `Σ`. Typically, this should be the only assumption your instance
needs, showing that the assumptions of the module (and all the modules it
uses internally) can trivially be satisfied by picking the right `Σ`.
Now you can add this assumption to all your module definitions and proofs. We
typically use a section for this:
+Now you can add `one_shotG` as an assumption to all your module definitions and
+proofs. We typically use a section for this:
```
Section proof.
Context `{!heapG Σ, !one_shotG Σ}.
@@ 99,12 +100,19 @@ Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
Some Iris modules involve a form of "global state". For example, defining the
`↦` for HeapLang involves a piece of ghost state that matches the current
physical heap. The `gname` of that ghost state must be picked once when the
proof starts, and then globally known everywhere.
+proof starts, and then globally known everywhere. Hence it is added to
+`gen_heapG`, the type class for the generalized heap module:
+```
+Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+ gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
+ gen_heap_name : gname
+}.
+```
Such modules always need some kind of "initialization" to create an instance
of their type class. For example, the initialization for `heapG` is happening as
part of [`heap_adequacy`](theories/heap_lang/adequacy.v); the initialization
lemma for the general heap construction it is using is
+of their type class. For example, the initialization for `heapG` is happening
+as part of [`heap_adequacy`](theories/heap_lang/adequacy.v); this in turn uses
+the initialization lemma for `gen_heapG` from
[`gen_heap_init`](theories/base_logic/lib/gen_heap.v):
```
Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
@@ 112,14 +120,24 @@ Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
```
These lemmas themselves only make assumptions the way normal modules (those
without global state) do, which are typically collected in a `somethingPreG`
type class (such as `gen_heapPreG`). Just like in the normal case,
`somethingPreG` type classes have an `Instance` showing that a `subG` is enough
to instantiate them. The initialization lemma then shows that the
`somethingPreG` type class is enough to create an instance of the main
`somethingG` class *below a view shift*. This is written with an existential
quantifier in the lemma because the statement after the view shift
(`gen_heap_ctx σ` in this case) depends on having an instance of `gen_heapG` in
the context.
+type class (such as `gen_heapPreG`):
+```
+Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+ gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V))
+}.
+```
+Just like in the normal case, `somethingPreG` type classes have an `Instance`
+showing that a `subG` is enough to instantiate them:
+```
+Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
+ subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
+Proof. solve_inG. Qed.
+```
+The initialization lemma then shows that the `somethingPreG` type class is
+enough to create an instance of the main `somethingG` class *below a view
+shift*. This is written with an existential quantifier in the lemma because the
+statement after the view shift (`gen_heap_ctx σ` in this case) depends on having
+an instance of `gen_heapG` in the context.
Given that these global ghost state instances are singletons, they must be
assumed explicitly everywhere. Bundling `heapG` in a module type class like
@@ 131,7 +149,7 @@ instance that is shared by everyone.
Some modules need additional assumptions. For example, the STS module is
parameterized by an STS and assumes that the STS state space is inhabited:
```
Class stsG Σ (sts : stsT) := StsG {
+Class stsG Σ (sts : stsT) := {
sts_inG :> inG Σ (stsR sts);
sts_inhabited :> Inhabited (sts.state sts);
}.

GitLab
From 316b4d4def5304d5adc3dffd3bd46e56e0b869ac Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Thu, 7 Mar 2019 16:17:16 +0100
Subject: [PATCH 14/15] example for more than 1 functor

ProofGuide.md  8 ++++++
1 file changed, 6 insertions(+), 2 deletions()
diff git a/ProofGuide.md b/ProofGuide.md
index 766777d7a..ae1572fb8 100644
 a/ProofGuide.md
+++ b/ProofGuide.md
@@ 40,8 +40,12 @@ Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
```
This time, there is no `Σ` in the context, so we cannot accidentally introduce a
bad dependency. If you are using another module as part of yours, add their
`somethingΣ` to yours. Now we can define the one and only instance that our
type class will ever need:
+`somethingΣ` to yours, as in `#[GFunctor one_shotR; somethingΣ]`. (The
+`#[F1; F2; ...]` syntax *appends* the functor lists `F1`, `F2`, ... to each
+other; together with a coercion from a single functor to a singleton list, this
+means lists can be nested arbitrarily.)
+
+Now we can define the one and only instance that our type class will ever need:
```
Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
Proof. solve_inG. Qed.

GitLab
From e4b963fc37c8987f196f71e07f86a28c1bf762fd Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Fri, 8 Mar 2019 11:17:35 +0100
Subject: [PATCH 15/15] linebreak

ProofGuide.md  12 ++++++++
StyleGuide.md  32 ++++++++++++++++++++++
2 files changed, 30 insertions(+), 14 deletions()
diff git a/ProofGuide.md b/ProofGuide.md
index ae1572fb8..df476850f 100644
 a/ProofGuide.md
+++ b/ProofGuide.md
@@ 1,7 +1,10 @@
# Iris Proof Guide
This workinprogress document serves to explain how Iris proofs are typically carried out in Coq: what are the common patterns, what are the common pitfalls.
This complements the tactic documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in the [style guide](StyleGuide.md).
+This workinprogress document serves to explain how Iris proofs are typically
+carried out in Coq: what are the common patterns, what are the common pitfalls.
+This complements the tactic documentation for the [proof mode](ProofMode.md) and
+[HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in
+the [style guide](StyleGuide.md).
## Resource algebra management
@@ 177,8 +180,9 @@ type class search diverge.
## Canonical structures and type classes
In Iris, we use both canonical structures and type classes, and some careful tweaking is necessary to make the two work together properly.
The details of this still need to be written up properly, but here is some background material:
+In Iris, we use both canonical structures and type classes, and some careful
+tweaking is necessary to make the two work together properly. The details of
+this still need to be written up properly, but here is some background material:
* [Type Classes for Mathematics in Type Theory](http://www.eelis.net/research/mathclasses/mscs.pdf)
* [Canonical Structures for the working Coq user](https://hal.inria.fr/hal00816703v1/document)
diff git a/StyleGuide.md b/StyleGuide.md
index c71e25d86..56d55f39e 100644
 a/StyleGuide.md
+++ b/StyleGuide.md
@@ 1,24 +1,36 @@
# Iris Style Guide
This document lays down syntactic conventions about how we usually write our Iris proofs in Coq.
It is a workinprogress.
This complements the tactic documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as well as the [proof guide](ProofGuide.md).
+This document lays down syntactic conventions about how we usually write our
+Iris proofs in Coq. It is a workinprogress. This complements the tactic
+documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as
+well as the [proof guide](ProofGuide.md).
## Implicit generalization
We often use the implicit generalization feature of Coq, triggered by a backtic: `` `{!term A B}`` means that an implicit argument of type `term A B` is added, and if any of the identifiers that are used here is not yet bound, it gets added as well.
Usually, `term` will be some existing type class or similar, and we use this syntax to also generalize over `A` and `B`; then the above is equivalent to `{A B} {Hterm: term A B}`.
The `!` in front of the term disables an even stronger form of generalization, where if `term` is a type class then all missing arguments get implicitly generalized as well.
This is sometimes useful, e.g. we can write `` `{Countable C}`` instead of `` `{!EqDecision C, !Countable C}``.
However, generally it is more important to be aware of the assumptions you are making, so implicit generalization without `!` should be avoided.
+We often use the implicit generalization feature of Coq, triggered by a backtic:
+`` `{!term A B}`` means that an implicit argument of type `term A B` is added,
+and if any of the identifiers that are used here is not yet bound, it gets added
+as well. Usually, `term` will be some existing type class or similar, and we
+use this syntax to also generalize over `A` and `B`; then the above is
+equivalent to `{A B} {Hterm: term A B}`. The `!` in front of the term disables
+an even stronger form of generalization, where if `term` is a type class then
+all missing arguments get implicitly generalized as well. This is sometimes
+useful, e.g. we can write `` `{Countable C}`` instead of `` `{!EqDecision C,
+!Countable C}``. However, generally it is more important to be aware of the
+assumptions you are making, so implicit generalization without `!` should be
+avoided.
## Type class resolution control
When you are writing a module that exports some Iris term for others to use (e.g., `join_handle` in the [spawn module](theories/heap_lang/lib/spawn.v)), be sure to mark these terms as opaque for type class search at the *end* of your module (and outside any section):
+When you are writing a module that exports some Iris term for others to use
+(e.g., `join_handle` in the [spawn module](theories/heap_lang/lib/spawn.v)), be
+sure to mark these terms as opaque for type class search at the *end* of your
+module (and outside any section):
```
Typeclasses Opaque join_handle.
```
This makes sure that the proof mode does not "look into" your definition when it is used by clients.
+This makes sure that the proof mode does not "look into" your definition when it
+is used by clients.
## Naming conventions for variables/arguments/hypotheses

GitLab