prove some properties of the embedding into the global CMRA

algebra/fin_maps.v

@@ -164,15 +164,27 @@ Lemma map_lookup_validN n m i x : ✓{n} m → m !! i ={n}= Some x → ✓{n} x.
 Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
 Lemma map_insert_validN n m 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 m1 m2 i x :
   m2 !! i = None → <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2.
 Proof. by intros Hi; apply (insert_merge_l _ m1 m2); rewrite Hi. Qed.
+
+Lemma map_validN_singleton n (i : K) (x : A) :
+  ✓{n} x <-> ✓{n} ({[ i ↦ x ]} : gmap K A).
+Proof.
+  split.
+  - move=>Hx j. destruct (decide (i = j)); simplify_map_equality; done.
+  - move=>Hm. move: (Hm i). by simplify_map_equality.
+Qed.
+
 Lemma map_unit_singleton (i : K) (x : A) :
   unit ({[ i ↦ x ]} : gmap K A) = {[ i ↦ unit x ]}.
 Proof. apply map_fmap_singleton. Qed.
+
 Lemma map_op_singleton (i : K) (x y : A) :
   {[ i ↦ x ]} ⋅ {[ i ↦ y ]} = ({[ i ↦ x ⋅ y ]} : gmap K A).
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
+
 Lemma singleton_includedN n m i x :
   {[ i ↦ x ]} ≼{n} m ↔ ∃ y, m !! i ={n}= Some y ∧ x ≼ y.
   (* not m !! i = Some y ∧ x ≼{n} y to deal with n = 0 *)

algebra/iprod.v

@@ -7,9 +7,10 @@ Definition iprod {A} (B : A → cofeT) := ∀ x, B x.
 Definition iprod_insert `{∀ x x' : A, Decision (x = x')} {B : A → cofeT}
     (x : A) (y : B x) (f : iprod B) : iprod B := λ x',
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
+Global Instance iprod_empty {A} {B : A → cofeT} `{∀ x, Empty (B x)} : Empty (iprod B) := λ x, ∅.
 Definition iprod_singleton
     `{∀ x x' : A, Decision (x = x')} {B : A → cofeT} `{∀ x : A, Empty (B x)}
-  (x : A) (y : B x) : iprod B := iprod_insert x y (λ _, ∅).
+  (x : A) (y : B x) : iprod B := iprod_insert x y ∅.
 
 Section iprod_cofe.
   Context {A} {B : A → cofeT}.
@@ -100,7 +101,6 @@ Section iprod_cmra.
   Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
   Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
   Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
-  Global Instance iprod_empty `{∀ x, Empty (B x)} : Empty (iprod B) := λ x, ∅.
   Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} (f x).
   Instance iprod_minus : Minus (iprod B) := λ f g x, f x ⩪ g x.
   Definition iprod_lookup_minus f g x : (f ⩪ g) x = f x ⩪ g x := eq_refl.
@@ -148,7 +148,9 @@ Section iprod_cmra.
     * by intros f Hf x; apply (timeless _).
   Qed.
 
+  (** Properties of iprod_update. *)
   Context `{∀ x x' : A, Decision (x = x')}.
+
   Lemma iprod_insert_updateP x (P : B x → Prop) (Q : iprod B → Prop) g y1 :
     y1 ~~>: P → (∀ y2, P y2 → Q (iprod_insert x y2 g)) →
     iprod_insert x y1 g ~~>: Q.
@@ -173,7 +175,20 @@ Section iprod_cmra.
       eauto using iprod_insert_updateP with congruence.
   Qed.
 
+  (** Properties of iprod_singleton. *)
   Context `{∀ x, Empty (B x)} `{∀ x, CMRAIdentity (B x)}.
+
+  Lemma iprod_validN_singleton n x (y : B x) :
+    ✓{n} y <-> ✓{n} (iprod_singleton x y).
+  Proof.
+    split.
+    - move=>Hx x'. destruct (decide (x = x')).
+      + subst x'. by rewrite iprod_lookup_singleton.
+      + rewrite iprod_lookup_singleton_ne //; [].
+        by apply cmra_empty_valid.
+    - move=>Hm. move: (Hm x). by rewrite iprod_lookup_singleton.
+  Qed.
+
   Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
     iprod_singleton x y1 ⋅ iprod_singleton x y2 ≡ iprod_singleton x (y1 ⋅ y2).
   Proof.

program_logic/global_cmra.v

-Require Export program_logic.ownership program_logic.pviewshifts.
+Require Export algebra.iprod program_logic.ownership program_logic.pviewshifts.
 Import uPred.
 
 Definition gid := positive.
@@ -15,26 +15,41 @@ Definition to_globalC {Λ} {Δ : gid → iFunctor}
   iprod_singleton i {[ γ ↦ to_funC _ a ]}.
 Definition own {Λ} {Δ : gid → iFunctor}
     (i : gid) `{!InG Λ Δ i A} (γ : gid) (a : A) : iProp Λ (globalC Δ) :=
-  ownG (Σ:=globalC Δ) (iprod_singleton i {[ γ ↦ to_funC _ a ]}).
+  ownG (Σ:=globalC Δ) (to_globalC i γ a).
 
 Section global.
 Context {Λ : language} {Δ : gid → iFunctor} (i : gid) `{!InG Λ Δ i A}.
 Implicit Types a : A.
 
+(* Proeprties of to_globalC *)
+Lemma globalC_op γ a1 a2 :
+  to_globalC i γ (a1 ⋅ a2) ≡ to_globalC i γ a1 ⋅ to_globalC i γ a2.
+Proof.
+  rewrite /to_globalC iprod_op_singleton map_op_singleton.
+  apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
+  by rewrite /to_funC; destruct inG.
+Qed.
+
+Lemma globalC_validN n γ a :
+  ✓{n} (to_globalC i γ a) <-> ✓{n} a.
+Proof.
+  rewrite /to_globalC.
+  rewrite -iprod_validN_singleton -map_validN_singleton.
+  by rewrite /to_funC; destruct inG.
+Qed.
+
+(* Properties of own *)
+
 Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
 Proof.
   intros m m' Hm; apply ownG_ne, iprod_singleton_ne, singleton_ne.
-  by rewrite /to_funC; destruct inG.
+  by rewrite /to_globalC /to_funC; destruct inG.
 Qed.
 
 Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper _.
 
 Lemma own_op γ a1 a2 : own i γ (a1 ⋅ a2) ≡ (own i γ a1 ★ own i γ a2)%I.
-Proof.
-  rewrite /own -ownG_op iprod_op_singleton map_op_singleton.
-  apply ownG_proper, iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
-  by rewrite /to_funC; destruct inG.
-Qed.
+Proof. rewrite /own -ownG_op. apply ownG_proper, globalC_op. Qed.
 
 (* TODO: This also holds if we just have ✓a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
@@ -50,7 +65,7 @@ Proof.
     + simpl. move=>? [γ [-> ?]]. exists γ. done.
   - apply exist_elim=>m. apply const_elim_l.
     move=>[p ->] {P}. by rewrite -(exist_intro p).
-Qed.      
+Qed.
 
 Lemma always_own_unit γ m : (□ own i γ (unit m))%I ≡ own i γ (unit m).
 Proof.
@@ -59,10 +74,9 @@ Admitted.
 
 Lemma own_valid γ m : (own i γ m) ⊑ (✓ m).
 Proof.
-  rewrite /own ownG_valid; apply uPred.valid_mono.
-intros n ?.
-SearchAbout validN singletonM.
-Admitted.
+  rewrite /own ownG_valid. apply uPred.valid_mono=>n.
+  by apply globalC_validN.
+Qed.
 
 Lemma own_valid_r' γ m : (own i γ m) ⊑ (own i γ m ★ ✓ m).
 Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
@@ -70,7 +84,6 @@ Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
 Global Instance ownG_timeless γ m : Timeless m → TimelessP (own i γ m).
 Proof.
   intros. apply ownG_timeless.
-SearchAbout singletonM Timeless.
 Admitted.
 
 End global.