From 3ee753fd210b6829c44fac3877e8c56358ffa60b Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Sat, 15 Aug 2020 15:47:13 +0200
Subject: [PATCH] Cleaned up a proof

---
 theories/examples/basics.v | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index c967fd7..4eec9dd 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -1,4 +1,4 @@
-(** This file includes basic examples that each describe a unique feature of 
+(** This file includes basic examples that each describe a unique feature of
 dependent separation protocols. *)
 From actris.channel Require Import proofmode.
 From iris.heap_lang Require Import lib.spin_lock.
@@ -268,11 +268,9 @@ Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
   wp_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
-  - iAssert (∀ Ψ, WP (rec: "go" <> := let: "x" := recv c in
-      send c ("x" + #2) ;; "go" #())%V #() {{ Ψ }})%I with "[Hc]" as "H".
-    { iIntros (Ψ). iLöb as "IH". wp_recv (x) as "_". wp_send with "[//]".
-      wp_seq. by iApply "IH". }
-    wp_lam. wp_closure. wp_let. iApply "H".
+  - wp_pures. iLöb as "IH".
+    wp_recv (x) as "_". wp_send with "[//]".
+    wp_pures. by iApply "IH".
   - wp_send with "[//]". wp_recv as "_". wp_send with "[//]". wp_recv as "_".
     wp_pures. by iApply "HΦ".
 Qed.
-- 
GitLab