Merge branch 'jh/cmr_morphisms' into 'master'

A notion of CMRA morphims based on the compatibility with validity, core and composition.

See merge request !56

theories/algebra/agree.v

@@ -443,15 +443,15 @@ Section agree_map.
     apply list_fmap_ext_ne=>y. by apply equiv_dist.
   Qed.
 
-  Global Instance agree_map_monotone : CMRAMonotone (agree_map f).
+  Global Instance agree_map_morphism : CMRAMorphism (agree_map f).
   Proof using Hyps.
     split; first apply _.
     - intros n x. rewrite /cmra_validN /validN /= /agree_validN /= => ?.
       change (list_agrees (dist n) (f <$> agree_list x)).
       eapply (list_agrees_fmap _ _ _); done.
-    - intros x y; rewrite !agree_included=> ->.
-      rewrite /equiv /agree_equiv /agree_map /agree_op /agree_list /=.
-      rewrite !fmap_app=>n. apply: list_setequiv_equiv. set_solver+.
+    - done.
+    - intros x y n. apply: list_setequiv_equiv=>b.
+      rewrite /agree_list /= !fmap_app. set_solver+.
   Qed.
 End agree_map.
 

theories/algebra/auth.v

@@ -272,14 +272,14 @@ Proof.
   intros f g Hf [??] [??] [??]; split; simpl in *; [|by apply Hf].
   apply option_fmap_ne; [|done]=> x y ?; by apply excl_map_ne.
 Qed.
-Instance auth_map_cmra_monotone {A B : ucmraT} (f : A → B) :
-  CMRAMonotone f → CMRAMonotone (auth_map f).
+Instance auth_map_cmra_morphism {A B : ucmraT} (f : A → B) :
+  CMRAMorphism f → CMRAMorphism (auth_map f).
 Proof.
   split; try apply _.
   - intros n [[[a|]|] b]; rewrite !auth_validN_eq; try
-      naive_solver eauto using cmra_monotoneN, cmra_monotone_validN.
-  - by intros [x a] [y b]; rewrite !auth_included /=;
-      intros [??]; split; simpl; apply: cmra_monotone.
+      naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN.
+  - intros [??]. apply Some_proper. by f_equiv; rewrite /= cmra_morphism_core.
+  - intros [[?|]?] [[?|]?]; try apply Auth_proper=>//=; by rewrite cmra_morphism_op.
 Qed.
 Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
   CofeMor (auth_map f).

theories/algebra/cmra.v

@@ -235,13 +235,15 @@ Class CMRADiscrete (A : cmraT) := {
 }.
 
 (** * Morphisms *)
-Class CMRAMonotone {A B : cmraT} (f : A → B) := {
-  cmra_monotone_ne :> NonExpansive f;
-  cmra_monotone_validN n x : ✓{n} x → ✓{n} f x;
-  cmra_monotone x y : x ≼ y → f x ≼ f y
+Class CMRAMorphism {A B : cmraT} (f : A → B) := {
+  cmra_morphism_ne :> NonExpansive f;
+  cmra_morphism_validN n x : ✓{n} x → ✓{n} f x;
+  cmra_morphism_pcore x : pcore (f x) ≡ f <$> pcore x;
+  cmra_morphism_op x y : f x ⋅ f y ≡ f (x ⋅ y)
 }.
-Arguments cmra_monotone_validN {_ _} _ {_} _ _ _.
-Arguments cmra_monotone {_ _} _ {_} _ _ _.
+Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
+Arguments cmra_morphism_pcore {_ _} _ {_} _.
+Arguments cmra_morphism_op {_ _} _ {_} _ _.
 
 (** * Properties **)
 Section cmra.
@@ -716,30 +718,33 @@ Section cmra_total.
   Qed.
 End cmra_total.
 
-(** * Properties about monotone functions *)
-Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
-Proof. repeat split; by try apply _. Qed.
-Instance cmra_monotone_compose {A B C : cmraT} (f : A → B) (g : B → C) :
-  CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ∘ f).
+(** * Properties about morphisms *)
+Instance cmra_morphism_id {A : cmraT} : CMRAMorphism (@id A).
+Proof. split=>//=. apply _. intros. by rewrite option_fmap_id. Qed.
+Instance cmra_morphism_proper {A B : cmraT} (f : A → B) `{!CMRAMorphism f} :
+  Proper ((≡) ==> (≡)) f := ne_proper _.
+Instance cmra_morphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
+  CMRAMorphism f → CMRAMorphism g → CMRAMorphism (g ∘ f).
 Proof.
   split.
   - apply _.
-  - move=> n x Hx /=. by apply cmra_monotone_validN, cmra_monotone_validN.
-  - move=> x y Hxy /=. by apply cmra_monotone, cmra_monotone.
+  - move=> n x Hx /=. by apply cmra_morphism_validN, cmra_morphism_validN.
+  - move=> x /=. by rewrite 2!cmra_morphism_pcore option_fmap_compose.
+  - move=> x y /=. by rewrite !cmra_morphism_op.
 Qed.
 
-Section cmra_monotone.
+Section cmra_morphism.
   Local Set Default Proof Using "Type*".
-  Context {A B : cmraT} (f : A → B) `{!CMRAMonotone f}.
-  Global Instance cmra_monotone_proper : Proper ((≡) ==> (≡)) f := ne_proper _.
-  Lemma cmra_monotoneN n x y : x ≼{n} y → f x ≼{n} f y.
-  Proof.
-    intros [z ->].
-    apply cmra_included_includedN, (cmra_monotone f), cmra_included_l.
-  Qed.
+  Context {A B : cmraT} (f : A → B) `{!CMRAMorphism f}.
+  Lemma cmra_morphism_core x : core (f x) ≡ f (core x).
+  Proof. unfold core, core'. rewrite cmra_morphism_pcore. by destruct (pcore x). Qed.
+  Lemma cmra_morphism_monotone x y : x ≼ y → f x ≼ f y.
+  Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
+  Lemma cmra_morphism_monotoneN n x y : x ≼{n} y → f x ≼{n} f y.
+  Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
   Lemma cmra_monotone_valid x : ✓ x → ✓ f x.
-  Proof. rewrite !cmra_valid_validN; eauto using cmra_monotone_validN. Qed.
-End cmra_monotone.
+  Proof. rewrite !cmra_valid_validN; eauto using cmra_morphism_validN. Qed.
+End cmra_morphism.
 
 (** Functors *)
 Structure rFunctor := RFunctor {
@@ -752,10 +757,10 @@ Structure rFunctor := RFunctor {
   rFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
-  rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
-    CMRAMonotone (rFunctor_map fg)
+  rFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
+    CMRAMorphism (rFunctor_map fg)
 }.
-Existing Instances rFunctor_ne rFunctor_mono.
+Existing Instances rFunctor_ne rFunctor_mor.
 Instance: Params (@rFunctor_map) 5.
 
 Delimit Scope rFunctor_scope with RF.
@@ -785,10 +790,10 @@ Structure urFunctor := URFunctor {
   urFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x);
-  urFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
-    CMRAMonotone (urFunctor_map fg) 
+  urFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
+    CMRAMorphism (urFunctor_map fg)
 }.
-Existing Instances urFunctor_ne urFunctor_mono.
+Existing Instances urFunctor_ne urFunctor_mor.
 Instance: Params (@urFunctor_map) 5.
 
 Delimit Scope urFunctor_scope with URF.
@@ -1148,13 +1153,19 @@ End prod_unit.
 
 Arguments prodUR : clear implicits.
 
-Instance prod_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B') :
-  CMRAMonotone f → CMRAMonotone g → CMRAMonotone (prod_map f g).
+Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
+  CMRAMorphism f → CMRAMorphism g → CMRAMorphism (prod_map f g).
 Proof.
   split; first apply _.
-  - by intros n x [??]; split; simpl; apply cmra_monotone_validN.
-  - intros x y; rewrite !prod_included=> -[??] /=.
-    by split; apply cmra_monotone.
+  - by intros n x [??]; split; simpl; apply cmra_morphism_validN.
+  - intros x. etrans. apply (reflexivity (mbind _ _)).
+    etrans; last apply (reflexivity (_ <$> mbind _ _)). simpl.
+    assert (Hf := cmra_morphism_pcore f (x.1)).
+    destruct (pcore (f (x.1))), (pcore (x.1)); inversion_clear Hf=>//=.
+    assert (Hg := cmra_morphism_pcore g (x.2)).
+    destruct (pcore (g (x.2))), (pcore (x.2)); inversion_clear Hg=>//=.
+    by setoid_subst.
+  - intros. by rewrite /prod_map /= -!cmra_morphism_op.
 Qed.
 
 Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
@@ -1283,9 +1294,6 @@ Section option.
   Canonical Structure optionUR := UCMRAT (option A) option_ucmra_mixin.
 
   (** Misc *)
-  Global Instance Some_cmra_monotone : CMRAMonotone Some.
-  Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed.
-
   Lemma op_None mx my : mx ⋅ my = None ↔ mx = None ∧ my = None.
   Proof. destruct mx, my; naive_solver. Qed.
   Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
@@ -1351,14 +1359,13 @@ Section option_prod.
   Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total y1). Qed.
 End option_prod.
 
-Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f} :
-  CMRAMonotone (fmap f : option A → option B).
+Instance option_fmap_cmra_morphism {A B : cmraT} (f: A → B) `{!CMRAMorphism f} :
+  CMRAMorphism (fmap f : option A → option B).
 Proof.
   split; first apply _.
-  - intros n [x|] ?; rewrite /cmra_validN //=. by apply (cmra_monotone_validN f).
-  - intros mx my; rewrite !option_included.
-    intros [->|(x&y&->&->&[Hxy|?])]; simpl; eauto 10 using @cmra_monotone.
-    right; exists (f x), (f y). by rewrite {3}Hxy; eauto.
+  - intros n [x|] ?; rewrite /cmra_validN //=. by apply (cmra_morphism_validN f).
+  - move=> [x|] //. by apply Some_proper, cmra_morphism_pcore.
+  - move=> [x|] [y|] //=. by rewrite -(cmra_morphism_op f).
 Qed.
 
 Program Definition optionRF (F : rFunctor) : rFunctor := {|

theories/algebra/csum.v

@@ -356,14 +356,13 @@ End cmra.
 Arguments csumR : clear implicits.
 
 (* Functor *)
-Instance csum_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B') :
-  CMRAMonotone f → CMRAMonotone g → CMRAMonotone (csum_map f g).
+Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
+  CMRAMorphism f → CMRAMorphism g → CMRAMorphism (csum_map f g).
 Proof.
   split; try apply _.
-  - intros n [a|b|]; simpl; auto using cmra_monotone_validN.
-  - intros x y; rewrite !csum_included.
-    intros [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]; simpl;
-    eauto 10 using cmra_monotone.
+  - intros n [a|b|]; simpl; auto using cmra_morphism_validN.
+  - move=> [a|b|]=>//=; rewrite cmra_morphism_pcore; by destruct pcore.
+  - intros [xa|ya|] [xb|yb|]=>//=; by rewrite -cmra_morphism_op.
 Qed.
 
 Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|

theories/algebra/excl.v

@@ -141,14 +141,9 @@ Proof. by destruct x; constructor. Qed.
 Instance excl_map_ne {A B : ofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
 Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
-Instance excl_map_cmra_monotone {A B : ofeT} (f : A → B) :
-  NonExpansive f → CMRAMonotone (excl_map f).
-Proof.
-  split; try apply _.
-  - by intros n [a|].
-  - intros x y [z Hy]; exists (excl_map f z); apply equiv_dist=> n.
-    move: Hy=> /equiv_dist /(_ n) ->; by destruct x, z.
-Qed.
+Instance excl_map_cmra_morphism {A B : ofeT} (f : A → B) :
+  NonExpansive f → CMRAMorphism (excl_map f).
+Proof. split; try done; try apply _. by intros n [a|]. Qed.
 Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
   CofeMor (excl_map f).
 Instance exclC_map_ne A B : NonExpansive (@exclC_map A B).

theories/algebra/gmap.v

@@ -474,13 +474,14 @@ End properties.
 Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (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.
-Instance gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B)
-  `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B).
+Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmraT} (f : A → B)
+  `{!CMRAMorphism f} : CMRAMorphism (fmap f : gmap K A → gmap K B).
 Proof.
   split; try apply _.
-  - by intros n m ? i; rewrite lookup_fmap; apply (cmra_monotone_validN _).
-  - intros m1 m2; rewrite !lookup_included=> Hm i.
-    by rewrite !lookup_fmap; apply: cmra_monotone.
+  - by intros n m ? i; rewrite lookup_fmap; apply (cmra_morphism_validN _).
+  - intros m. apply Some_proper=>i. rewrite lookup_fmap !lookup_omap lookup_fmap.
+    case: (m!!i)=>//= ?. apply cmra_morphism_pcore, _.
+  - intros m1 m2 i. by rewrite lookup_op !lookup_fmap lookup_op cmra_morphism_op.
 Qed.
 Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
   gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A → gmapC K B).

theories/algebra/iprod.v

@@ -282,14 +282,14 @@ Instance iprod_map_ne `{Finite A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x
   (∀ x, Proper (dist n ==> dist n) (f x)) →
   Proper (dist n ==> dist n) (iprod_map f).
 Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
-Instance iprod_map_cmra_monotone
+Instance iprod_map_cmra_morphism
     `{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
-  (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f).
+  (∀ x, CMRAMorphism (f x)) → CMRAMorphism (iprod_map f).
 Proof.
   split; first apply _.
-  - intros n g Hg x; rewrite /iprod_map; apply (cmra_monotone_validN (f _)), Hg.
-  - intros g1 g2; rewrite !iprod_included_spec=> Hf x.
-    rewrite /iprod_map; apply (cmra_monotone _), Hf.
+  - intros n g Hg x; rewrite /iprod_map; apply (cmra_morphism_validN (f _)), Hg.
+  - intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
+  - intros g1 g2 i. by rewrite /iprod_map iprod_lookup_op cmra_morphism_op.
 Qed.
 
 Definition iprodC_map `{Finite A} {B1 B2 : A → ofeT}

theories/algebra/list.v

@@ -433,14 +433,16 @@ Section properties.
 End properties.
 
 (** Functor *)
-Instance list_fmap_cmra_monotone {A B : ucmraT} (f : A → B)
-  `{!CMRAMonotone f} : CMRAMonotone (fmap f : list A → list B).
+Instance list_fmap_cmra_morphism {A B : ucmraT} (f : A → B)
+  `{!CMRAMorphism f} : CMRAMorphism (fmap f : list A → list B).
 Proof.
   split; try apply _.
   - intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
-    by apply (cmra_monotone_validN (fmap f : option A → option B)).
-  - intros l1 l2. rewrite !list_lookup_included=> Hl i. rewrite !list_lookup_fmap.
-    by apply (cmra_monotone (fmap f : option A → option B)).
+    by apply (cmra_morphism_validN (fmap f : option A → option B)).
+  - intros l. apply Some_proper. rewrite -!list_fmap_compose.
+    apply list_fmap_equiv_ext, cmra_morphism_core, _.
+  - intros l1 l2. apply list_equiv_lookup=>i.
+    by rewrite list_lookup_op !list_lookup_fmap list_lookup_op cmra_morphism_op.
 Qed.
 
 Program Definition listURF (F : urFunctor) : urFunctor := {|

theories/base_logic/upred.v

@@ -93,31 +93,31 @@ Qed.
 
 (** functor *)
 Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
-  `{!CMRAMonotone f} (P : uPred M1) :
+  `{!CMRAMorphism f} (P : uPred M1) :
   uPred M2 := {| uPred_holds n x := P n (f x) |}.
-Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
-Next Obligation. naive_solver eauto using uPred_closed, cmra_monotone_validN. Qed.
+Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed.
+Next Obligation. naive_solver eauto using uPred_closed, cmra_morphism_validN. Qed.
 
 Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
-  `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
+  `{!CMRAMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
 Proof.
   intros x1 x2 Hx; split=> n' y ??.
-  split; apply Hx; auto using cmra_monotone_validN.
+  split; apply Hx; auto using cmra_morphism_validN.
 Qed.
 Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P ≡ P.
 Proof. by split=> n x ?. Qed.
 Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
-    `{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
+    `{!CMRAMorphism f, !CMRAMorphism g} (P : uPred M3):
   uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
 Proof. by split=> n x Hx. Qed.
 Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
-      `{!CMRAMonotone f} `{!CMRAMonotone g}:
+      `{!CMRAMorphism f} `{!CMRAMorphism g}:
   (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
 Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
-Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
+Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CMRAMorphism f} :
   uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
 Lemma uPredC_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
-    `{!CMRAMonotone f, !CMRAMonotone g} n :
+    `{!CMRAMorphism f, !CMRAMorphism g} n :
   f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
 Proof.
   by intros Hfg P; split=> n' y ??;