functor.v 1.94 KB
Newer Older
1
From algebra Require Export cmra.
2

Robbert Krebbers's avatar
Robbert Krebbers committed
3
(** * Functors from COFE to CMRA *)
Ralf Jung's avatar
Ralf Jung committed
4
(* TODO RJ: Maybe find a better name for this? It is not PL-specific any more. *)
5
6
7
8
9
10
11
12
13
14
15
16
17
Structure iFunctor := IFunctor {
  ifunctor_car :> cofeT  cmraT;
  ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
  ifunctor_map_ne {A B} n : Proper (dist n ==> dist n) (@ifunctor_map A B);
  ifunctor_map_id {A : cofeT} (x : ifunctor_car A) : ifunctor_map cid x  x;
  ifunctor_map_compose {A B C} (f : A -n> B) (g : B -n> C) x :
    ifunctor_map (g  f) x  ifunctor_map g (ifunctor_map f x);
  ifunctor_map_mono {A B} (f : A -n> B) : CMRAMonotone (ifunctor_map f)
}.
Existing Instances ifunctor_map_ne ifunctor_map_mono.

Lemma ifunctor_map_ext (Σ : iFunctor) {A B} (f g : A -n> B) m :
  ( x, f x  g x)  ifunctor_map Σ f m  ifunctor_map Σ g m.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
Proof. by intros; apply (ne_proper (@ifunctor_map Σ A B)). Qed.

(** * Functor combinators *)
(** We create a functor combinators for all CMRAs in the algebra directory.
These combinators can be used to conveniently construct the global CMRA of
the Iris program logic. Note that we have explicitly built in functor
composition into these combinators, instead of having a notion of a functor
from the category of CMRAs to the category of CMRAs which we can compose. This
way we can convenient deal with (indexed) products in a uniform way. *)
Program Definition constF (B : cmraT) : iFunctor :=
  {| ifunctor_car A := B; ifunctor_map A1 A2 f := cid |}.
Solve Obligations with done.

Program Definition prodF (Σ1 Σ2 : iFunctor) : iFunctor := {|
  ifunctor_car A := prodRA (Σ1 A) (Σ2 A);
  ifunctor_map A B f := prodC_map (ifunctor_map Σ1 f) (ifunctor_map Σ2 f)
|}.
Next Obligation.
  by intros Σ1 Σ2 A B n f g Hfg; apply prodC_map_ne; apply ifunctor_map_ne.
Qed.
Next Obligation. by intros Σ1 Σ2 A [??]; rewrite /= !ifunctor_map_id. Qed.
Next Obligation.
  by intros Σ1 Σ2 A B C f g [??]; rewrite /= !ifunctor_map_compose.
Qed.