Minor cleanup

theories/examples/exchanger/proof_graph_resource.v

@@ -171,8 +171,7 @@ Proof.
       iFrame "P". iExists γb. by iFrame "EL' II". }
     iIntros "HΦ !>". iSplitR "GA I' Ps".
     - iIntros "_ !>". iApply "HΦ". iIntros ([]). lia.
-    - iNext. iExists G'. iFrame "I'".
-      rewrite {2}/to_set EqL set_seq_S_end_union_L /= Eqe1. iFrame "GA".
+    - iNext. iExists G'. rewrite EqG' to_set_append -Eqe1. iFrame "I' GA".
       rewrite {2}/TradeResources EqG' big_sepL_app Eqso' big_sepL_singleton.
       iFrame "Ps". iIntros (?). lia. }
 
@@ -229,8 +228,7 @@ Proof.
     iIntros "HΦ !>".
     iSplitR "GA I' Ps".
     + iIntros "_ !>". iApply "HΦ". iIntros ([_ ?]). lia.
-    + iNext. iExists G'. iFrame "I' Ps".
-      rewrite {2}/to_set EqL set_seq_S_end_union_L /= Eqe1. iFrame "GA".
+    + iNext. iExists G'. rewrite EqG' to_set_append -Eqe1. iFrame "I' Ps GA".
 
   - (* my event is earlier. First put P v1 in our invariant to close it. *)
     destruct F' as (Lt12 & ? & Eqso' & Eqco').
@@ -239,8 +237,7 @@ Proof.
       iSplit; [done|]. iExists γb. by iFrame "EL' II". }
     iIntros "HΦ !>".
     iSplitR "Ps P GA I'"; last first.
-    { iNext. iExists G'. iFrame "I'".
-      rewrite {2}/to_set EqL set_seq_S_end_union_L /= Eqe1. iFrame "GA".
+    { iNext. iExists G'. rewrite EqG' to_set_append -Eqe1. iFrame "I' GA".
       rewrite /TradeResources EqG' big_sepL_app Eqso' big_sepL_singleton.
       iFrame "Ps". iIntros (_). iLeft. rewrite EqV. iFrame "P". }
 

theories/examples/queue/proof_mp_graph.v

@@ -109,18 +109,13 @@ Proof using All.
                         EsG' & SoG' & ComG' & EqM' & _).
     rewrite /is_enqueue in IQ. subst enq.
     iDestruct (own_valid_2 with "nodesA nodes") as %EqL%excl_auth_agree_L.
-    inversion EqL as [EQL]. apply to_set_empty in EQL.
-    have EqL' : length G.(Es) = O by rewrite EQL.
+    inversion EqL as [EQL].
 
     iMod (own_update_2 with "nodesA nodes") as "[nodesA nodes]".
     { apply (excl_auth_update _ _ (GSet {[enqId]})). }
     iIntros "!>".
     iSplitL "QI' nodesA".
-    { iNext. iExists G'.
-      (* TODO: cleanup *)
-      rewrite /to_set EsG' app_length /= Nat.add_1_r set_seq_S_end_union_L
-              MAX' EqL' /= right_id_L.
-      iFrame. }
+    { iNext. iExists G'. rewrite EsG' to_set_append EQL right_id_L -MAX'. iFrame. }
 
     iIntros "_". wp_seq.
     wp_apply (push_spec _ _ _ 2 _ (λ _, True%I) with "[-$S]"); [|auto].

theories/examples/queue/proof_per_elem_graph.v

@@ -76,10 +76,8 @@ Proof.
                     EsG' & SoG' & ComG' & EqM' & NInM0).
   rewrite /is_enqueue in IQ. subst enq.
 
-  have EqL: length G'.(Es) = S (length G.(Es)).
-  { rewrite EsG' app_length /=. lia. }
   have Eqts : to_set G'.(Es) = {[enqId]} ∪ to_set G.(Es).
-  { by rewrite {1}/to_set EqL set_seq_S_end_union_L /= Eqenq. }
+  { by rewrite EsG' to_set_append -Eqenq. }
   have EqEm' : G'.(Es) !! enqId = Some (mkGraphEvent (Enq x) Venq M').
   { by rewrite EsG' Eqenq lookup_app_1_eq. }
 
@@ -145,10 +143,8 @@ Proof.
       iDestruct (view_at_elim with "sV' Local") as "Local".
       iExists _, _. by iFrame. }
 
-    have EqL : length G'.(Es) = S (length G.(Es)).
-    { rewrite EsG' app_length /=. lia. }
     have Eqts : to_set G'.(Es) = {[deqId]} ∪ to_set G.(Es).
-    { by rewrite /to_set EqL set_seq_S_end_union_L /= Eqdeq. }
+    { by rewrite EsG' to_set_append -Eqdeq. }
     have EqEm' : G'.(Es) !! deqId = Some (mkGraphEvent EmpDeq Vdeq M').
     { rewrite EsG' Eqdeq lookup_app_1_eq. by subst deq. }
 
@@ -179,10 +175,8 @@ Proof.
 
   have ?: enqId ≠ deqId.
   { intros ?. subst deqId enqId. apply lookup_lt_Some in EqEId. lia. }
-  have EqL : length G'.(Es) = S (length G.(Es)).
-  { rewrite EsG' app_length /=. lia. }
   have Eqts : to_set G'.(Es) = {[deqId]} ∪ to_set G.(Es).
-  { by rewrite /to_set EqL set_seq_S_end_union_L /= Eqdeq. }
+  { by rewrite EsG' to_set_append -Eqdeq. }
   have EqDm' : G'.(Es) !! deqId = Some (mkGraphEvent (Deq x) Vdeq M').
   { by rewrite EsG' Eqdeq lookup_app_1_eq. }
   have EqEm' : G'.(Es) !! enqId = Some (mkGraphEvent (Enq x) Venq Menq).
@@ -201,7 +195,7 @@ Proof.
     rewrite -big_sepS_union; last first.
     { apply disjoint_singleton_l.
       move => /elem_of_filter [[? FA] InG']. apply (FA deqId).
-      - apply elem_of_set_seq. rewrite EqL Eqdeq. clear; lia.
+      - rewrite Eqts. set_solver-.
       - rewrite SoG'. clear. set_solver. }
     iApply (big_sepS_mono' with "Elems"); last first.
     { rewrite Eqts filter_union_L filter_singleton_not_L; last first.

theories/examples/set_helper.v

@@ -26,4 +26,9 @@ Section set_seq.
           set_solver.
     - intros [-> ->]. by rewrite set_seq_S_end_union_L, (right_id_L _ _).
   Qed.
+
+  Lemma to_set_append E e : to_set (E ++ [e]) = {[ length E ]} ∪ to_set E.
+  Proof.
+    unfold to_set. by rewrite app_length, Nat.add_1_r, set_seq_S_end_union_L.
+  Qed.
 End set_seq.

theories/examples/stack/proof_mp_client.v

@@ -100,16 +100,13 @@ Section Stack.
                         EsG' & SoG' & ComG' & EqM' & _).
       rewrite / is_push in IQ. subst push.
       iDestruct (own_valid_2 with "nodesA nodes") as %EqL%excl_auth_agree_L.
-      inversion EqL as [EQL]. apply to_set_empty in EQL.
-      have EqL' : length G.(Es) = O by rewrite EQL.
+      inversion EqL as [EQL].
 
       iMod (own_update_2 with "nodesA nodes") as "[nodesA nodes]".
       { apply (excl_auth_update _ _ (GSet {[pushId]})). }
       iIntros "!>".
       iSplitL "SI' nodesA".
-      { iNext. iExists G'.
-        rewrite /to_set EsG' app_length /= Nat.add_1_r set_seq_S_end_union_L
-                MAX' EqL' /= right_id_L.
+      { iNext. iExists G'. rewrite EsG' to_set_append -MAX' EQL right_id_L.
         iFrame. }
       iIntros "_". wp_seq.
       wp_apply (enqueue_spec _ _ _ 2 _ (λ _, True%I) with "[-$Q]"); [|auto].