diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v index b2b65e30d63bfa063e33b1ba657669f9000bd712..b89da649504de7f6614f2425cee26a51c0eb0726 100644 --- a/algebra/fin_maps.v +++ b/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 *) diff --git a/algebra/iprod.v b/algebra/iprod.v index 52ceca40e1bd8287101ac74a8fde92970abd8636..6fd4dcef7b6588235c33fe43e7806e012324bda4 100644 --- a/algebra/iprod.v +++ b/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. diff --git a/program_logic/global_cmra.v b/program_logic/global_cmra.v index fb817192862fccc957ac0c2a2bdc4506f4ecea43..c93d2518c90e1af2bb7d72b52167f2ad51db21b0 100644 --- a/program_logic/global_cmra.v +++ b/program_logic/global_cmra.v @@ -1,4 +1,4 @@ -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.