val is_list_cases (#t: _) (x: llist t) (l: list t) : vprop
val is_list_cases (#t: _) (x: llist t) (l: list t) : vprop
let is_list_cases #t (x:llist t) (l:list t)
: vprop 
= match x with
  | None -> pure (l == [])
  | Some v -> 
    exists* (n:node t) (tl:list t).
      pts_to v n **
      pure (l == n.head::tl) **
      is_list n.tail tl
module PulseTutorial.LinkedList
open Pulse.Lib.Pervasives
module S = Pulse.Lib.Stick.Util
module FA = Pulse.Lib.Forall.Util
open FStar.List.Tot

//llist$
noeq
type node (t:Type0) = {
    head : t;
    tail : llist t;
}

and node_ptr (t:Type0) = ref (node t)

//A nullable pointer to a node
and llist (t:Type0) = option (node_ptr t)
//llist$

//is_list$
let rec is_list #t (x:llist t) (l:list t)
: Tot vprop (decreases l)
= match l with
  | [] -> pure (x == None)
  | head::tl -> 
    exists* (p:node_ptr t) (tail:llist t).
      pure (x == Some p) **
      pts_to p { head; tail } **
      is_list tail tl
//is_list$

//boilerplate$
```pulse
ghost
fn elim_is_list_nil (#t:Type0) (x:llist t)
requires is_list x l ** pure (l == [])
ensures pure (x == None)
{
   rewrite each l as Nil #t;
   unfold (is_list x [])
}
```

```pulse
ghost
fn intro_is_list_nil (#t:Type0) (x:llist t)
requires pure (x == None)
ensures is_list x []
{
    fold (is_list x []);
}
```

```pulse
ghost
fn elim_is_list_cons (#t:Type0) (x:llist t) (l:list t) (head:t) (tl:list t)
requires is_list x l ** pure (l == head::tl)
ensures (
  exists* (p:node_ptr t) (tail:llist t).
    pure (x == Some p) **
    pts_to p { head; tail } **
    is_list tail tl
)
{
  rewrite each l as (head::tl);
  rewrite_by
    (is_list x (head::tl))
    (exists* (p:node_ptr t) (tail:llist t).
      pure (x == Some p) **
      pts_to p { head; tail } **
      is_list tail tl)
    vprop_equiv_norm
    ()
}
```
    

```pulse
ghost
fn intro_is_list_cons (#t:Type0) (x:llist t) (v:node_ptr t) (#node:node t) (#tl:list t)
requires
  pts_to v node **
  is_list node.tail tl **
  pure (x == Some v)
ensures
  is_list x (node.head::tl)
{
    rewrite (pts_to v node) as (pts_to v { head=node.head; tail=node.tail });
    rewrite_by
        (exists* (v:node_ptr t) (tail:llist t).
          pure (x == Some v) **
          pts_to v { head=node.head; tail } **
          is_list tail tl)
        (is_list x (node.head::tl))
        vprop_equiv_norm
        ()
}
```
//boilerplate$
/
Pulse.Lib.Stick.Util.fst.checked Pulse.Lib.Pervasives.fst.checked Pulse.Lib.Forall.Util.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
PulseTutorial.LinkedList.fst
x: PulseTutorial.LinkedList.llist t -> l: Prims.list t -> Pulse.Lib.Core.vprop
PulseTutorial.LinkedList.llist Prims.list Pulse.Lib.Core.pure Prims.eq2 Prims.Nil Pulse.Lib.Reference.ref PulseTutorial.LinkedList.node Pulse.Lib.Core.op_exists_Star Pulse.Lib.Core.op_Star_Star Pulse.Lib.Reference.pts_to PulseCore.FractionalPermission.full_perm Prims.Cons PulseTutorial.LinkedList.__proj__Mknode__item__head PulseTutorial.LinkedList.is_list PulseTutorial.LinkedList.__proj__Mknode__item__tail Pulse.Lib.Core.vprop
let is_list_cases #t (x: llist t) (l: list t) : vprop =
  
match x with
| None -> pure (l == [])
| Some v ->
  exists* (n: node t) (tl: list t). (pts_to v n ** pure (l == n.head :: tl)) ** is_list n.tail tl