diff --git a/algebra/agree.v b/algebra/agree.v index 65464cdd1f56cc45e7340b298be7693e53a470bc..62ec7ff26efe431e1e7d04ad195aeaa86620024f 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 32e76cd48c8b2a06d1214a3b8a8a0b27cf4eeb18..ea9b3a076c88288cc579d59e1c28cd907eb6f0ab 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 6296a27148cacf4858c15944e1c05468908c8a45..bc4b94d25402eefa0e0afce062c0666ddd40f93b 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 a0be19baf60fa079e29e5923df257a8805f523ee..bd70fec9cd37f9a2e155e31f844f37e6a802050c 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 1ee9030b41646f450961d08e3d9d39a6cb65cd95..9ca47881ee00675aa81c3647642e18d7ebdef24a 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 071ecafb2c0719a064709dce1bf71fe1b0d1afb5..367d9f0d33765ebc89c3f674004e3e6207c3c4e7 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 40be67805f849501a21349ae326bdf2eb9a8286e..0be5893119674191213015c60a98f5186879b861 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 5692e645de60392349d6ce941908278035301622..68aa80863f73cb4c0bb2a59091b6dcb97e7edea2 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.