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

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

(* Solution *)
34
Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp.result Λ Σ.
35
Definition iRes Λ Σ := res Λ Σ (laterC (iPreProp Λ Σ)).
36 37 38
Definition iResR Λ Σ := resR Λ Σ (laterC (iPreProp Λ Σ)).
Definition iWld Λ Σ := mapR positive (agreeR (laterC (iPreProp Λ Σ))).
Definition iPst Λ := exclR (istateC Λ).
39
Definition iGst Λ Σ := ifunctor_car Σ (laterC (iPreProp Λ Σ)).
40
Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResR Λ Σ).
41 42 43
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.
44
Proof. apply solution_unfold_fold. Qed.
45 46
Lemma iProp_unfold_fold {Λ Σ} (P : iPreProp Λ Σ) :
  iProp_unfold (iProp_fold P)  P.
47 48
Proof. apply solution_fold_unfold. Qed.
Bind Scope uPred_scope with iProp.
49

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