model.v 3.22 KB
Newer Older
1
2
From iris.algebra Require Export upred.
From iris.program_logic Require Export resources.
3
4
5
(* We'd prefer to only import this in the sealed module, to make sure it does
   not "escape". However, for some reason, that breaks importing model.v
   elsewhere. *)
6
From iris.algebra Require Import cofe_solver.
7

8
9
10
11
12
13
14
15
(* 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 {
  iFunctor_F :> rFunctor;
  iFunctor_contractive : rFunctorContractive iFunctor_F;
  iFunctor_empty (A : cofeT) : Empty (iFunctor_F A);
Ralf Jung's avatar
Ralf Jung committed
16
  iFunctor_identity (A : cofeT) : CMRAUnit (iFunctor_F A);
17
18
19
}.
Arguments IFunctor _ {_ _ _}.
Existing Instances iFunctor_contractive iFunctor_empty iFunctor_identity.
20
21

Module Type iProp_solution_sig.
22
23
Parameter iPreProp : language  iFunctor  cofeT.
Definition iGst (Λ : language) (Σ : iFunctor) : cmraT := Σ (iPreProp Λ Σ).
24
25
26
27
Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
Definition iPst Λ := excl (state Λ).
28
Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResR Λ Σ).
29
30
31
32
33
34
35
36
37
38

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.
39
Definition iProp_result (Λ : language) (Σ : iFunctor) :
40
  solution (uPredCF (resRF Λ ( ) Σ)) := solver.result _.
41

42
43
Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp_result Λ Σ.
Definition iGst (Λ : language) (Σ : iFunctor) : cmraT := Σ (iPreProp Λ Σ).
44
45
46
47
48
Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
Definition iPst Λ := excl (state Λ).

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

60
Bind Scope uPred_scope with iProp.
61

62
Instance iProp_fold_inj n Λ Σ : Inj (dist n) (dist n) (@iProp_fold Λ Σ).
63
Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
64
Instance iProp_unfold_inj n Λ Σ :
65
  Inj (dist n) (dist n) (@iProp_unfold Λ Σ).
66
Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.