Library iris.program_logic.wsat
From iris.prelude Require Export coPset.
From iris.program_logic Require Export model.
From iris.algebra Require Export cmra_big_op cmra_tactics.
From iris.algebra Require Import updates.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 10 (✓{_} _) ⇒ solve_validN.
Local Hint Extern 1 (✓{_} gst _) ⇒ apply gst_validN.
Local Hint Extern 1 (✓{_} wld _) ⇒ apply wld_validN.
Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
(σ : state Λ) (rs : gmap positive (iRes Λ Σ)) (r : iRes Λ Σ) (rl: iRes Λ Σ) := {
wsat_pre_valid : ✓{S n} (r ⋅ rl);
wsat_pre_state : pst r ≡ Excl' σ;
wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i);
wsat_pre_wld i P :
i ∈ E →
wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) →
∃ r', rs !! i = Some r' ∧ P n r' ∅
}.
Arguments wsat_pre_valid {_ _ _ _ _ _ _ _} _ .
Arguments wsat_pre_state {_ _ _ _ _ _ _ _} _.
Arguments wsat_pre_dom {_ _ _ _ _ _ _} _ _ {_} _.
Arguments wsat_pre_wld {_ _ _ _ _ _ _} _ _ _ _ {_} _.
Definition wsat {Λ Σ}
(n : nat) (E : coPset) (σ : state Λ) (r : iRes Λ Σ) (rl: iRes Λ Σ): Prop :=
match n with 0 ⇒ True | S n ⇒ ∃ rs, wsat_pre n E σ rs (r ⋅ big_opM rs) rl end.
Instance: Params (@wsat) 5.
Arguments wsat : simpl never.
Section wsat.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types σ : state Λ.
Implicit Types r : iRes Λ Σ.
Implicit Types rs : gmap positive (iRes Λ Σ).
Implicit Types P : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Instance wsat_ne' : Proper (dist n ==> dist n ==> impl) (@wsat Λ Σ n E σ).
Proof.
intros [|n] E σ r1 r2 Hr rl1 rl2 Hrl; first done; intros [rs [Hdom Hv Hs Hinv]].
∃ rs; constructor; intros until 0; setoid_rewrite <-Hr; try setoid_rewrite <-Hrl; eauto.
Qed.
Global Instance wsat_ne n : Proper (dist n ==> dist n ==> iff) (@wsat Λ Σ n E σ) | 1.
Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed.
Global Instance wsat_proper' n : Proper ((≡) ==> (≡) ==> iff) (@wsat Λ Σ n E σ) | 1.
Proof. by intros E σ w1 w2 Hw wl1 wl2 Hwl; apply wsat_ne; apply equiv_dist. Qed.
Lemma wsat_proper n E1 E2 σ r1 r2 rl1 rl2 :
E1 = E2 → r1 ≡ r2 → rl1 ≡ rl2 → wsat n E1 σ r1 rl1 → wsat n E2 σ r2 rl2.
Proof. by move=>->->->. Qed.
Lemma wsat_le n n' E σ r rl : wsat n E σ r rl → n' ≤ n → wsat n' E σ r rl.
Proof.
destruct n as [|n], n' as [|n']; simpl; try by (auto with lia).
intros [rs [Hval Hσ HE Hwld]] ?; ∃ rs; constructor; auto.
intros i P ? (P'&HiP&HP')%dist_Some_inv_r'.
destruct (to_agree_uninj (S n) P') as [laterP' HlaterP'].
{ apply (lookup_validN_Some _ (wld (r ⋅ big_opM rs)) i); rewrite ?HiP; auto. }
assert (P' ≡{S n}≡ to_agree $ Next $ iProp_unfold $
iProp_fold $ later_car $ laterP') as HPiso.
{ by rewrite iProp_unfold_fold later_eta HlaterP'. }
assert (P ≡{n'}≡ iProp_fold (later_car laterP')) as HPP'.
{ apply (inj iProp_unfold), (inj Next), (inj to_agree).
by rewrite HP' -(dist_le _ _ _ _ HPiso). }
destruct (Hwld i (iProp_fold (later_car laterP'))) as (r'&?&?); auto.
{ by rewrite HiP -HPiso. }
assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto).
∃ r'; split; [done|]. apply HPP', uPred_closed with n; auto.
Qed.
Lemma wsat_weaken n E σ r rl rfl: wsat n E σ r (rl ⋅ rfl) → wsat n E σ r rl.
Proof.
destruct n as [|n]; auto.
intros [rs [Hval Hσ HE Hwld]]; ∃ rs; constructor; auto.
Qed.
Lemma wsat_valid n E σ r rl : n ≠ 0 → wsat n E σ r rl → ✓{n} (r ⋅ rl).
Proof.
destruct n; first done.
intros _ [rs ?]; eapply cmra_validN_op_l. rewrite -assoc (comm _ rl) assoc.
eapply wsat_pre_valid; eauto.
Qed.
Lemma wsat_init k E σ m ml : ✓{S k} (m ⋅ ml) → wsat (S k) E σ (Res ∅ (Excl' σ) m) (Res ∅ ∅ ml).
Proof.
intros Hv. ∃ ∅; constructor; auto.
- rewrite big_opM_empty right_id.
split_and!; try (apply cmra_valid_validN, ra_empty_valid);
constructor || apply Hv.
- by intros i; rewrite lookup_empty=>-[??].
- intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
Qed.
Lemma wsat_open n E σ r rl i P :
wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E →
wsat (S n) ({[i]} ∪ E) σ r rl → ∃ rP, wsat (S n) E σ (rP ⋅ r) rl ∧ P n rP ∅.
Proof.
intros HiP Hi [rs [Hval Hσ HE Hwld]].
destruct (Hwld i P) as (rP&?&?); [set_solver +|by apply lookup_wld_op_l; auto|].
assert (rP ⋅ r ⋅ big_opM (delete i rs) ≡ r ⋅ big_opM rs) as Hr.
{ by rewrite (comm _ rP) -assoc big_opM_delete. }
∃ rP; split; [∃ (delete i rs); constructor; rewrite ?Hr|]; auto.
- intros j; rewrite lookup_delete_is_Some Hr.
generalize (HE j); set_solver +Hi.
- intros j P'; rewrite Hr⇒ Hj ?.
setoid_rewrite lookup_delete_ne; last (set_solver +Hi Hj).
apply Hwld; [set_solver +Hj|done].
Qed.
Lemma wsat_close n E σ r rl i P rP :
wld rP !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E →
wsat (S n) E σ (rP ⋅ r) rl → P n rP ∅ → wsat (S n) ({[i]} ∪ E) σ r rl.
Proof.
intros HiP HiE [rs [Hval Hσ HE Hwld]] ?.
assert (rs !! i = None) by (apply eq_None_not_Some; naive_solver).
assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
{ by rewrite (comm _ rP) -assoc big_opM_insert. }
∃ (<[i:=rP]>rs); constructor; rewrite ?Hr; auto.
- intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
+ split. set_solver. rewrite !lookup_op HiP !op_is_Some; eauto.
+ destruct (HE j) as [Hj Hj']; auto; set_solver +Hj Hj'.
- intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst.
+ rewrite !lookup_wld_op_l ?HiP; auto⇒ HP.
apply (inj Some), (inj to_agree), (inj Next), (inj iProp_unfold) in HP.
∃ rP; split; [rewrite lookup_insert|apply HP]; auto.
+ intros. destruct (Hwld j P') as (r'&?&?); auto.
∃ r'; rewrite lookup_insert_ne; naive_solver.
Qed.
Lemma wsat_update_pst n E σ1 σ1' r rl rf :
pst r ≡{S n}≡ Excl' σ1 → wsat (S n) E σ1' (r ⋅ rf) rl →
σ1' = σ1 ∧ ∀ σ2, wsat (S n) E σ2 (update_pst σ2 r ⋅ rf) rl.
Proof.
intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in ×.
assert (pst rf ⋅ pst (big_opM rs) = ∅) as Hpst'.
{ by apply: (excl_validN_inv_l (S n) _ σ1); rewrite -Hpst_r assoc;
eauto using cmra_validN_op_r. }
assert (pst rf ⋅ pst (big_opM rs) ⋅ pst rl = ∅) as Hpst''.
{ by apply: (excl_validN_inv_l (S n) _ σ1); rewrite -Hpst_r assoc;
eauto using cmra_validN_op_r. }
assert (σ1' = σ1) as →.
{ apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
apply (inj Excl), (inj Some).
by rewrite -Hpst_r -Hpst -assoc Hpst' right_id. }
split; [done|∃ rs].
constructor; first split_and!; try rewrite /= -assoc Hpst'; auto.
simpl. by rewrite -?assoc (assoc _ (pst rf)) Hpst''.
Qed.
Lemma wsat_update_gst n E σ r rf rl m1 (P : iGst Λ Σ → Prop) :
m1 ≼{S n} gst r → m1 ~~>: P →
wsat (S n) E σ (r ⋅ rf) rl → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) rl ∧ P m2.
Proof.
intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
destruct (Hup (S n) (Some (mf ⋅ gst (rf ⋅ big_opM rs ⋅ rl)))) as (m2&?&Hval'); try done.
{ rewrite /= (assoc _ m1) -Hr assoc. solve_validN. }
∃ m2; split; [∃ rs|done].
by constructor; first split_and!; auto.
Qed.
Lemma wsat_update_gst' n E σ r rf rl rfl m1 ml1 (P : iGst Λ Σ → iGst Λ Σ → Prop) :
m1 ≼{S n} gst r → ml1 ≡{S n}≡ gst rl → m1 # ml1 ~~>>: P →
wsat (S n) E σ (r ⋅ rf) (rl ⋅ rfl) →
∃ m2 ml2, wsat (S n) E σ (update_gst m2 r ⋅ rf) (update_gst ml2 rl ⋅ rfl)
∧ P m2 ml2 ∧ rl ⤳_(S n) update_gst ml2 rl.
Proof.
intros [mf Hr] Hrl Hup [rs [(?&?&?) Hσ HE Hwld]].
destruct (Hup (S n) (Some (mf ⋅ gst (rf ⋅ big_opM rs ⋅ rfl)))) as (m2&ml2&?&Hval'&Hs); try done.
{ rewrite /= -assoc (comm _ ml1) /= (assoc _ m1) (assoc _ m1) -Hr Hrl assoc. solve_validN. }
∃ m2, ml2; split_and!; [∃ rs|done|].
- by constructor; first split_and!; auto.
- rewrite /stepN /cmra_stepN //= /res_stepN.
rewrite -(dist_le _ _ _ _ Hrl); eauto.
Qed.
Lemma wsat_alloc n E1 E2 σ r rl P rP :
¬set_finite E1 → P n rP ∅ → wsat (S n) (E1 ∪ E2) σ (rP ⋅ r) rl →
∃ i, wsat (S n) (E1 ∪ E2) σ
(Res {[i := to_agree (Next (iProp_unfold P))]} ∅ ∅ ⋅ r) rl ∧
wld r !! i = None ∧ i ∈ E1.
Proof.
intros HE1 ? [rs [Hval Hσ HE Hwld]].
assert (∃ i, i ∈ E1 ∧ wld r !! i = None ∧ wld rP !! i = None ∧
wld (big_opM rs) !! i = None ∧ wld rl !! i = None)
as (i&Hi&Hri&HrPi&Hrsi&Hrli).
{ ∃ (coPpick (E1 ∖
(dom _ (wld r) ∪ (dom _ (wld rP) ∪ (dom _ (wld (big_opM rs)) ∪ dom _ (wld rl)))))).
rewrite -!not_elem_of_dom -?not_elem_of_union -elem_of_difference.
apply coPpick_elem_of⇒HE'; eapply HE1, (difference_finite_inv _ _), HE'.
by repeat apply union_finite; apply dom_finite. }
assert (rs !! i = None).
{ apply eq_None_not_Some=>?; destruct (HE i) as [_ Hri']; auto; revert Hri'.
rewrite /= !lookup_op !op_is_Some -!not_eq_None_Some; tauto. }
assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
{ by rewrite (comm _ rP) -assoc big_opM_insert. }
∃ i; split_and?; [∃ (<[i:=rP]>rs); constructor| |]; auto.
- destruct Hval as (?&?&?). rewrite -(assoc _ _ r) Hr.
split_and!; rewrite /= ?left_id; [|eauto|eauto].
intros j; destruct (decide (j = i)) as [->|].
+ by rewrite !lookup_op Hri HrPi Hrsi Hrli !right_id lookup_singleton.
+ by rewrite -?assoc lookup_op lookup_singleton_ne // left_id ?assoc.
- by rewrite -assoc Hr /= left_id.
- intros j; rewrite -assoc Hr; destruct (decide (j = i)) as [->|].
+ intros _; split; first set_solver +Hi.
rewrite /= !lookup_op lookup_singleton !op_is_Some; eauto.
+ rewrite lookup_insert_ne //.
rewrite lookup_op lookup_singleton_ne // left_id; eauto.
- intros j P'; rewrite -assoc Hr; destruct (decide (j=i)) as [->|].
+ rewrite /= !lookup_op Hri HrPi Hrsi right_id lookup_singleton=>? HP.
apply (inj Some), (inj to_agree), (inj Next), (inj iProp_unfold) in HP.
∃ rP; rewrite lookup_insert; split; [|apply HP]; auto.
+ rewrite /= lookup_op lookup_singleton_ne // left_id⇒ ??.
destruct (Hwld j P') as [r' ?]; auto.
by ∃ r'; rewrite lookup_insert_ne.
Qed.
End wsat.
From iris.program_logic Require Export model.
From iris.algebra Require Export cmra_big_op cmra_tactics.
From iris.algebra Require Import updates.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 10 (✓{_} _) ⇒ solve_validN.
Local Hint Extern 1 (✓{_} gst _) ⇒ apply gst_validN.
Local Hint Extern 1 (✓{_} wld _) ⇒ apply wld_validN.
Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
(σ : state Λ) (rs : gmap positive (iRes Λ Σ)) (r : iRes Λ Σ) (rl: iRes Λ Σ) := {
wsat_pre_valid : ✓{S n} (r ⋅ rl);
wsat_pre_state : pst r ≡ Excl' σ;
wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i);
wsat_pre_wld i P :
i ∈ E →
wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) →
∃ r', rs !! i = Some r' ∧ P n r' ∅
}.
Arguments wsat_pre_valid {_ _ _ _ _ _ _ _} _ .
Arguments wsat_pre_state {_ _ _ _ _ _ _ _} _.
Arguments wsat_pre_dom {_ _ _ _ _ _ _} _ _ {_} _.
Arguments wsat_pre_wld {_ _ _ _ _ _ _} _ _ _ _ {_} _.
Definition wsat {Λ Σ}
(n : nat) (E : coPset) (σ : state Λ) (r : iRes Λ Σ) (rl: iRes Λ Σ): Prop :=
match n with 0 ⇒ True | S n ⇒ ∃ rs, wsat_pre n E σ rs (r ⋅ big_opM rs) rl end.
Instance: Params (@wsat) 5.
Arguments wsat : simpl never.
Section wsat.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types σ : state Λ.
Implicit Types r : iRes Λ Σ.
Implicit Types rs : gmap positive (iRes Λ Σ).
Implicit Types P : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Instance wsat_ne' : Proper (dist n ==> dist n ==> impl) (@wsat Λ Σ n E σ).
Proof.
intros [|n] E σ r1 r2 Hr rl1 rl2 Hrl; first done; intros [rs [Hdom Hv Hs Hinv]].
∃ rs; constructor; intros until 0; setoid_rewrite <-Hr; try setoid_rewrite <-Hrl; eauto.
Qed.
Global Instance wsat_ne n : Proper (dist n ==> dist n ==> iff) (@wsat Λ Σ n E σ) | 1.
Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed.
Global Instance wsat_proper' n : Proper ((≡) ==> (≡) ==> iff) (@wsat Λ Σ n E σ) | 1.
Proof. by intros E σ w1 w2 Hw wl1 wl2 Hwl; apply wsat_ne; apply equiv_dist. Qed.
Lemma wsat_proper n E1 E2 σ r1 r2 rl1 rl2 :
E1 = E2 → r1 ≡ r2 → rl1 ≡ rl2 → wsat n E1 σ r1 rl1 → wsat n E2 σ r2 rl2.
Proof. by move=>->->->. Qed.
Lemma wsat_le n n' E σ r rl : wsat n E σ r rl → n' ≤ n → wsat n' E σ r rl.
Proof.
destruct n as [|n], n' as [|n']; simpl; try by (auto with lia).
intros [rs [Hval Hσ HE Hwld]] ?; ∃ rs; constructor; auto.
intros i P ? (P'&HiP&HP')%dist_Some_inv_r'.
destruct (to_agree_uninj (S n) P') as [laterP' HlaterP'].
{ apply (lookup_validN_Some _ (wld (r ⋅ big_opM rs)) i); rewrite ?HiP; auto. }
assert (P' ≡{S n}≡ to_agree $ Next $ iProp_unfold $
iProp_fold $ later_car $ laterP') as HPiso.
{ by rewrite iProp_unfold_fold later_eta HlaterP'. }
assert (P ≡{n'}≡ iProp_fold (later_car laterP')) as HPP'.
{ apply (inj iProp_unfold), (inj Next), (inj to_agree).
by rewrite HP' -(dist_le _ _ _ _ HPiso). }
destruct (Hwld i (iProp_fold (later_car laterP'))) as (r'&?&?); auto.
{ by rewrite HiP -HPiso. }
assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto).
∃ r'; split; [done|]. apply HPP', uPred_closed with n; auto.
Qed.
Lemma wsat_weaken n E σ r rl rfl: wsat n E σ r (rl ⋅ rfl) → wsat n E σ r rl.
Proof.
destruct n as [|n]; auto.
intros [rs [Hval Hσ HE Hwld]]; ∃ rs; constructor; auto.
Qed.
Lemma wsat_valid n E σ r rl : n ≠ 0 → wsat n E σ r rl → ✓{n} (r ⋅ rl).
Proof.
destruct n; first done.
intros _ [rs ?]; eapply cmra_validN_op_l. rewrite -assoc (comm _ rl) assoc.
eapply wsat_pre_valid; eauto.
Qed.
Lemma wsat_init k E σ m ml : ✓{S k} (m ⋅ ml) → wsat (S k) E σ (Res ∅ (Excl' σ) m) (Res ∅ ∅ ml).
Proof.
intros Hv. ∃ ∅; constructor; auto.
- rewrite big_opM_empty right_id.
split_and!; try (apply cmra_valid_validN, ra_empty_valid);
constructor || apply Hv.
- by intros i; rewrite lookup_empty=>-[??].
- intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
Qed.
Lemma wsat_open n E σ r rl i P :
wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E →
wsat (S n) ({[i]} ∪ E) σ r rl → ∃ rP, wsat (S n) E σ (rP ⋅ r) rl ∧ P n rP ∅.
Proof.
intros HiP Hi [rs [Hval Hσ HE Hwld]].
destruct (Hwld i P) as (rP&?&?); [set_solver +|by apply lookup_wld_op_l; auto|].
assert (rP ⋅ r ⋅ big_opM (delete i rs) ≡ r ⋅ big_opM rs) as Hr.
{ by rewrite (comm _ rP) -assoc big_opM_delete. }
∃ rP; split; [∃ (delete i rs); constructor; rewrite ?Hr|]; auto.
- intros j; rewrite lookup_delete_is_Some Hr.
generalize (HE j); set_solver +Hi.
- intros j P'; rewrite Hr⇒ Hj ?.
setoid_rewrite lookup_delete_ne; last (set_solver +Hi Hj).
apply Hwld; [set_solver +Hj|done].
Qed.
Lemma wsat_close n E σ r rl i P rP :
wld rP !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E →
wsat (S n) E σ (rP ⋅ r) rl → P n rP ∅ → wsat (S n) ({[i]} ∪ E) σ r rl.
Proof.
intros HiP HiE [rs [Hval Hσ HE Hwld]] ?.
assert (rs !! i = None) by (apply eq_None_not_Some; naive_solver).
assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
{ by rewrite (comm _ rP) -assoc big_opM_insert. }
∃ (<[i:=rP]>rs); constructor; rewrite ?Hr; auto.
- intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
+ split. set_solver. rewrite !lookup_op HiP !op_is_Some; eauto.
+ destruct (HE j) as [Hj Hj']; auto; set_solver +Hj Hj'.
- intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst.
+ rewrite !lookup_wld_op_l ?HiP; auto⇒ HP.
apply (inj Some), (inj to_agree), (inj Next), (inj iProp_unfold) in HP.
∃ rP; split; [rewrite lookup_insert|apply HP]; auto.
+ intros. destruct (Hwld j P') as (r'&?&?); auto.
∃ r'; rewrite lookup_insert_ne; naive_solver.
Qed.
Lemma wsat_update_pst n E σ1 σ1' r rl rf :
pst r ≡{S n}≡ Excl' σ1 → wsat (S n) E σ1' (r ⋅ rf) rl →
σ1' = σ1 ∧ ∀ σ2, wsat (S n) E σ2 (update_pst σ2 r ⋅ rf) rl.
Proof.
intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in ×.
assert (pst rf ⋅ pst (big_opM rs) = ∅) as Hpst'.
{ by apply: (excl_validN_inv_l (S n) _ σ1); rewrite -Hpst_r assoc;
eauto using cmra_validN_op_r. }
assert (pst rf ⋅ pst (big_opM rs) ⋅ pst rl = ∅) as Hpst''.
{ by apply: (excl_validN_inv_l (S n) _ σ1); rewrite -Hpst_r assoc;
eauto using cmra_validN_op_r. }
assert (σ1' = σ1) as →.
{ apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
apply (inj Excl), (inj Some).
by rewrite -Hpst_r -Hpst -assoc Hpst' right_id. }
split; [done|∃ rs].
constructor; first split_and!; try rewrite /= -assoc Hpst'; auto.
simpl. by rewrite -?assoc (assoc _ (pst rf)) Hpst''.
Qed.
Lemma wsat_update_gst n E σ r rf rl m1 (P : iGst Λ Σ → Prop) :
m1 ≼{S n} gst r → m1 ~~>: P →
wsat (S n) E σ (r ⋅ rf) rl → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) rl ∧ P m2.
Proof.
intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
destruct (Hup (S n) (Some (mf ⋅ gst (rf ⋅ big_opM rs ⋅ rl)))) as (m2&?&Hval'); try done.
{ rewrite /= (assoc _ m1) -Hr assoc. solve_validN. }
∃ m2; split; [∃ rs|done].
by constructor; first split_and!; auto.
Qed.
Lemma wsat_update_gst' n E σ r rf rl rfl m1 ml1 (P : iGst Λ Σ → iGst Λ Σ → Prop) :
m1 ≼{S n} gst r → ml1 ≡{S n}≡ gst rl → m1 # ml1 ~~>>: P →
wsat (S n) E σ (r ⋅ rf) (rl ⋅ rfl) →
∃ m2 ml2, wsat (S n) E σ (update_gst m2 r ⋅ rf) (update_gst ml2 rl ⋅ rfl)
∧ P m2 ml2 ∧ rl ⤳_(S n) update_gst ml2 rl.
Proof.
intros [mf Hr] Hrl Hup [rs [(?&?&?) Hσ HE Hwld]].
destruct (Hup (S n) (Some (mf ⋅ gst (rf ⋅ big_opM rs ⋅ rfl)))) as (m2&ml2&?&Hval'&Hs); try done.
{ rewrite /= -assoc (comm _ ml1) /= (assoc _ m1) (assoc _ m1) -Hr Hrl assoc. solve_validN. }
∃ m2, ml2; split_and!; [∃ rs|done|].
- by constructor; first split_and!; auto.
- rewrite /stepN /cmra_stepN //= /res_stepN.
rewrite -(dist_le _ _ _ _ Hrl); eauto.
Qed.
Lemma wsat_alloc n E1 E2 σ r rl P rP :
¬set_finite E1 → P n rP ∅ → wsat (S n) (E1 ∪ E2) σ (rP ⋅ r) rl →
∃ i, wsat (S n) (E1 ∪ E2) σ
(Res {[i := to_agree (Next (iProp_unfold P))]} ∅ ∅ ⋅ r) rl ∧
wld r !! i = None ∧ i ∈ E1.
Proof.
intros HE1 ? [rs [Hval Hσ HE Hwld]].
assert (∃ i, i ∈ E1 ∧ wld r !! i = None ∧ wld rP !! i = None ∧
wld (big_opM rs) !! i = None ∧ wld rl !! i = None)
as (i&Hi&Hri&HrPi&Hrsi&Hrli).
{ ∃ (coPpick (E1 ∖
(dom _ (wld r) ∪ (dom _ (wld rP) ∪ (dom _ (wld (big_opM rs)) ∪ dom _ (wld rl)))))).
rewrite -!not_elem_of_dom -?not_elem_of_union -elem_of_difference.
apply coPpick_elem_of⇒HE'; eapply HE1, (difference_finite_inv _ _), HE'.
by repeat apply union_finite; apply dom_finite. }
assert (rs !! i = None).
{ apply eq_None_not_Some=>?; destruct (HE i) as [_ Hri']; auto; revert Hri'.
rewrite /= !lookup_op !op_is_Some -!not_eq_None_Some; tauto. }
assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
{ by rewrite (comm _ rP) -assoc big_opM_insert. }
∃ i; split_and?; [∃ (<[i:=rP]>rs); constructor| |]; auto.
- destruct Hval as (?&?&?). rewrite -(assoc _ _ r) Hr.
split_and!; rewrite /= ?left_id; [|eauto|eauto].
intros j; destruct (decide (j = i)) as [->|].
+ by rewrite !lookup_op Hri HrPi Hrsi Hrli !right_id lookup_singleton.
+ by rewrite -?assoc lookup_op lookup_singleton_ne // left_id ?assoc.
- by rewrite -assoc Hr /= left_id.
- intros j; rewrite -assoc Hr; destruct (decide (j = i)) as [->|].
+ intros _; split; first set_solver +Hi.
rewrite /= !lookup_op lookup_singleton !op_is_Some; eauto.
+ rewrite lookup_insert_ne //.
rewrite lookup_op lookup_singleton_ne // left_id; eauto.
- intros j P'; rewrite -assoc Hr; destruct (decide (j=i)) as [->|].
+ rewrite /= !lookup_op Hri HrPi Hrsi right_id lookup_singleton=>? HP.
apply (inj Some), (inj to_agree), (inj Next), (inj iProp_unfold) in HP.
∃ rP; rewrite lookup_insert; split; [|apply HP]; auto.
+ rewrite /= lookup_op lookup_singleton_ne // left_id⇒ ??.
destruct (Hwld j P') as [r' ?]; auto.
by ∃ r'; rewrite lookup_insert_ne.
Qed.
End wsat.