Commit 12ac96cd authored by Ralf Jung's avatar Ralf Jung

add pair_included, auth_frag_core, singleton_core_total

parent 9b2ad256
......@@ -286,6 +286,8 @@ Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
Proof. done. Qed.
Lemma auth_frag_mono a b : a b a b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
Lemma auth_frag_core a : core ( a) = (core a).
Proof. done. Qed.
Global Instance auth_frag_sep_homomorphism :
MonoidHomomorphism op op () (@auth_frag A).
......
......@@ -1221,6 +1221,9 @@ Section prod.
Proof. done. Qed.
Lemma pair_valid (a : A) (b : B) : (a, b) a b.
Proof. done. Qed.
Lemma pair_included (a a' : A) (b b' : B) :
(a, b) (a', b') a a' b b'.
Proof. apply prod_included. Qed.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
......
......@@ -292,6 +292,9 @@ Lemma core_singleton' (i : K) (x : A) cx :
Proof.
intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx').
Qed.
Lemma singleton_core_total `{!CmraTotal A} (i : K) (x : A) :
core ({[ i := x ]} : gmap K A) = {[ i := core x ]}.
Proof. apply core_singleton. rewrite cmra_pcore_core //. Qed.
Lemma op_singleton (i : K) (x y : A) :
{[ i := x ]} {[ i := y ]} = ({[ i := x y ]} : gmap K A).
Proof. by apply (merge_singleton _ _ _ x y). Qed.
......
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