Skip to content
Snippets Groups Projects
Commit 8cfe4ceb authored by Ralf Jung's avatar Ralf Jung
Browse files

split RA docs into separate file, and general doc updates

parent 7f8b01a9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
docs/heap_lang.md
+ 1
− 1
View file @ 8cfe4ceb
......@@ -33,7 +33,7 @@ constructor).
## Notation
Notation for writing HeapLang terms is defined in
[`notation.v`](theories/heap_lang/notation.v). There are two scopes, `%E` for
[`notation.v`](../theories/heap_lang/notation.v). There are two scopes, `%E` for
expressions and `%V` for values. For example, `(a, b)%E` is an expression pair
and `(a, b)%V` a value pair. The `e` of a `WP e {{ Q }}` is implicitly in `%E`
scope.
......
docs/proof_guide.md
+ 40
− 242
View file @ 8cfe4ceb
......@@ -16,241 +16,13 @@ In particular, when importing Iris, Stdpp and Coq stdlib modules, we
recommend importing in the following order:
- Coq
- stdpp
- iris.algebra
- iris.bi
- iris.proofmode
- iris.algebra
- iris.base_logic
- iris.program_logic
- iris.heap_lang
## Combinators for functors
In Iris, the type of propositions [iProp] is described by the solution to the
recursive domain equation:
```
iProp ≅ uPred (F (iProp))
```
Here, `F` is a user-chosen locally contractive bifunctor from COFEs to unital
Cameras (a step-indexed generalization of unital resource algebras). To make it
convenient to construct such functors out of smaller pieces, we provide a number
of abstractions:
- [`cFunctor`](theories/algebra/ofe.v): bifunctors from COFEs to OFEs.
- [`rFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to cameras.
- [`urFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to unital
cameras.
Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and
`urFunctorContractive` which describe the subset of the above functors that
are contractive.
To compose these functors, we provide a number of combinators, e.g.:
- `constCF (A : ofeT) : cFunctor := λ (B,B⁻), A `
- `idCF : cFunctor := λ (B,B⁻), B`
- `prodCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
- `ofe_morCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
- `laterCF (F : cFunctor) : cFunctor := λ (B,B⁻), later (F (B,B⁻))`
- `agreeRF (F : cFunctor) : rFunctor := λ (B,B⁻), agree (F (B,B⁻))`
- `gmapURF K (F : rFunctor) : urFunctor := λ (B,B⁻), gmap K (F (B,B⁻))`
Using these combinators, one can easily construct bigger functors in point-free
style, e.g:
```
F := gmapURF K (agreeRF (prodCF (constCF natC) (laterCF idCF)))
```
which effectively defines `F := λ (B,B⁻), gmap K (agree (nat * later B))`.
Furthermore, for functors written using these combinators like the functor `F`
above, Coq can automatically `urFunctorContractive F`.
To make it a little bit more convenient to write down such functors, we make
the constant functors (`constCF`, `constRF`, and `constURF`) a coercion, and
provide the usual notation for products, etc. So the above functor can be
written as follows (which is similar to the effective definition of `F` above):
```
F := gmapURF K (agreeRF (natC * ▶ ∙))
```
## 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` defining which resource algebras are
available. The `Σ` is the *global* list of resources that the entire proof can
use. We keep the `Σ` universally quantified to enable composition of proofs.
You can think of this as a list of resource algebras, though in reality it is a
list of locally contractive functors from COFEs to Cameras. This list is used
to define the parameter `F` of Iris mentioned in the previous section. The
formal side of this is described in §7.4 of
[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.1.pdf); here we
describe the user-side Coq aspects of this approach.
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
[one-shot 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 type-class 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 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
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. If you are using another module as part of yours, add their
`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.
```
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 module (and all the modules it
uses internally) can trivially be satisfied by picking the right `Σ`.
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 Σ}.
```
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
(see "global ghost state instances" below).
The backtick (`` ` ``) is used to make anonymous assumptions and to automatically
generalize the `Σ`. When adding assumptions with backtick, 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 type-classes 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 type class
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 modules,
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 Σ}.
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: 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
physical heap. The `gname` of that ghost state must be picked once when the
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); 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 Σ} σ :
(|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
```
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`):
```
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
`one_shotG` would lose track of the fact that there exists just one `heapG`
instance that is shared by everyone.
### Advanced topic: Additional module assumptions
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) := {
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 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
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
type class search diverge.
## Canonical structures and type classes
In Iris, we use both canonical structures and type classes, and some careful
......@@ -278,7 +50,7 @@ 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
(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):
```
......@@ -287,6 +59,32 @@ Typeclasses Opaque join_handle.
This makes sure that the proof mode does not "look into" your definition when it
is used by clients.
## Library type class assumptions
When a parameterized library needs to make some type class assumptions about its
parameters, it is convenient to add those to the `libG` class that the library
will likely need anyway (see the [resource algebra docs](resource_algebras.md)
for further details on `libG` classes). For example, the STS library is
parameterized by an STS and assumes that the STS state space is inhabited:
```
Class stsG Σ (sts : stsT) := {
sts_inG :> inG Σ (stsR sts);
sts_inhabited :> Inhabited (sts.state sts);
}.
```
In this case, the `Instance` for this `libG` class has more than just a `subG`
assumption:
```
Instance subG_stsΣ Σ sts :
subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
Proof. solve_inG. Qed.
```
One 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
type class search diverge.
## Notations
Notations starting with `(` or `{` should be left at their default level (`0`),
......@@ -321,13 +119,13 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
* j
* k
* l
* m : iGst = ghost state
* m* = prefix for option
* m : M : cmraT = RA/Camera ("monoid") element
* m* = prefix for option ("maybe")
* n
* o
* p
* q
* r : iRes = resources
* r : iRes = (global) resources inside the Iris model
* s = state (STSs)
* s = stuckness bits
* t
......@@ -343,8 +141,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
* A : Type, cmraT or ofeT
* B : Type, cmraT or ofeT
* C
* D
* E : coPset = Viewshift masks
* D
* E : coPset = mask of fancy update or WP
* F = a functor
* G
* H = hypotheses
......@@ -362,7 +160,7 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
* S : set state = state sets in STSs
* T : set token = token sets in STSs
* U
* V : abstraction of value type in frame shift assertions
* V
* W
* X : sets
* Y : sets
......@@ -370,14 +168,14 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
### small greek letters
* γ : gname
* γ : gname = name of ghost state instance
* σ : state = state of language
* φ : interpretation of STS/Auth
* φ : Prop = pure proposition embedded into uPred or iProp
### capital greek letters
* Φ : general predicate (over uPred, iProp or Prop)
* Ψ : general predicate (over uPred, iProp or Prop)
* Φ : general predicate (in uPred, iProp or Prop)
* Ψ : general predicate (in uPred, iProp or Prop)
## Naming conventions for algebraic classes
......@@ -387,8 +185,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
* R: cameras
* UR: unital cameras or resources algebras
* F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
* G: global camera functor management (typeclass; see [proof\_guide.md](./proof_guide.md))
* G: global camera functor management (typeclass; see the [resource algebra docs](resource_algebras.md))
* I: bunched implication logic (of type `bi`)
* SI: step-indexed bunched implication logic (of type `sbi`)
* T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
* Σ: global camera functor management (`gFunctors`; see [proof\_guide.md](./proof_guide.md))
* Σ: global camera functor management (`gFunctors`; see the [resource algebra docs](resource_algebras.md))
docs/resource_algebras.md 0 → 100644
+ 283
− 0
View file @ 8cfe4ceb
## Global resource algebra management
The type of Iris propositions `iProp Σ` is parameterized by a *global* list `Σ:
gFunctors` of resource algebras that the proof may use. (Actually this list
contains functors instead of resource algebras, but you only need to worry about
that when dealing with higher-order ghost state -- see "Camera functors" below.)
In our proofs, we always keep the `Σ` universally quantified to enable composition of proofs.
Each proof just assumes that some particular resource algebras are contained in that global list.
This is expressed via the `inG Σ R` typeclass, which roughly says that `R ∈ Σ`.
Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
not have to expose to clients what exactly their resource algebras are. For
example, in the [one-shot example](../tests/one_shot.v), we have:
```
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
```
The `:>` means that the projection `one_shot_inG` is automatically registered as
an instance for type-class 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 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 (see "Camera functors" below), but for now
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. If you are using another module as part of yours, add their
`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.
```
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 module (and all the modules it
uses internally) can trivially be satisfied by picking the right `Σ`.
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 Σ}.
```
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
(see "global ghost state instances" below).
The backtick (`` ` ``) is used to make anonymous assumptions and to automatically
generalize the `Σ`. When adding assumptions with backtick, 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 type-classes 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 type class
resolutions.
## Resource algebra combinators
Defining a new resource algebra `one_shotR` for each new proof and verifying all
the algebra laws would be quite cumbersome, so instead Iris provides a rich set
of resource algebra combinators that one can use to build up the desired
resource algebras. For example, `one_shotR` is defined as follows:
```
Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
```
The suffixes `R` and `O` indicate that we are not working on the level of Coq
types here, but on the level of `R`esource algebras and `O`FEs,
respectively. Unfortunately this means we cannot use Coq's usual type notation
(such as `*` for products and `()` for the unit type); we have to spell out the
underlying OFE or resource algebra names instead.
## 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 modules,
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 Σ}.
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: 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
physical heap. The `gname` of that ghost state must be picked once when the
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); 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 Σ} σ :
(|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
```
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`):
```
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
`one_shotG` would lose track of the fact that there exists just one `heapG`
instance that is shared by everyone.
## Advanced topic: Camera functors and higher-order ghost state
As we already alluded to, `Σ` actually consists of functors, not resource
algebras. This enables you to use *higher-order ghost state*: ghost state that
recursively refers to `iProp`.
**Background: Iris Model.** To understand how this works, we have to dig a bit
into the model of Iris. In Iris, the type of propositions `iProp` is described
by the solution to the recursive domain equation:
```
iProp ≅ uPred (F (iProp))
```
Here, `uPred M` describes "propositions with resources of type `M`". The
peculiar aspect of this definition is that the notion of resources can itself
refer to the set propositions that we are just defining; that dependency is
expressed by `F`. `F` is a user-chosen locally contractive bifunctor from COFEs
to unital Cameras (a step-indexed generalization of unital resource
algebras). Having just a single fixed `F` would however be rather inconvenient,
so instead we have a list `Σ`, and then we define the global functor `F_global`
roughly as follows:
```
F_global X := Π_{F ∈ Σ} gmap nat (F X)
```
In other words, each functor in `Σ` is applied to the recursive argument `X`,
wrapped in a finite partial function, and then we take a big product of all of
that. The product ensures that all `F ∈ Σ` are available, and the `gmap` is
needed to provide the proof rule `own_alloc`, which lets you create new
instances of the given type of resource any time.
However, this on its own would be too restrictive, as it requires all
occurrences of `X` to be in positive positions (otherwise the functor laws
would not hold for `F`). To mitigate this, we instead work with "bifunctors":
functors that take two arguments, `X` and `X⁻`, where `X⁻` is used for
negative positions. This leads us to the following domain equation:
```
iProp ≅ uPred (F_global (iProp,iProp))
F_global (X,X⁻) := Π_{F ∈ Σ} gmap nat (F (X,X⁻))
```
To make this equation well-defined, the bifunctors `F ∈ Σ` need to be "contractive".
For further details, see §7.4 of
[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.3.pdf); here we
describe the user-side Coq aspects of this approach.
Below, when we say "functor", we implicitly mean "bifunctor".
**Higher-order ghost state.** To use higher-order ghost state, you need to give
a functor whose "hole" will later be filled with `iProp` itself. For example,
let us say you would like to have ghost state of type `gmap K (agree (nat *
later iProp))`, using the "type-level" `later` operator which ensures
contractivity. Then you will have to define a functor such as:
```
F (X,X⁻) := gmap K (agree (nat * ▶ X))
```
To make it convenient to construct such functors and prove their contractivity,
we provide a number of abstractions:
- [`cFunctor`](theories/algebra/ofe.v): functors from COFEs to OFEs.
- [`rFunctor`](theories/algebra/cmra.v): functors from COFEs to cameras.
- [`urFunctor`](theories/algebra/cmra.v): functors from COFEs to unital
cameras.
Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and
`urFunctorContractive` which describe the subset of the above functors that are
contractive.
To compose these functors, we provide a number of combinators, e.g.:
- `constOF (A : ofeT) : cFunctor := λ (B,B⁻), A `
- `idOF : cFunctor := λ (B,B⁻), B`
- `prodOF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
- `ofe_morOF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
- `laterOF (F : cFunctor) : cFunctor := λ (B,B⁻), later (F (B,B⁻))`
- `agreeRF (F : cFunctor) : rFunctor := λ (B,B⁻), agree (F (B,B⁻))`
- `gmapURF K (F : rFunctor) : urFunctor := λ (B,B⁻), gmap K (F (B,B⁻))`
Note in particular how the functor for the function space, `ofe_morOF`, swaps
`B` and `B⁻` for the functor `F1` describing the domain. This reflects the fact
that that functor is used in a negative position.
Using these combinators, one can easily construct bigger functors in point-free
style and automatically infer their contractivity, e.g:
```
F := gmaURF K (agreeRF (prodOF (constOF natO) (laterOF idOF)))
```
which effectively defines the desired example functor
`F := λ (B,B⁻), gmap K (agree (nat * later B))`.
To make it a little bit more convenient to write down such functors, we make
the constant functors (`constOF`, `constRF`, and `constURF`) a coercion, and
provide the usual notation for products, etc. So the above functor can be
written as follows:
```
F := gmapRF K (agreeRF (natO * ▶ ∙))
```
Basically, the functor can be written "as if" you were writing a resource
algebra, except that there need to be extra "F" suffixes to indicate that we are
working with functors, and the desired recursive `iProp` is replaced by the
"hole" `∙`.
Putting it all together, the `libG` typeclass and `libΣ` list of functors for
your example would look as follows:
```
Class libG Σ := { lib_inG :> inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
Proof. solve_inG. Qed.
```
It is instructive to remove the `▶` and see what happens: the `libG` class still
works just fine, but `libΣ` complains that the functor is not contractive. This
demonstrates the importance of always defining a `libΣ` alongside the `libG` and
proving their relation.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment