From 7c762be1d2769fe486b34197ad38a3611194ea3d Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 27 Sep 2016 10:00:47 +0200 Subject: [PATCH] CMRA structure on uPred. --- algebra/upred.v | 63 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/algebra/upred.v b/algebra/upred.v index 261c727d..38dd2217 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -1486,3 +1486,66 @@ Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I. Hint Immediate True_intro False_elim : I. Hint Immediate iff_refl eq_refl' : I. End uPred. + +(* CMRA structure on uPred *) +Section cmra. + Context {M : ucmraT}. + + Instance uPred_valid' : Valid (uPred M) := λ P, ∀ n x, ✓{n} x → P n x. + Instance uPred_validN' : ValidN (uPred M) := λ n P, + ∀ n' x, n' ≤ n → ✓{n'} x → P n' x. + Instance uPred_op : Op (uPred M) := uPred_sep. + Instance uPred_pcore : PCore (uPred M) := λ _, Some True%I. + + Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN' n). + Proof. intros P Q HPQ; split=> H n' x ??; by apply HPQ, H. Qed. + + Lemma uPred_validN_alt n (P : uPred M) : ✓{n} P → P ≡{n}≡ True%I. + Proof. + uPred.unseal=> HP; split=> n' x ??; split; [done|]. + intros _. by apply HP. + Qed. + + Lemma uPred_cmra_validN_op_l n P Q : ✓{n} (P ★ Q)%I → ✓{n} P. + Proof. + uPred.unseal. intros HPQ n' x ??. + destruct (HPQ n' x) as (x1&x2&->&?&?); auto. + eapply uPred_mono with x1; eauto using cmra_includedN_l. + Qed. + + Definition uPred_cmra_mixin : CMRAMixin (uPred M). + Proof. + apply cmra_total_mixin; try apply _ || by eauto. + - intros n P Q ??. by cofe_subst. + - intros P; split. + + intros HP n n' x ?. apply HP. + + intros HP n x. by apply (HP n). + - intros n P HP n' x ?. apply HP; auto. + - intros P. by rewrite left_id. + - intros P Q _. exists True%I. by rewrite left_id. + - intros n P Q. apply uPred_cmra_validN_op_l. + - intros n P Q1 Q2 HP HPQ. exists True%I, P; split_and!. + + by rewrite left_id. + + move: HP; by rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt. + + move: HP; rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt=> ->. + by rewrite left_id. + Qed. + + Canonical Structure uPredR := + CMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin. + + Instance uPred_empty : Empty (uPred M) := True%I. + + Definition uPred_ucmra_mixin : UCMRAMixin (uPred M). + Proof. + split; last done. + - by rewrite /empty /uPred_empty uPred_pure_eq. + - intros P. by rewrite left_id. + Qed. + + Canonical Structure uPredUR := + UCMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin uPred_ucmra_mixin. +End cmra. + +Arguments uPredR : clear implicits. +Arguments uPredUR : clear implicits. -- GitLab