From 833f7c15d919a7f639cafb9fb553c88e6a487025 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 27 Nov 2017 16:53:52 +0100
Subject: [PATCH] `to_agree` preserves discrete OFE elements.

---
 theories/algebra/agree.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index e3c7f4fc3..1f6404d4b 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -166,6 +166,15 @@ Proof.
 Qed.
 Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
 
+Global Instance to_agree_discrete a : Discrete a → Discrete (to_agree a).
+Proof.
+  intros ? y [H H'] n; split.
+  - intros a' ->%elem_of_list_singleton. destruct (H a) as [b ?]; first by left.
+    exists b. by rewrite -discrete_iff_0.
+  - intros b Hb. destruct (H' b) as (b'&->%elem_of_list_singleton&?); auto.
+    exists a. by rewrite elem_of_list_singleton -discrete_iff_0.
+Qed.
+
 Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
 Proof.
   move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver.
-- 
GitLab