Added list length example

theories/examples/subprotocols.v

@@ -48,4 +48,41 @@ Section subprotocol_basics.
     iApply "IH".
   Qed.
 
+  Fixpoint is_list (v : val) (ws : list val) : iProp Σ :=
+    match ws with
+    | []    => True
+    | w::ws => ∃ (v' : val), ⌜v = PairV w v'⌝ ∗ is_list v' ws
+  end.
+
+  Fixpoint is_int_list (v : val) (xs : list Z) : iProp Σ :=
+    match xs with
+    | []    => True
+    | x::xs => ∃ (v' : val), ⌜v = PairV (LitV $ LitInt $ x) v'⌝ ∗ is_int_list v' xs
+  end.
+
+  Lemma is_list_int_list v xs :
+    is_int_list v xs -∗ ∃ (ws : list val), is_list v ws ∗
+                        [∗ list] i↦x;w ∈ xs;ws, ⌜LitV $ LitInt $ x = w⌝%I.
+  Proof.
+    iIntros "H".
+    iInduction (xs) as [|x xs] "IH" forall (v).
+    - eauto.
+    - iDestruct "H" as (v' Heq) "H".
+      iDestruct ("IH" with "H") as (ws) "[Hlist Heq]".
+      iExists (#x::ws)=> /=; eauto.
+  Qed.
+
+  Lemma list_length_example :
+    ⊢ (<? (v:val) (xs : list Z)> MSG v {{ is_int_list v xs }} ;
+       <!> MSG #(length xs) ; END) ⊑
+      (<? (v:val) (ws : list val)> MSG v {{ is_list v ws }} ;
+       <!> MSG #(length ws) ; END).
+  Proof.
+    iIntros (v xs) "H".
+    iDestruct (is_list_int_list with "H") as (ws) "[H Hlen]".
+    iDestruct (big_sepL2_length with "Hlen") as %Hlen.
+    iExists v, ws. iFrame "H".
+    iModIntro. rewrite Hlen. eauto.
+  Qed.
+
 End subprotocol_basics.