diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v index 0824f520216ecda77b1f93b5c7aa5dff3a5fcb04..c67de29860eaa428e8f8eb90f441f225e96dffc3 100644 --- a/theories/algebra/auth.v +++ b/theories/algebra/auth.v @@ -293,6 +293,19 @@ Global Instance auth_frag_sep_homomorphism : MonoidHomomorphism op op (≡) (@auth_frag A). Proof. by split; [split; try apply _|]. Qed. +Lemma big_opL_auth_frag {B} (g : nat → B → A) (l : list B) : + (◯ [^op list] k↦x ∈ l, g k x) ≡ [^op list] k↦x ∈ l, ◯ (g k x). +Proof. apply (big_opL_commute _). Qed. +Lemma big_opM_auth_frag `{Countable K} {B} (g : K → B → A) (m : gmap K B) : + (◯ [^op map] k↦x ∈ m, g k x) ≡ [^op map] k↦x ∈ m, ◯ (g k x). +Proof. apply (big_opM_commute _). Qed. +Lemma big_opS_auth_frag `{Countable B} (g : B → A) (X : gset B) : + (◯ [^op set] x ∈ X, g x) ≡ [^op set] x ∈ X, ◯ (g x). +Proof. apply (big_opS_commute _). Qed. +Lemma big_opMS_auth_frag `{Countable B} (g : B → A) (X : gmultiset B) : + (◯ [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯ (g x). +Proof. apply (big_opMS_commute _). Qed. + Lemma auth_both_frac_op q a b : Auth (Some (q,to_agree a)) b ≡ ●{q} a ⋅ ◯ b. Proof. by rewrite /op /auth_op /= left_id. Qed. Lemma auth_both_op a b : Auth (Some (1%Qp,to_agree a)) b ≡ ● a ⋅ ◯ b. diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v index fd2f103eb33d048bf3686005c3c61d37be32b71a..c9b0414bd036adee6ccf79ead28807d6001fb6f2 100644 --- a/theories/base_logic/lib/auth.v +++ b/theories/base_logic/lib/auth.v @@ -99,6 +99,49 @@ Section auth. WeakMonoidHomomorphism op uPred_sep (≡) (auth_own γ). Proof. split; try apply _. apply auth_own_op. Qed. + Lemma big_opL_auth_own {B} γ (g : nat → B → A) (l : list B) : + l ≠ [] → + auth_own γ ([^op list] k↦x ∈ l, g k x) ⊣⊢ + [∗ list] k↦x ∈ l, auth_own γ (g k x). + Proof. apply (big_opL_commute1 _). Qed. + Lemma big_opM_auth_own `{Countable K} {B} γ (g : K → B → A) (m : gmap K B) : + m ≠ ∅ → + auth_own γ ([^op map] k↦x ∈ m, g k x) ⊣⊢ + [∗ map] k↦x ∈ m, auth_own γ (g k x). + Proof. apply (big_opM_commute1 _). Qed. + Lemma big_opS_auth_own `{Countable B} γ (g : B → A) (X : gset B) : + X ≠ ∅ → + auth_own γ ([^op set] x ∈ X, g x) ⊣⊢ [∗ set] x ∈ X, auth_own γ (g x). + Proof. apply (big_opS_commute1 _). Qed. + Lemma big_opMS_auth_own `{Countable B} γ (g : B → A) (X : gmultiset B) : + X ≠ ∅ → + auth_own γ ([^op mset] x ∈ X, g x) ⊣⊢ [∗ mset] x ∈ X, auth_own γ (g x). + Proof. apply (big_opMS_commute1 _). Qed. + + Global Instance auth_own_cmra_sep_entails_homomorphism γ : + MonoidHomomorphism op uPred_sep (⊢) (auth_own γ). + Proof. + split; [split|]; try apply _. + - intros. by rewrite auth_own_op. + - apply (affine _). + Qed. + + Lemma big_opL_auth_own_1 {B} γ (g : nat → B → A) (l : list B) : + auth_own γ ([^op list] k↦x ∈ l, g k x) ⊢ + [∗ list] k↦x ∈ l, auth_own γ (g k x). + Proof. apply (big_opL_commute _). Qed. + Lemma big_opM_auth_own_1 `{Countable K} {B} γ (g : K → B → A) + (m : gmap K B) : + auth_own γ ([^op map] k↦x ∈ m, g k x) ⊢ [∗ map] k↦x ∈ m, auth_own γ (g k x). + Proof. apply (big_opM_commute _). Qed. + Lemma big_opS_auth_own_1 `{Countable B} γ (g : B → A) (X : gset B) : + auth_own γ ([^op set] x ∈ X, g x) ⊢ [∗ set] x ∈ X, auth_own γ (g x). + Proof. apply (big_opS_commute _). Qed. + Lemma big_opMS_auth_own_1 `{Countable B} γ (g : B → A) + (X : gmultiset B) : + auth_own γ ([^op mset] x ∈ X, g x) ⊢ [∗ mset] x ∈ X, auth_own γ (g x). + Proof. apply (big_opMS_commute _). Qed. + Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (auth_own γ). Proof. intros a1 a2. apply auth_own_mono. Qed. diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v index 3b80db9787db36bd8396cf1ff34c92fd2679045d..6bfc39ba2c23d4ee28888817a60361d584ad5a6b 100644 --- a/theories/base_logic/lib/own.v +++ b/theories/base_logic/lib/own.v @@ -233,12 +233,55 @@ Proof. Qed. (** Big op class instances *) -Instance own_cmra_sep_homomorphism `{!inG Σ (A:ucmraT)} : - WeakMonoidHomomorphism op uPred_sep (≡) (own γ). -Proof. split; try apply _. apply own_op. Qed. +Section big_op_instances. + Context `{!inG Σ (A:ucmraT)}. + + Global Instance own_cmra_sep_homomorphism : + WeakMonoidHomomorphism op uPred_sep (≡) (own γ). + Proof. split; try apply _. apply own_op. Qed. + + Lemma big_opL_own {B} γ (f : nat → B → A) (l : list B) : + l ≠ [] → + own γ ([^op list] k↦x ∈ l, f k x) ⊣⊢ [∗ list] k↦x ∈ l, own γ (f k x). + Proof. apply (big_opL_commute1 _). Qed. + Lemma big_opM_own `{Countable K} {B} γ (g : K → B → A) (m : gmap K B) : + m ≠ ∅ → + own γ ([^op map] k↦x ∈ m, g k x) ⊣⊢ [∗ map] k↦x ∈ m, own γ (g k x). + Proof. apply (big_opM_commute1 _). Qed. + Lemma big_opS_own `{Countable B} γ (g : B → A) (X : gset B) : + X ≠ ∅ → + own γ ([^op set] x ∈ X, g x) ⊣⊢ [∗ set] x ∈ X, own γ (g x). + Proof. apply (big_opS_commute1 _). Qed. + Lemma big_opMS_own `{Countable B} γ (g : B → A) (X : gmultiset B) : + X ≠ ∅ → + own γ ([^op mset] x ∈ X, g x) ⊣⊢ [∗ mset] x ∈ X, own γ (g x). + Proof. apply (big_opMS_commute1 _). Qed. + + + Global Instance own_cmra_sep_entails_homomorphism : + MonoidHomomorphism op uPred_sep (⊢) (own γ). + Proof. + split; [split|]; try apply _. + - intros. by rewrite own_op. + - apply (affine _). + Qed. + + Lemma big_opL_own_1 {B} γ (f : nat → B → A) (l : list B) : + own γ ([^op list] k↦x ∈ l, f k x) ⊢ [∗ list] k↦x ∈ l, own γ (f k x). + Proof. apply (big_opL_commute _). Qed. + Lemma big_opM_own_1 `{Countable K, B} γ (g : K → B → A) (m : gmap K B) : + own γ ([^op map] k↦x ∈ m, g k x) ⊢ [∗ map] k↦x ∈ m, own γ (g k x). + Proof. apply (big_opM_commute _). Qed. + Lemma big_opS_own_1 `{Countable B} γ (g : B → A) (X : gset B) : + own γ ([^op set] x ∈ X, g x) ⊢ [∗ set] x ∈ X, own γ (g x). + Proof. apply (big_opS_commute _). Qed. + Lemma big_opMS_own_1 `{Countable B} γ (g : B → A) (X : gmultiset B) : + own γ ([^op mset] x ∈ X, g x) ⊢ [∗ mset] x ∈ X, own γ (g x). + Proof. apply (big_opMS_commute _). Qed. +End big_op_instances. (** Proofmode class instances *) -Section proofmode_classes. +Section proofmode_instances. Context `{!inG Σ A}. Implicit Types a b : A. @@ -259,4 +302,4 @@ Section proofmode_classes. intros ? Hb. rewrite /FromAnd (is_op a) own_op. destruct Hb; by rewrite persistent_and_sep. Qed. -End proofmode_classes. +End proofmode_instances.