Commit 0b440787 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak implicit arguments of CMRAMonotone.

parent ca3da7ca
......@@ -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.
......
......@@ -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.
......
......@@ -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)) :
......
......@@ -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.
......
......@@ -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).
......
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