(** {1 Polymorphic Lists} *) (** {2 Basic theory of polymorphic lists} *) theory List type list 'a = Nil | Cons 'a (list 'a) end (** {2 Length of a list} *) theory Length use import int.Int use import List function 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 (** {2 Membership in a list} *) theory Mem use export List predicate mem (x: 'a) (l: list 'a) = match l with | Nil -> false | Cons y r -> x = y \/ mem x r end end theory Elements use import List use Mem use set.Fset as FSet function elements (list 'a) : FSet.set 'a axiom elements_mem: forall l:list 'a, x:'a. Mem.mem x l <-> FSet.mem x (elements l) lemma elements_Nil: elements (Nil : list 'a) = FSet.empty end (** {2 Nth element of a list} *) theory Nth use export List use export option.Option use import int.Int function 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 NthNoOpt use export List use import int.Int function nth (n: int) (l: list 'a) : 'a axiom nth_cons_0: forall x:'a, r:list 'a. nth 0 (Cons x r) = x axiom nth_cons_n: forall x:'a, r:list 'a, n:int. n > 0 -> nth n (Cons x r) = nth (n-1) r end theory NthLength use export Nth use export Length use import int.Int lemma nth_none_1: forall l: list 'a, i: int. i < 0 -> nth i l = None lemma nth_none_2: forall l: list 'a, i: int. i >= length l -> nth i l = None lemma nth_none_3: forall l: list 'a, i: int. nth i l = None -> i < 0 \/ i >= length l end (** {2 Head and tail} *) theory HdTl use export List use export option.Option function hd (l: list 'a) : option 'a = match l with | Nil -> None | Cons h _ -> Some h end function tl (l: list 'a) : option (list 'a) = match l with | Nil -> None | Cons _ t -> Some t end end theory HdTlNoOpt use export List function hd (l: list 'a) : 'a axiom hd_cons: forall x:'a, r:list 'a. hd (Cons x r) = x function tl (l: list 'a) : list 'a axiom tl_cons: forall x:'a, r:list 'a. tl (Cons x r) = r end (** {2 Relation between head, tail, and nth} *) theory NthHdTl use import int.Int use import Nth use import HdTl lemma Nth_tl: forall l1 l2: list 'a. tl l1 = Some l2 -> forall i: int. i <> -1 -> nth i l2 = nth (i+1) l1 lemma Nth0_head: forall l: list 'a. nth 0 l = hd l end (** {2 Appending two lists} *) theory Append use export List function (++) (l1 l2: list 'a) : list 'a = match l1 with | Nil -> l2 | Cons x1 r1 -> Cons x1 (r1 ++ l2) end lemma Append_assoc: forall l1 l2 l3: list 'a. l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3 lemma Append_l_nil: forall l: list 'a. l ++ Nil = l use import Length use import int.Int lemma Append_length: forall l1 l2: list 'a. length (l1 ++ l2) = length l1 + length l2 use import Mem lemma mem_append: forall x: 'a, l1 l2: list 'a. mem x (l1 ++ l2) <-> mem x l1 \/ mem x l2 lemma mem_decomp: forall x: 'a, l: list 'a. mem x l -> exists l1 l2: list 'a. l = l1 ++ Cons x l2 end theory NthLengthAppend use export NthLength use export Append use import int.Int lemma nth_append_1: forall l1 l2: list 'a, i: int. i < length l1 -> nth i (l1 ++ l2) = nth i l1 lemma nth_append_2: forall l1 l2: list 'a, i: int. length l1 <= i -> nth i (l1 ++ l2) = nth (i - length l1) l2 end (** {2 Reversing a list} *) theory Reverse use export List use import Append function reverse (l: list 'a) : list 'a = match l with | Nil -> Nil | Cons x r -> reverse r ++ Cons x Nil end lemma reverse_append: forall l1 l2: list 'a, x: 'a. (reverse (Cons x l1)) ++ l2 = (reverse l1) ++ (Cons x l2) lemma reverse_reverse: forall l: list 'a. reverse (reverse l) = l use import Length lemma Reverse_length: forall l: list 'a. length (reverse l) = length l end (** {2 Reverse append} *) theory RevAppend use import List function rev_append (s t: list 'a) : list 'a = match s with | Cons x r -> rev_append r (Cons x t) | Nil -> t end use import Append lemma rev_append_append_l: forall r s t: list 'a. rev_append (r ++ s) t = rev_append s (rev_append r t) lemma rev_append_append_r: forall r s t: list 'a. rev_append r (s ++ t) = rev_append (rev_append s r) t use import int.Int use import Length lemma rev_append_length: forall s t: list 'a. length (rev_append s t) = length s + length t end (** {2 Zip} *) theory Combine use export List function combine (x: list 'a) (y: list 'b) : list ('a, 'b) = match x, y with | Cons x0 x, Cons y0 y -> Cons (x0, y0) (combine x y) | _ -> Nil end end (** {2 Sorted lists for some order as parameter} *) theory Sorted use export List type t predicate le t t inductive sorted (l: list t) = | Sorted_Nil: sorted Nil | Sorted_One: forall x: t. sorted (Cons x Nil) | Sorted_Two: forall x y: t, l: list t. le x y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) use import Mem lemma sorted_mem: forall x: t, l: list t. (forall y: t. mem y l -> le x y) /\ sorted l <-> sorted (Cons x l) end (** {2 Sorted lists of integers} *) theory SortedInt use import int.Int clone export Sorted with type t = int, predicate le = (<=) end theory RevSorted type t predicate le t t predicate ge (x y: t) = le y x use import List clone Sorted as Incr with type t = t, predicate le = le clone Sorted as Decr with type t = t, predicate le = ge predicate compat (s t: list t) = match s, t with | Cons x _, Cons y _ -> le x y | _, _ -> true end use import RevAppend lemma rev_append_sorted_incr: forall s t: list t. Incr.sorted (rev_append s t) <-> Decr.sorted s /\ Incr.sorted t /\ compat s t lemma rev_append_sorted_decr: forall s t: list t. Decr.sorted (rev_append s t) <-> Incr.sorted s /\ Decr.sorted t /\ compat t s (* use import Reverse lemma rev_sorted_incr: forall s: list t. Incr.sorted (reverse s) <-> Decr.sorted s lemma rev_sorted_decr: forall s: list t. Decr.sorted (reverse s) <-> Incr.sorted s *) end (** {2 Number of occurrences in a list} *) theory NumOcc use import int.Int use import List (** number of occurrences of [x] in [l] *) function 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 use import Append lemma Append_Num_Occ : forall x: 'a, l1 l2: list 'a. num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2 end (** {2 Permutation of lists} *) theory Permut use import NumOcc use import List predicate 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 Append lemma Permut_cons_append: forall x : 'a, l1 l2 : list 'a. permut (Cons x l1 ++ l2) (l1 ++ Cons x l2) lemma Permut_assoc: forall l1 l2 l3: list 'a. permut ((l1 ++ l2) ++ l3) (l1 ++ (l2 ++ l3)) lemma Permut_append: forall l1 l2 k1 k2 : list 'a. permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2) lemma Permut_append_swap: forall l1 l2 : list 'a. permut (l1 ++ l2) (l2 ++ l1) 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 (** {2 List with pairwise distinct elements} *) theory Distinct use import List use import Mem inductive distinct (l: list 'a) = | distinct_zero: distinct (Nil: list 'a) | distinct_one : forall x:'a. distinct (Cons x Nil) | distinct_many: forall x:'a, l: list 'a. not (mem x l) -> distinct l -> distinct (Cons x l) use import Append lemma distinct_append: forall l1 l2: list 'a. distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) -> distinct (l1 ++ l2) end theory Prefix use export List use import int.Int function prefix (n: int) (l: list 'a) : list 'a = if n <= 0 then Nil else match l with | Nil -> Nil | Cons x r -> Cons x (prefix (n-1) r) end end (** {2 Induction on lists} *) theory Induction use import List type elt predicate 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 (** {2 Maps as lists of pairs} *) theory Map use import List type a type b function f a : b function map (l: list a) : list b = match l with | Nil -> Nil | Cons x r -> Cons (f x) (map r) end end (** {2 Generic recursors on lists} *) theory FoldLeft use import List type a type b function f b a : b function fold_left (acc: b) (l: list a) : b = match l with | Nil -> acc | Cons x r -> fold_left (f acc x) r end end theory FoldRight use import List type a type b function f a b : b function fold_right (l: list a) (acc: b) : b = match l with | Nil -> acc | Cons x r -> f x (fold_right r acc) end end (** {2 Importation of all list theories in one} *) theory ListRich use export List use export Length use export Mem use export Nth use export HdTl use export NthHdTl use export Append use export Reverse use export Sorted use export NumOcc use export Permut end