Commit eeb3fb17 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'jh/own_big_op' into 'master'

Lemmas stating that big ops are commuting with op/sep.

See merge request !422
parents dd931ed6 357655e2
......@@ -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] kx l, g k x) [^op list] kx 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] kx m, g k x) [^op map] kx 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.
......
......@@ -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] kx l, g k x)
[ list] kx 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] kx m, g k x)
[ map] kx 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] kx l, g k x)
[ list] kx 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] kx m, g k x) [ map] kx 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.
......
......@@ -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] kx l, f k x) [ list] kx 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] kx m, g k x) [ map] kx 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] kx l, f k x) [ list] kx 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] kx m, g k x) [ map] kx 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.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment