From 85f7b19683d2b5bc868b9515200380f3cb95f659 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Jul 2019 12:50:13 +0200
Subject: [PATCH] Lemma about `fmap` and `llist`.

---
 theories/utils/llist.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index c4be3f0..a948859 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -79,6 +79,15 @@ Implicit Types xs : list A.
 Implicit Types l : loc.
 Local Arguments llist {_ _ _} _ _ !_ /.
 
+Lemma llist_fmap {B} (J : B → val → iProp Σ) (f : A → B) l xs :
+  □ (∀ x v, I x v -∗ J (f x) v) -∗
+  llist I l xs -∗ llist J l (f <$> xs).
+Proof.
+  iIntros "#Hf Hll". iInduction xs as [|x xs] "IH" forall (l); csimpl; auto.
+  iDestruct "Hll" as (v l') "(Hx & Hl & Hll)". iExists _, _. iFrame "Hl".
+  iSplitL "Hx". by iApply "Hf". by iApply "IH".
+Qed.
+
 Lemma lnil_spec :
   {{{ True }}} lnil #() {{{ l, RET #l; llist I l [] }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. wp_alloc l. by iApply "HΦ". Qed.
-- 
GitLab