Commit 233aa0fa authored by Robbert Krebbers's avatar Robbert Krebbers

Prove that the auth fragment is a UCMRA homomorphism.

parent 1bbe5d15
...@@ -191,7 +191,7 @@ Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b. ...@@ -191,7 +191,7 @@ Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Proof. done. Qed. Proof. done. Qed.
Lemma auth_frag_mono a b : a b a b. Lemma auth_frag_mono a b : a b a b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed. Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
Global Instance auth_frag_cmra_homomorphism : CMRAHomomorphism (Auth None). Global Instance auth_frag_cmra_homomorphism : UCMRAHomomorphism (Auth None).
Proof. done. Qed. Proof. done. Qed.
Lemma auth_both_op a b : Auth (Excl' a) b a b. Lemma auth_both_op a b : Auth (Excl' a) b a b.
......
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