Why3 Standard Library index

# Polymorphic Lists

## Basic theory of polymorphic lists

```theory List

type list 'a = Nil | Cons 'a (list 'a)

end

```

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

```

## Membership in a list

```theory Mem
use import 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

```

## Nth element of a list

```theory Nth

use import List
use import 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 import 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 import int.Int
use import option.Option
use import 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

```

```theory HdTl

use import List
use import 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 import 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

```theory NthHdTl

use import int.Int
use import option.Option
use import List
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

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

end

```

## Appending two lists

```theory Append

use import 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 "induction" 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 "induction" l2: list 'a. length (l1 ++ l2) = length l1 + length l2

use import 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

theory NthLengthAppend

use import int.Int
use import 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

```theory Reverse

use import 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_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 import Mem

lemma reverse_mem:
forall l: list 'a, x: 'a. mem x l <-> mem x (reverse l)

use import Length

lemma Reverse_length:
forall l: list 'a. length (reverse l) = length l

end

```

## 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 "induction" s t: list 'a.
rev_append (r ++ s) t = rev_append s (rev_append r t)

use import int.Int
use import Length

lemma rev_append_length:
forall s "induction" t: list 'a.
length (rev_append s t) = length s + length t

use import 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

```theory Combine

use import 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

```

## Sorted lists for some order as parameter

```theory Sorted

use import List

type t
predicate le t t
clone relations.Transitive with type t = t, predicate rel = le

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)

use import 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

```theory SortedInt

use import int.Int
clone export Sorted with type t = int, predicate le = (<=), goal Transitive.Trans

end

theory RevSorted

type t
predicate le t t
clone import relations.Transitive with type t = t, predicate rel = le
predicate ge (x y: t) = le y x

use import List

clone Sorted as Incr with type t = t, predicate le = le, goal Transitive.Trans
clone Sorted as Decr with type t = t, predicate le = ge, goal Transitive.Trans

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

```theory NumOcc

use import int.Int
use import 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 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 "induction" l2: list 'a.
num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2

use import Reverse

lemma reverse_num_occ :
forall x: 'a, l: list 'a.
num_occ x l = num_occ x (reverse l)

end

```

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

```

## 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 "induction" l2: list 'a.
distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) ->
distinct (l1 ++ l2)

end

theory Prefix

use import 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

theory Sum

use import List
use import int.Int

function sum (l: list int) : int = match l with
| Nil -> 0
| Cons x r -> x + sum r
end

end

```

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

```

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

```

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

```

## 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 RevAppend
use export NumOcc
use export Permut

end
```

Generated by why3doc 0.87.2