From 9460ce2384cafe646ef81d8981a8325475553e36 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jan 2016 08:58:35 +0100
Subject: [PATCH] Identity and composition laws for excl and auth functor.

---
 modures/auth.v | 7 +++++++
 modures/excl.v | 5 +++++
 2 files changed, 12 insertions(+)

diff --git a/modures/auth.v b/modures/auth.v
index c821b5de3..a860a0b9b 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -3,6 +3,7 @@ Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
+Add Printing Constructor auth.
 Arguments Auth {_} _ _.
 Arguments authoritative {_} _.
 Arguments own {_} _.
@@ -151,6 +152,12 @@ Arguments authRA : clear implicits.
 (* Functor *)
 Instance auth_fmap : FMap auth := λ A B f x,
   Auth (f <$> authoritative x) (f (own x)).
+Arguments auth_fmap _ _ _ !_ /.
+Lemma auth_fmap_id {A} (x : auth A) : id <$> x = x.
+Proof. by destruct x; rewrite /= excl_fmap_id. Qed.
+Lemma excl_fmap_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
+  g ∘ f <$> x = g <$> f <$> x.
+Proof. by destruct x; rewrite /= excl_fmap_compose. Qed.
 Instance auth_fmap_cmra_ne {A B : cmraT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap auth _ A B).
 Proof.
diff --git a/modures/excl.v b/modures/excl.v
index e1a73d31f..fdb667dcf 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -156,6 +156,11 @@ Instance excl_fmap : FMap excl := λ A B f x,
   match x with
   | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
   end.
+Lemma excl_fmap_id {A} (x : excl A) : id <$> x = x.
+Proof. by destruct x. Qed.
+Lemma excl_fmap_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
+  g ∘ f <$> x = g <$> f <$> x.
+Proof. by destruct x. Qed.
 Instance excl_fmap_cmra_ne {A B : cofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap excl _ A B).
 Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
-- 
GitLab