theory List type list 'a = Nil | Cons 'a (list 'a) end theory Length use import int.Int use import List logic length (l : list 'a) : int = match l with | Nil -> 0 | Cons _ r -> 1 + length(r) end lemma Length_nonnegative : forall l:list 'a. length(l) >= 0 lemma Length_nil : forall l:list 'a. length l = 0 <-> l = Nil end theory Mem use export List logic mem (x: 'a) (l : list 'a) = match l with | Nil -> false | Cons y r -> x = y or mem x r end end theory Nth use export List use export option.Option use import int.Int logic nth (n : int) (l : list 'a) : option 'a = match l with | Nil -> None | Cons x r -> if n = 0 then Some x else nth (n - 1) r end end theory HdTl "head and tail" use export List use export option.Option logic hd (l : list 'a) : option 'a = match l with | Nil -> None | Cons h _ -> Some h end logic tl (l : list 'a) : option (list 'a) = match l with | Nil -> None | Cons _ t -> Some t end (* TODO: move these lemmas into another theory? *) use import Nth use import int.Int lemma Nth_tl : forall l1 l2 : list 'a. tl l1 = Some l2 -> forall i : int. nth i l2 = nth (i+1) l1 lemma Nth0_head: forall l : list 'a. nth 0 l = hd l end theory Append use export List logic append (l1 l2 : list 'a) : list 'a = match l1 with | Nil -> l2 | Cons x1 r1 -> Cons x1 (append r1 l2) end lemma Append_assoc : forall l1 l2 l3 : list 'a. append l1 (append l2 l3) = append (append l1 l2) l3 lemma Append_l_nil : forall l : list 'a. append l Nil = l use import Length use import int.Int lemma Append_length : forall l1 l2 : list 'a. length (append l1 l2) = length l1 + length l2 end theory Reverse use export List use import Append logic reverse (l : list 'a) : list 'a = match l with | Nil -> Nil | Cons x r -> append (reverse r) (Cons x Nil) end use import Length lemma Reverse_length : forall l : list 'a. length (reverse l) = length l end theory Sorted use export List use import int.Int inductive sorted (l : list int) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:int. sorted (Cons x Nil) | Sorted_Two : forall x y : int, l : list int. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) use import Mem lemma Sorted_mem : forall x : int, l : list int. (forall y : int. mem y l -> x <= y) and sorted l <-> sorted (Cons x l) end theory NumOcc use import int.Int use import List (* number of occurence of x in l *) logic num_occ (x : 'a) (l : list 'a) : int = match l with | Nil -> 0 | Cons y r -> (if x = y then 1 else 0) + num_occ x r end use import Mem lemma Mem_Num_Occ : forall x:'a, l:list 'a. mem x l <-> num_occ x l > 0 end theory Permut use import NumOcc use import List logic permut (l1 : list 'a) (l2 : list 'a) = forall x : 'a. num_occ x l1 = num_occ x l2 lemma Permut_refl : forall l : list 'a. permut l l lemma Permut_sym : forall l1 l2 : list 'a. permut l1 l2 -> permut l2 l1 lemma Permut_trans : forall l1 l2 l3 : list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3 lemma Permut_cons : forall x : 'a, l1 l2 : list 'a. permut l1 l2 -> permut (Cons x l1) (Cons x l2) lemma Permut_swap : forall x y : 'a, l : list 'a. permut (Cons x (Cons y l)) (Cons y (Cons x l)) use import Mem lemma Permut_mem : forall x : 'a, l1 l2 : list 'a. permut l1 l2 -> mem x l1 -> mem x l2 use import Length lemma Permut_length : forall l1 l2 : list 'a. permut l1 l2 -> length l1 = length l2 end theory Induction use import List type elt logic p (list elt) axiom Induction : p (Nil : list elt) -> (forall x:elt. forall l:list elt. p l -> p (Cons x l)) -> forall l:list elt. p l end theory Map use import List type a type b logic f a : b logic map(l : list a) : list b = match l with | Nil -> Nil | Cons x r -> Cons (f x) (map r) end end theory Fold (* TODO (a la Map) *) end