Commit 85f7b196 authored by Robbert Krebbers's avatar Robbert Krebbers

Lemma about `fmap` and `llist`.

parent 6dd37799
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment