From f079e68052c0247b33c0fb9b51d5f0e85be99e10 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Dec 2015 13:33:05 +0100
Subject: [PATCH] Extensionality of map on agreement.

---
 iris/agree.v | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/iris/agree.v b/iris/agree.v
index f7a59285e..41f991216 100644
--- a/iris/agree.v
+++ b/iris/agree.v
@@ -124,15 +124,21 @@ Proof.
 Qed.
 End agree.
 
+Program Definition agree_map `{Dist A, Dist B}
+    (f : A → B) (x : agree A) : agree B :=
+  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
+Solve Obligations with auto using agree_valid_0, agree_valid_S.
+
 Section agree_map.
-  Context `{Cofe A,Cofe B} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
-  Program Definition agree_map (x : agree A) : agree B :=
-    {| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
-  Solve Obligations with auto using agree_valid_0, agree_valid_S.
-  Global Instance agree_map_ne n : Proper (dist n ==> dist n) agree_map.
+  Context `{Cofe A, Cofe B} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
+  Global Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
   Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
-  Global Instance agree_map_proper: Proper ((≡)==>(≡)) agree_map := ne_proper _.
-  Global Instance agree_map_monotone : CMRAMonotone agree_map.
+  Global Instance agree_map_proper :
+    Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _.
+  Lemma agree_map_ext (g : A → B) x :
+    (∀ x, f x ≡ g x) → agree_map f x ≡ agree_map g x.
+  Proof. by intros Hfg; split; simpl; intros; rewrite ?Hfg. Qed.
+  Global Instance agree_map_monotone : CMRAMonotone (agree_map f).
   Proof.
     split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]].
     intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy.
-- 
GitLab