Commit e0a9fa60 authored by Robbert Krebbers's avatar Robbert Krebbers

Functioriality stuff.

parent 06417e80
......@@ -189,3 +189,5 @@ Qed.
Definition prodRA_map {A A' B B' : cmraT}
(f : A -n> A') (g : B -n> B') : prodRA A B -n> prodRA A' B' :=
CofeMor (prod_map f g : prodRA A B prodRA A' B').
Instance prodRA_map_ne {A A' B B'} n :
Proper (dist n==> dist n==> dist n) (@prodRA_map A A' B B') := prodC_map_ne n.
......@@ -56,6 +56,14 @@ Proof.
* by exists (None,Some x); inversion Hx'; repeat constructor.
* exists (None,None); repeat constructor.
Qed.
Instance option_fmap_cmra_preserving `{CMRA A, CMRA B} (f : A B)
`{!CMRAPreserving f} : CMRAPreserving (fmap f : option A option B).
Proof.
split.
* by destruct 1 as [|[?|]]; constructor; apply included_preserving.
* by intros n [x|] ?;
unfold validN, option_validN; simpl; try apply validN_preserving.
Qed.
(** fin maps *)
Section map.
......@@ -123,12 +131,36 @@ Section map.
by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
Qed.
Definition mapRA (A : cmraT) : cmraT := CMRAT (M A).
Global Instance map_fmap_cmra_preserving `{CMRA A, CMRA B} (f : A B)
`{!CMRAPreserving f} : CMRAPreserving (fmap f : M A M B).
Proof.
split.
* by intros m1 m2 Hm i; rewrite !lookup_fmap; apply included_preserving.
* by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
Qed.
Local Hint Extern 0 => simpl; apply map_fmap_ne : typeclass_instances.
Definition mapRA_map {A B : cmraT} (f : A -n> B) : mapRA A -n> mapRA B :=
CofeMor (fmap f : mapRA A mapRA B).
Global Instance mapRA_map_ne {A B} n :
Proper (dist n ==> dist n) (@mapRA_map A B) := mapC_map_ne n.
Global Instance mapRA_mapcmra_preserving {A B : cmraT} (f : A -n> B)
`{!CMRAPreserving f} : CMRAPreserving (mapRA_map f) := _.
End map.
Arguments mapRA {_} _ {_ _ _ _ _ _ _ _ _} _.
Canonical Structure natmapRA := mapRA natmap.
Definition natmapRA_map {A B : cmraT}
(f : A -n> B) : natmapRA A -n> natmapRA B := mapRA_map f.
Canonical Structure PmapRA := mapRA Pmap.
Definition PmapRA_map {A B : cmraT}
(f : A -n> B) : PmapRA A -n> PmapRA B := mapRA_map f.
Canonical Structure NmapRA := mapRA Nmap.
Definition NmapC_map {A B : cmraT}
(f : A -n> B) : NmapRA A -n> NmapRA B := mapRA_map f.
Canonical Structure ZmapRA := mapRA Zmap.
Definition ZmapRA_map {A B : cmraT}
(f : A -n> B) : ZmapRA A -n> ZmapRA B := mapRA_map f.
Canonical Structure stringmapRA := mapRA stringmap.
Definition stringmapRA_map {A B : cmraT}
(f : A -n> B) : stringmapRA A -n> stringmapRA B := mapRA_map f.
......@@ -290,6 +290,6 @@ Section later.
Proof. by destruct x. Qed.
Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
CofeMor (fmap f : laterC A laterC B).
Instance laterC_contractive (A B : cofeT) : Contractive (@laterC_map A B).
Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
Proof. intros n f g Hf n'; apply Hf. Qed.
End later.
......@@ -85,10 +85,10 @@ Section map.
Definition mapC (A : cofeT) : cofeT := CofeT (M A).
Definition mapC_map {A B} (f: A -n> B) : mapC A -n> mapC B :=
CofeMor (fmap f : mapC A mapC B).
Global Instance mapC_map_ne (A B : cofeT) :
Global Instance mapC_map_ne {A B} n :
Proper (dist n ==> dist n) (@mapC_map A B).
Proof.
intros n f g Hf m k; simpl; rewrite !lookup_fmap.
intros f g Hf m k; simpl; rewrite !lookup_fmap.
destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
End map.
......
......@@ -4,7 +4,7 @@ Local Hint Extern 1 (_ ≼ _) => etransitivity; [|eassumption].
Local Hint Extern 10 (_ _) => omega.
Structure uPred (M : cmraT) : Type := IProp {
uPred_holds :> nat M -> Prop;
uPred_holds :> nat M Prop;
uPred_ne x1 x2 n : uPred_holds n x1 x1 ={n}= x2 uPred_holds n x2;
uPred_weaken x1 x2 n1 n2 :
x1 x2 n2 n1 validN n2 x2 uPred_holds n1 x1 uPred_holds n2 x2
......@@ -59,6 +59,12 @@ Proof.
Qed.
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAPreserving f} :
uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 uPredC M2).
Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
`{!CMRAPreserving f, !CMRAPreserving g} n :
f ={n}= g uPredC_map f ={n}= uPredC_map g.
Proof.
by intros Hfg P y n' ??; simpl; rewrite (dist_le _ _ _ _(Hfg y)) by lia.
Qed.
(** logical entailement *)
Instance uPred_entails {M} : SubsetEq (uPred M) := λ P Q, x n,
......
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