Category of cmras

iris/algebra/category/morphism.v

+From stdpp Require Import gmap list.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import big_op.
+From iris.prelude Require Import options.
+
+Lemma list_union_comm {A} `{!EqDecision A} (xs ys : list A) : NoDup xs → NoDup ys → list_union xs ys ≡ₚ list_union ys xs.
+Proof.
+  intros Hxs Hys.
+  apply NoDup_Permutation.
+  - by apply NoDup_list_union.
+  - by apply NoDup_list_union.
+  - intros x.
+    rewrite !elem_of_list_union.
+    naive_solver.
+Qed.
+
+Class Morphism {A B : cmra} (f : A → B) := {
+  #[global] morph_ne :: NonExpansive f;
+  morph_validN n (x : A) : ✓{n} x → ✓{n} (f x);
+  morph_op (x y : A) : f (x ⋅ y) ≡ f x ⋅ f y;
+}.
+Global Hint Mode Morphism - - ! : typeclass_instances.
+Global Arguments morph_validN {_ _} _ {_} _ _ _.
+Global Arguments morph_op {_ _} _ {_} _ _.
+
+Class PerservesUnit {A B : ucmra} (f : A → B) :=
+  morph_unit : f ε ≡ ε.
+Global Hint Mode PerservesUnit - - ! : typeclass_instances.
+Global Arguments morph_op {_ _} _ {_}.
+
+Section morph.
+Context {A B : cmra} (f : A → B) `{!Morphism f}.
+
+Global Instance morph_proper : Proper ((≡) ==> (≡)) f.
+Proof using Type*. apply ne_proper, _. Qed.
+
+Lemma morph_valid (x : A) : ✓ x → ✓ (f x).
+Proof using Type*.
+  rewrite !cmra_valid_validN. eauto using morph_validN.
+Qed.
+End morph.
+
+Record morph (A B : cmra) := Morph {
+  morph_car :> A → B;
+  #[global] morph_morphism :: Morphism morph_car;
+}.
+Global Arguments Morph {_ _} _ {_}.
+Global Arguments morph_car {_ _} _ _.
+
+Section morph_ofe.
+Context {A B : cmra}.
+
+Local Instance morph_equiv_instance : Equiv (morph A B) := λ f g,
+  ∀ n x, ✓{n} x → f x ≡{n}≡ g x.
+Local Instance morph_dist_instance : Dist (morph A B) := λ n f g,
+  ∀ m x, m ≤ n → ✓{m} x → f x ≡{m}≡ g x.
+
+Lemma morph_ofe_mixin : OfeMixin (morph A B).
+Proof.
+  split.
+  - intros f g; split.
+    + intros H n m x _.
+      apply H.
+    + intros H n x.
+      by apply (H n).
+  - intros n; split.
+    + by intros f m x _ _.
+    + intros f g H m x Hm Hx.
+      symmetry.
+      by apply H.
+    + intros f g h H1 H2 m x Hm Hx.
+      by trans (g x); revert m x Hm Hx.
+  - intros n1 n2 f g H Hn12 n3 x Hn23.
+    apply H. lia.
+Qed.
+Canonical Structure morphO := Ofe (morph A B) morph_ofe_mixin.
+End morph_ofe.
+Global Arguments morphO : clear implicits.
+Notation "A -r> B" := (morphO A B) (at level 99, B at level 200, right associativity).
+
+Record umorph (A B : ucmra) := UMorph {
+  umorph_car :> A → B;
+  #[global] umorph_morphism :: Morphism umorph_car;
+  #[global] umorph_unit :: PerservesUnit umorph_car;
+}.
+Global Arguments UMorph {_ _} _ {_ _}.
+Global Arguments umorph_car {_ _} _ _.
+
+Section umorph_ofe.
+Context {A B : ucmra}.
+
+Canonical Structure umorph_morph (f : umorph A B) := Morph (umorph_car f).
+
+Local Instance umorph_equiv_instance : Equiv (umorph A B) := λ f g,
+  ∀ n x, ✓{n} x → f x ≡{n}≡ g x.
+Local Instance umorph_dist_instance : Dist (umorph A B) := λ n f g,
+  ∀ m x, m ≤ n → ✓{m} x → f x ≡{m}≡ g x.
+
+Lemma umorph_ofe_mixin : OfeMixin (umorph A B).
+Proof.
+  split.
+  - intros f g; split.
+    + intros H n m x _.
+      apply H.
+    + intros H n x.
+      by apply (H n).
+  - intros n; split.
+    + by intros f m x _ _.
+    + intros f g H m x Hm Hx.
+      symmetry.
+      by apply H.
+    + intros f g h H1 H2 m x Hm Hx.
+      by trans (g x); revert m x Hm Hx.
+  - intros n1 n2 f g H Hn12 n3 x Hn23.
+    apply H. lia.
+Qed.
+Canonical Structure umorphO := Ofe (umorph A B) umorph_ofe_mixin.
+
+Global Instance umorph_morph_ne : NonExpansive umorph_morph.
+Proof. by intros n f g. Qed.
+Global Instance umorph_morph_proper : Proper ((≡) ==> (≡)) umorph_morph.
+Proof. apply ne_proper, _. Qed.
+End umorph_ofe.
+Global Arguments umorphO : clear implicits.
+Notation "A -ur> B" := (umorphO A B) (at level 99, B at level 200, right associativity).
+
+(** Category *)
+Global Instance id_morph {A : cmra} : Morphism (@id A).
+Proof. split=>//. apply _. Qed.
+Global Instance id_umorph {A : ucmra} : PerservesUnit (@id A).
+Proof. by red. Qed.
+Global Instance comp_morph {A B C : cmra} (f : B → C) (g : A → B) : Morphism f → Morphism g → Morphism (f ∘ g).
+Proof.
+  split=>/=.
+  - apply _.
+  - intros n x Hx.
+    by do 2 apply (morph_validN _).
+  - intros x y.
+    by rewrite !morph_op.
+Qed.
+Global Instance ucomp_morph {A B C : ucmra} (f : B → C) (g : A → B) : Morphism f → PerservesUnit f → PerservesUnit g → PerservesUnit (f ∘ g).
+Proof.
+  intros ???; red=>/=.
+  by rewrite !morph_unit.
+Qed.
+
+Canonical idM {A : cmra} := Morph (@id A).
+Canonical idUM {A : ucmra} := UMorph (@id A).
+Canonical compM {A B C} (f : B -r> C) (g : A -r> B) := Morph (f ∘ g).
+Canonical compUM {A B C} (f : B -ur> C) (g : A -ur> B) := UMorph (f ∘ g).
+Infix "®" := compM (at level 40, left associativity).
+Infix "○" := compUM (at level 40, left associativity).
+
+Global Instance compM_ne {A B C} : NonExpansive2 (@compM A B C).
+Proof.
+  intros n f1 f2 Hf g1 g2 Hg m x Hm Hx=>/=.
+  trans (f2 (g1 x)).
+  - by apply Hf, (morph_validN g1).
+  - f_equiv. by apply Hg.
+Qed.
+Global Instance compM_proper {A B C} : Proper ((≡) ==> (≡) ==> (≡)) (@compM A B C).
+Proof. apply ne_proper_2, _. Qed.
+
+Global Instance compUM_ne {A B C} : NonExpansive2 (@compUM A B C).
+Proof. exact compM_ne. Qed.
+Global Instance compUM_proper {A B C} : Proper ((≡) ==> (≡) ==> (≡)) (@compUM A B C).
+Proof. apply ne_proper_2, _. Qed.
+
+Lemma compM_idM_l {A B : cmra} (f : A -r> B) : idM ® f ≡ f.
+Proof. by intros n x. Qed.
+
+Lemma compM_idM_r {A B : cmra} (f : A -r> B) : f ® idM ≡ f.
+Proof. by intros n x. Qed.
+
+Lemma compM_assoc {A B C D : cmra} (f : C -r> D)  (g : B -r> C) (h : A -r> B) : f ® (g ® h) ≡ (f ® g) ® h.
+Proof. by intros n x. Qed.
+
+Lemma compUM_idUM_l {A B : ucmra} (f : A -ur> B) : idUM ○ f ≡ f.
+Proof. by intros n x. Qed.
+
+Lemma compUM_idUM_r {A B : ucmra} (f : A -ur> B) : f ○ idUM ≡ f.
+Proof. by intros n x. Qed.
+
+Lemma compUM_assoc {A B C D : ucmra} (f : C -ur> D)  (g : B -ur> C) (h : A -ur> B) : f ○ (g ○ h) ≡ (f ○ g) ○ h.
+Proof. by intros n x. Qed.
+
+Lemma umorph_morph_id {A : ucmra} : umorph_morph idUM ≡ @idM A.
+Proof. done. Qed.
+Lemma umorph_morph_comp {A B C : ucmra} (f : B -ur> C) (g : A -ur> B) : umorph_morph (f ○ g) ≡ umorph_morph f ® umorph_morph g.
+Proof. done. Qed.
+
+(** Terminal *)
+Definition to_unit {A} (_ : A) : () := ().
+Global Instance to_unit_morph {A : cmra} : Morphism (@to_unit A).
+Proof. by split. Qed.
+Global Instance to_unit_umorph {A : ucmra} : PerservesUnit (@to_unit A).
+Proof. done. Qed.
+Canonical to_unitM {A : cmra} := Morph (@to_unit A).
+Canonical to_unitUM {A : ucmra} := UMorph (@to_unit A).
+
+Lemma to_unit_unique {A} (f : A -r> unitR) : to_unitM ≡ f.
+Proof. intros n x _. by destruct (f x). Qed.
+Lemma to_unitU_unique {A} (f : A -ur> unitR) : to_unitUM ≡ f.
+Proof. apply to_unit_unique. Qed.
+
+(** Product *)
+Definition fpair {A B C} (f : A → B) (g : A → C) (x : A) := (f x, g x).
+Global Instance fpair_morph {A B C : cmra} (f : A → B) (g : A → C) : Morphism f → Morphism g → Morphism (fpair f g).
+Proof.
+  intros ??. split.
+  - solve_proper.
+  - intros n x ?; split=>/=; by apply morph_validN.
+  - intros x y; split=>/=; by apply morph_op.
+Qed.
+Global Instance fpair_umorph {A B C : ucmra} (f : A → B) (g : A → C) : PerservesUnit f → PerservesUnit g → PerservesUnit (fpair f g).
+Proof. intros ??. by split. Qed.
+Canonical fpairM {A B C} (f : A -r> B) (g : A -r> C) := Morph (fpair f g).
+Canonical fpairUM {A B C} (f : A -ur> B) (g : A -ur> C) := UMorph (fpair f g).
+
+Global Instance fpairM_ne {A B C} : NonExpansive2 (@fpairM A B C).
+Proof.
+  intros n f1 f2 Hf g1 g2 Hg m x Hm Hx.
+  by split; revert m x Hm Hx.
+Qed.
+Global Instance fpairM_proper {A B C} : Proper ((≡) ==> (≡) ==> (≡)) (@fpairM A B C).
+Proof. apply ne_proper_2, _. Qed.
+Global Instance fpairUM_ne {A B C} : NonExpansive2 (@fpairUM A B C).
+Proof. exact fpairM_ne. Qed.
+Global Instance fpairUM_proper {A B C} : Proper ((≡) ==> (≡) ==> (≡)) (@fpairUM A B C).
+Proof. apply ne_proper_2, _. Qed.
+
+Global Instance fst_morph {A B : cmra} : Morphism (@fst A B).
+Proof.
+  split.
+  - apply _.
+  - by intros n x [? _].
+  - done.
+Qed.
+Global Instance fst_umorph {A B : ucmra} : PerservesUnit (@fst A B).
+Proof. by red. Qed.
+Canonical fstM {A B : cmra} := Morph (@fst A B).
+Canonical fstUM {A B : ucmra} := UMorph (@fst A B).
+
+Global Instance snd_morph {A B : cmra} : Morphism (@snd A B).
+Proof.
+  split.
+  - apply _.
+  - by intros n x [_ ?].
+  - done.
+Qed.
+Global Instance snd_umorph {A B : ucmra} : PerservesUnit (@snd A B).
+Proof. by red. Qed.
+Canonical sndM {A B : cmra} := Morph (@snd A B).
+Canonical sndUM {A B : ucmra} := UMorph (@snd A B).
+
+Lemma fstM_fpairM {A B C} (f : A -r> B) (g : A -r> C) : fstM ® fpairM f g ≡ f.
+Proof. by intros n x. Qed.
+Lemma sndM_fpairM {A B C} (f : A -r> B) (g : A -r> C) : sndM ® fpairM f g ≡ g.
+Proof. by intros n x. Qed.
+Lemma fpairM_eta {A B C} (f : A -r> prodR B C) : f ≡ fpairM (fstM ® f) (sndM ® f).
+Proof. by intros n x. Qed.
+
+Lemma fpairM_umpN {A B C} n (f : A -r> prodR B C) (g : A -r> B) (h : A -r> C) : f ≡{n}≡ fpairM g h ↔ fstM ® f ≡{n}≡ g ∧ sndM ® f ≡{n}≡ h.
+Proof.
+  split.
+  - intros ->; split.
+    + by rewrite fstM_fpairM.
+    + by rewrite sndM_fpairM.
+  - intros [<- <-].
+    by rewrite -fpairM_eta.
+Qed.
+Lemma fpairM_ump {A B C} (f : A -r> prodR B C) (g : A -r> B) (h : A -r> C) : f ≡ fpairM g h ↔ fstM ® f ≡ g ∧ sndM ® f ≡ h.
+Proof.
+  split.
+  - intros ->; split.
+    + apply fstM_fpairM.
+    + apply sndM_fpairM.
+  - intros [<- <-].
+    apply fpairM_eta.
+Qed.
+
+Lemma fstUM_fpairUM {A B C} (f : A -ur> B) (g : A -ur> C) : fstUM ○ fpairUM f g ≡ f.
+Proof. apply fstM_fpairM. Qed.
+Lemma sndUM_fpairUM {A B C} (f : A -ur> B) (g : A -ur> C) : sndUM ○ fpairUM f g ≡ g.
+Proof. apply sndM_fpairM. Qed.
+Lemma fpairUM_eta {A B C} (f : A -ur> prodUR B C) : f ≡ fpairUM (fstUM ○ f) (sndUM ○ f).
+Proof. apply fpairM_eta. Qed.
+
+Lemma fpairUM_umpN {A B C} n (f : A -ur> prodUR B C) (g : A -ur> B) (h : A -ur> C) : f ≡{n}≡ fpairUM g h ↔ fstUM ○ f ≡{n}≡ g ∧ sndUM ○ f ≡{n}≡ h.
+Proof. apply fpairM_umpN. Qed.
+Lemma fpairUM_ump {A B C} (f : A -ur> prodUR B C) (g : A -ur> B) (h : A -ur> C) : f ≡ fpairUM g h ↔ fstUM ○ f ≡ g ∧ sndUM ○ f ≡ h.
+Proof. apply fpairM_ump. Qed.
+
+(** option *)
+Global Instance Some_morph {A : cmra} : Morphism (@Some A).
+Proof. split=>//. apply _. Qed.
+Canonical SomeM {A : cmra} := Morph (@Some A).
+
+Global Instance option_fmap_morph {A B : cmra} (f : A → B) : Morphism f → Morphism (fmap (M:=option) f).
+Proof.
+  intros ?; split.
+  - apply _.
+  - intros n [x|]=>//.
+    apply (morph_validN f).
+  - intros [x|] [y|]=>//=.
+    constructor.
+    apply (morph_op f).
+Qed.
+Global Instance option_fmap_umorph {A B : cmra} (f : A → B) : PerservesUnit (fmap (M:=option) f).
+Proof. by red. Qed.
+Canonical option_fmapM {A B} (f : A -r> B) := Morph (fmap (M:=option) f).
+Canonical option_fmapUM {A B} (f : A -r> B) := UMorph (fmap (M:=option) f).
+
+Lemma option_fmapUM_idM {A} : option_fmapUM (@idM A) ≡ idUM.
+Proof. by intros n [x|]. Qed.
+Lemma option_fmapUM_compUM {A B C} (f : B -r> C) (g : A -r> B) : option_fmapUM (f ® g) ≡ option_fmapUM f ○ option_fmapUM g.
+Proof. by intros n [x|]. Qed.
+
+Lemma option_fmapM_SomeM {A B} (f : A -r> B) : umorph_morph (option_fmapUM f) ® SomeM ≡ SomeM ® f.
+Proof. by intros n x. Qed.
+
+Definition option_elim {A : ucmra} : option A → A := default ε.
+Global Instance option_elim_morph {A} : Morphism (@option_elim A).
+Proof.
+  split.
+  - solve_proper.
+  - intros n [x|]=>// _.
+    apply ucmra_unit_validN.
+  - intros [x|] [y|]=>//=.
+    + by rewrite right_id.
+    + by rewrite left_id.
+    + by rewrite left_id.
+Qed.
+Global Instance option_elim_umorph {A} : PerservesUnit (@option_elim A).
+Proof. by red. Qed.
+Canonical option_elimM {A} := Morph (@option_elim A).
+Canonical option_elimUM {A} := UMorph (@option_elim A).
+
+Lemma option_elim_fmap {A B} (f : A -ur> B) : option_elimUM ○ option_fmapUM (umorph_morph f) ≡ f ○ option_elimUM.
+Proof.
+  intros n [x|]=>//= _.
+  by rewrite morph_unit.
+Qed.
+
+Lemma option_elim_Some {A : cmra} : option_elimUM ○ option_fmapUM SomeM ≡ @idUM (optionUR A).
+Proof. by intros n [x|]. Qed.
+Lemma Some_option_elim {A : ucmra} : umorph_morph option_elimUM ® SomeM ≡ @idM A.
+Proof. by intros n x. Qed.
+
+(** Direct Sum *)
+Record dsum {A} `{!EqDecision A} (B : A → Type) := {
+  #[local] dsum_car a :> option (B a);
+  dsum_support : list A;
+  dsum_support_strict a : a ∈ dsum_support ↔ is_Some (dsum_car a);
+  dsum_support_inhab : ∃ a, a ∈ dsum_support;
+  dsum_support_no_dup : NoDup dsum_support;
+}.
+Global Arguments dsum_car {_ _ _} _ _.
+Global Arguments dsum_support {_ _ _} _.
+Global Arguments dsum_support_strict {_ _ _} _ _.
+Global Arguments dsum_support_inhab {_ _ _} _.
+Global Arguments dsum_support_no_dup {_ _ _} _.
+
+Section dsum.
+Context {A} `{!EqDecision A} {B : A → Type}.
+
+Program Definition DSum (a : A) (b : B a) := {|
+  dsum_car a' :=
+    match decide (a = a') return option (B a') with
+    | left e => Some match e in _ = a return B a with eq_refl => b end
+    | right _ => None
+    end;
+  dsum_support := [a];
+|}.
+Next Obligation.
+  intros a b a'.
+  rewrite elem_of_list_singleton.
+  split.
+  - intros <-.
+    by rewrite decide_True_pi.
+  - intros [x ?].
+    by destruct decide.
+Qed.
+Next Obligation.
+  intros a b.
+  exists a.
+  by apply elem_of_list_singleton.
+Qed.
+Next Obligation.
+  intros a b.
+  apply NoDup_singleton.
+Qed.
+
+Global Instance dsum_elem_of : ElemOf A (dsum B) := λ a f, a ∈ dsum_support f.
+
+Lemma elem_of_dsum a (f : dsum B) : a ∈ f ↔ is_Some (f a).
+Proof. apply dsum_support_strict. Qed.
+
+Lemma elem_of_DSum a a' (b : B a') : a ∈ DSum a' b ↔ a = a'.
+Proof. apply elem_of_list_singleton. Qed.
+End dsum.
+
+Section dsum_cmra.
+Context {A} `{!EqDecision A} {B : A → cmra}.
+
+Local Instance dsum_dist_instance : Dist (dsum B) := λ n f g,
+  ∀ a, f a ≡{n}≡ g a.
+Local Instance dsum_equiv_instance : Equiv (dsum B) := λ f g,
+  ∀ a, f a ≡ g a.
+
+Lemma dsum_ofe_mixin : OfeMixin (dsum B).
+Proof.
+  split.
+  - intros f g; split.
+    + intros H n a.
+      apply equiv_dist, H.
+    + intros H a.
+      apply equiv_dist=> n.
+      apply H.
+  - intros n; split.
+    + by intros f a.
+    + by intros f g H a.
+    + intros f g h ?? a.
+      by trans (g a).
+  - intros n m f g H Hm a.
+    eapply dist_lt, Hm.
+    apply H.
+Qed.
+Canonical Structure dsumO := Ofe (dsum B) dsum_ofe_mixin.
+
+Global Instance dsum_elem_of_ne n a : Proper (dist (A:=dsumO) n ==> iff) (a ∈.).
+Proof.
+  intros f g H.
+  by rewrite !elem_of_dsum (H a).
+Qed.
+Global Instance dsum_elem_of_proper a : Proper (equiv (A:=dsumO) ==> iff) (a ∈.).
+Proof.
+  intros f g H.
+  by rewrite !elem_of_dsum (H a).
+Qed.
+
+Local Instance dsum_validN_instance : ValidN (dsum B) := λ n f,
+  ∀ a, ✓{n} f a.
+Local Instance dsum_valid_instance : Valid (dsum B) := λ f,
+  ∀ a, ✓ f a.
+
+Local Program Instance dsum_op_instance : Op (dsum B) := λ f g, {|
+  dsum_car a := f a ⋅ g a;
+  dsum_support := list_union (dsum_support f) (dsum_support g);
+|}.
+Next Obligation.
+  intros f g a.
+  rewrite elem_of_list_union !dsum_support_strict.
+  destruct (f a), (g a); naive_solver.
+Qed.
+Next Obligation.
+  intros f g.
+  destruct (dsum_support_inhab f) as [a H].
+  exists a.
+  rewrite elem_of_list_union.
+  by left.
+Qed.
+Next Obligation.
+  intros f g. apply NoDup_list_union; apply dsum_support_no_dup.
+Qed.
+
+Definition dsum_core_cond (f : dsum B) : Prop :=
+  is_Some (head (filter (λ a, is_Some (core (f a))) (dsum_support f))).
+Global Instance dsum_core_cond_decide (f : dsum B) : Decision (dsum_core_cond f) := _.
+Global Instance dsum_core_cond_proof_irrel (f : dsum B) : ProofIrrel (dsum_core_cond f) := _.
+
+Lemma dsum_core_cond_alt (f : dsum B) : dsum_core_cond f ↔ ∃ a, is_Some (core (f a)).
+Proof.
+  rewrite /dsum_core_cond head_is_Some.
+  trans (∃ a, a ∈ filter (λ a : A, is_Some (core (f a))) (dsum_support f)).
+  {
+    destruct filter; split=>//.
+    - intros [? []%elem_of_nil].
+    - intros _. exists a. by left.
+  }
+  f_equiv=> a.
+  rewrite elem_of_list_filter dsum_support_strict.
+  destruct (f a); naive_solver.
+Qed.
+
+Program Definition dsum_core (f : dsum B) (Hf : dsum_core_cond f) : dsum B := {|
+  dsum_car a := core (f a);
+  dsum_support := filter (λ a, is_Some (core (f a))) (dsum_support f);
+|}.
+Next Obligation.
+  intros f Hf a.
+  rewrite elem_of_list_filter dsum_support_strict.
+  destruct (f a); naive_solver.
+Qed.
+Next Obligation.
+  intros f (a & ? & ?)%dsum_core_cond_alt.
+  exists a.
+  rewrite elem_of_list_filter dsum_support_strict.
+  destruct (f a); naive_solver.
+Qed.
+Next Obligation.
+  intros f _. apply NoDup_filter, dsum_support_no_dup.
+Qed.
+
+Local Instance dsum_pcore_instance : PCore (dsum B) := λ f,
+  match (decide (dsum_core_cond f)) with
+  | left Hf => Some $ dsum_core f Hf
+  | right _ => None
+  end.
+
+Lemma dsum_pcore_Some (f cf : dsum B) : pcore f = Some cf ↔ ∃ Hf, dsum_core f Hf = cf.
+Proof.
+  rewrite /pcore /dsum_pcore_instance.
+  destruct decide as [Hf|Hf]; split.
+  - intros [= <-].
+    by exists Hf.
+  - intros [Hf' <-].
+    do 2 f_equal.
+    apply proof_irrel.
+  - done.
+  - by intros [? _].
+Qed.
+
+Lemma dsum_includedN_1 n (f g : dsum B) a : f ≼{n} g → f a ≼{n} g a.
+Proof.
+  intros [h H].
+  by exists (h a).
+Qed.
+
+Lemma dsum_cmra_mixin : CmraMixin (dsum B).
+Proof.
+  split.
+  - intros f n g1 g2 Hg a=>/=.
+    f_equiv. apply Hg.
+  - intros n f g _ H [Hf <-]%dsum_pcore_Some.
+    assert (dsum_core_cond g) as Hg.
+    {
+      rewrite !dsum_core_cond_alt in Hf |- *.
+      destruct Hf as [a Hf].
+      exists a.
+      by rewrite -(H a).
+    }
+    exists (dsum_core g Hg); split.
+    { apply dsum_pcore_Some. by exists Hg. }
+    intros a=>/=.
+    f_equiv.
+    apply H.
+  - intros n f g H Hf a.
+    by rewrite -(H a).
+  - intros f; split.
+    + intros H n a.
+      apply cmra_valid_validN, H.
+    + intros H a.
+      apply cmra_valid_validN=> n.
+      apply H.
+  - intros n f Hf a.
+    apply cmra_validN_S, Hf.
+  - intros f g h a=>/=.
+    apply assoc, _.
+  - intros f g a=>/=.
+    apply comm, _.
+  - intros f _ [Hf <-]%dsum_pcore_Some a=>/=.
+    apply cmra_core_l.
+  - intros f _ [Hf <-]%dsum_pcore_Some.
+    assert (dsum_core_cond (dsum_core f Hf)) as Hcf.
+    {
+      rewrite /dsum_core_cond list_filter_filter_r //=.
+      intros x ?.
+      by rewrite cmra_core_idemp.
+    }
+    rewrite /pcore /dsum_pcore_instance.
+    rewrite decide_True_pi.
+    constructor=> a /=.
+    apply cmra_core_idemp.
+  - intros f g _ [h H] [Hf <-]%dsum_pcore_Some.
+    assert (dsum_core_cond g) as Hg.
+    {
+      rewrite !dsum_core_cond_alt in Hf |- *.
+      destruct Hf as (a & cx & Hf).
+      exists a.
+      rewrite (H a) /=.
+      destruct (f a) as [x|] eqn:Hx=>//.
+      rewrite /core /= in Hf.
+      destruct (h a) as [y|]=>//.
+      rewrite /core /=.
+      by destruct (cmra_pcore_mono x (x ⋅ y) cx) as (? & -> & _).
+    }
+    exists (dsum_core g Hg); split.
+    { apply dsum_pcore_Some. by exists Hg. }
+    exists (dsum_core g Hg)=> a /=.
+    destruct (cmra_core_mono (f a) (g a)) as [y Hc].
+    { exists (h a). apply H. }
+    by rewrite Hc assoc -cmra_core_dup.
+  - intros n f g H a.
+    eapply cmra_validN_op_l, H.
+  - intros n f g1 g2 Hf H.
+    pose proof (E := λ a, cmra_extend n (f a) (g1 a) (g2 a) (Hf a) (H a)).
+    clear -E.
+    set (h1 := λ a, projT1 (E a)).
+    set (h2 := λ a, proj1_sig $ projT2 (E a)).
+    assert (∀ a, f a ≡ h1 a ⋅ h2 a) as Hf.
+    { intros a. apply (proj2_sig $ projT2 (E a)). }
+    assert (∀ a, h1 a ≡{n}≡ g1 a) as H1.
+    { intros a. apply (proj2_sig $ projT2 (E a)). }
+    assert (∀ a, h2 a ≡{n}≡ g2 a) as H2.
+    { intros a. apply (proj2_sig $ projT2 (E a)). }
+    clearbody h1 h2; clear E.
+    assert (∀ a, a ∈ dsum_support g1 ↔ is_Some (h1 a)) as Hh1.
+    {
+      intros a.
+      by rewrite dsum_support_strict H1.
+    }
+    assert (∀ a, a ∈ dsum_support g2 ↔ is_Some (h2 a)) as Hh2.
+    {
+      intros a.
+      by rewrite dsum_support_strict H2.
+    }
+    by exists {|
+      dsum_car := h1;
+      dsum_support := dsum_support g1;
+      dsum_support_strict := Hh1;
+      dsum_support_inhab := dsum_support_inhab g1;
+      dsum_support_no_dup := dsum_support_no_dup g1;
+    |}, {|
+      dsum_car := h2;
+      dsum_support := dsum_support g2;
+      dsum_support_strict := Hh2;
+      dsum_support_inhab := dsum_support_inhab g2;
+      dsum_support_no_dup := dsum_support_no_dup g2;
+    |}.
+  - intros n f Hf.
+    set (λ a, proj1_sig (cmra_maximum_idemp_total n (f a) (Hf a))) as g.
+    assert (∀ a, g a ≼{n} f a) as Hgf.
+    { intros a. apply (proj2_sig (cmra_maximum_idemp_total n (f a) (Hf a))). }
+    assert (∀ a, g a ⋅ g a ≡{n}≡ g a) as Hg.
+    { intros a. apply (proj2_sig (cmra_maximum_idemp_total n (f a) (Hf a))). }
+    assert (∀ m a my, ✓{m} my → m ≤ n → my ≼{m} f a → my ⋅ my ≡{m}≡ my → my ≼{m} g a) as H.
+    { intros m a. apply (proj2_sig (cmra_maximum_idemp_total n (f a) (Hf a))). }
+    clearbody g; clear Hf.
+    destruct (decide (Exists (λ a, is_Some (g a)) (dsum_support f))) as [Ha|Ha].
+    + left.
+      assert {g' | dsum_car g' = g} as [g' <-].
+      {
+        unshelve eexists; first exists g (filter (λ a, is_Some (g a)) (dsum_support f)); last done.
+        - intros a.
+          rewrite elem_of_list_filter dsum_support_strict.
+          specialize (Hgf a).
+          apply option_includedN in Hgf as [->|(x & y & -> & -> & _)]=>//.
+          by split=> -[??].
+        - apply Exists_exists in Ha as (a & ? & ?).
+          exists a. by apply elem_of_list_filter.
+        - apply NoDup_filter, dsum_support_no_dup.
+      }
+      exists g'; split_and!.
+      {
+        exists f=> a /=.
+        specialize (Hgf a) as [x ->].
+        by rewrite assoc Hg.
+      }
+      { exact Hg. }
+      intros m h ??? Hh.
+      exists g'=> a /=.
+      specialize (H m a (h a)) as [x ->]=>//.
+      { by apply dsum_includedN_1. }
+      by rewrite assoc -{1}(Hh a).
+    + right.
+      intros m h ?? Hhf Hh.
+      contradict Ha.
+      apply Exists_exists.
+      destruct (dsum_support_inhab h) as [a [x Ha]%dsum_support_strict].
+      exists a; split.
+      * apply dsum_support_strict.
+        destruct Hhf as [i Hi].
+        rewrite (Hi a) /= Ha.
+        by destruct (i a).
+      * assert (h a ≼{m} g a) as [Ha'|(_ & y & _ & ? & _)]%option_includedN=>//.
+        {
+          apply H=>//.
+          by apply dsum_includedN_1.
+        }
+        by rewrite Ha in Ha'.
+Qed.
+Canonical dsumR := Cmra (dsum B) dsum_cmra_mixin.
+
+Lemma elem_of_dsum_op a (f g : dsum B) : a ∈ f ⋅ g ↔ a ∈ f ∨ a ∈ g.
+Proof. apply elem_of_list_union. Qed.
+
+Global Instance DSum_morph a : Morphism (DSum a).
+Proof.
+  split.
+  - solve_proper.
+  - intros n b Hb a'=>/=.
+    by destruct decide as [<- |?].
+  - intros b1 b2 a'=>/=.
+    by destruct decide as [<- |?].
+Qed.
+
+Canonical Structure DSumM a := Morph (DSum a).
+
+Program Definition dsum_fold' {C : cmra} (f : ∀ a, B a → C) (g : dsum B) : option C :=
+  [^ op list] a ∈ dsum_support g, f a <$> (g a).
+
+Lemma dsum_fold'_is_Some {C : cmra} (f : ∀ a, B a → C) (g : dsum B) : is_Some (dsum_fold' f g).
+Proof.
+  rewrite /dsum_fold'.
+  destruct (dsum_support_inhab g) as [a Ha].
+  destruct (elem_of_list_split _ _ Ha) as (l1 & l2 & ->).
+  rewrite big_opL_app big_opL_cons.
+  apply dsum_support_strict in Ha as [x ->].
+  by rewrite /= assoc (comm _ _ (Some _)) -assoc Some_op_opM.
+Qed.
+
+Definition dsum_fold {C : cmra} (f : ∀ a, B a → C) (g : dsum B) :=
+  is_Some_proj (dsum_fold'_is_Some f g).
+
+Lemma dsum_fold_eq {C : cmra} (f : ∀ a, B a → C) (g : dsum B) (y : C) :
+  dsum_fold f g = y ↔ ([^ op list] a ∈ dsum_support g, f a <$> (g a)) = Some y.
+Proof.
+  rewrite /dsum_fold /is_Some_proj.
+  generalize (dsum_fold'_is_Some f g)=> H.
+  rewrite -/(dsum_fold' f g).
+  destruct dsum_fold'.
+  - split.
+    + apply f_equal.
+    + by injection 1.
+  - by destruct H.
+Qed.
+
+Lemma Some_dsum_fold {C : cmra} (f : ∀ a, B a → C) (g : dsum B) :
+  Some (dsum_fold f g) = [^ op list] a ∈ dsum_support g, f a <$> (g a).
+Proof. symmetry. by apply dsum_fold_eq. Qed.
+
+Lemma dsum_fold_DSum {C : cmra} (f : ∀ a, B a → C) a (b : B a) :
+  dsum_fold f (DSum a b) = f a b.
+Proof.
+  apply dsum_fold_eq=>/=.
+  by rewrite decide_True_pi.
+Qed.
+
+Lemma dsum_fold_op {C : cmra} (f : ∀ a, B a → C) (g1 g2 : dsum B) :
+  (∀ a, Morphism (f a)) →
+  dsum_fold f (g1 ⋅ g2) ≡ dsum_fold f g1 ⋅ dsum_fold f g2.
+Proof.
+  intros Hf.
+  apply (inj Some).
+  rewrite Some_op !Some_dsum_fold.
+  trans (
+    ([^op list] a ∈ dsum_support (g1 ⋅ g2), fmap (M:=option) (f a) $ g1 a) ⋅
+    ([^op list] a ∈ dsum_support (g1 ⋅ g2), f a <$> g2 a)
+  ).
+  {
+    rewrite -big_opL_op.
+    f_equiv=> _ a /=.
+    destruct (g1 a) as [x|], (g2 a) as [y|]=>//=.
+    constructor.
+    apply morph_op, _.
+  }
+  f_equiv.
+  - rewrite /= list_union_comm; [|apply dsum_support_no_dup..].
+    rewrite /list_union big_opL_app.
+    rewrite (big_opL_proper _ (λ _ _, ε)); first last.
+    {
+      intros k x H%elem_of_list_lookup_2.
+      rewrite elem_of_list_difference !dsum_support_strict -eq_None_not_Some in H.
+      by destruct H as [_ ->].
+    }
+    by rewrite big_opL_unit left_id.
+  - rewrite /= /list_union big_opL_app.
+    rewrite (big_opL_proper _ (λ _ _, ε)); first last.
+    {
+      intros k x H%elem_of_list_lookup_2.
+      rewrite elem_of_list_difference !dsum_support_strict -eq_None_not_Some in H.
+      by destruct H as [_ ->].
+    }
+    by rewrite big_opL_unit left_id.
+Qed.
+
+Global Instance dsum_fold_ne {C : cmra} (f : ∀ a, B a → C) : (∀ a, NonExpansive (f a)) → NonExpansive (dsum_fold f).
+Proof.
+  intros Hf n g1 g2 Hg.
+  apply (inj Some).
+  rewrite !Some_dsum_fold.
+  assert (dsum_support g1 ≡ₚ dsum_support g2) as <-.
+  {
+    apply NoDup_Permutation.
+    - apply dsum_support_no_dup.
+    - apply dsum_support_no_dup.
+    - intros a.
+      by rewrite !dsum_support_strict (Hg a).
+  }
+  f_equiv=> _ a.
+  by rewrite (Hg a).
+Qed.
+
+Global Instance dsum_fold_proper {C : cmra} (f : ∀ a, B a → C) : (∀ a, Proper ((≡) ==> (≡)) (f a)) → Proper ((≡) ==> (≡)) (dsum_fold f).
+Proof.
+  intros Hf g1 g2 Hg.
+  apply (inj Some).
+  rewrite !Some_dsum_fold.
+  assert (dsum_support g1 ≡ₚ dsum_support g2) as <-.
+  {
+    apply NoDup_Permutation.
+    - apply dsum_support_no_dup.
+    - apply dsum_support_no_dup.
+    - intros a.
+      by rewrite !dsum_support_strict (Hg a).
+  }
+  f_equiv=> _ a.
+  by rewrite (Hg a).
+Qed.
+
+End dsum_cmra.
+Global Arguments dsumO {_} _.
+Global Arguments dsumR {_} _.
+
+(** Coproduct *)
+Record coProd {A} `{!EqDecision A} (B : A → Type) := CoProd' { coProd_car : dsum B }.
+Add Printing Constructor coProd.
+Global Arguments CoProd' {_ _ _} _.
+Global Arguments coProd_car {_ _ _} _.
+
+Definition CoProd {A} `{!EqDecision A} {B : A → Type} (a : A) (b : B a) :=
+  CoProd' (DSum a b).
+
+Section coProd_cmra.
+Context {A} `{!EqDecision A} {B : A → cmra}.
+
+Local Instance coProd_dist_instance : Dist (coProd B) := λ n f g,
+  coProd_car f ≡{n}≡ coProd_car g.
+Local Instance coProd_equiv_instance : Equiv (coProd B) := λ f g,
+  coProd_car f ≡ coProd_car g.
+
+Lemma coProd_ofe_mixin : OfeMixin (coProd B).
+Proof. by apply (iso_ofe_mixin coProd_car). Qed.
+Canonical Structure coProdO := Ofe (coProd B) coProd_ofe_mixin.
+
+Global Instance coProd_car_ne : NonExpansive (coProd_car (B:=B)).
+Proof. by intros n f g. Qed.
+Global Instance coProd_car_proper : Proper ((≡) ==> (≡)) (coProd_car (B:=B)).
+Proof. apply ne_proper, _. Qed.
+Global Instance CoProd'_ne : NonExpansive (CoProd' (B:=B)).
+Proof. by intros n f g. Qed.
+Global Instance CoProd'_proper : Proper ((≡) ==> (≡)) (CoProd' (B:=B)).
+Proof. apply ne_proper, _. Qed.
+
+Local Instance coProd_validN_instance : ValidN (coProd B) := λ n f,
+  (∀ a1 a2, a1 ∈ coProd_car f → a2 ∈ coProd_car f → a1 = a2) ∧ ✓{n} coProd_car f.
+Local Instance coProd_valid_instance : Valid (coProd B) := λ f,
+  (∀ a1 a2, a1 ∈ coProd_car f → a2 ∈ coProd_car f → a1 = a2) ∧ ✓ coProd_car f.
+
+Local Program Instance coProd_op_instance : Op (coProd B) := λ f g,
+  CoProd' (coProd_car f ⋅ coProd_car g).
+
+Local Instance coProd_pcore_instance : PCore (coProd B) := λ f,
+  CoProd' <$> pcore (coProd_car f).
+
+Lemma coProd_cmra_mixin : CmraMixin (coProd B).
+Proof.
+  apply (iso_cmra_mixin_restrict_validity CoProd' coProd_car)=>//.
+  - intros f.
+    rewrite {2}/pcore /coProd_pcore_instance.
+    by destruct pcore.
+  - by intros n f [_ ?].
+  - intros n f g H [Hf1 Hf].
+    split.
+    + intros a1 a2. rewrite -H. apply Hf1.
+    + by rewrite -H.
+  - intros f; split.
+    + intros [Hf1 Hf] n; split=>//.
+      by apply cmra_valid_validN.
+    + intros Hf; split.
+      * apply (Hf 0).
+      * apply cmra_valid_validN, Hf.
+  - intros n f [? Hf]; split=>//.
+    by apply cmra_validN_S.
+  - intros n f g [H Hfg]; split.
+    + intros a1 a2 H1 H2.
+      by apply H; rewrite elem_of_dsum_op; left.
+    + eapply cmra_validN_op_l, Hfg.
+Qed.
+Canonical coProdR := Cmra (coProd B) coProd_cmra_mixin.
+
+Global Instance CoProd_morph a : Morphism (CoProd a).
+Proof.
+  split.
+  - solve_proper.
+  - intros n b Hb.
+    split=>/=.
+    + by intros a1 a2 ->%elem_of_DSum ->%elem_of_DSum.
+    + by apply (morph_validN _).
+  - intros b1 b2.
+    do 5 red. simpl.
+    apply morph_op, _.
+Qed.
+
+Canonical Structure CoProdM a := Morph (CoProd a).
+
+Lemma coProd_validN n (f : coProd B) : ✓{n} f ↔ ∃ a b, f ≡ CoProd a b ∧ ✓{n} b.
+Proof.
+  split.
+  - intros [H Hf].
+    destruct (dsum_support_inhab (coProd_car f)) as [a Ha].
+    assert (is_Some (coProd_car f a)) as [b Hb].
+    { by rewrite -dsum_support_strict. }
+    exists a, b.
+    split.
+    + intros a' =>/=.
+      destruct (coProd_car f a') as [b'|] eqn: Hb'.
+      * assert (a = a') as <-.
+        { apply H; apply dsum_support_strict; by eexists. }
+        rewrite decide_True_pi.
+        by rewrite -Hb -Hb'.
+      * enough (a ≠ a') as ne.
+        { by destruct decide. }
+        intros <-.
+        by rewrite Hb in Hb'.
+    + specialize (Hf a).
+      by rewrite Hb in Hf.
+  - intros (a & b & -> & Hb).
+    by apply (morph_validN _).
+Qed.
+Lemma coProd_valid (f : coProd B) : ✓ f ↔ ∃ a b, f ≡ CoProd a b ∧ ✓ b.
+Proof.
+  split.
+  - intros [H Hf].
+    destruct (dsum_support_inhab (coProd_car f)) as [a Ha].
+    assert (is_Some (coProd_car f a)) as [b Hb].
+    { by rewrite -dsum_support_strict. }
+    exists a, b.
+    split.
+    + intros a' =>/=.
+      destruct (coProd_car f a') as [b'|] eqn: Hb'.
+      * assert (a = a') as <-.
+        { apply H; apply dsum_support_strict; by eexists. }
+        rewrite decide_True_pi.
+        by rewrite -Hb -Hb'.
+      * enough (a ≠ a') as ne.
+        { by destruct decide. }
+        intros <-.
+        by rewrite Hb in Hb'.
+    + specialize (Hf a).
+      by rewrite Hb in Hf.
+  - intros (a & b & -> & Hb).
+    by apply (morph_valid _).
+Qed.
+
+End coProd_cmra.
+Global Arguments coProdO {_ _} _.
+Global Arguments coProdR {_ _} _.
+
+Definition fmatch {A} `{!EqDecision A} {B : A → cmra} {C : cmra} (f : ∀ a, B a → C) (g : coProd B) : C :=
+  dsum_fold f (coProd_car g).
+Global Instance fmatch_morph {A} `{!EqDecision A} {B : A → cmra} {C : cmra} (f : ∀ a, B a → C) : (∀ a, Morphism (f a)) → Morphism (fmatch f).
+Proof.
+  intros Hf.
+  assert (NonExpansive (fmatch f)) by solve_proper.
+  assert (Proper ((≡) ==> (≡)) (fmatch f)) by apply ne_proper, _.
+  split=>//.
+  - intros n g (a & b & -> & ?)%coProd_validN.
+    rewrite /fmatch /= dsum_fold_DSum.
+    by apply (morph_validN _).
+  - intros g1 g2.
+    rewrite /fmatch /=.
+    apply dsum_fold_op, _.
+Qed.
+Canonical fmatchM {A} `{!EqDecision A} {B : A → cmra} {C : cmra} (f : ∀ a, B a -r> C) := Morph (fmatch f).
+
+Lemma fmatch_CoProd {A} `{!EqDecision A} {B : A → cmra} {C : cmra} (f : ∀ a, B a -r> C) a : fmatchM f ® CoProdM a ≡ f a.
+Proof.
+  intros n b _.
+  by rewrite /= /fmatch /= dsum_fold_DSum.
+Qed.
+
+Lemma fmatch_umpN {A} `{!EqDecision A} {B : A → cmra} {C : cmra} n (f : coProdR B -r> C) (g : ∀ a, B a -r> C) : f ≡{n}≡ fmatchM g ↔ ∀ a, f ® CoProdM a ≡{n}≡ g a.
+Proof.
+  split.
+  - intros ? a; ofe_subst.
+    by rewrite fmatch_CoProd.
+  - intros H m _ ? (a & b & -> & ?)%coProd_validN.
+    setoid_rewrite (fmatch_CoProd g a m b)=>//.
+    by apply H.
+Qed.
+Lemma fmatch_ump {A} `{!EqDecision A} {B : A → cmra} {C : cmra} (f : coProdR B -r> C) (g : ∀ a, B a -r> C) : f ≡ fmatchM g ↔ ∀ a, f ® CoProdM a ≡ g a.
+Proof.
+  split.
+  - intros H a; rewrite H.
+    apply fmatch_CoProd.
+  - intros H n _ (a & b & -> & ?)%coProd_validN.
+    setoid_rewrite (fmatch_CoProd g a n b)=>//.
+    by apply H.
+Qed.