Why3 Standard Library index

Polymorphic Lists

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

```

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

```

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

```

Quantifiers on lists

```module Quant

use List
use Mem

let rec function for_all (p: 'a -> bool) (l:list 'a) : bool
ensures { result <-> forall x. mem x l -> p x }
=
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
ensures { result <-> exists x. mem x l /\ p x }
=
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
ensures  { result <-> exists y. mem y l /\ eq x y }
=
for_some (eq x) l

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

```

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

```

```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

```

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

forall l: list 'a. nth 0 l = hd l

end

```

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

```

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

```

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

```

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

```

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

```

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

```

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

```

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

```

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
*)

```

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

```

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

```

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
```

Generated by why3doc 1.6.0