From 7f61fa72df5a9a490dadb0842136e84c625b22a6 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 29 Sep 2020 18:29:25 +0200 Subject: [PATCH] Add inclusion lemmas for view & auth. --- theories/algebra/view.v | 38 ++++++++++++++++++++++++++++++++++---- 1 file changed, 34 insertions(+), 4 deletions(-) diff --git a/theories/algebra/view.v b/theories/algebra/view.v index b7475392b..c0a93d35f 100644 --- a/theories/algebra/view.v +++ b/theories/algebra/view.v @@ -119,14 +119,14 @@ Section cmra. Implicit Types b : B. Implicit Types x y : view rel. - Global Instance view_frag_ne: NonExpansive (@view_frag A B rel). - Proof. done. Qed. - Global Instance view_frag_proper : Proper ((≡) ==> (≡)) (@view_frag A B rel). - Proof. done. Qed. Global Instance view_auth_ne q : NonExpansive (@view_auth A B rel q). Proof. solve_proper. Qed. Global Instance view_auth_proper q : Proper ((≡) ==> (≡)) (@view_auth A B rel q). Proof. solve_proper. Qed. + Global Instance view_frag_ne: NonExpansive (@view_frag A B rel). + Proof. done. Qed. + Global Instance view_frag_proper : Proper ((≡) ==> (≡)) (@view_frag A B rel). + Proof. done. Qed. Instance view_valid : Valid (view rel) := λ x, match view_auth_proj x with @@ -305,6 +305,36 @@ Section cmra. (â—¯V [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, â—¯V (g x). Proof. apply (big_opMS_commute _). Qed. + (** Inclusion *) + Lemma view_auth_includedN n p1 p2 a1 a2 b : + â—V{p1} a1 ≼{n} â—V{p2} a2 â‹… â—¯V b → (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2. + Proof. + intros [[[[qf agf]|] bf] + [[?%(discrete_iff _ _) ?]%(inj Some) _]]; simplify_eq/=. + - split; [apply Qp_le_plus_l|]. apply to_agree_includedN. by exists agf. + - split; [done|]. by apply (inj to_agree). + Qed. + Lemma view_auth_included p1 p2 a1 a2 b : + â—V{p1} a1 ≼ â—V{p2} a2 â‹… â—¯V b → (p1 ≤ p2)%Qc ∧ a1 ≡ a2. + Proof. + intros. split. + - by eapply (view_auth_includedN 0), cmra_included_includedN. + - apply equiv_dist=> n. by eapply view_auth_includedN, cmra_included_includedN. + Qed. + + Lemma view_frag_includedN n p a b1 b2 : + â—¯V b1 ≼{n} â—V{p} a â‹… â—¯V b2 → b1 ≼{n} b2. + Proof. + intros [xf [_ Hb]]; simpl in *. + revert Hb; rewrite left_id. by exists (view_frag_proj xf). + Qed. + Lemma view_frag_included p a b1 b2 : + â—¯V b1 ≼ â—V{p} a â‹… â—¯V b2 → b1 ≼ b2. + Proof. + intros [xf [_ Hb]]; simpl in *. + revert Hb; rewrite left_id. by exists (view_frag_proj xf). + Qed. + (** Internalized properties *) Lemma view_both_validI {M} (relI : uPred M) q a b : (∀ n (x : M), relI n x ↔ rel n a b) → -- GitLab