From 1fa70657a105de0d132c022507306651b9013ad8 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 4 Feb 2016 16:00:39 +0100 Subject: [PATCH] Make functor stuff more consistent. --- algebra/agree.v | 6 +++--- algebra/auth.v | 8 ++++---- algebra/cmra.v | 9 --------- algebra/excl.v | 4 ++-- algebra/fin_maps.v | 24 +++++++++--------------- algebra/option.v | 12 ++++++++---- program_logic/model.v | 4 ++-- program_logic/resources.v | 16 ++++++++-------- 8 files changed, 36 insertions(+), 47 deletions(-) diff --git a/algebra/agree.v b/algebra/agree.v index 65464cdd..62ec7ff2 100644 --- a/algebra/agree.v +++ b/algebra/agree.v @@ -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. diff --git a/algebra/auth.v b/algebra/auth.v index 32e76cd4..ea9b3a07 100644 --- a/algebra/auth.v +++ b/algebra/auth.v @@ -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. diff --git a/algebra/cmra.v b/algebra/cmra.v index 6296a271..bc4b94d2 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -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) := _. diff --git a/algebra/excl.v b/algebra/excl.v index a0be19ba..bd70fec9 100644 --- a/algebra/excl.v +++ b/algebra/excl.v @@ -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. diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v index 1ee9030b..9ca47881 100644 --- a/algebra/fin_maps.v +++ b/algebra/fin_maps.v @@ -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. diff --git a/algebra/option.v b/algebra/option.v index 071ecafb..367d9f0d 100644 --- a/algebra/option.v +++ b/algebra/option.v @@ -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. diff --git a/program_logic/model.v b/program_logic/model.v index 40be6780..0be58931 100644 --- a/program_logic/model.v +++ b/program_logic/model.v @@ -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. diff --git a/program_logic/resources.v b/program_logic/resources.v index 5692e645..68aa8086 100644 --- a/program_logic/resources.v +++ b/program_logic/resources.v @@ -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. -- GitLab