Commit 9460ce23 authored by Robbert Krebbers's avatar Robbert Krebbers

Identity and composition laws for excl and auth functor.

parent a50d7b04
......@@ -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.
......
......@@ -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.
......
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