diff --git a/algebra/cmra.v b/algebra/cmra.v index 7bdfd642e9abc66f87fe72a2def6637a74b2966d..f2f0da685f5ccd26beddb65db2bd10a02046619a 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -127,7 +127,7 @@ End cmra_mixin. (** * CMRAs with a global identity element *) (** We use the notation ∅ because for most instances (maps, sets, etc) the `empty' element is the global identity. *) -Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := { +Class CMRAIdentity (A : cmraT) `{Empty A} := { cmra_empty_valid : ✓ ∅; cmra_empty_left_id :> LeftId (≡) ∅ (⋅); cmra_empty_timeless :> Timeless ∅ @@ -135,7 +135,7 @@ Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := { Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate ∅. (** * Discrete CMRAs *) -Class CMRADiscrete (A : cmraT) : Prop := { +Class CMRADiscrete (A : cmraT) := { cmra_discrete :> Discrete A; cmra_discrete_valid (x : A) : ✓{0} x → ✓ x }. @@ -146,6 +146,8 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := { validN_preserving n x : ✓{n} x → ✓{n} f x; included_preserving x y : x ≼ y → f x ≼ f y }. +Arguments validN_preserving {_ _} _ {_} _ _ _. +Arguments included_preserving {_ _} _ {_} _ _ _. (** * Local updates *) (** The idea is that lemams taking this class will usually have L explicit, @@ -447,7 +449,7 @@ Section cmra_monotone. Lemma includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y. Proof. intros [z ->]. - apply cmra_included_includedN, included_preserving, cmra_included_l. + apply cmra_included_includedN, (included_preserving f), cmra_included_l. Qed. Lemma valid_preserving x : ✓ x → ✓ f x. Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed. diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v index bbf585b0f8addb311f8fafabbaecfc1167f1e22c..625f209698a7d7a9339809ccffc929cf1ca07756 100644 --- a/algebra/fin_maps.v +++ b/algebra/fin_maps.v @@ -339,7 +339,7 @@ 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. split; try apply _. - - by intros n m ? i; rewrite lookup_fmap; apply validN_preserving. + - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _). - intros m1 m2; rewrite !map_included_spec=> Hm i. by rewrite !lookup_fmap; apply: included_preserving. Qed. diff --git a/algebra/iprod.v b/algebra/iprod.v index 1e8f85ee59e360913d44f702458da7e56c978772..cea3278f5335f77f43de583c31d6125a1c3effe2 100644 --- a/algebra/iprod.v +++ b/algebra/iprod.v @@ -277,9 +277,9 @@ Instance iprod_map_cmra_monotone {A} {B1 B2: A → cmraT} (f : ∀ x, B1 x → B (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f). Proof. split; first apply _. - - intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg. + - intros n g Hg x; rewrite /iprod_map; apply (validN_preserving (f _)), Hg. - intros g1 g2; rewrite !iprod_included_spec=> Hf x. - rewrite /iprod_map; apply included_preserving, Hf. + rewrite /iprod_map; apply (included_preserving _), Hf. Qed. Definition iprodC_map {A} {B1 B2 : A → cofeT} (f : iprod (λ x, B1 x -n> B2 x)) : diff --git a/algebra/option.v b/algebra/option.v index 6e959103067eade9b650db26fd282df68eef3313..f0a5d5f6677ff6a15d10c2b901c57ff30d07a9b7 100644 --- a/algebra/option.v +++ b/algebra/option.v @@ -179,7 +179,7 @@ Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f} CMRAMonotone (fmap f : option A → option B). Proof. split; first apply _. - - intros n [x|] ?; rewrite /cmra_validN /=; by repeat apply validN_preserving. + - intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f). - intros mx my; rewrite !option_included. intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @included_preserving. Qed. diff --git a/program_logic/resources.v b/program_logic/resources.v index 48531ad88250983d5cf08e59c27c1f5da6df6bda..3b16ac81e6c3d8f3aa8e6d65a61b564341dd6bcc 100644 --- a/program_logic/resources.v +++ b/program_logic/resources.v @@ -206,9 +206,9 @@ Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) : CMRAMonotone (@res_map Λ Σ _ _ f). Proof. split; first apply _. - - by intros n r (?&?&?); split_and!; simpl; try apply validN_preserving. + - by intros n r (?&?&?); split_and!; simpl; try apply: validN_preserving. - by intros r1 r2; rewrite !res_included; - intros (?&?&?); split_and!; simpl; try apply included_preserving. + intros (?&?&?); split_and!; simpl; try apply: included_preserving. Qed. Definition resC_map {Λ Σ A B} (f : A -n> B) : resC Λ Σ A -n> resC Λ Σ B := CofeMor (res_map f : resRA Λ Σ A → resRA Λ Σ B).