iprop.v 6.82 KB
Newer Older
1
From iris.algebra Require Import gmap.
2
From iris.algebra Require cofe_solver.
3
From iris.base_logic Require Export base_logic.
4
Set Default Proof Using "Type".
5

6 7 8
(** In this file we construct the type [iProp] of propositions of the Iris
logic. This is done by solving the following recursive domain equation:

9
  iProp ≈ uPred (∀ i : gid, gname -fin-> (Σ i) iProp)
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26

where:

  Σ : gFunctors  := lists of locally constractive functors
  i : gid        := indexes addressing individual functors in [Σ]
  γ : gname      := ghost variable names

The Iris logic is parametrized by a list of locally contractive functors [Σ]
from the category of COFEs to the category of CMRAs. These functors are
instantiated with [iProp], the type of Iris propositions, which allows one to
construct impredicate CMRAs, such as invariants and stored propositions using
the agreement CMRA. *)


(** * Locally contractive functors *)
(** The type [gFunctor] bundles a functor from the category of COFEs to the
category of CMRAs with a proof that it is locally contractive. *)
27 28
Structure gFunctor := GFunctor {
  gFunctor_F :> rFunctor;
29
  gFunctor_map_contractive : rFunctorContractive gFunctor_F;
30
}.
31
Arguments GFunctor _ {_}.
32
Existing Instance gFunctor_map_contractive.
Ralf Jung's avatar
Ralf Jung committed
33
Add Printing Constructor gFunctor.
34

35 36 37 38 39 40
(** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
of [gFunctor]s.

Note that [gFunctors] is isomorphic to [list gFunctor], but defined in an
alternative way to avoid universe inconsistencies with respect to the universe
monomorphic [list] type. *)
41
Definition gFunctors := { n : nat & fin n  gFunctor }.
42

43
Definition gid (Σ : gFunctors) := fin (projT1 Σ).
44
Definition gFunctors_lookup (Σ : gFunctors) : gid Σ  gFunctor := projT2 Σ.
45 46

Definition gname := positive.
47
Canonical Structure gnameO := leibnizO gname.
48

49
(** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
50
Definition iResF (Σ : gFunctors) : urFunctor :=
51
  discrete_funURF (λ i, gmapURF gname (gFunctors_lookup Σ i)).
52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75


(** We define functions for the empty list of functors, the singleton list of
functors, and the append operator on lists of functors. These are used to
compose [gFunctors] out of smaller pieces. *)
Module gFunctors.
  Definition nil : gFunctors := existT 0 (fin_0_inv _).

  Definition singleton (F : gFunctor) : gFunctors :=
    existT 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)).

  Definition app (Σ1 Σ2 : gFunctors) : gFunctors :=
    existT (projT1 Σ1 + projT1 Σ2) (fin_plus_inv _ (projT2 Σ1) (projT2 Σ2)).
End gFunctors.

Coercion gFunctors.singleton : gFunctor >-> gFunctors.
Notation "#[ ]" := gFunctors.nil (format "#[ ]").
Notation "#[ Σ1 ; .. ; Σn ]" :=
  (gFunctors.app Σ1 .. (gFunctors.app Σn gFunctors.nil) ..).


(** * Subfunctors *)
(** In order to make proofs in the Iris logic modular, they are not done with
respect to some concrete list of functors [Σ], but are instead parametrized by
Zhen Zhang's avatar
Zhen Zhang committed
76 77 78
an arbitrary list of functors [Σ] that contains at least certain functors. For
example, the lock library is parameterized by a functor [Σ] that should have
the functors corresponding to the heap and the exclusive monoid to manage to
79 80 81 82
lock invariant.

The contraints to can be expressed using the type class [subG Σ1 Σ2], which
expresses that the functors [Σ1] are contained in [Σ2]. *)
83 84
Class subG (Σ1 Σ2 : gFunctors) := in_subG i :
  { j | gFunctors_lookup Σ1 i = gFunctors_lookup Σ2 j }.
85 86 87

(** Avoid trigger happy type class search: this line ensures that type class
search is only triggered if the arguments of [subG] do not contain evars. Since
88
instance search for [subG] is restrained, instances should persistently have [subG] as
89 90
their first parameter to avoid loops. For example, the instances [subG_authΣ]
and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
Ralf Jung's avatar
Ralf Jung committed
91
Hint Mode subG ! + : typeclass_instances.
92 93 94 95 96 97 98 99 100 101 102 103 104 105 106

Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ  subG Σ1 Σ * subG Σ2 Σ.
Proof.
  move=> H; split.
  - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_plus_inv_L; eauto.
  - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_plus_inv_R; eauto.
Qed.

Instance subG_refl Σ : subG Σ Σ.
Proof. move=> i; by exists i. Qed.
Instance subG_app_l Σ Σ1 Σ2 : subG Σ Σ1  subG Σ (gFunctors.app Σ1 Σ2).
Proof.
  move=> H i; move: H=> /(_ i) [j ?].
  exists (Fin.L _ j). by rewrite /= fin_plus_inv_L.
Qed.
107
Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2  subG Σ (gFunctors.app Σ1 Σ2).
108 109 110 111 112 113 114
Proof.
  move=> H i; move: H=> /(_ i) [j ?].
  exists (Fin.R _ j). by rewrite /= fin_plus_inv_R.
Qed.


(** * Solution of the recursive domain equation *)
Zhen Zhang's avatar
Zhen Zhang committed
115
(** We first declare a module type and then an instance of it so as to seal all of
116 117
the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *)
118
Module Type iProp_solution_sig.
119 120
  Parameter iPrePropO : gFunctors  ofeT.
  Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).
121

122
  Definition iResUR (Σ : gFunctors) : ucmraT :=
123
    discrete_funUR (λ i,
124
      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
125 126
  Notation iProp Σ := (uPred (iResUR Σ)).
  Notation iPropO Σ := (uPredO (iResUR Σ)).
Ralf Jung's avatar
Ralf Jung committed
127 128
  Notation iPropI Σ := (uPredI (iResUR Σ)).
  Notation iPropSI Σ := (uPredSI (iResUR Σ)).
129

130 131
  Parameter iProp_unfold:  {Σ}, iPropO Σ -n> iPrePropO Σ.
  Parameter iProp_fold:  {Σ}, iPrePropO Σ -n> iPropO Σ.
132 133
  Parameter iProp_fold_unfold:  {Σ} (P : iProp Σ),
    iProp_fold (iProp_unfold P)  P.
134
  Parameter iProp_unfold_fold:  {Σ} (P : iPrePropO Σ),
135
    iProp_unfold (iProp_fold P)  P.
136 137 138
End iProp_solution_sig.

Module Export iProp_solution : iProp_solution_sig.
139 140
  Import cofe_solver.
  Definition iProp_result (Σ : gFunctors) :
141
    solution (uPredOF (iResF Σ)) := solver.result _.
142 143
  Definition iPrePropO (Σ : gFunctors) : ofeT := iProp_result Σ.
  Global Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.
144

145
  Definition iResUR (Σ : gFunctors) : ucmraT :=
146
    discrete_funUR (λ i,
147
      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
148 149
  Notation iProp Σ := (uPred (iResUR Σ)).
  Notation iPropO Σ := (uPredO (iResUR Σ)).
150

151
  Definition iProp_unfold {Σ} : iPropO Σ -n> iPrePropO Σ :=
152 153 154
    ofe_iso_1 (iProp_result Σ).
  Definition iProp_fold {Σ} : iPrePropO Σ -n> iPropO Σ :=
    ofe_iso_2 (iProp_result Σ).
155
  Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P)  P.
156
  Proof. apply ofe_iso_21. Qed.
157
  Lemma iProp_unfold_fold {Σ} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P)  P.
158
  Proof. apply ofe_iso_12. Qed.
159 160
End iProp_solution.

161 162

(** * Properties of the solution to the recursive domain equation *)
163
Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
Ralf Jung's avatar
Ralf Jung committed
164
  iProp_unfold P  iProp_unfold Q @{iPropI Σ} P  Q.
165
Proof.
166
  rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: bi.f_equiv.
167
Qed.