Commit 4dee0de2 authored by Robbert Krebbers's avatar Robbert Krebbers

Better `iDestruct` support for big ops. This fixes issue #76.

parent 8b23578e
......@@ -202,6 +202,8 @@ Section list.
Lemma big_sepL_nil Φ : ([ list] ky nil, Φ k y) ⊣⊢ True.
Proof. done. Qed.
Lemma big_sepL_nil' P Φ : P [ list] ky nil, Φ k y.
Proof. apply True_intro. Qed.
Lemma big_sepL_cons Φ x l :
([ list] ky x :: l, Φ k y) ⊣⊢ Φ 0 x [ list] ky l, Φ (S k) y.
Proof. by rewrite big_opL_cons. Qed.
......@@ -362,6 +364,8 @@ Section gmap.
Lemma big_sepM_empty Φ : ([ map] kx , Φ k x) ⊣⊢ True.
Proof. by rewrite big_opM_empty. Qed.
Lemma big_sepM_empty' P Φ : P [ map] kx , Φ k x.
Proof. rewrite big_sepM_empty. apply True_intro. Qed.
Lemma big_sepM_insert Φ m i x :
m !! i = None
......@@ -525,6 +529,8 @@ Section gset.
Lemma big_sepS_empty Φ : ([ set] x , Φ x) ⊣⊢ True.
Proof. by rewrite big_opS_empty. Qed.
Lemma big_sepS_empty' P Φ : P [ set] x , Φ x.
Proof. rewrite big_sepS_empty. apply True_intro. Qed.
Lemma big_sepS_insert Φ X x :
x X ([ set] y {[ x ]} X, Φ y) ⊣⊢ (Φ x [ set] y X, Φ y).
......@@ -674,6 +680,8 @@ Section gmultiset.
Lemma big_sepMS_empty Φ : ([ mset] x , Φ x) ⊣⊢ True.
Proof. by rewrite big_opMS_empty. Qed.
Lemma big_sepMS_empty' P Φ : P [ mset] x , Φ x.
Proof. rewrite big_sepMS_empty. apply True_intro. Qed.
Lemma big_sepMS_union Φ X Y :
([ mset] y X Y, Φ y) ⊣⊢ ([ mset] y X, Φ y) [ mset] y Y, Φ y.
......@@ -730,3 +738,5 @@ Section gmultiset.
Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
End big_op.
Hint Resolve big_sepL_nil' big_sepM_empty' big_sepS_empty' big_sepMS_empty' | 0.
......@@ -14,8 +14,7 @@ Class boxG Σ :=
Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) *
optionRF (agreeRF ( )) ) ].
Instance subG_stsΣ Σ :
subG boxΣ Σ boxG Σ.
Instance subG_stsΣ Σ : subG boxΣ Σ boxG Σ.
Proof. solve_inG. Qed.
Section box_defs.
......@@ -210,8 +209,8 @@ Proof.
rewrite internal_eq_iff later_iff big_sepM_later.
iDestruct ("HeqP" with "HP") as "HP".
iCombine "Hf" "HP" as "Hf".
rewrite big_sepM_fmap; iApply (fupd_big_sepM _ _ f).
iApply (big_sepM_impl _ _ f); iFrame "Hf".
rewrite -big_sepM_sepM big_sepM_fmap; iApply (fupd_big_sepM _ _ f).
iApply (@big_sepM_impl with "[$Hf]").
iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]" "Hclose".
iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
......@@ -224,9 +223,10 @@ Lemma box_empty E f P :
box N f P ={E}= P box N (const false <$> f) P.
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iAssert ([ map] γ↦b f, Φ γ box_own_auth γ ( Excl' false)
box_own_prop γ (Φ γ) inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
{ iApply (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
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_sepM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto.
iInv N as (b) "[>Hγ HΦ]" "Hclose".
......
......@@ -87,11 +87,10 @@ Proof.
iIntros (Hstep) "(HW & He & Ht)".
destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
- iExists e2', (t2' ++ efs); iSplitR; first eauto.
rewrite big_sepL_app. iFrame "Ht". iApply wp_step; try iFrame; eauto.
iFrame "Ht". iApply wp_step; eauto with iFrame.
- iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
rewrite !big_sepL_app !big_sepL_cons big_sepL_app.
iDestruct "Ht" as "($ & He' & $)"; iFrame "He".
iApply wp_step; try iFrame; eauto.
iDestruct "Ht" as "($ & He' & $)". iFrame "He".
iApply wp_step; eauto with iFrame.
Qed.
Lemma wptp_steps n e1 t1 t2 σ1 σ2 Φ :
......@@ -177,14 +176,14 @@ Proof.
rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]".
iModIntro. iNext. iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto.
iFrame. by iApply big_sepL_nil.
by iFrame.
- intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]".
iModIntro. iNext. iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto.
iFrame. by iApply big_sepL_nil.
by iFrame.
Qed.
Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
......@@ -201,5 +200,5 @@ Proof.
rewrite {1}fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
iModIntro. iNext. iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto.
iFrame "Hw HE Hwp HIstate Hclose". by iApply big_sepL_nil.
by iFrame.
Qed.
......@@ -343,27 +343,13 @@ Global Instance from_sep_bupd P Q1 Q2 :
FromSep P Q1 Q2 FromSep (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
Global Instance from_sep_big_sepL {A} (Φ Ψ1 Ψ2 : nat A uPred M) l :
( k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x))
FromSep ([ list] k x l, Φ k x)
([ list] k x l, Ψ1 k x) ([ list] k x l, Ψ2 k x).
Proof. rewrite /FromSep=>?. rewrite -big_sepL_sepL. by apply big_sepL_mono. Qed.
Global Instance from_sep_big_sepM
`{Countable K} {A} (Φ Ψ1 Ψ2 : K A uPred M) m :
( k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x))
FromSep ([ map] k x m, Φ k x)
([ map] k x m, Ψ1 k x) ([ map] k x m, Ψ2 k x).
Proof. rewrite /FromSep=>?. rewrite -big_sepM_sepM. by apply big_sepM_mono. Qed.
Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A uPred M) X :
( x, FromSep (Φ x) (Ψ1 x) (Ψ2 x))
FromSep ([ set] x X, Φ x) ([ set] x X, Ψ1 x) ([ set] x X, Ψ2 x).
Proof. rewrite /FromSep=>?. rewrite -big_sepS_sepS. by apply big_sepS_mono. Qed.
Global Instance from_sep_big_sepMS `{Countable A} (Φ Ψ1 Ψ2 : A uPred M) X :
( x, FromSep (Φ x) (Ψ1 x) (Ψ2 x))
FromSep ([ mset] x X, Φ x) ([ mset] x X, Ψ1 x) ([ mset] x X, Ψ2 x).
Proof.
rewrite /FromSep=> ?. rewrite -big_sepMS_sepMS. by apply big_sepMS_mono.
Qed.
Global Instance from_sep_big_sepL_cons {A} (Φ : nat A uPred M) x l :
FromSep ([ list] k y x :: l, Φ k y) (Φ 0 x) ([ list] k y l, Φ (S k) y).
Proof. by rewrite /FromSep big_sepL_cons. Qed.
Global Instance from_sep_big_sepL_app {A} (Φ : nat A uPred M) l1 l2 :
FromSep ([ list] k y l1 ++ l2, Φ k y)
([ list] k y l1, Φ k y) ([ list] k y l2, Φ (length l1 + k) y).
Proof. by rewrite /FromSep big_sepL_app. Qed.
(* FromOp *)
Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a b) a b.
......@@ -424,41 +410,14 @@ Global Instance into_and_laterN n p P Q1 Q2 :
IntoAnd p P Q1 Q2 IntoAnd p (^n P) (^n Q1) (^n Q2).
Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?laterN_and ?laterN_sep. Qed.
Global Instance into_and_big_sepL {A} (Φ Ψ1 Ψ2 : nat A uPred M) p l :
( k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x))
IntoAnd p ([ list] k x l, Φ k x)
([ list] k x l, Ψ1 k x) ([ list] k x l, Ψ2 k x).
Proof.
rewrite /IntoAnd=> HΦ. destruct p.
- rewrite -big_sepL_and. apply big_sepL_mono; auto.
- rewrite -big_sepL_sepL. apply big_sepL_mono; auto.
Qed.
Global Instance into_and_big_sepM
`{Countable K} {A} (Φ Ψ1 Ψ2 : K A uPred M) p m :
( k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x))
IntoAnd p ([ map] k x m, Φ k x)
([ map] k x m, Ψ1 k x) ([ map] k x m, Ψ2 k x).
Proof.
rewrite /IntoAnd=> HΦ. destruct p.
- rewrite -big_sepM_and. apply big_sepM_mono; auto.
- rewrite -big_sepM_sepM. apply big_sepM_mono; auto.
Qed.
Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A uPred M) p X :
( x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x))
IntoAnd p ([ set] x X, Φ x) ([ set] x X, Ψ1 x) ([ set] x X, Ψ2 x).
Proof.
rewrite /IntoAnd=> HΦ. destruct p.
- rewrite -big_sepS_and. apply big_sepS_mono; auto.
- rewrite -big_sepS_sepS. apply big_sepS_mono; auto.
Qed.
Global Instance into_and_big_sepMS `{Countable A} (Φ Ψ1 Ψ2 : A uPred M) p X :
( x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x))
IntoAnd p ([ mset] x X, Φ x) ([ mset] x X, Ψ1 x) ([ mset] x X, Ψ2 x).
Proof.
rewrite /IntoAnd=> HΦ. destruct p.
- rewrite -big_sepMS_and. apply big_sepMS_mono; auto.
- rewrite -big_sepMS_sepMS. apply big_sepMS_mono; auto.
Qed.
Global Instance into_and_big_sepL_cons {A} p (Φ : nat A uPred M) x l :
IntoAnd p ([ list] k y x :: l, Φ k y)
(Φ 0 x) ([ list] k y l, Φ (S k) y).
Proof. apply mk_into_and_sep. by rewrite big_sepL_cons. Qed.
Global Instance into_and_big_sepL_app {A} p (Φ : nat A uPred M) l1 l2 :
IntoAnd p ([ list] k y l1 ++ l2, Φ k y)
([ list] k y l1, Φ k y) ([ list] k y l2, Φ (length l1 + k) y).
Proof. apply mk_into_and_sep. by rewrite big_sepL_app. Qed.
(* Frame *)
Global Instance frame_here R : Frame R R True.
......@@ -480,6 +439,16 @@ Global Instance frame_sep_r R P1 P2 Q Q' :
Frame R P2 Q MakeSep P1 Q Q' Frame R (P1 P2) Q' | 10.
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc (comm _ R) assoc. Qed.
Global Instance frame_big_sepL_cons {A} (Φ : nat A uPred M) R Q x l :
Frame R (Φ 0 x [ list] k y l, Φ (S k) y) Q
Frame R ([ list] k y x :: l, Φ k y) Q.
Proof. by rewrite /Frame big_sepL_cons. Qed.
Global Instance frame_big_sepL_app {A} (Φ : nat A uPred M) R Q l1 l2 :
Frame R (([ list] k y l1, Φ k y)
[ list] k y l2, Φ (length l1 + k) y) Q
Frame R ([ list] k y l1 ++ l2, Φ k y) Q.
Proof. by rewrite /Frame big_sepL_app. Qed.
Class MakeAnd (P Q PQ : uPred M) := make_and : P Q ⊣⊢ PQ.
Global Instance make_and_true_l P : MakeAnd True P P.
Proof. by rewrite /MakeAnd left_id. Qed.
......
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