Split up option and fin_map stuff.

modures/cofe_maps.v

-Require Export modures.cofe prelude.fin_maps.
-Require Import prelude.pmap prelude.gmap prelude.natmap.
-Local Obligation Tactic := idtac.
-
-(** option *)
-Inductive option_dist `{Dist A} : Dist (option A) :=
-  | option_0_dist (x y : option A) : x ={0}= y
-  | Some_dist n x y : x ={n}= y → Some x ={n}= Some y
-  | None_dist n : None ={n}= None.
-Existing Instance option_dist.
-Program Definition option_chain `{Cofe A}
-    (c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A :=
-  {| chain_car n := from_option x (c n) |}.
-Next Obligation.
-  intros A ???? c x ? n i ?; simpl; 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 option_compl `{Cofe A} : Compl (option A) := λ c,
-  match Some_dec (c 1) with
-  | inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None
-  end.
-Instance option_cofe `{Cofe A} : Cofe (option 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, option_compl.
-    destruct (decide (n = 0)) as [->|]; [constructor|].
-    destruct (Some_dec (c 1)) as [[x Hx]|].
-    { assert (is_Some (c n)) as [y Hy].
-      { feed inversion (chain_cauchy c 1 n); try congruence; eauto with lia. }
-      rewrite Hy; constructor.
-      by rewrite (conv_compl (option_chain c x Hx) n); simpl; rewrite Hy. }
-    feed inversion (chain_cauchy c 1 n); auto with lia congruence; constructor.
-Qed.
-Instance Some_ne `{Dist A} : Proper (dist n ==> dist n) Some.
-Proof. by constructor. Qed.
-Instance None_timeless `{Dist A, Equiv A} : Timeless (@None A).
-Proof. inversion_clear 1; constructor. Qed.
-Instance Some_timeless `{Dist A, Equiv A} x : Timeless x → Timeless (Some x).
-Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
-Instance option_fmap_ne `{Dist A, Dist B} (f : A → B) n:
-  Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
-Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
-
-(** Finite maps *)
-Section map.
-  Context `{FinMap K M}.
-  Global Instance map_dist `{Dist A} : Dist (M A) := λ n m1 m2,
-    ∀ i, m1 !! i ={n}= m2 !! i.
-  Program Definition map_chain `{Dist A} (c : chain (M A))
-    (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
-  Next Obligation. by intros A ? c k n i ?; apply (chain_cauchy c). Qed.
-  Global Instance map_compl `{Cofe A} : Compl (M A) := λ c,
-    map_imap (λ i _, compl (map_chain c i)) (c 1).
-  Global Instance map_cofe `{Cofe A} : Cofe (M A).
-  Proof.
-    split.
-    * intros m1 m2; split.
-      + by intros Hm n k; apply equiv_dist.
-      + intros Hm k; apply equiv_dist; intros n; apply Hm.
-    * intros n; split.
-      + by intros m k.
-      + by intros m1 m2 ? k.
-      + by intros m1 m2 m3 ?? k; transitivity (m2 !! k).
-    * by intros n m1 m2 ? k; apply dist_S.
-    * by intros m1 m2 k.
-    * intros c n k; unfold compl, map_compl; rewrite lookup_imap.
-      destruct (decide (n = 0)) as [->|]; [constructor|].
-      feed inversion (λ H, chain_cauchy c 1 n H k); simpl; auto with lia.
-      by rewrite conv_compl; simpl; apply reflexive_eq.
-  Qed.
-  Global Instance lookup_ne `{Dist A} n k :
-    Proper (dist n ==> dist n) (lookup k : M A → option A).
-  Proof. by intros m1 m2. Qed.
-  Global Instance insert_ne `{Dist A} (i : K) n :
-    Proper (dist n ==> dist n ==> dist n) (insert (M:=M A) i).
-  Proof.
-    intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
-      [by constructor|by apply lookup_ne].
-  Qed.
-  Global Instance delete_ne `{Dist A} (i : K) n :
-    Proper (dist n ==> dist n) (delete (M:=M A) i).
-  Proof.
-    intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
-      [by constructor|by apply lookup_ne].
-  Qed.
-  Global Instance map_empty_timeless `{Dist A, Equiv A} : Timeless (∅ : M A).
-  Proof.
-    intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
-    inversion_clear Hm; constructor.
-  Qed.
-  Global Instance map_lookup_timeless `{Cofe A} (m : M A) i :
-    Timeless m → Timeless (m !! i).
-  Proof.
-    intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
-    rewrite (timeless m (<[i:=x]>m)), lookup_insert; auto.
-    by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id.
-  Qed.
-  Global Instance map_ra_insert_timeless `{Cofe A} (m : M A) i x :
-    Timeless x → Timeless m → Timeless (<[i:=x]>m).
-  Proof.
-    intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality.
-    { by apply (timeless _); rewrite <-Hm, lookup_insert. }
-    by apply (timeless _); rewrite <-Hm, lookup_insert_ne by done.
-  Qed.
-  Global Instance map_ra_singleton_timeless `{Cofe A} (i : K) (x : A) :
-    Timeless x → Timeless ({[ i, x ]} : M A) := _.
-  Instance map_fmap_ne `{Dist A, Dist B} (f : A → B) n :
-    Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=M) f).
-  Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
-  Definition mapC (A : cofeT) : cofeT := CofeT (M A).
-  Definition mapC_map {A B} (f: A -n> B) : mapC A -n> mapC B :=
-    CofeMor (fmap f : mapC A → mapC B).
-  Global Instance mapC_map_ne {A B} n :
-    Proper (dist n ==> dist n) (@mapC_map A B).
-  Proof.
-    intros f g Hf m k; simpl; rewrite !lookup_fmap.
-    destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
-  Qed.
-End map.
-Arguments mapC {_} _ {_ _ _ _ _ _ _ _ _} _.
-
-Canonical Structure natmapC := mapC natmap.
-Definition natmapC_map {A B}
-  (f : A -n> B) : natmapC A -n> natmapC B := mapC_map f.
-Canonical Structure PmapC := mapC Pmap.
-Definition PmapC_map {A B} (f : A -n> B) : PmapC A -n> PmapC B := mapC_map f.
-Canonical Structure gmapC K `{Countable K} := mapC (gmap K).
-Definition gmapC_map `{Countable K} {A B}
-  (f : A -n> B) : gmapC K A -n> gmapC K B := mapC_map f.

modures/fin_maps.v

+Require Export modures.cmra.
+Require Import prelude.pmap prelude.natmap prelude.gmap modures.option.
+
+Section map.
+Context `{FinMap K M}.
+
+(* COFE *)
+Global Instance map_dist `{Dist A} : Dist (M A) := λ n m1 m2,
+  ∀ i, m1 !! i ={n}= m2 !! i.
+Program Definition map_chain `{Dist A} (c : chain (M A))
+  (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
+Next Obligation. by intros A ? c k n i ?; apply (chain_cauchy c). Qed.
+Global Instance map_compl `{Cofe A} : Compl (M A) := λ c,
+  map_imap (λ i _, compl (map_chain c i)) (c 1).
+Global Instance map_cofe `{Cofe A} : Cofe (M A).
+Proof.
+  split.
+  * intros m1 m2; split.
+    + by intros Hm n k; apply equiv_dist.
+    + intros Hm k; apply equiv_dist; intros n; apply Hm.
+  * intros n; split.
+    + by intros m k.
+    + by intros m1 m2 ? k.
+    + by intros m1 m2 m3 ?? k; transitivity (m2 !! k).
+  * by intros n m1 m2 ? k; apply dist_S.
+  * by intros m1 m2 k.
+  * intros c n k; unfold compl, map_compl; rewrite lookup_imap.
+    destruct (decide (n = 0)) as [->|]; [constructor|].
+    feed inversion (λ H, chain_cauchy c 1 n H k); simpl; auto with lia.
+    by rewrite conv_compl; simpl; apply reflexive_eq.
+Qed.
+Global Instance lookup_ne `{Dist A} n k :
+  Proper (dist n ==> dist n) (lookup k : M A → option A).
+Proof. by intros m1 m2. Qed.
+Global Instance insert_ne `{Dist A} (i : K) n :
+  Proper (dist n ==> dist n ==> dist n) (insert (M:=M A) i).
+Proof.
+  intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
+    [by constructor|by apply lookup_ne].
+Qed.
+Global Instance delete_ne `{Dist A} (i : K) n :
+  Proper (dist n ==> dist n) (delete (M:=M A) i).
+Proof.
+  intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
+    [by constructor|by apply lookup_ne].
+Qed.
+Global Instance map_empty_timeless `{Dist A, Equiv A} : Timeless (∅ : M A).
+Proof.
+  intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
+  inversion_clear Hm; constructor.
+Qed.
+Global Instance map_lookup_timeless `{Cofe A} (m : M A) i :
+  Timeless m → Timeless (m !! i).
+Proof.
+  intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
+  rewrite (timeless m (<[i:=x]>m)), lookup_insert; auto.
+  by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id.
+Qed.
+Global Instance map_ra_insert_timeless `{Cofe A} (m : M A) i x :
+  Timeless x → Timeless m → Timeless (<[i:=x]>m).
+Proof.
+  intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality.
+  { by apply (timeless _); rewrite <-Hm, lookup_insert. }
+  by apply (timeless _); rewrite <-Hm, lookup_insert_ne by done.
+Qed.
+Global Instance map_ra_singleton_timeless `{Cofe A} (i : K) (x : A) :
+  Timeless x → Timeless ({[ i, x ]} : M A) := _.
+Instance map_fmap_ne `{Dist A, Dist B} (f : A → B) n :
+  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=M) f).
+Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
+Definition mapC (A : cofeT) : cofeT := CofeT (M A).
+Definition mapC_map {A B} (f: A -n> B) : mapC A -n> mapC B :=
+  CofeMor (fmap f : mapC A → mapC B).
+Global Instance mapC_map_ne {A B} n :
+  Proper (dist n ==> dist n) (@mapC_map A B).
+Proof.
+  intros f g Hf m k; simpl; rewrite !lookup_fmap.
+  destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
+Qed.
+
+(* CMRA *)
+Global Instance map_op `{Op A} : Op (M A) := merge op.
+Global Instance map_unit `{Unit A} : Unit (M A) := fmap unit.
+Global Instance map_valid `{Valid A} : Valid (M A) := λ m, ∀ i, ✓ (m !! i).
+Global Instance map_validN `{ValidN A} : ValidN (M A) := λ n m,
+  ∀ i, ✓{n} (m!!i).
+Global Instance map_minus `{Minus A} : Minus (M A) := merge minus.
+Lemma lookup_op `{Op A} m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
+Proof. by apply lookup_merge. Qed.
+Lemma lookup_minus `{Minus A} m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i.
+Proof. by apply lookup_merge. Qed.
+Lemma lookup_unit `{Unit A} m i : unit m !! i = unit (m !! i).
+Proof. by apply lookup_fmap. Qed.
+Lemma map_included_spec `{CMRA A} (m1 m2 : M A) :
+  m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
+Proof.
+  split.
+  * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
+  * intros Hm; exists (m2 ⩪ m1); intros i.
+    by rewrite lookup_op, lookup_minus, ra_op_minus.
+Qed.
+Lemma map_includedN_spec `{CMRA A} (m1 m2 : M A) n :
+  m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
+Proof.
+  split.
+  * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
+  * intros Hm; exists (m2 ⩪ m1); intros i.
+    by rewrite lookup_op, lookup_minus, cmra_op_minus.
+Qed.
+Global Instance map_cmra `{CMRA A} : CMRA (M A).
+Proof.
+  split.
+  * apply _.
+  * by intros n m1 m2 m3 Hm i; rewrite !lookup_op, (Hm i).
+  * by intros n m1 m2 Hm i; rewrite !lookup_unit, (Hm i).
+  * by intros n m1 m2 Hm ? i; rewrite <-(Hm i).
+  * intros n m1 m1' Hm1 m2 m2' Hm2 i.
+    by rewrite !lookup_minus, (Hm1 i), (Hm2 i).
+  * by intros m i.
+  * intros n m Hm i; apply cmra_valid_S, Hm.
+  * intros m; split; [by intros Hm n i; apply cmra_valid_validN|].
+    intros Hm i; apply cmra_valid_validN; intros n; apply Hm.
+  * by intros m1 m2 m3 i; rewrite !lookup_op, (associative _).
+  * by intros m1 m2 i; rewrite !lookup_op, (commutative _).
+  * by intros m i; rewrite lookup_op, !lookup_unit, ra_unit_l.
+  * by intros m i; rewrite !lookup_unit, ra_unit_idempotent.
+  * intros n x y; rewrite !map_includedN_spec; intros Hm i.
+    by rewrite !lookup_unit; apply cmra_unit_preserving.
+  * intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i).
+    by rewrite <-lookup_op.
+  * intros x y n; rewrite map_includedN_spec; intros ? i.
+    by rewrite lookup_op, lookup_minus, cmra_op_minus by done.
+Qed.
+Global Instance map_ra_empty `{RA A} : RAEmpty (M A).
+Proof.
+  split.
+  * by intros ?; rewrite lookup_empty.
+  * by intros m i; simpl; rewrite lookup_op, lookup_empty; destruct (m !! i).
+Qed.
+Global Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (M A).
+Proof.
+  intros n m m1 m2 Hm Hm12.
+  assert (∀ i, m !! i ={n}= m1 !! i ⋅ m2 !! i) as Hm12'
+    by (by intros i; rewrite <-lookup_op).
+  set (f i := cmra_extend_op n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
+  set (f_proj i := proj1_sig (f i)).
+  exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
+    repeat split; simpl; intros i; rewrite ?lookup_op, !lookup_imap.
+  * destruct (m !! i) as [x|] eqn:Hx; simpl; [|constructor].
+    rewrite <-Hx; apply (proj2_sig (f i)).
+  * destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
+    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
+    by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
+  * destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
+    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
+    by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
+Qed.
+Global Instance map_empty_valid_timeless `{Valid A, ValidN A} :
+  ValidTimeless (∅ : M A).
+Proof. by intros ??; rewrite lookup_empty. Qed.
+Global Instance map_ra_insert_valid_timeless `{Valid A,ValidN A} (m: M A) i x:
+  ValidTimeless x → ValidTimeless m → m !! i = None →
+  ValidTimeless (<[i:=x]>m).
+Proof.
+  intros ?? Hi Hm j; destruct (decide (i = j)); simplify_map_equality.
+  { specialize (Hm j); simplify_map_equality. by apply (valid_timeless _). }
+  generalize j; clear dependent j; rapply (valid_timeless m).
+  intros j; destruct (decide (i = j)); simplify_map_equality;[by rewrite Hi|].
+  by specialize (Hm j); simplify_map_equality.
+Qed.
+Global Instance map_ra_singleton_valid_timeless `{Valid A, ValidN A} (i : K) x :
+  ValidTimeless x → ValidTimeless ({[ i, x ]} : M A).
+Proof.
+  intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _); simpl.
+  by rewrite lookup_empty.
+Qed.
+Lemma map_insert_valid `{ValidN A} (m : M A) n i x :
+  ✓{n} x → ✓{n} m → ✓{n} (<[i:=x]>m).
+Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
+Lemma map_insert_op `{Op A} (m1 m2 : M A) i x :
+  m2 !! i = None →  <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2.
+Proof. by intros Hi; apply (insert_merge_l _); rewrite Hi. Qed.
+Definition mapRA (A : cmraT) : cmraT := CMRAT (M A).
+Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B)
+  `{!CMRAMonotone f} : CMRAMonotone (fmap f : M A → M B).
+Proof.
+  split.
+  * intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
+    by rewrite !lookup_fmap; apply includedN_preserving.
+  * by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
+Qed.
+Definition mapRA_map {A B : cmraT} (f : A -n> B) : mapRA A -n> mapRA B :=
+  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_map_monotone {A B : cmraT} (f : A -n> B)
+  `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.
+End map.
+
+Section map_dom.
+  Context `{FinMapDom K M D, Fresh K D, !FreshSpec K D}.
+  Lemma map_dom_op `{Op A} (m1 m2: M A) : dom D (m1 ⋅ m2) ≡ dom D m1 ∪ dom D m2.
+  Proof.
+    apply elem_of_equiv; intros i; rewrite elem_of_union, !elem_of_dom.
+    unfold is_Some; setoid_rewrite lookup_op.
+    destruct (m1 !! i), (m2 !! i); naive_solver.
+  Qed.
+  Lemma map_update_alloc `{CMRA A} (m : M A) x :
+    ✓ x → m ⇝: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
+  Proof.
+    intros ? mf n Hm. set (i := fresh (dom D (m ⋅ mf))).
+    assert (i ∉ dom D m ∧ i ∉ dom D mf) as [??].
+    { rewrite <-not_elem_of_union, <-map_dom_op; apply is_fresh. }
+    exists (<[i:=x]>m); split; [exists i; split; [done|]|].
+    * by apply not_elem_of_dom.
+    * rewrite <-map_insert_op by (by apply not_elem_of_dom).
+      by apply map_insert_valid; [apply cmra_valid_validN|].
+  Qed.
+End map_dom.
+
+Arguments mapC {_} _ {_ _ _ _ _ _ _ _ _} _.
+Arguments mapRA {_} _ {_ _ _ _ _ _ _ _ _} _.
+
+Canonical Structure natmapC := mapC natmap.
+Definition natmapC_map {A B}
+  (f : A -n> B) : natmapC A -n> natmapC B := mapC_map f.
+Canonical Structure PmapC := mapC Pmap.
+Definition PmapC_map {A B} (f : A -n> B) : PmapC A -n> PmapC B := mapC_map f.
+Canonical Structure gmapC K `{Countable K} := mapC (gmap K).
+Definition gmapC_map `{Countable K} {A B}
+  (f : A -n> B) : gmapC K A -n> gmapC K B := mapC_map f.
+
+Canonical Structure natmapRA := mapRA natmap.
+Definition natmapRA_map {A B : cmraT}
+  (f : A -n> B) : natmapRA A -n> natmapRA B := mapRA_map f.
+Canonical Structure PmapRA := mapRA Pmap.
+Definition PmapRA_map {A B : cmraT}
+  (f : A -n> B) : PmapRA A -n> PmapRA B := mapRA_map f.
+Canonical Structure gmapRA K `{Countable K} := mapRA (gmap K).
+Definition gmapRA_map `{Countable K} {A B : cmraT}
+  (f : A -n> B) : gmapRA K A -n> gmapRA K B := mapRA_map f.

modures/cmra_maps.v → modures/option.v

-Require Export modures.cmra modures.cofe_maps.
-Require Import prelude.pmap prelude.natmap prelude.gmap.
+Require Export modures.cmra.
 
-(** option *)
+(* COFE *)
+Inductive option_dist `{Dist A} : Dist (option A) :=
+  | option_0_dist (x y : option A) : x ={0}= y
+  | Some_dist n x y : x ={n}= y → Some x ={n}= Some y
+  | None_dist n : None ={n}= None.
+Existing Instance option_dist.
+Program Definition option_chain `{Cofe A}
+    (c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A :=
+  {| chain_car n := from_option x (c n) |}.
+Next Obligation.
+  intros A ???? c x ? n i ?; simpl; 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 option_compl `{Cofe A} : Compl (option A) := λ c,
+  match Some_dec (c 1) with
+  | inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None
+  end.
+Instance option_cofe `{Cofe A} : Cofe (option 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, option_compl.
+    destruct (decide (n = 0)) as [->|]; [constructor|].
+    destruct (Some_dec (c 1)) as [[x Hx]|].
+    { assert (is_Some (c n)) as [y Hy].
+      { feed inversion (chain_cauchy c 1 n); try congruence; eauto with lia. }
+      rewrite Hy; constructor.
+      by rewrite (conv_compl (option_chain c x Hx) n); simpl; rewrite Hy. }
+    feed inversion (chain_cauchy c 1 n); auto with lia congruence; constructor.
+Qed.
+Instance Some_ne `{Dist A} : Proper (dist n ==> dist n) Some.
+Proof. by constructor. Qed.
+Instance None_timeless `{Dist A, Equiv A} : Timeless (@None A).
+Proof. inversion_clear 1; constructor. Qed.
+Instance Some_timeless `{Dist A, Equiv A} x : Timeless x → Timeless (Some x).
+Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
+Instance option_fmap_ne `{Dist A, Dist B} (f : A → B) n:
+  Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
+Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
+
+(* CMRA *)
 Instance option_valid `{Valid A} : Valid (option A) := λ mx,
   match mx with Some x => ✓ x | None => True end.
 Instance option_validN `{ValidN A} : ValidN (option A) := λ n mx,
@@ -88,159 +137,4 @@ Proof.
     intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving.
   * by intros n [x|] ?;
       unfold validN, option_validN; simpl; try apply validN_preserving.
-Qed.
-
-(** fin maps *)
-Section map.
-  Context `{FinMap K M}.
-  Existing Instances map_dist map_compl map_cofe.
-  Global Instance map_op `{Op A} : Op (M A) := merge op.
-  Global Instance map_unit `{Unit A} : Unit (M A) := fmap unit.
-  Global Instance map_valid `{Valid A} : Valid (M A) := λ m, ∀ i, ✓ (m !! i).
-  Global Instance map_validN `{ValidN A} : ValidN (M A) := λ n m,
-    ∀ i, ✓{n} (m!!i).
-  Global Instance map_minus `{Minus A} : Minus (M A) := merge minus.
-  Lemma lookup_op `{Op A} m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
-  Proof. by apply lookup_merge. Qed.
-  Lemma lookup_minus `{Minus A} m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i.
-  Proof. by apply lookup_merge. Qed.
-  Lemma lookup_unit `{Unit A} m i : unit m !! i = unit (m !! i).
-  Proof. by apply lookup_fmap. Qed.
-  Lemma map_included_spec `{CMRA A} (m1 m2 : M A) :
-    m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
-  Proof.
-    split.
-    * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
-    * intros Hm; exists (m2 ⩪ m1); intros i.
-      by rewrite lookup_op, lookup_minus, ra_op_minus.
-  Qed.
-  Lemma map_includedN_spec `{CMRA A} (m1 m2 : M A) n :
-    m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
-  Proof.
-    split.
-    * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
-    * intros Hm; exists (m2 ⩪ m1); intros i.
-      by rewrite lookup_op, lookup_minus, cmra_op_minus.
-  Qed.
-  Global Instance map_cmra `{CMRA A} : CMRA (M A).
-  Proof.
-    split.
-    * apply _.
-    * by intros n m1 m2 m3 Hm i; rewrite !lookup_op, (Hm i).
-    * by intros n m1 m2 Hm i; rewrite !lookup_unit, (Hm i).
-    * by intros n m1 m2 Hm ? i; rewrite <-(Hm i).
-    * intros n m1 m1' Hm1 m2 m2' Hm2 i.
-      by rewrite !lookup_minus, (Hm1 i), (Hm2 i).
-    * by intros m i.
-    * intros n m Hm i; apply cmra_valid_S, Hm.
-    * intros m; split; [by intros Hm n i; apply cmra_valid_validN|].
-      intros Hm i; apply cmra_valid_validN; intros n; apply Hm.
-    * by intros m1 m2 m3 i; rewrite !lookup_op, (associative _).
-    * by intros m1 m2 i; rewrite !lookup_op, (commutative _).
-    * by intros m i; rewrite lookup_op, !lookup_unit, ra_unit_l.
-    * by intros m i; rewrite !lookup_unit, ra_unit_idempotent.
-    * intros n x y; rewrite !map_includedN_spec; intros Hm i.
-      by rewrite !lookup_unit; apply cmra_unit_preserving.
-    * intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i).
-      by rewrite <-lookup_op.
-    * intros x y n; rewrite map_includedN_spec; intros ? i.
-      by rewrite lookup_op, lookup_minus, cmra_op_minus by done.
-  Qed.