(** {1 Polymorphic Lists} *) (** {2 Basic theory of polymorphic lists} *) module List type list 'a = Nil | Cons 'a (list 'a) let predicate is_nil (l:list 'a) ensures { result <-> l = Nil } = match l with Nil -> true | Cons _ _ -> false end end (** {2 Length of a list} *) module Length use int.Int use List let rec 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 Quantifiers on lists} *) module Quant use List let rec function for_all (p: 'a -> bool) (l:list 'a) : bool = match l with | Nil -> true | Cons x r -> p x && for_all p r end let rec function for_some (p: 'a -> bool) (l:list 'a) : bool = match l with | Nil -> false | Cons x r -> p x || for_some p r end let function mem (eq:'a -> 'a -> bool) (x:'a) (l:list 'a) : bool = for_some (eq x) l end (** {2 Membership in a list} *) module Mem use List predicate mem (x: 'a) (l: list 'a) = match l with | Nil -> false | Cons y r -> x = y \/ mem x r end end module Elements use set.Fset use List use Mem function elements (l: list 'a) : fset 'a = match l with | Nil -> empty | Cons x r -> add x (elements r) end lemma elements_mem: forall x: 'a, l: list 'a. mem x l <-> Fset.mem x (elements l) end (** {2 Nth element of a list} *) module Nth use List use option.Option use int.Int let rec 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 module NthNoOpt use List use 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 module NthLength use int.Int use option.Option use List use export Nth use export Length 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} *) module HdTl use List use option.Option let function hd (l: list 'a) : option 'a = match l with | Nil -> None | Cons h _ -> Some h end let function tl (l: list 'a) : option (list 'a) = match l with | Nil -> None | Cons _ t -> Some t end end module HdTlNoOpt use 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} *) module NthHdTl use int.Int use option.Option use List use Nth use 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} *) module Append use List let rec 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 [@induction] l2 l3: list 'a. l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3 lemma Append_l_nil: forall l: list 'a. l ++ Nil = l use Length use int.Int lemma Append_length: forall l1 [@induction] l2: list 'a. length (l1 ++ l2) = length l1 + length l2 use Mem lemma mem_append: forall x: 'a, l1 [@induction] 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 module NthLengthAppend use int.Int use List use export NthLength use export Append 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 [@induction] l2: list 'a, i: int. length l1 <= i -> nth i (l1 ++ l2) = nth (i - length l1) l2 end (** {2 Reversing a list} *) module Reverse use List use Append let rec 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_cons: forall l: list 'a, x: 'a. reverse (Cons x l) = reverse l ++ Cons x Nil lemma cons_reverse: forall l: list 'a, x: 'a. Cons x (reverse l) = reverse (l ++ Cons x Nil) lemma reverse_reverse: forall l: list 'a. reverse (reverse l) = l use Mem lemma reverse_mem: forall l: list 'a, x: 'a. mem x l <-> mem x (reverse l) use Length lemma Reverse_length: forall l: list 'a. length (reverse l) = length l end (** {2 Reverse append} *) module RevAppend use List let rec 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 Append lemma rev_append_append_l: forall r [@induction] s t: list 'a. rev_append (r ++ s) t = rev_append s (rev_append r t) use int.Int use Length lemma rev_append_length: forall s [@induction] t: list 'a. length (rev_append s t) = length s + length t use Reverse lemma rev_append_def: forall r [@induction] s: list 'a. rev_append r s = reverse r ++ s lemma rev_append_append_r: forall r s t: list 'a. rev_append r (s ++ t) = rev_append (rev_append s r) t end (** {2 Zip} *) module Combine use List let rec 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} *) module Sorted use List type t predicate le t t clone relations.Transitive with type t = t, predicate rel = le, axiom Trans 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 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) use Append lemma sorted_append: forall l1 [@induction] l2: list t. (sorted l1 /\ sorted l2 /\ (forall x y: t. mem x l1 -> mem y l2 -> le x y)) <-> sorted (l1 ++ l2) end (** {2 Sorted lists of integers} *) module SortedInt use int.Int clone export Sorted with type t = int, predicate le = (<=), goal Transitive.Trans end module RevSorted type t predicate le t t clone relations.Transitive with type t = t, predicate rel = le, axiom Trans predicate ge (x y: t) = le y x use List clone Sorted as Incr with type t = t, predicate le = le, goal . clone Sorted as Decr with type t = t, predicate le = ge, goal . predicate compat (s t: list t) = match s, t with | Cons x _, Cons y _ -> le x y | _, _ -> true end use RevAppend lemma rev_append_sorted_incr: forall s [@induction] 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 [@induction] t: list t. Decr.sorted (rev_append s t) <-> Incr.sorted s /\ Decr.sorted t /\ compat t s end (** {2 Number of occurrences in a list} *) module NumOcc use int.Int use List 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 (** number of occurrences of `x` in `l` *) lemma Num_Occ_NonNeg: forall x:'a, l: list 'a. num_occ x l >= 0 use Mem lemma Mem_Num_Occ : forall x: 'a, l: list 'a. mem x l <-> num_occ x l > 0 use Append lemma Append_Num_Occ : forall x: 'a, l1 [@induction] l2: list 'a. num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2 use Reverse lemma reverse_num_occ : forall x: 'a, l: list 'a. num_occ x l = num_occ x (reverse l) end (** {2 Permutation of lists} *) module Permut use NumOcc use 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 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 Mem lemma Permut_mem: forall x: 'a, l1 l2: list 'a. permut l1 l2 -> mem x l1 -> mem x l2 use Length lemma Permut_length: forall l1 [@induction] l2: list 'a. permut l1 l2 -> length l1 = length l2 end (** {2 List with pairwise distinct elements} *) module Distinct use List use 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 Append lemma distinct_append: forall l1 [@induction] l2: list 'a. distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) -> distinct (l1 ++ l2) end module Prefix use List use int.Int let rec 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 module Sum use List use int.Int let rec function sum (l: list int) : int = match l with | Nil -> 0 | Cons x r -> x + sum r end end (* (** {2 Induction on lists} *) module Induction use List (* type elt *) (* predicate p (list elt) *) axiom Induction: forall p: list 'a -> bool. p (Nil: list 'a) -> (forall x:'a. forall l:list 'a. p l -> p (Cons x l)) -> forall l:list 'a. p l end *) (** {2 Maps as lists of pairs} *) module Map use List function map (f: 'a -> 'b) (l: list 'a) : list 'b = match l with | Nil -> Nil | Cons x r -> Cons (f x) (map f r) end end (** {2 Generic recursors on lists} *) module FoldLeft use List function fold_left (f: 'b -> 'a -> 'b) (acc: 'b) (l: list 'a) : 'b = match l with | Nil -> acc | Cons x r -> fold_left f (f acc x) r end use Append lemma fold_left_append: forall l1 [@induction] l2: list 'a, f: 'b -> 'a -> 'b, acc : 'b. fold_left f acc (l1++l2) = fold_left f (fold_left f acc l1) l2 end module FoldRight use List function fold_right (f: 'a -> 'b -> 'b) (l: list 'a) (acc: 'b) : 'b = match l with | Nil -> acc | Cons x r -> f x (fold_right f r acc) end use Append lemma fold_right_append: forall l1 [@induction] l2: list 'a, f: 'a -> 'b -> 'b, acc : 'b. fold_right f (l1++l2) acc = fold_right f l1 (fold_right f l2 acc) end (** {2 Importation of all list theories in one} *) module 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 RevAppend use export NumOcc use export Permut end