model.v 2.82 KB
Newer Older
1
From iris.algebra Require Export upred.
2
From iris.algebra Require Import iprod gmap.
3
From iris.algebra Require cofe_solver.
4

5
6
7
8
9
10
11
12
(* The Iris program logic is parametrized by a dependent product of a bunch of
[gFunctor]s, which are locally contractive functor 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. *)
Structure gFunctor := GFunctor {
  gFunctor_F :> rFunctor;
  gFunctor_contractive : rFunctorContractive gFunctor_F;
13
}.
14
15
Arguments GFunctor _ {_}.
Existing Instance gFunctor_contractive.
16

17
18
19
20
21
22
23
24
(** The global CMRA: Indexed product over a gid i to (gname --fin--> Σ i) *)
Definition gFunctors := { n : nat & fin n  gFunctor }.
Definition gid (Σ : gFunctors) := fin (projT1 Σ).

(** Name of one instance of a particular CMRA in the ghost state. *)
Definition gname := positive.

(** Solution of the recursive domain equation *)
25
Module Type iProp_solution_sig.
26
27
28
29
30
31
32
33
Parameter iPreProp : gFunctors  cofeT.
Definition iResUR (Σ : gFunctors) : ucmraT :=
  iprodUR (λ i, gmapUR gname (projT2 Σ i (iPreProp Σ))).
Definition iProp (Σ : gFunctors) : cofeT := uPredC (iResUR Σ).

Parameter iProp_unfold:  {Σ}, iProp Σ -n> iPreProp Σ.
Parameter iProp_fold:  {Σ}, iPreProp Σ -n> iProp Σ.
Parameter iProp_fold_unfold:  {Σ} (P : iProp Σ),
34
  iProp_fold (iProp_unfold P)  P.
35
Parameter iProp_unfold_fold:  {Σ} (P : iPreProp Σ),
36
37
38
39
  iProp_unfold (iProp_fold P)  P.
End iProp_solution_sig.

Module Export iProp_solution : iProp_solution_sig.
40
Import cofe_solver.
41
42
43
44
45
46
47
48
49
50
51
52
53
54
Definition iResF (Σ : gFunctors) : urFunctor :=
  iprodURF (λ i, gmapURF gname (projT2 Σ i)).
Definition iProp_result (Σ : gFunctors) :
  solution (uPredCF (iResF Σ)) := solver.result _.

Definition iPreProp (Σ : gFunctors) : cofeT := iProp_result Σ.
Definition iResUR (Σ : gFunctors) : ucmraT :=
  iprodUR (λ i, gmapUR gname (projT2 Σ i (iPreProp Σ))).
Definition iProp (Σ : gFunctors) : cofeT := uPredC (iResUR Σ).

Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
  solution_fold (iProp_result Σ).
Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P)  P.
55
Proof. apply solution_unfold_fold. Qed.
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
63
64
65
66
67
68
Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
  iProp_unfold P  iProp_unfold Q  (P  Q : iProp Σ).
Proof.
  rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
  eapply (uPred.eq_rewrite _ _ (λ z,
    iProp_fold (iProp_unfold P)  iProp_fold z))%I; auto with I; solve_proper.
Qed.