Commit 1fa70657 authored by Robbert Krebbers's avatar Robbert Krebbers

Make functor stuff more consistent.

parent 1cfbdb17
......@@ -167,9 +167,9 @@ Section agree_map.
Qed.
End agree_map.
Definition agreeRA_map {A B} (f : A -n> B) : agreeRA A -n> agreeRA B :=
CofeMor (agree_map f : agreeRA A agreeRA B).
Instance agreeRA_map_ne A B n : Proper (dist n ==> dist n) (@agreeRA_map A B).
Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
CofeMor (agree_map f : agreeC A agreeC B).
Instance agreeC_map_ne A B n : Proper (dist n ==> dist n) (@agreeC_map A B).
Proof.
intros f g Hfg x; split; simpl; intros; first done.
by apply dist_le with n; try apply Hfg.
......
......@@ -177,7 +177,7 @@ 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 :
Instance auth_fmap_cmra_ne {A B : cofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap auth _ A B).
Proof.
intros f g Hf [??] [??] [??]; split; [by apply excl_fmap_cmra_ne|by apply Hf].
......@@ -192,7 +192,7 @@ Proof.
* intros n [[a| |] b]; rewrite /= /cmra_validN;
naive_solver eauto using @includedN_preserving, @validN_preserving.
Qed.
Definition authRA_map {A B : cmraT} (f : A -n> B) : authRA A -n> authRA B :=
CofeMor (fmap f : authRA A authRA B).
Lemma authRA_map_ne A B n : Proper (dist n ==> dist n) (@authRA_map A B).
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
CofeMor (fmap f : authC A authC B).
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.
......@@ -522,11 +522,6 @@ Proof.
by split; apply includedN_preserving.
* by intros n x [??]; split; simpl; apply validN_preserving.
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.
(** ** Indexed product *)
Section iprod_cmra.
......@@ -631,7 +626,3 @@ Proof.
rewrite /iprod_map; apply includedN_preserving, Hf.
* intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg.
Qed.
Definition iprodRA_map {A} {B1 B2: A cmraT} (f : iprod (λ x, B1 x -n> B2 x)) :
iprodRA B1 -n> iprodRA B2 := CofeMor (iprod_map f).
Instance laterRA_map_ne {A} {B1 B2 : A cmraT} n :
Proper (dist n ==> dist n) (@iprodRA_map A B1 B2) := _.
......@@ -174,7 +174,7 @@ Proof.
by destruct x, z; constructor.
* by intros n [a| |].
Qed.
Definition exclRA_map {A B} (f : A -n> B) : exclRA A -n> exclRA B :=
Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
CofeMor (fmap f : exclRA A exclRA B).
Lemma exclRA_map_ne A B n : Proper (dist n ==> dist n) (@exclRA_map A B).
Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
......@@ -226,18 +226,10 @@ Lemma map_updateP_alloc' m x :
Proof. eauto using map_updateP_alloc. Qed.
End properties.
(** Functor *)
Instance map_fmap_ne `{Countable K} {A B : cofeT} (f : A B) n :
Proper (dist n ==> dist n) f Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B :=
CofeMor (fmap f : mapC K A mapC K B).
Instance mapC_map_ne `{Countable K} {A B} n :
Proper (dist n ==> dist n) (@mapC_map K _ _ A B).
Proof.
intros f g Hf m k; rewrite /= !lookup_fmap.
destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
Instance map_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A B)
`{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A gmap K B).
Proof.
......@@ -246,9 +238,11 @@ Proof.
by rewrite !lookup_fmap; apply: includedN_preserving.
* by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
Qed.
Definition mapRA_map `{Countable K} {A B : cmraT} (f : A -n> B) :
mapRA K A -n> mapRA K B := CofeMor (fmap f : mapRA K A mapRA K B).
Instance mapRA_map_ne `{Countable K} {A B} n :
Proper (dist n ==> dist n) (@mapRA_map K _ _ A B) := mapC_map_ne n.
Instance mapRA_map_monotone `{Countable K} {A B : cmraT} (f : A -n> B)
`{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.
Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B :=
CofeMor (fmap f : mapC K A mapC K B).
Instance mapC_map_ne `{Countable K} {A B} n :
Proper (dist n ==> dist n) (@mapC_map K _ _ A B).
Proof.
intros f g Hf m k; rewrite /= !lookup_fmap.
destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
......@@ -57,10 +57,6 @@ End cofe.
Arguments optionC : clear implicits.
Instance option_fmap_ne {A B : cofeT} (f : A B) n:
Proper (dist n ==> dist n) f Proper (dist n==>dist n) (fmap (M:=option) f).
Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
(* CMRA *)
Section cmra.
Context {A : cmraT}.
......@@ -158,6 +154,10 @@ End cmra.
Arguments optionRA : clear implicits.
(** Functor *)
Instance option_fmap_ne {A B : cofeT} (f : A B) n:
Proper (dist n ==> dist n) f Proper (dist n==>dist n) (fmap (M:=option) f).
Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
Instance option_fmap_cmra_monotone {A B : cmraT} (f: A B) `{!CMRAMonotone f} :
CMRAMonotone (fmap f : option A option B).
Proof.
......@@ -166,3 +166,7 @@ Proof.
intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving.
* by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving.
Qed.
Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
CofeMor (fmap f : optionC A optionC B).
Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
......@@ -6,7 +6,7 @@ Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
uPredC (resRA Λ Σ (laterC A)).
Definition map {Λ : language} {Σ : iFunctor} {A1 A2 B1 B2 : cofeT}
(f : (A2 -n> A1) * (B1 -n> B2)) : F Λ Σ A1 B1 -n> F Λ Σ A2 B2 :=
uPredC_map (resRA_map (laterC_map (f.1))).
uPredC_map (resC_map (laterC_map (f.1))).
Definition result Λ Σ : solution (F Λ Σ).
Proof.
apply (solver.result _ (@map Λ Σ)).
......@@ -18,7 +18,7 @@ Proof.
rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
by rewrite -later_map_compose.
* intros A1 A2 B1 B2 n f f' [??] P.
by apply upredC_map_ne, resRA_map_ne, laterC_map_contractive.
by apply upredC_map_ne, resC_map_ne, laterC_map_contractive.
Qed.
End iProp.
......
......@@ -39,9 +39,7 @@ Proof. by destruct 1. Qed.
Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ Σ A).
Proof. by destruct 1. Qed.
Global Instance pst_ne' n : Proper (dist (S n) ==> ()) (@pst Λ Σ A).
Proof.
intros σ σ' [???]; apply (timeless _), dist_le with (S n); auto with lia.
Qed.
Proof. destruct 1; apply (timeless _), dist_le with (S n); auto with lia. Qed.
Global Instance pst_proper : Proper (() ==> (=)) (@pst Λ Σ A).
Proof. by destruct 1; unfold_leibniz. Qed.
Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ Σ A).
......@@ -164,6 +162,8 @@ Qed.
Global Instance Res_timeless eσ m : Timeless m Timeless (Res eσ m).
Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
End res.
Arguments resC : clear implicits.
Arguments resRA : clear implicits.
Definition res_map {Λ Σ A B} (f : A -n> B) (r : res Λ Σ A) : res Λ Σ B :=
......@@ -196,8 +196,6 @@ Proof.
* by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
* by apply ifunctor_map_ext.
Qed.
Definition resRA_map {Λ Σ A B} (f : A -n> B) : resRA Λ Σ A -n> resRA Λ Σ B :=
CofeMor (res_map f : resRA Λ Σ A resRA Λ Σ B).
Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) :
CMRAMonotone (@res_map Λ Σ _ _ f).
Proof.
......@@ -206,10 +204,12 @@ Proof.
intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
* by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
Qed.
Instance resRA_map_ne {Λ Σ A B} n :
Proper (dist n ==> dist n) (@resRA_map Λ Σ A B).
Definition resC_map {Λ Σ A B} (f : A -n> B) : resC Λ Σ A -n> resC Λ Σ B :=
CofeMor (res_map f : resRA Λ Σ A resRA Λ Σ B).
Instance resC_map_ne {Λ Σ A B} n :
Proper (dist n ==> dist n) (@resC_map Λ Σ A B).
Proof.
intros f g Hfg r; split; simpl; auto.
* by apply (mapRA_map_ne _ (agreeRA_map f) (agreeRA_map g)), agreeRA_map_ne.
* by apply (mapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
* by apply ifunctor_map_ne.
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