Finish `flocked_inv_open`.

theories/lib/flock.v

@@ -407,30 +407,8 @@ Section flock.
         by rewrite to_props_map_delete.
   Qed.
 
-  Lemma newflock_spec :
-    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
-  Proof.
-    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
-    iMod (own_alloc (● (Excl' Unlocked) ⋅ ◯ (Excl' Unlocked)))
-      as (γ_state) "[Hauth Hfrag]"; first done.
-    iMod (own_alloc (● to_props_map ∅)) as (γ_props) "Hprops".
-    { apply auth_valid_discrete. simpl.
-      split; last done. apply ucmra_unit_least. }
-    iMod (own_alloc ((● Excl' ∅) ⋅ (◯ Excl' ∅))) as (γ_ac_props) "[Hacprops1 Hacprops2]".
-    { apply auth_valid_discrete. simpl.
-      split; last done. by rewrite left_id. }
-    iApply (newlock_spec lockN (own γ_state (◯ (Excl' Unlocked))) with "Hfrag").
-    iNext. iIntros (lk γ_lock) "#Hlock".
-    pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
-    iMod (inv_alloc invN _ (flock_inv γ) with "[-HΦ]") as "#Hinv".
-    { iNext. iExists Unlocked, ∅, ∅. rewrite /from_active fmap_empty right_id. iFrame.
-      iSplit; eauto. by rewrite /all_tokens big_sepM_empty. }
-    iModIntro. iApply ("HΦ" $! lk γ with "[-]").
-    rewrite /is_flock. by iFrame "Hlock".
-  Qed.
-
   (** `flocked` supports invariant access just like regular invariants *)
-  Lemma flocked_inv_open E i X γ I :
+  Lemma flocked_inv_open_single E i X γ I :
     ↑resN ⊆ E →
     I !! i = Some X →
     flocked γ I ={E}=∗
@@ -456,6 +434,68 @@ Section flock.
     iApply "Htokens". by iFrame.
   Qed.
 
+  Lemma flocked_inv_open E γ I :
+    ↑resN ⊆ E →
+    flocked γ I ={E}=∗
+    ▷ ([∗ map] s ↦ X ∈ I, res_prop X) ∗
+   (▷ ([∗ map] s ↦ X ∈ I, res_prop X) ={E}=∗ flocked γ I).
+  Proof.
+    iIntros (?). rewrite {1}/flocked.
+    iDestruct 1 as (fa ?) "(Hst & Hfa & Htokens)".
+    rewrite !big_sepM_sepM.
+    iDestruct "Htokens" as "(T2s & Hinvs & Hρs)".
+    rewrite /flocked -(bi.exist_intro fa).
+    iAssert (⌜fa = (λ X, (res_frac X, res_name X)) <$> I⌝)%I as "$".
+    { eauto. }
+    iFrame "Hst Hfa". subst fa.
+    iInduction I as [|s X I Hs] "IH" using map_ind.
+    - rewrite /flocked !big_sepM_empty. eauto with iFrame.
+    - rewrite !big_sepM_insert //.
+      iDestruct "T2s"   as "[T2 T2s]".
+      iDestruct "Hinvs" as "[#Hinv Hinvs]".
+      iDestruct "Hρs"   as "[Hρ Hρs]".
+      iMod ("IH" with "T2s Hinvs Hρs") as "[$ IH']".
+      iClear "IH".
+
+      (* The main induction step *)
+      iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
+      rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
+      { iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
+      iMod ("Hcl" with "[T2]") as "_".
+      { iNext. iRight. done. }
+      iModIntro. iFrame "HR". iIntros "[HR HRs]".
+      iMod ("IH'" with "HRs") as "$".
+
+      iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
+      iDestruct "HC" as "[[? >T1'] | >$]".
+      { iDestruct (own_valid_2 with "T1 T1'") as %?. done. }
+      iMod ("Hcl" with "[T1 HR]") as "_".
+      { iNext. iLeft. iFrame. }
+      iModIntro. by iFrame.
+  Qed.
+
+  Lemma newflock_spec :
+    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
+    iMod (own_alloc (● (Excl' Unlocked) ⋅ ◯ (Excl' Unlocked)))
+      as (γ_state) "[Hauth Hfrag]"; first done.
+    iMod (own_alloc (● to_props_map ∅)) as (γ_props) "Hprops".
+    { apply auth_valid_discrete. simpl.
+      split; last done. apply ucmra_unit_least. }
+    iMod (own_alloc ((● Excl' ∅) ⋅ (◯ Excl' ∅))) as (γ_ac_props) "[Hacprops1 Hacprops2]".
+    { apply auth_valid_discrete. simpl.
+      split; last done. by rewrite left_id. }
+    iApply (newlock_spec lockN (own γ_state (◯ (Excl' Unlocked))) with "Hfrag").
+    iNext. iIntros (lk γ_lock) "#Hlock".
+    pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
+    iMod (inv_alloc invN _ (flock_inv γ) with "[-HΦ]") as "#Hinv".
+    { iNext. iExists Unlocked, ∅, ∅. rewrite /from_active fmap_empty right_id. iFrame.
+      iSplit; eauto. by rewrite /all_tokens big_sepM_empty. }
+    iModIntro. iApply ("HΦ" $! lk γ with "[-]").
+    rewrite /is_flock. by iFrame "Hlock".
+  Qed.
+
   Lemma acquire_flock_single_spec γ lk i X :
     {{{ is_flock γ lk ∗ flock_res γ i X }}}
       acquire lk