From d0f8d5812c67a7a64bb4d638ac7a2de79c7457f4 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 3 Sep 2020 13:16:19 +0200
Subject: [PATCH] Made list reversal proof in line with mechanisation section
 proof

---
 theories/examples/list_rev.v | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/theories/examples/list_rev.v b/theories/examples/list_rev.v
index 038a8de..676c718 100644
--- a/theories/examples/list_rev.v
+++ b/theories/examples/list_rev.v
@@ -57,14 +57,17 @@ Section list_rev_example.
      <?> MSG #() {{ llist IT l (reverse xs) }} ; END)%proto.
 
   Lemma list_rev_subprot {T} (IT : T → val → iProp Σ) :
-    ⊢ list_rev_prot ⊑ (list_rev_protI IT).
+    ⊢ list_rev_prot ⊑ list_rev_protI IT.
   Proof.
     iIntros (l xs) "Hl".
-    iDestruct (llist_split with "Hl") as (vs) "[Hl HI]".
+    iDestruct (llist_split with "Hl") as (vs) "[Hl HIT]".
     iExists l, vs. iFrame "Hl".
-    iModIntro. iIntros "Hl". iSplitL.
-    { rewrite big_sepL2_reverse_2. iApply llist_split. eauto with iFrame. }
-    eauto.
+    iModIntro.
+    iIntros "Hl".
+    iSplitL "Hl HIT".
+    { iApply llist_split. rewrite big_sepL2_reverse_2.
+      iExists (reverse vs). iFrame "Hl HIT". }
+    done.
   Qed.
 
   Lemma list_rev_client_spec {T} (IT : T → val → iProp Σ) l xs :
-- 
GitLab