use int.Int

type list 'a = Nil | Cons 'a (list 'a)

function append (l1:list 'a) (l2:list 'a) : list 'a =
  match l1 with
  | Nil -> l2
  | Cons x l -> Cons x (append l l2)
  end

(*
lemma append_nil: forall l:list 'a. append l Nil = l
*)

let rec lemma append_nil (l:list 'a)
  ensures { append l Nil = l }
= match l with
  | Nil -> ()
  | Cons _ r -> append_nil r
  end



(*
lemma append_assoc:
  forall l1 l2 l3:list 'a.
    append (append l1 l2) l3 = append l1 (append l2 l3)
*)

let rec lemma append_assoc (l1 l2 l3:list 'a)
  ensures { append (append l1 l2) l3 = append l1 (append l2 l3) }
= match l1 with
  | Nil -> ()
  | Cons _ t -> append_assoc t l2 l3
  end

function length (l:list 'a) : int =
  match l with
  | Nil -> 0
  | Cons _ r -> 1 + length r
  end

(*
lemma length_nonneg: forall l:list 'a. length l >= 0
*)

function rev (l:list 'a) : list 'a =
  match l with
  | Nil -> Nil
  | Cons x r -> append (rev r) (Cons x Nil)
  end

val ref l : list int

let rec rev_append (r:list int) : unit
  writes  { l }
  variant { r }
  ensures { l = append (rev r) (old l) }
  =
  match r with
  | Nil -> ()
  | Cons x r' ->
     l <- Cons x l;
     (* l = Cons x (old l) *)
     label L in
     rev_append r'
     (* l = append (rev r') (l at L)
          = append (rev r') (Cons x (old L))

        append (rev r) (old L) =
          append (rev (Cons x r')) (old L))
          append (append (rev e') (Cons x Nil)) (old L))
          append (rev e') (append (Cons x Nil) (old L))
          *)
  end

let reverse (r:list int) : unit
  writes  { l }
  ensures { l = rev r }
  =
    l <- Nil; rev_append r