model.v 2.57 KB
Newer Older
1
Require Export algebra.upred program_logic.resources.
2
Require Import algebra.cofe_solver.
3

Ralf Jung's avatar
Ralf Jung committed
4
5
6
7
8
(* The Iris program logic is parametrized by a functor from the category of
COFEs to the category of CMRAs, which is instantiated with [laterC iProp]. The
[laterC iProp] can be used to construct impredicate CMRAs, such as the stored
propositions using the agreement CMRA. *)

Ralf Jung's avatar
Ralf Jung committed
9
(* TODO RJ: Can we make use of resF, the resource functor? *)
10
Module iProp.
11
12
13
14
Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
  uPredC (resRA Λ Σ (laterC A)).
Definition map {Λ : language} {Σ : iFunctor} {A1 A2 B1 B2 : cofeT}
    (f : (A2 -n> A1) * (B1 -n> B2)) : F Λ Σ A1 B1 -n> F Λ Σ A2 B2 :=
15
  uPredC_map (resC_map (laterC_map (f.1))).
16
Definition result Λ Σ : solution (F Λ Σ).
17
Proof.
18
19
20
21
  apply (solver.result _ (@map Λ Σ)).
  * intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=> r.
    rewrite /= -{2}(res_map_id r); apply res_map_ext=>{r} r /=.
    by rewrite later_map_id.
22
23
24
25
26
  * intros A1 A2 A3 B1 B2 B3 f g f' g' P. rewrite /map /=.
    rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
    rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
    by rewrite -later_map_compose.
  * intros A1 A2 B1 B2 n f f' [??] P.
27
    by apply upredC_map_ne, resC_map_ne, laterC_map_contractive.
28
29
30
31
Qed.
End iProp.

(* Solution *)
32
33
34
35
36
37
38
39
40
41
Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp.result Λ Σ.
Notation iRes Λ Σ := (res Λ Σ (laterC (iPreProp Λ Σ))).
Notation iResRA Λ Σ := (resRA Λ Σ (laterC (iPreProp Λ Σ))).
Notation iWld Λ Σ := (mapRA positive (agreeRA (laterC (iPreProp Λ Σ)))).
Notation iPst Λ := (exclRA (istateC Λ)).
Notation iGst Λ Σ := (ifunctor_car Σ (laterC (iPreProp Λ Σ))).
Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResRA Λ Σ).
Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ := solution_fold _.
Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.
Lemma iProp_fold_unfold {Λ Σ} (P : iProp Λ Σ) : iProp_fold (iProp_unfold P)  P.
42
Proof. apply solution_unfold_fold. Qed.
43
44
Lemma iProp_unfold_fold {Λ Σ} (P : iPreProp Λ Σ) :
  iProp_unfold (iProp_fold P)  P.
45
46
Proof. apply solution_fold_unfold. Qed.
Bind Scope uPred_scope with iProp.
47

48
Instance iProp_fold_inj n Λ Σ : Injective (dist n) (dist n) (@iProp_fold Λ Σ).
49
Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
50
51
Instance iProp_unfold_inj n Λ Σ :
  Injective (dist n) (dist n) (@iProp_unfold Λ Σ).
52
Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.