From 0cf2bdf742287d9acdecd222c466772e2fa000ae Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 26 Aug 2020 17:48:04 +0200
Subject: [PATCH] Clean-up

---
 theories/examples/list_rev.v | 22 ++++++----------------
 theories/utils/llist.v       | 15 ++++++---------
 2 files changed, 12 insertions(+), 25 deletions(-)

diff --git a/theories/examples/list_rev.v b/theories/examples/list_rev.v
index f6de705..038a8de 100644
--- a/theories/examples/list_rev.v
+++ b/theories/examples/list_rev.v
@@ -25,12 +25,8 @@ Section list_rev_example.
     {{{ RET #(); c ↣ prot }}}.
   Proof.
     iIntros (Φ) "Hc HΦ".
-    wp_lam.
-    wp_recv (l vs) as "Hl".
-    wp_apply (lreverse_spec with "Hl").
-    iIntros "Hl".
-    wp_send with "[$Hl]".
-    iApply ("HΦ" with "Hc").
+    wp_lam. wp_recv (l vs) as "Hl". wp_apply (lreverse_spec with "Hl").
+    iIntros "Hl". wp_send with "[$Hl]". iApply ("HΦ" with "Hc").
   Qed.
 
   Lemma llist_split {T} (IT : T → val → iProp Σ) xs l :
@@ -50,8 +46,7 @@ Section list_rev_example.
       + by iDestruct (big_sepL2_nil_inv_l with "HIT") as %->.
       + iDestruct (big_sepL2_cons_inv_l with "HIT") as (v vs' ->) "[HIT HITs]".
         iDestruct "Hvs" as (w lcons Heq) "[Hl Hvs]".
-        iExists w, lcons.
-        iFrame.
+        iExists w, lcons. iFrame "Hl".
         iSplitL "HIT".
         { by iEval (rewrite -Heq). }
         iApply ("IH" with "Hvs HITs").
@@ -67,11 +62,8 @@ Section list_rev_example.
     iIntros (l xs) "Hl".
     iDestruct (llist_split with "Hl") as (vs) "[Hl HI]".
     iExists l, vs. iFrame "Hl".
-    iModIntro.
-    iIntros "Hl".
-    iSplitL.
-    { rewrite big_sepL2_reverse_2.
-      iApply llist_split. iExists (reverse vs). iFrame. }
+    iModIntro. iIntros "Hl". iSplitL.
+    { rewrite big_sepL2_reverse_2. iApply llist_split. eauto with iFrame. }
     eauto.
   Qed.
 
@@ -86,9 +78,7 @@ Section list_rev_example.
       iApply (list_rev_service_spec with "Hc"). eauto.
     - iDestruct (iProto_mapsto_le _ _ (list_rev_protI IT) with "Hc []") as "Hc".
       { iApply list_rev_subprot. }
-      wp_send (l xs) with "[$Hl]".
-      wp_recv as "Hl".
-      by iApply "HΦ".
+      wp_send (l xs) with "[$Hl]". wp_recv as "Hl". by iApply "HΦ".
   Qed.
 
 End list_rev_example.
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index a4f0c02..d99c9d0 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -265,15 +265,12 @@ Lemma lreverse_at_spec l xs acc ys :
 Proof.
   iIntros (Φ) "[Hl Hacc] HΦ".
   iInduction xs as [|x xs] "IH" forall (l acc Φ ys).
-  - wp_lam. wp_pures.
-    wp_load. wp_pures. iApply "HΦ". rewrite app_nil_l. iApply "Hacc".
-  - wp_lam. wp_pures. simpl.
-    iDestruct "Hl" as (v l') "[HI [Hl Hl']]".
-    wp_load. wp_pures. wp_apply (lcons_spec with "[$Hacc $HI]").
-    iIntros "Hacc". wp_pures.
-    iApply ("IH" with "Hl' Hacc").
-    iIntros "!>" (l'') "Hl''".
-    iApply "HΦ". rewrite reverse_cons -app_assoc. iApply "Hl''".
+  - wp_lam. wp_load. wp_pures. iApply "HΦ". rewrite app_nil_l. iApply "Hacc".
+  - wp_lam. iDestruct "Hl" as (v l') "[HI [Hl Hl']]".
+    wp_load. wp_apply (lcons_spec with "[$Hacc $HI]").
+    iIntros "Hacc". wp_apply ("IH" with "Hl' Hacc").
+    iIntros (l'') "Hl''". iApply "HΦ".
+    rewrite reverse_cons -app_assoc. iApply "Hl''".
 Qed.
 
 Lemma lreverse_spec l xs :
-- 
GitLab