model.v 2.95 KB
Newer Older
1 2
From iris.algebra Require Export upred.
From iris.program_logic Require Export resources.
3
From iris.algebra Require cofe_solver.
4

5 6 7 8 9
(* The Iris program logic is parametrized by a locally contractive functor
from the category of COFEs to the category of CMRAs, which is instantiated
with [iProp]. The [iProp] can be used to construct impredicate CMRAs, such as
the stored propositions using the agreement CMRA. *)
Structure iFunctor := IFunctor {
10 11
  iFunctor_F :> urFunctor;
  iFunctor_contractive : urFunctorContractive iFunctor_F
12
}.
13 14
Arguments IFunctor _ {_}.
Existing Instances iFunctor_contractive.
15 16

Module Type iProp_solution_sig.
17
Parameter iPreProp : language  iFunctor  cofeT.
18
Definition iGst (Λ : language) (Σ : iFunctor) : ucmraT := Σ (iPreProp Λ Σ).
19
Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
20
Definition iResUR Λ Σ := resUR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
21
Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
Robbert Krebbers's avatar
Robbert Krebbers committed
22
Definition iPst Λ := option (excl (state Λ)).
23
Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResUR Λ Σ).
24 25 26 27 28 29 30 31 32 33

Parameter iProp_unfold:  {Λ Σ}, iProp Λ Σ -n> iPreProp Λ Σ.
Parameter iProp_fold:  {Λ Σ}, iPreProp Λ Σ -n> iProp Λ Σ.
Parameter iProp_fold_unfold:  {Λ Σ} (P : iProp Λ Σ),
  iProp_fold (iProp_unfold P)  P.
Parameter iProp_unfold_fold:  {Λ Σ} (P : iPreProp Λ Σ),
  iProp_unfold (iProp_fold P)  P.
End iProp_solution_sig.

Module Export iProp_solution : iProp_solution_sig.
34
Import cofe_solver.
35
Definition iProp_result (Λ : language) (Σ : iFunctor) :
36
  solution (uPredCF (resURF Λ ( ) Σ)) := solver.result _.
37

38
Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp_result Λ Σ.
39
Definition iGst (Λ : language) (Σ : iFunctor) : ucmraT := Σ (iPreProp Λ Σ).
40
Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
41
Definition iResUR Λ Σ := resUR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
42
Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
Robbert Krebbers's avatar
Robbert Krebbers committed
43
Definition iPst Λ := option (excl (state Λ)).
44

45
Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResUR Λ Σ).
46 47
Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ :=
  solution_fold (iProp_result Λ Σ).
48 49
Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.
Lemma iProp_fold_unfold {Λ Σ} (P : iProp Λ Σ) : iProp_fold (iProp_unfold P)  P.
50
Proof. apply solution_unfold_fold. Qed.
51 52
Lemma iProp_unfold_fold {Λ Σ} (P : iPreProp Λ Σ) :
  iProp_unfold (iProp_fold P)  P.
53
Proof. apply solution_fold_unfold. Qed.
54 55
End iProp_solution.

56
Bind Scope uPred_scope with iProp.
57

58
Instance iProp_fold_inj n Λ Σ : Inj (dist n) (dist n) (@iProp_fold Λ Σ).
59
Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
60
Instance iProp_unfold_inj n Λ Σ : Inj (dist n) (dist n) (@iProp_unfold Λ Σ).
61
Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.