algebra: prove some frame-preserving updates from empty

algebra/cmra.v

@@ -396,16 +396,27 @@ End cmra_monotone.
 (** * Transporting a CMRA equality *)
 Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
   eq_rect A id x _ H.
+Definition cmra_transport_back {A B : cmraT} (H : A = B) (x : B) : A :=
+  eq_rect B id x _ (eq_sym H).
 
 Section cmra_transport.
   Context {A B : cmraT} (H : A = B).
   Notation T := (cmra_transport H).
+  Notation T' := (cmra_transport_back H).
   Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T.
   Proof. by intros ???; destruct H. Qed.
   Global Instance cmra_transport_proper : Proper ((≡) ==> (≡)) T.
   Proof. by intros ???; destruct H. Qed.
+  Lemma cmra_transport_and_back x : T' (T x) = x.
+  Proof. by destruct H. Qed.
+  Lemma cmra_transport_back_and x : T (T' x) = x.
+  Proof. by destruct H. Qed.
   Lemma cmra_transport_op x y : T (x ⋅ y) = T x ⋅ T y.
   Proof. by destruct H. Qed.
+  Lemma cmra_transport_back_op_r y x : T (x ⋅ T' y) = T x ⋅ y.
+  Proof. by destruct H. Qed.
+  Lemma cmra_transport_back_op_l y x : T (T' x ⋅ y) = x ⋅ T y.
+  Proof. by destruct H. Qed.
   Lemma cmra_transport_unit x : T (unit x) = unit (T x).
   Proof. by destruct H. Qed.
   Lemma cmra_transport_validN n x : ✓{n} (T x) ↔ ✓{n} x.

algebra/fin_maps.v

@@ -228,11 +228,31 @@ Lemma map_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x :
   x ~~>: P → (∀ y, P y → Q {[ i ↦ y ]}) → {[ i ↦ x ]} ~~>: Q.
 Proof. apply map_insert_updateP. Qed.
 Lemma map_singleton_updateP' (P : A → Prop) i x :
-  x ~~>: P → {[ i ↦ x ]} ~~>: λ m', ∃ y, m' = {[ i ↦ y ]} ∧ P y.
+  x ~~>: P → {[ i ↦ x ]} ~~>: λ m, ∃ y, m = {[ i ↦ y ]} ∧ P y.
 Proof. apply map_insert_updateP'. Qed.
 Lemma map_singleton_update i (x y : A) : x ~~> y → {[ i ↦ x ]} ~~> {[ i ↦ y ]}.
 Proof. apply map_insert_update. Qed.
 
+Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A}
+      (P : A → Prop) (Q : gmap K A → Prop) i :
+  ∅ ~~>: P → (∀ y, P y → Q {[ i ↦ y ]}) → ∅ ~~>: Q.
+  Proof.
+    intros Hx HQ gf n Hg.
+    destruct (Hx (default ∅ (gf !! i) id) n) as (y&?&Hy).
+    { move:(Hg i). rewrite !left_id. case _: (gf !! i); first done.
+      intros. apply cmra_empty_valid. }
+    exists {[ i ↦ y]}. split; first by apply HQ.
+    intros i'. rewrite lookup_op.
+    destruct (decide (i' = i)).
+    - subst i'. rewrite lookup_singleton. move:Hy.
+      case _: (gf !! i); first done.
+      by rewrite right_id.
+    - move:(Hg i'). rewrite lookup_singleton_ne // !left_id. done.
+Qed.
+Lemma map_singleton_updateP_empty' `{Empty A, !CMRAIdentity A} (P : A → Prop) i :
+  ∅ ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i ↦ y ]} ∧ P y.
+Proof. eauto using map_singleton_updateP_empty. Qed.
+
 Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
 Lemma map_updateP_alloc (Q : gmap K A → Prop) m x :
   ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.

algebra/iprod.v

@@ -48,7 +48,7 @@ Section iprod_cofe.
   Section empty.
     Context `{∀ x, Empty (B x)}.
     Definition iprod_lookup_empty  x : ∅ x = ∅ := eq_refl.
-    Instance iprod_empty_timeless :
+    Global Instance iprod_empty_timeless :
       (∀ x : A, Timeless (∅ : B x)) → Timeless (∅ : iprod B).
     Proof. intros ? f Hf x. by apply (timeless _). Qed.
   End empty.
@@ -168,7 +168,7 @@ Section iprod_cmra.
     intros ?; split.
     * intros n x; apply cmra_empty_valid.
     * by intros f x; rewrite iprod_lookup_op left_id.
-    * by intros f Hf x; apply (timeless _).
+    * by apply _.
   Qed.
 
   (** Properties of iprod_insert. *)
@@ -230,7 +230,7 @@ Section iprod_cmra.
   Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP. Qed.
   Lemma iprod_singleton_updateP' x (P : B x → Prop) y1 :
     y1 ~~>: P →
-    iprod_singleton x y1 ~~>: λ g', ∃ y2, g' = iprod_singleton x y2 ∧ P y2.
+    iprod_singleton x y1 ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
   Proof. eauto using iprod_singleton_updateP. Qed.
   Lemma iprod_singleton_update x y1 y2 :
     y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2.
@@ -245,6 +245,9 @@ Section iprod_cmra.
     * by rewrite iprod_lookup_op iprod_lookup_singleton.
     * rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
   Qed.
+  Lemma iprod_singleton_updateP_empty' x (P : B x → Prop) :
+    ∅ ~~>: P → ∅ ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
+  Proof. eauto using iprod_singleton_updateP_empty. Qed.
 End iprod_cmra.
 
 Arguments iprodRA {_} _.