Timeless cofe elements.

iris/cmra.v

@@ -96,6 +96,14 @@ Proof.
   rewrite ra_included_spec; intros [z Hx2] Hx1; exists (x1' ⋅ z); split.
   apply ra_included_l. by rewrite Hx1, Hx2.
 Qed.
+Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 :
+  validN 1 (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
+Proof.
+  intros ??? z Hz.
+  destruct (cmra_extend_op z x1 x2 1) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
+  { by rewrite <-?Hz. }
+  by rewrite Hz', (timeless x1 y1), (timeless x2 y2).
+Qed.
 End cmra.
 
 Instance cmra_preserving_id `{CMRA A} : CMRAPreserving (@id A).

iris/cofe.v

@@ -92,6 +92,10 @@ Section cofe.
     Proper ((≡) ==> (≡)) f | 100 := _.
 End cofe.
 
+(** Timeless elements *)
+Class Timeless `{Dist A, Equiv A} (x : A) := timeless y : x ={1}= y → x ≡ y.
+Arguments timeless {_ _ _} _ {_} _ _.
+
 (** Fixpoint *)
 Program Definition fixpoint_chain `{Cofe A, Inhabited A} (f : A → A)
   `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
@@ -222,6 +226,9 @@ Proof.
   * intros c n; split. apply (conv_compl (fst_chain c) n).
     apply (conv_compl (snd_chain 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).
+Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
 Canonical Structure prodC (A B : cofeT) : cofeT := CofeT (A * B).
 Instance prod_map_ne `{Dist A, Dist A', Dist B, Dist B'} n :
   Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
@@ -254,6 +261,8 @@ Section discrete_cofe.
     * done.
     * intros c [|n]; [done|apply (chain_cauchy c 1 (S n)); lia].
   Qed.
+  Global Instance discrete_timeless (x : A) : Timeless x.
+  Proof. by intros y. Qed.
   Definition discrete_cofeC : cofeT := CofeT A.
 End discrete_cofe.
 Arguments discrete_cofeC _ {_ _}.

iris/cofe_maps.v

@@ -45,6 +45,10 @@ Proof.
 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.
@@ -79,6 +83,39 @@ Section map.
   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.

prelude/base.v

@@ -466,7 +466,7 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
 Class Insert (K A M : Type) := insert: K → A → M → M.
-Instance: Params (@insert) 4.
+Instance: Params (@insert) 5.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
 Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
@@ -475,7 +475,7 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)
 Class Delete (K M : Type) := delete: K → M → M.
-Instance: Params (@delete) 3.
+Instance: Params (@delete) 4.
 Arguments delete _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function [alter f k m] should update the value at key [k] using the
@@ -537,7 +537,7 @@ Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : C_scope.
 Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch.
 
 Class InsertE (E K A M : Type) := insertE: E → K → A → M → M.
-Instance: Params (@insert) 6.
+Instance: Params (@insertE) 6.
 Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
   (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
 Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.