proving_stuff.fst

module Hello

val factorial: x:int{x>=0} -> Tot int (*factorial is a totalfunction over non negative ints*)


val length: list 'a -> Tot nat
let rec length l = match l with
  | [] -> 0
  | _ :: tl -> 1 + length tl


val mem: x:'a -> l:list 'a -> Tot bool

let rec mem x l = match l with
  | [] -> false
  | head::tl ->  head=x || (mem x tl)




val append: x:list 'a -> y:list 'a -> Tot (z:list 'a {length z = length x + length y})

let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2

val append_mem:  l1:list 'a -> l2:list 'a -> a:'a
        -> Lemma (ensures (mem a (append l1 l2)  <==>  mem a l1 || mem a l2))

let rec append_mem l1 l2 a = match l1 with
  | [] -> ()
  | hd::tl ->append_mem tl l2 a



let rec factorial n = if n = 0 then 1 else n * factorial (n - 1)



let max x y = if x > y then x else y

let a = assert (
  forall x y. max x y >= x && max x y >= y && 
  (max x y = x || max x y = y)
)