Commit c07a5eec authored by Ralf Jung's avatar Ralf Jung
Browse files

show that pair cosntruction commutes with taking the core

parent 86da40a5
......@@ -476,6 +476,10 @@ Section total_core.
Local Set Default Proof Using "Type*".
Context `{CmraTotal A}.
Lemma cmra_pcore_core x : pcore x = Some (core x).
rewrite /core /core'. destruct (cmra_total x) as [cx ->]. done.
Lemma cmra_core_l x : core x x x.
destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_l.
......@@ -1136,6 +1140,14 @@ Section prod.
Lemma pair_valid (a : A) (b : B) : (a, b) a b.
Proof. done. Qed.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
rewrite /core /core' {1}/pcore /=.
rewrite (cmra_pcore_core a). simpl.
rewrite (cmra_pcore_core b). done.
Global Instance prod_cmra_total : CmraTotal A CmraTotal B CmraTotal prodR.
intros H1 H2 [a b]. destruct (H1 a) as [ca ?], (H2 b) as [cb ?].
Supports Markdown
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