Commit b11b0f04 authored by Robbert Krebbers's avatar Robbert Krebbers

Refactor proofs for `|={E}=>` commuting with bigops, and make names consistent.

parent aa5a89e0
......@@ -210,7 +210,7 @@ Proof.
iEval (rewrite internal_eq_iff later_iff big_sepM_later) in "HeqP".
iDestruct ("HeqP" with "HP") as "HP".
iCombine "Hf" "HP" as "Hf".
rewrite -big_sepM_sep big_opM_fmap; iApply (fupd_big_sepM _ _ f).
rewrite -big_sepM_sep big_opM_fmap; iApply (big_sepM_fupd _ _ f).
iApply (@big_sepM_impl with "Hf").
iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]".
......@@ -227,7 +227,7 @@ Proof.
iAssert (([ map] γ↦b f, Φ γ)
[ map] γ↦b f, box_own_auth γ ( Excl' false) box_own_prop γ (Φ γ)
inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
{ rewrite -big_sepM_sep -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
{ rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto.
iInv N as (b) "[>Hγ HΦ]".
......
......@@ -308,24 +308,23 @@ Section fupd_derived.
Lemma fupd_sep E P Q : (|={E}=> P) (|={E}=> Q) ={E}= P Q.
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
Lemma fupd_big_sepL {A} E (Φ : nat A PROP) (l : list A) :
Global Instance fupd_homomorphism E :
MonoidHomomorphism bi_sep bi_sep (flip ()) (fupd (PROP:=PROP) E E).
Proof. split; [split|]; try apply _. apply fupd_sep. apply fupd_intro. Qed.
Lemma big_sepL_fupd {A} E (Φ : nat A PROP) l :
([ list] kx l, |={E}=> Φ k x) ={E}= [ list] kx l, Φ k x.
Proof.
apply (big_opL_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K A PROP) (m : gmap K A) :
Proof. by rewrite (big_opL_commute _). Qed.
Lemma big_sepM_fupd `{Countable K} {A} E (Φ : K A PROP) m :
([ map] kx m, |={E}=> Φ k x) ={E}= [ map] kx m, Φ k x.
Proof.
apply (big_opM_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_big_sepS `{Countable A} E (Φ : A PROP) X :
Proof. by rewrite (big_opM_commute _). Qed.
Lemma big_sepS_fupd `{Countable A} E (Φ : A PROP) X :
([ set] x X, |={E}=> Φ x) ={E}= [ set] x X, Φ x.
Proof.
apply (big_opS_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Proof. by rewrite (big_opS_commute _). Qed.
Lemma big_sepMS_fupd `{Countable A} E (Φ : A PROP) l :
([ mset] x l, |={E}=> Φ x) |={E}=> [ mset] x l, Φ x.
Proof. by rewrite (big_opMS_commute _). Qed.
(** Fancy updates that take a step derived rules. *)
Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}=> P) - (P - Q) - |={E1,E2,E3}=> Q.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment