More flock.v cleaning

- Use all_props lemmas

theories/lib/flock.v

@@ -112,6 +112,8 @@ Section flock.
   Definition flock_res_single (γ : flock_name) (s : prop_id) (R : iProp Σ) : iProp Σ :=
     (own (flock_props_name γ) (◯ {[ s := to_agree R ]}))%I.
 
+  (** **************************************** *)
+  (** to_props_map lemmas *)
   Lemma to_props_map_insert f i P :
     to_props_map (<[i:=P]>f) = <[i:=to_agree P]>(to_props_map f).
   Proof. by rewrite /to_props_map fmap_insert. Qed.
@@ -127,9 +129,18 @@ Section flock.
   Lemma to_props_map_singleton s R : to_props_map {[s := R]} = {[s := to_agree R]}.
   Proof. by rewrite /to_props_map map_fmap_singleton. Qed.
 
+  (** all_props lemmas *)
+  Lemma all_props_empty : all_props ∅.
+  Proof. by rewrite /all_props bi.big_sepM_empty. Qed.
+
   Lemma all_props_singleton s R : all_props {[s := R]} ≡ R.
   Proof. by rewrite /all_props bi.big_sepM_singleton. Qed.
 
+  Lemma all_props_insert s (R : iProp Σ) f :
+    f !! s = None →
+    all_props (<[s := R]>f) ≡ (R ∗ all_props f)%I.
+  Proof. intros ?. rewrite /all_props bi.big_sepM_insert //. Qed.
+
   Lemma all_props_union f g :
     all_props f ∗ all_props g ⊢ all_props (f ∪ g).
   Proof.
@@ -185,6 +196,8 @@ Section flock.
       by apply bi.sep_proper.
   Qed.
 
+  (** **************************************** *)
+  (** rules & properties of the predicates *)
   Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk).
   Proof. apply _. Qed.
 
@@ -237,7 +250,7 @@ Section flock.
       iExists s. iFrame "Hres Hunfl".
       iMod ("Hcl" with "[-]") as "_".
       { iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2".
-        rewrite /all_props bi.big_sepM_insert. iFrame.
+        iApply all_props_insert; last iFrame.
         apply (not_elem_of_dom _ s (D:=gset prop_id)).
         revert Hs. rewrite dom_union_L not_elem_of_union. set_solver. }
       iModIntro. iPureIntro.
@@ -266,7 +279,7 @@ Section flock.
       iMod ("Hcl" with "[-]") as "_".
       { iNext. iExists _,∅,_. rewrite left_id. iFrame. iFrame "Hactive".
         iSplit; auto.
-        rewrite /all_props bi.big_sepM_insert. iFrame.
+        iApply all_props_insert; last by iFrame.
         by apply (not_elem_of_dom _ s (D:=gset prop_id)). }
       iModIntro. iPureIntro.
       clear Hs. intros Hs.
@@ -281,7 +294,7 @@ Section flock.
     iMod (flock_res_single_alloc_unflocked ∅ with "Hlk Hunfl HR") as (s ?) "[HR $]".
     iModIntro. iExists {[s := R]}.
     rewrite /flock_res_single to_props_map_singleton. iFrame "HR".
-    iPureIntro. by rewrite /all_props bi.big_sepM_singleton.
+    iPureIntro. symmetry. apply all_props_singleton.
   Qed.
 
   Lemma flock_res_insert_unflocked γ lk π P R :
@@ -311,9 +324,9 @@ Section flock.
         remember (to_props_map f !! i) as o. rewrite -Heqo.
         by destruct o. }
     rewrite Hmerge. iFrame "HR".
-    iPureIntro. rewrite /all_props bi.big_sepM_insert; last first.
+    iPureIntro. rewrite all_props_insert.
+    - by rewrite comm Hfeq.
     - by apply (not_elem_of_dom (D:=gset prop_id)).
-    - rewrite comm Hfeq /all_props. reflexivity.
   Qed.
 
   Lemma newlock_cancel_spec :
@@ -334,7 +347,7 @@ Section flock.
        (fun γ => flock_inv (Build_flock_name γ_lock γ γ_state γ_props γ_ac_props)) with "[-HΦ]") as (γ_cinv) "(_ & #Hcinv & Hown)".
     { iNext. rewrite /flock_inv /=. iIntros (γ _).
       iExists Unlocked, ∅, ∅. rewrite left_id. iFrame.
-      by rewrite /all_props !bi.big_sepM_empty. }
+      iSplit; auto. iApply all_props_empty. }
     pose (γ := (Build_flock_name γ_lock γ_cinv γ_state γ_props γ_ac_props)).
     iModIntro. iApply ("HΦ" $! lk γ with "[-]"). iFrame "Hown".
     rewrite /is_flock. by iFrame "Hlock".
@@ -351,14 +364,15 @@ Section flock.
       as %[Hfoo _]%auth_valid_discrete.
     iPureIntro. revert Hfoo. simpl. rewrite left_id.
     rewrite lookup_included. intros Hffp.
-    exists (fp ∖ f). rewrite Heq /all_props. revert Hffp.
+    exists (fp ∖ f). rewrite Heq. clear Heq. revert Hffp.
     simple refine (map_ind (fun f => (∀ i, _) → _ ≡ _) _ _ f); simpl.
     - (* TODO: this should be somewhere in std++ *)
       assert (fp ∖ ∅ = fp) as ->.
       { apply map_eq=>i. remember (fp !! i) as XX. destruct XX.
         - apply lookup_difference_Some. eauto.
         - apply lookup_difference_None. eauto. }
-      by rewrite bi.big_sepM_empty left_id.
+      intros _. iSplit; [iIntros "$" | iIntros "[_ $]"].
+      iApply all_props_empty.
     - intros i P f' Hi IH Hffp. rewrite IH; last first.
       { intros j. specialize (Hffp j).
         destruct (decide (i = j)) as [->|?].
@@ -366,7 +380,7 @@ Section flock.
           apply option_included. eauto.
         - revert Hffp.
           rewrite !to_props_map_lookup lookup_insert_ne; auto. }
-      rewrite bi.big_sepM_insert; last assumption.
+      rewrite all_props_insert; last assumption.
       specialize (Hffp i). revert Hffp.
       rewrite !to_props_map_lookup lookup_insert; auto. simpl.
       rewrite option_included.
@@ -386,7 +400,7 @@ Section flock.
         - rewrite lookup_insert_ne; auto.
           unfold difference, map_difference; rewrite !lookup_difference_with.
           rewrite lookup_insert_ne; auto. }
-      rewrite bi.big_sepM_insert; last first.
+      rewrite all_props_insert; last first.
       { apply lookup_difference_None. left. apply lookup_delete. }
       assert ((<[i:=Q]> (delete i fp) ∖ <[i:=P]> f') = (delete i fp ∖ f')) as ->.
       { apply map_eq=>j. destruct (decide (i = j)) as [->|?].
@@ -424,7 +438,7 @@ Section flock.
       destruct Hfoo as [f' Hf'].
       iMod ("Hcl" with "[Hstate Hcown Hlocked Hauth Hfactive]") as "_".
       { iNext. iExists (Locked π),∅,fa. rewrite left_id. iFrame.
-        by rewrite /all_props bi.big_sepM_empty. }
+        iApply all_props_empty. }
       iModIntro. rewrite Hf'. iDestruct "Hfa" as "[HR Hf']".
       iApply ("HΦ" $! fa). iFrame.
       iApply bi.later_wand. iNext. iIntros "HR".