model.v 3.04 KB
 Robbert Krebbers committed Feb 13, 2016 1 2 3 ``````From algebra Require Export upred. From program_logic Require Export resources. From algebra Require Import cofe_solver. `````` Robbert Krebbers committed Jan 16, 2016 4 `````` `````` Ralf Jung committed Mar 07, 2016 5 6 7 8 9 10 11 12 13 14 15 16 ``````(* 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); iFunctor_identity (A : cofeT) : CMRAIdentity (iFunctor_F A); }. Arguments IFunctor _ {_ _ _}. Existing Instances iFunctor_contractive iFunctor_empty iFunctor_identity. `````` Robbert Krebbers committed Mar 03, 2016 17 18 `````` Module Type iProp_solution_sig. `````` Ralf Jung committed Mar 07, 2016 19 20 ``````Parameter iPreProp : language → iFunctor → cofeT. Definition iGst (Λ : language) (Σ : iFunctor) : cmraT := Σ (iPreProp Λ Σ). `````` Robbert Krebbers committed Mar 03, 2016 21 22 23 24 ``````Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ). Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ). Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))). Definition iPst Λ := excl (state Λ). `````` Ralf Jung committed Mar 07, 2016 25 ``````Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResR Λ Σ). `````` Robbert Krebbers committed Mar 03, 2016 26 27 28 29 30 31 32 33 34 35 `````` 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. `````` Ralf Jung committed Mar 07, 2016 36 ``````Definition iProp_result (Λ : language) (Σ : iFunctor) : `````` Ralf Jung committed Mar 07, 2016 37 `````` solution (uPredCF (resRF Λ (▶ ∙) Σ)) := solver.result _. `````` Robbert Krebbers committed Jan 16, 2016 38 `````` `````` Ralf Jung committed Mar 07, 2016 39 40 ``````Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp_result Λ Σ. Definition iGst (Λ : language) (Σ : iFunctor) : cmraT := Σ (iPreProp Λ Σ). `````` Robbert Krebbers committed Mar 02, 2016 41 42 43 44 45 ``````Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ). Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ). Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))). Definition iPst Λ := excl (state Λ). `````` Ralf Jung committed Mar 07, 2016 46 ``````Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResR Λ Σ). `````` Robbert Krebbers committed Mar 02, 2016 47 48 ``````Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ := solution_fold (iProp_result Λ Σ). `````` Robbert Krebbers committed Feb 01, 2016 49 50 ``````Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _. Lemma iProp_fold_unfold {Λ Σ} (P : iProp Λ Σ) : iProp_fold (iProp_unfold P) ≡ P. `````` Robbert Krebbers committed Jan 16, 2016 51 ``````Proof. apply solution_unfold_fold. Qed. `````` Robbert Krebbers committed Feb 01, 2016 52 53 ``````Lemma iProp_unfold_fold {Λ Σ} (P : iPreProp Λ Σ) : iProp_unfold (iProp_fold P) ≡ P. `````` Robbert Krebbers committed Jan 16, 2016 54 ``````Proof. apply solution_fold_unfold. Qed. `````` Robbert Krebbers committed Mar 03, 2016 55 56 ``````End iProp_solution. `````` Robbert Krebbers committed Jan 16, 2016 57 ``````Bind Scope uPred_scope with iProp. `````` Robbert Krebbers committed Jan 16, 2016 58 `````` `````` Robbert Krebbers committed Feb 11, 2016 59 ``````Instance iProp_fold_inj n Λ Σ : Inj (dist n) (dist n) (@iProp_fold Λ Σ). `````` Robbert Krebbers committed Jan 16, 2016 60 ``````Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed. `````` Robbert Krebbers committed Feb 01, 2016 61 ``````Instance iProp_unfold_inj n Λ Σ : `````` Robbert Krebbers committed Feb 11, 2016 62 `````` Inj (dist n) (dist n) (@iProp_unfold Λ Σ). `````` Robbert Krebbers committed Jan 16, 2016 63 ``Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.``