prove that 'deleting' in the exclusive CMRA is a local update

d7d3cacf · Ralf Jung · c51a909a · d7d3cacf
Commit d7d3cacf authored Feb 12, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

algebra/excl.v algebra/excl.v +4 -0

No files found.
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -143,6 +143,10 @@ Global Instance excl_local_update b :
  LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b).
 Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.

+Global Instance excl_local_update_del :
+LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, ExclUnit).
+Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
+
 (** Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y.
 Proof. by destruct y; intros ? [?| |]. Qed.