From 4dee0de28f2879d81f1304470d653b367670ddc7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Mar 2017 13:35:59 +0100
Subject: [PATCH] Better `iDestruct` support for big ops. This fixes issue #76.

---
 theories/base_logic/big_op.v         | 10 ++++
 theories/base_logic/lib/boxes.v      | 14 ++---
 theories/program_logic/adequacy.v    | 13 +++--
 theories/proofmode/class_instances.v | 81 +++++++++-------------------
 4 files changed, 48 insertions(+), 70 deletions(-)

diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 215568a46..8dfa1f983 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -202,6 +202,8 @@ Section list.
 
   Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ True.
   Proof. done. Qed.
+  Lemma big_sepL_nil' P Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y.
+  Proof. apply True_intro. Qed.
   Lemma big_sepL_cons Φ x l :
     ([∗ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∗ [∗ list] k↦y ∈ l, Φ (S k) y.
   Proof. by rewrite big_opL_cons. Qed.
@@ -362,6 +364,8 @@ Section gmap.
 
   Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True.
   Proof. by rewrite big_opM_empty. Qed.
+  Lemma big_sepM_empty' P Φ : P ⊢ [∗ map] k↦x ∈ ∅, Φ 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.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 413fbdd5d..5104c7f90 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -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".
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 6f442eb45..1227a4219 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -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.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index d2b7bc298..9ff78cf40 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -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.
-- 
GitLab