Commit 8f41613d authored by Robbert's avatar Robbert

Merge branch 'ralf/pair-core' into 'master'

show that pair construction commutes with taking the core

See merge request iris/iris!286
parents e6f6758c 162755de
......@@ -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).
Proof.
rewrite /core /core'. destruct (cmra_total x) as [cx ->]. done.
Qed.
Lemma cmra_core_l x : core x x x.
Proof.
destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_l.
......@@ -1136,6 +1140,13 @@ 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).
Proof.
rewrite /core /core' {1}/pcore /=.
rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
Qed.
Global Instance prod_cmra_total : CmraTotal A CmraTotal B CmraTotal prodR.
Proof.
intros H1 H2 [a b]. destruct (H1 a) as [ca ?], (H2 b) as [cb ?].
......
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