From algebra Require Export upred. From program_logic Require Export resources. From algebra Require Import cofe_solver. (* 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. *) (* TODO RJ: Can we make use of resF, the resource functor? *) Module iProp. Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT := uPredC (resR Λ Σ (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 := uPredC_map (resC_map (laterC_map (f.1))). Definition result Λ Σ : solution (F Λ Σ). Proof. 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. - 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' Hf P; split=> n' -[???]. apply upredC_map_ne, resC_map_ne, laterC_map_contractive. by intros i ?; apply Hf. Qed. End iProp. (* Solution *) Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp.result Λ Σ. Definition iRes Λ Σ := res Λ Σ (laterC (iPreProp Λ Σ)). Definition iResR Λ Σ := resR Λ Σ (laterC (iPreProp Λ Σ)). Definition iWld Λ Σ := mapR positive (agreeR (laterC (iPreProp Λ Σ))). Definition iPst Λ := exclR (istateC Λ). Definition iGst Λ Σ := ifunctor_car Σ (laterC (iPreProp Λ Σ)). Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResR Λ Σ). 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. Proof. apply solution_unfold_fold. Qed. Lemma iProp_unfold_fold {Λ Σ} (P : iPreProp Λ Σ) : iProp_unfold (iProp_fold P) ≡ P. Proof. apply solution_fold_unfold. Qed. Bind Scope uPred_scope with iProp. Instance iProp_fold_inj n Λ Σ : Inj (dist n) (dist n) (@iProp_fold Λ Σ). Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed. Instance iProp_unfold_inj n Λ Σ : Inj (dist n) (dist n) (@iProp_unfold Λ Σ). Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.