More CMRAs

* Framepreserving updates are now on CMRAs rather than RAs
* Excl and auth are now CMRAs
* Show that excl and auth are functors
* STS is now an CMRA

iris/auth.v

 Require Export iris.excl.
-Local Arguments disjoint _ _ !_ !_ /.
+Local Arguments valid _ _ !_ /.
+Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
 Arguments Auth {_} _ _.
@@ -8,11 +9,54 @@ Arguments own {_} _.
 Notation "∘ x" := (Auth ExclUnit x) (at level 20).
 Notation "∙ x" := (Auth (Excl x) ∅) (at level 20).
 
-Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
-Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x,
-  valid (authoritative x) ∧ excl_above (own x) (authoritative x).
+(* COFE *)
 Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
   authoritative x ≡ authoritative y ∧ own x ≡ own y.
+Instance auth_dist `{Dist A} : Dist (auth A) := λ n x y,
+  authoritative x ={n}= authoritative y ∧ own x ={n}= own y.
+
+Instance Auth_ne `{Dist A} : Proper (dist n ==> dist n ==> dist n) (@Auth A).
+Proof. by split. Qed.
+Instance authoritative_ne `{Dist A} :
+  Proper (dist n ==> dist n) (@authoritative A).
+Proof. by destruct 1. Qed.
+Instance own_ne `{Dist A} : Proper (dist n ==> dist n) (@own A).
+Proof. by destruct 1. Qed.
+
+Instance auth_compl `{Cofe A} : Compl (auth A) := λ c,
+  Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
+
+Local Instance auth_cofe `{Cofe A} : Cofe (auth A).
+Proof.
+  split.
+  * intros x y; unfold dist, auth_dist, equiv, auth_equiv.
+    rewrite !equiv_dist; naive_solver.
+  * intros n; split.
+    + by intros ?; split.
+    + by intros ?? [??]; split; symmetry.
+    + intros ??? [??] [??]; split; etransitivity; eauto.
+  * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
+  * by split.
+  * intros c n; split. apply (conv_compl (chain_map authoritative c) n).
+    apply (conv_compl (chain_map own c) n).
+Qed.
+
+(* CMRA *)
+Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
+Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x,
+  match authoritative x with
+  | Excl a => own x ≼ a ∧ valid a
+  | ExclUnit => valid (own x)
+  | ExclBot => False
+  end.
+Arguments auth_valid _ _ _ _ !_ /.
+Instance auth_validN `{Dist A, ValidN A, Op A} : ValidN (auth A) := λ n x,
+  match authoritative x with
+  | Excl a => own x ≼{n} a ∧ validN n a
+  | ExclUnit => validN n (own x)
+  | ExclBot => n = 0
+  end.
+Arguments auth_validN _ _ _ _ _ !_ /.
 Instance auth_unit `{Unit A} : Unit (auth A) := λ x,
   Auth (unit (authoritative x)) (unit (own x)).
 Instance auth_op `{Op A} : Op (auth A) := λ x y,
@@ -25,32 +69,82 @@ Proof.
   split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
   intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
 Qed.
-
-Instance auth_ra `{RA A} : RA (auth A).
+Lemma auth_includedN `{Dist A, Op A} n (x y : auth A) :
+  x ≼{n} y ↔ authoritative x ≼{n} authoritative y ∧ own x ≼{n} own y.
+Proof.
+  split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
+  intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
+Qed.
+Lemma authoritative_validN `{CMRA A} n (x : auth A) :
+  validN n x → validN n (authoritative x).
+Proof. by destruct x as [[]]. Qed.
+Lemma own_validN `{CMRA A} n (x : auth A) : validN n x → validN n (own x).
+Proof. destruct x as [[]]; naive_solver eauto using cmra_valid_includedN. Qed.
+Instance auth_cmra `{CMRA A} : CMRA (auth A).
 Proof.
   split.
-  * split.
-    + by intros ?; split.
-    + by intros ?? [??]; split.
-    + intros ??? [??] [??]; split; etransitivity; eauto.
-  * by intros x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'.
-  * by intros y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'.
-  * by intros y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'.
-  * by intros x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
+  * apply _.
+  * by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'.
+  * by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'.
+  * intros n [x a] [y b] [Hx Ha]; simpl in *;
+      destruct Hx as [[][]| | |]; intros ?; cofe_subst; auto.
+  * by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
       split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'.
+  * by intros [[] ?]; simpl.
+  * intros n [[] ?] ?; naive_solver eauto using cmra_included_S, cmra_valid_S.
+  * destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN,
+      ?cmra_valid_validN; [naive_solver|naive_solver|].
+    split; [done|intros Hn; discriminate (Hn 1)].
   * by split; simpl; rewrite (associative _).
   * by split; simpl; rewrite (commutative _).
   * by split; simpl; rewrite ?(ra_unit_l _).
   * by split; simpl; rewrite ?(ra_unit_idempotent _).
-  * intros ??; rewrite! auth_included; intros [??].
-    by split; simpl; apply ra_unit_preserving.
-  * intros ?? [??]; split; [by apply ra_valid_op_l with (authoritative y)|].
-    by apply excl_above_weaken with (own x ⋅ own y)
-      (authoritative x ⋅ authoritative y); try apply ra_included_l.
-  * by intros ??; rewrite auth_included;
-      intros [??]; split; simpl; apply ra_op_minus.
-Qed.
-Instance auth_ra_empty `{RA A, Empty A, !RAEmpty A} : RAEmpty (auth A).
-Proof. split. done. by intros x; constructor; simpl; rewrite (left_id _ _). Qed.
-Lemma auth_frag_op `{RA A} a b : ∘(a ⋅ b) ≡ ∘a ⋅ ∘b.
-Proof. done. Qed.
\ No newline at end of file
+  * intros n ??; rewrite! auth_includedN; intros [??].
+    by split; simpl; apply cmra_unit_preserving.
+  * assert (∀ n a b1 b2, b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
+    { intros n a b1 b2 <-; apply cmra_included_l. }
+   intros n [[a1| |] b1] [[a2| |] b2];
+     naive_solver eauto using cmra_valid_op_l, cmra_valid_includedN.
+  * by intros n ??; rewrite auth_includedN;
+      intros [??]; split; simpl; apply cmra_op_minus.
+Qed.
+Instance auth_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (auth A).
+Proof.
+  intros n x y1 y2 ? [??]; simpl in *.
+  destruct (cmra_extend_op n (authoritative x) (authoritative y1)
+    (authoritative y2)) as (z1&?&?&?); auto using authoritative_validN.
+  destruct (cmra_extend_op n (own x) (own y1) (own y2))
+    as (z2&?&?&?); auto using own_validN.
+  by exists (Auth (z1.1) (z2.1), Auth (z1.2) (z2.2)).
+Qed.
+Instance auth_ra_empty `{CMRA A, Empty A, !RAEmpty A} : RAEmpty (auth A).
+Proof.
+  split; [apply (ra_empty_valid (A:=A))|].
+  by intros x; constructor; simpl; rewrite (left_id _ _).
+Qed.
+Lemma auth_frag_op `{CMRA A} a b : ∘(a ⋅ b) ≡ ∘a ⋅ ∘b.
+Proof. done. Qed.
+
+(* Functor *)
+Definition authRA (A : cmraT) : cmraT := CMRAT (auth A).
+Instance auth_fmap : FMap auth := λ A B f x,
+  Auth (f <$> authoritative x) (f (own x)).
+Instance auth_fmap_cmra_ne `{Dist A, Dist B} 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].
+Qed.
+Instance auth_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B) :
+  (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone f →
+  CMRAMonotone (fmap f : auth A → auth B).
+Proof.
+  split.
+  * by intros n [x a] [y b]; rewrite !auth_includedN; simpl;
+      intros [??]; split; apply includedN_preserving.
+  * intros n [[a| |] b];
+      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).
+Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.

iris/cmra.v

@@ -7,6 +7,7 @@ Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ={n}= x ⋅
 Notation "x ≼{ n } y" := (includedN n x y)
   (at level 70, format "x  ≼{ n }  y") : C_scope.
 Instance: Params (@includedN) 4.
+Hint Extern 0 (?x ≼{_} ?x) => reflexivity.
 
 Class CMRA A `{Equiv A, Compl A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
   (* setoids *)
@@ -38,6 +39,8 @@ Class CMRAMonotone
   validN_preserving n x : validN n x → validN n (f x)
 }.
 
+Hint Extern 0 (validN 0 _) => apply cmra_valid_0.
+
 (** Bundeled version *)
 Structure cmraT := CMRAT {
   cmra_car :> Type;
@@ -69,6 +72,17 @@ Existing Instances cmra_equiv cmra_dist cmra_compl cmra_unit cmra_op
 Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A.
 Canonical Structure cmra_cofeC.
 
+(** Updates *)
+Definition cmra_updateP `{Op A, ValidN A} (x : A) (P : A → Prop) :=
+  ∀ z n, validN n (x ⋅ z) → ∃ y, P y ∧ validN n (y ⋅ z).
+Instance: Params (@cmra_updateP) 3.
+Infix "⇝:" := cmra_updateP (at level 70).
+Definition cmra_update `{Op A, ValidN A} (x y : A) := ∀ z n,
+  validN n (x ⋅ z) → validN n (y ⋅ z).
+Infix "⇝" := cmra_update (at level 70).
+Instance: Params (@cmra_update) 3.
+
+(** Properties **)
 Section cmra.
 Context `{cmra : CMRA A}.
 Implicit Types x y z : A.
@@ -80,9 +94,9 @@ Proof.
   symmetry; apply cmra_op_minus, Hxy.
 Qed.
 
-Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (validN n).
+Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (validN n) | 1.
 Proof. by split; apply cmra_valid_ne. Qed.
-Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (validN n).
+Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (validN n) | 1.
 Proof. by intros n x1 x2 Hx; apply cmra_valid_ne', equiv_dist. Qed.
 Global Instance cmra_ra : RA A.
 Proof.
@@ -118,12 +132,13 @@ Qed.
 
 (** * Included *)
 Global Instance cmra_included_ne n :
-  Proper (dist n ==> dist n ==> iff) (includedN n).
+  Proper (dist n ==> dist n ==> iff) (includedN n) | 1.
 Proof.
   intros x x' Hx y y' Hy; unfold includedN.
   by setoid_rewrite Hx; setoid_rewrite Hy.
 Qed.
-Global Instance cmra_included_proper:Proper ((≡) ==> (≡) ==> iff) (includedN n).
+Global Instance cmra_included_proper : 
+  Proper ((≡) ==> (≡) ==> iff) (includedN n) | 1.
 Proof.
   intros n x x' Hx y y' Hy; unfold includedN.
   by setoid_rewrite Hx; setoid_rewrite Hy.
@@ -154,6 +169,16 @@ Proof.
   intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using ra_included_l.
   by rewrite Hx1, Hx2.
 Qed.
+
+(** * Properties of [(⇝)] relation *)
+Global Instance cmra_update_preorder : PreOrder cmra_update.
+Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
+Lemma cmra_update_updateP x y : x ⇝ y ↔ x ⇝: (y =).
+Proof.
+  split.
+  * by intros Hx z ?; exists y; split; [done|apply (Hx z)].
+  * by intros Hx z n ?; destruct (Hx z n) as (?&<-&?).
+Qed.
 End cmra.
 
 Instance cmra_monotone_id `{CMRA A} : CMRAMonotone (@id A).
@@ -168,6 +193,7 @@ Proof.
     by intros ? n; apply validN_preserving.
 Qed.
 
+Hint Extern 0 (_ ≼{0} _) => apply cmra_included_0.
 (* Also via [cmra_cofe; cofe_equivalence] *)
 Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances.
 
@@ -197,6 +223,15 @@ Section discrete.
     by exists (x,unit x); simpl; rewrite ra_unit_r.
   Qed.
   Definition discreteRA : cmraT := CMRAT A.
+  Lemma discrete_updateP (x : A) (P : A → Prop) `{!Inhabited (sig P)} :
+    (∀ z, valid (x ⋅ z) → ∃ y, P y ∧ valid (y ⋅ z)) → x ⇝: P.
+  Proof.
+    intros Hvalid z [|n]; [|apply Hvalid].
+    by destruct (_ : Inhabited (sig P)) as [[y ?]]; exists y.
+  Qed.
+  Lemma discrete_update (x y : A) :
+    (∀ z, valid (x ⋅ z) → valid (y ⋅ z)) → x ⇝ y.
+  Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed.
 End discrete.
 Arguments discreteRA _ {_ _ _ _ _ _}.
 

iris/cmra_maps.v

@@ -66,7 +66,7 @@ Proof.
   * by exists (None,Some x); inversion Hx'; repeat constructor.
   * exists (None,None); repeat constructor.
 Qed.
-Instance option_fmap_cmra_preserving `{CMRA A, CMRA B} (f : A → B)
+Instance option_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B)
   `{!CMRAMonotone f} : CMRAMonotone (fmap f : option A → option B).
 Proof.
   split.
@@ -169,7 +169,7 @@ Section map.
     CofeMor (fmap f : mapRA A → mapRA B).
   Global Instance mapRA_map_ne {A B} n :
     Proper (dist n ==> dist n) (@mapRA_map A B) := mapC_map_ne n.
-  Global Instance mapRA_mapcmra_monotone {A B : cmraT} (f : A -n> B)
+  Global Instance mapRA_map_monotone {A B : cmraT} (f : A -n> B)
     `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.
 End map.
 

iris/cofe.v

@@ -97,6 +97,12 @@ Section cofe.
     Proper ((≡) ==> (≡)) f | 100 := _.
 End cofe.
 
+(** Mapping a chain *)
+Program Definition chain_map `{Dist A, Dist B} (f : A → B)
+    `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
+  {| chain_car n := f (c n) |}.
+Next Obligation. by intros A ? B ? f Hf c n i ?; apply Hf, chain_cauchy. Qed.
+
 (** Timeless elements *)
 Class Timeless `{Dist A, Equiv A} (x : A) := timeless y : x ={1}= y → x ≡ y.
 Arguments timeless {_ _ _} _ {_} _ _.
@@ -212,14 +218,12 @@ Proof. by repeat split; try exists 0. Qed.
 (** Product *)
 Instance prod_dist `{Dist A, Dist B} : Dist (A * B) := λ n,
   prod_relation (dist n) (dist n).
-Program Definition fst_chain `{Dist A, Dist B} (c : chain (A * B)) : chain A :=
-  {| chain_car n := fst (c n) |}.
-Next Obligation. by intros A ? B ? c n i ?; apply (chain_cauchy c n). Qed.
-Program Definition snd_chain `{Dist A, Dist B} (c : chain (A * B)) : chain B :=
-  {| chain_car n := snd (c n) |}.
-Next Obligation. by intros A ? B ? c n i ?; apply (chain_cauchy c n). Qed.
+Instance pair_ne `{Dist A, Dist B} :
+  Proper (dist n ==> dist n ==> dist n) (@pair A B) := _.
+Instance fst_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@fst A B) := _.
+Instance snd_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@snd A B) := _.
 Instance prod_compl `{Compl A, Compl B} : Compl (A * B) := λ c,
-  (compl (fst_chain c), compl (snd_chain c)).
+  (compl (chain_map fst c), compl (chain_map snd c)).
 Instance prod_cofe `{Cofe A, Cofe B} : Cofe (A * B).
 Proof.
   split.
@@ -228,8 +232,8 @@ Proof.
   * apply _.
   * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
   * by split.
-  * intros c n; split. apply (conv_compl (fst_chain c) n).
-    apply (conv_compl (snd_chain c) n).
+  * intros c n; split. apply (conv_compl (chain_map fst c) n).
+    apply (conv_compl (chain_map snd c) n).
 Qed.
 Instance pair_timeless `{Dist A, Equiv A, Dist B, Equiv B} (x : A) (y : B) :
   Timeless x → Timeless y → Timeless (x,y).
@@ -245,10 +249,6 @@ Instance prodC_map_ne {A A' B B'} n :
   Proper (dist n ==> dist n ==> dist n) (@prodC_map A A' B B').
 Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
-Instance pair_ne `{Dist A, Dist B} :
-  Proper (dist n ==> dist n ==> dist n) (@pair A B) := _.
-Instance fst_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@fst A B) := _.
-Instance snd_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@snd A B) := _.
 Typeclasses Opaque prod_dist.
 
 (** Discrete cofe *)
@@ -268,11 +268,11 @@ Section discrete_cofe.
   Qed.
   Global Instance discrete_timeless (x : A) : Timeless x.
   Proof. by intros y. Qed.
-  Definition discrete_cofeC : cofeT := CofeT A.
+  Definition discreteC : cofeT := CofeT A.
 End discrete_cofe.
-Arguments discrete_cofeC _ {_ _}.
+Arguments discreteC _ {_ _}.
 
-Definition leibniz_cofeC (A : Type) : cofeT := @discrete_cofeC A equivL _.
+Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
 
 (** Later *)
 Inductive later (A : Type) : Type := Later { later_car : A }.

iris/dra.v

-Require Export iris.ra.
+Require Export iris.ra iris.cmra.
 
 (** From disjoint pcm *)
 Record validity {A} (P : A → Prop) : Type := Validity {
@@ -88,17 +88,20 @@ Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
 Hint Unfold dra_included.
 
 Notation T := (validity (valid : A → Prop)).
+Lemma validity_valid_car_valid (z : T) : V z → V (validity_car z).
+Proof. apply validity_prf. Qed.
+Hint Resolve validity_valid_car_valid.
 Program Instance validity_unit : Unit T := λ x,
   Validity (unit (validity_car x)) (V x) _.
-Next Obligation. by apply dra_unit_valid, validity_prf. Qed.
+Solve Obligations with naive_solver auto using dra_unit_valid.
 Program Instance validity_op : Op T := λ x y,
   Validity (validity_car x ⋅ validity_car y)
            (V x ∧ V y ∧ validity_car x ⊥ validity_car y) _.
-Next Obligation. by apply dra_op_valid; try apply validity_prf. Qed.
+Solve Obligations with naive_solver auto using dra_op_valid.
 Program Instance validity_minus : Minus T := λ x y,
   Validity (validity_car x ⩪ validity_car y)
            (V x ∧ V y ∧ validity_car y ≼ validity_car x) _.
-Next Obligation. by apply dra_minus_valid; try apply validity_prf. Qed.
+Solve Obligations with naive_solver auto using dra_minus_valid.
 Instance validity_ra : RA T.
 Proof.
   split.
@@ -130,10 +133,11 @@ Proof.
   * intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
       intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
 Qed.
-Definition dra_update (x y : T) :
+Definition validityRA : cmraT := discreteRA T.
+Definition validity_update (x y : validityRA) :
   (∀ z, V x → V z → validity_car x ⊥ z → V y ∧ validity_car y ⊥ z) → x ⇝ y.
 Proof.
-  intros Hxy z (?&?&?); split_ands'; auto;
-    eapply Hxy; eauto; by eapply validity_prf.
+  intros Hxy; apply discrete_update.
+  intros z (?&?&?); split_ands'; try eapply Hxy; eauto.
 Qed.
 End dra.

iris/excl.v

 Require Export iris.cmra.
-Local Arguments disjoint _ _ !_ !_ /.
+Local Arguments validN _ _ _ !_ /.
+Local Arguments valid _ _  !_ /.
 
 Inductive excl (A : Type) :=
   | Excl : A → excl A
-  | ExclUnit : Empty (excl A)
+  | ExclUnit : excl A
   | ExclBot : excl A.
 Arguments Excl {_} _.
 Arguments ExclUnit {_}.
 Arguments ExclBot {_}.
-Existing Instance ExclUnit.
+Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
+  match x with Excl a => Some a | _ => None end.
 
+(* Cofe *)
 Inductive excl_equiv `{Equiv A} : Equiv (excl A) :=
   | Excl_equiv (x y : A) : x ≡ y → Excl x ≡ Excl y
-  | ExclUnit_equiv : ∅ ≡ ∅
+  | ExclUnit_equiv : ExclUnit ≡ ExclUnit
   | ExclBot_equiv : ExclBot ≡ ExclBot.
 Existing Instance excl_equiv.
+Inductive excl_dist `{Dist A} : Dist (excl A) :=
+  | excl_dist_0 (x y : excl A) : x ={0}= y
+  | Excl_dist (x y : A) n : x ={n}= y → Excl x ={n}= Excl y
+  | ExclUnit_dist n : ExclUnit ={n}= ExclUnit
+  | ExclBot_dist n : ExclBot ={n}= ExclBot.
+Existing Instance excl_dist.
+Program Definition excl_chain `{Cofe A}
+    (c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A :=
+  {| chain_car n := match c n return _ with Excl y => y | _ => x end |}.
+Next Obligation.
+  intros A ???? c x ? n i ?; simpl; destruct (c 1) eqn:?; simplify_equality'.
+  destruct (decide (i = 0)) as [->|].
+  { by replace n with 0 by lia. }
+  feed inversion (chain_cauchy c 1 i); auto with lia congruence.
+  feed inversion (chain_cauchy c n i); simpl; auto with lia congruence.
+Qed.
+Instance excl_compl `{Cofe A} : Compl (excl A) := λ c,
+  match Some_dec (maybe Excl (c 1)) with
+  | inleft (exist x H) => Excl (compl (excl_chain c x H)) | inright _ => c 1
+  end.
+Local Instance excl_cofe `{Cofe A} : Cofe (excl A).
+Proof.
+  split.
+  * intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
+    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
+    by intros n; feed inversion (Hxy n).
+  * intros n; split.
+    + by intros [x| |]; constructor.
+    + by destruct 1; constructor.
+    + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
+  * by inversion_clear 1; constructor; apply dist_S.
+  * constructor.
+  * intros c n; unfold compl, excl_compl.
+    destruct (decide (n = 0)) as [->|]; [constructor|].
+    destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|].
+    { assert (c 1 = Excl x) by (by destruct (c 1); simplify_equality').
+      assert (∃ y, c n = Excl y) as [y Hy].
+      { feed inversion (chain_cauchy c 1 n); try congruence; eauto with lia. }
+      rewrite Hy; constructor.
+      by rewrite (conv_compl (excl_chain c x Hx) n); simpl; rewrite Hy. }
+    feed inversion (chain_cauchy c 1 n); auto with lia; constructor.
+    destruct (c 1); simplify_equality'.
+Qed.
+
+(* CMRA *)
 Instance excl_valid {A} : Valid (excl A) := λ x,
   match x with Excl _ | ExclUnit => True | ExclBot => False end.
+Instance excl_validN {A} : ValidN (excl A) := λ n x,
+  match x with Excl _ | ExclUnit => True | ExclBot => n = 0 end.
 Instance excl_empty {A} : Empty (excl A) := ExclUnit.
 Instance excl_unit {A} : Unit (excl A) := λ _, ∅.
 Instance excl_op {A} : Op (excl A) := λ x y,
@@ -31,43 +81,60 @@ Instance excl_minus {A} : Minus (excl A) := λ x y,
   | Excl _, Excl _ => ExclUnit
   | _, _ => ExclBot
   end.
-Instance excl_ra `{Equiv A, !Equivalence (@equiv A _)} : RA (excl A).
+Instance excl_cmra `{Cofe A} : CMRA (excl A).
 Proof.
   split.
-  * split.
-    + by intros []; constructor.
-    + by destruct 1; constructor.
-    + destruct 1; inversion 1; constructor; etransitivity; eauto.
-  * by intros []; destruct 1; constructor.
+  * apply _.
+  * by intros n []; destruct 1; constructor.
   * constructor.
-  * by destruct 1.
-  * by do 2 destruct 1; constructor.
+  * by destruct 1 as [? []| | |]; intros ?.
+  * by destruct 1; inversion_clear 1; constructor.
+  * by intros [].
+  * intros n [?| |]; simpl; auto with lia.
+  * intros x; split; [by intros ? [|n]; destruct x|].
+    by intros Hx; specialize (Hx 1); destruct x.
   * by intros [?| |] [?| |] [?| |]; constructor.
   * by intros [?| |] [?| |]; constructor.
   * by intros [?| |]; constructor.
   * constructor.
-  * intros [?| |] [?| |]; exists ∅; constructor.
-  * by intros [?| |] [?| |].
-  * by intros [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
+  * by intros n [?| |] [?| |]; exists ∅.
+  * by intros n [?| |] [?| |].
+  * by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
 Qed.
-Instance excl_empty_ra `{Equiv A, !Equivalence (@equiv A _)} : RAEmpty (excl A).
+Instance excl_empty_ra `{Cofe A} : RAEmpty (excl A).
 Proof. split. done. by intros []. Qed.
+Instance excl_extend `{Cofe A} : CMRAExtend (excl A).
+Proof.
+  intros [|n] x y1 y2 ? Hx; [by exists (x,∅); destruct x|].
+  by exists match y1, y2 with
+    | Excl a1, Excl a2 => (Excl a1, Excl a2)
+    | ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
+    | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)