length function on lists.

theories/lib/list.v

@@ -50,6 +50,13 @@ Definition llist_member : val :=
       else let: "l" := (Snd "p")  in "go" "x" "l"
     end.
 
+Definition llength : val :=
+  rec: "go" "l" :=
+    match: "l" with
+      NONE => #0
+    | SOME "p" => #1 + "go" (Snd "p")
+    end.
+
 Section lists.
 Context `{heapG Σ}.
 Implicit Types i : nat.
@@ -122,4 +129,15 @@ Proof.
   wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
   wp_apply "IH"; iIntros (hd' Hl). wp_let. by iApply (lcons_spec with "[//]").
 Qed.
+
+Lemma llength_spec hd vs :
+  {{{ ⌜ is_list hd vs ⌝ }}} llength hd {{{ RET #(length vs); True }}}.
+Proof.
+  iIntros (Φ Hl) "HΦ".
+  iInduction vs as [|v' vs] "IH" forall (hd Hl Φ); simplify_eq/=.
+  { wp_lam. wp_match. by iApply "HΦ". }
+  destruct Hl as (hd'&->&?). wp_lam. wp_match. wp_proj.
+  wp_apply ("IH" $! hd' with "[//]"); iIntros "_ /=". wp_op.
+  rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
+Qed.
 End lists.