Why3 Standard Library index

# Set theories

## General Sets

```theory SetGen

type set 'a

```

if `'a` is an infinite type, then `set 'a` is infinite

```  meta "material_type_arg" type set, 0

```

membership

```  predicate mem 'a (set 'a)

```

equality

```  predicate (==) (s1 s2: set 'a) = forall x : 'a. mem x s1 <-> mem x s2

axiom extensionality:
forall s1 s2: set 'a. s1 == s2 -> s1 = s2

```

inclusion

```  predicate subset (s1 s2: set 'a) = forall x : 'a. mem x s1 -> mem x s2

lemma subset_refl:
forall s: set 'a. subset s s

lemma subset_trans:
forall s1 s2 s3: set 'a. subset s1 s2 -> subset s2 s3 -> subset s1 s3

```

empty set

```  constant empty : set 'a

predicate is_empty (s: set 'a) = forall x: 'a. not (mem x s)

axiom empty_def1: is_empty (empty : set 'a)

lemma mem_empty: forall x:'a. mem x empty <-> false

```

```  function add 'a (set 'a) : set 'a

forall x y: 'a. forall s: set 'a.
mem x (add y s) <-> x = y \/ mem x s

function singleton (x: 'a) : set 'a = add x empty

```

removal

```  function remove 'a (set 'a) : set 'a

axiom remove_def1:
forall x y : 'a, s : set 'a.
mem x (remove y s) <-> x <> y /\ mem x s

forall x: 'a, s : set 'a. mem x s -> add x (remove x s) = s

forall x: 'a, s : set 'a. remove x (add x s) = remove x s

lemma subset_remove:
forall x: 'a, s: set 'a. subset (remove x s) s

```

union

```  function union (set 'a) (set 'a) : set 'a

axiom union_def1:
forall s1 s2: set 'a, x: 'a.
mem x (union s1 s2) <-> mem x s1 \/ mem x s2

```

intersection

```  function inter (set 'a) (set 'a) : set 'a

axiom inter_def1:
forall s1 s2: set 'a, x: 'a.
mem x (inter s1 s2) <-> mem x s1 /\ mem x s2

```

difference

```  function diff (set 'a) (set 'a) : set 'a

axiom diff_def1:
forall s1 s2: set 'a, x: 'a.
mem x (diff s1 s2) <-> mem x s1 /\ not (mem x s2)

lemma subset_diff:
forall s1 s2: set 'a. subset (diff s1 s2) s1

```

arbitrary element

```  function choose (s:set 'a) : 'a

axiom choose_def:
forall s: set 'a. not (is_empty s) -> mem (choose s) s

end

```

## Potentially infinite sets

```theory Set

clone export SetGen

```

the set of all x of type 'a

```  constant all: set 'a

axiom all_def: forall x: 'a. mem x all

end

```

## Set Comprehension

```theory SetComprehension

use export Set
use HighOrd as HO

```

{ x | p x }

```  function comprehension (p: HO.pred 'a) : set 'a

axiom comprehension_def:
forall p: HO.pred 'a.
forall x: 'a. mem x (comprehension p) <-> p x

```

{ x | x in U and p(x) }

```  function filter (p: HO.pred 'a) (u: set 'a) : set 'a =
comprehension (\ x: 'a. p x /\ mem x u)

```

{ f x | x in U }

```  function map (f: HO.func 'a 'b) (u: set 'a) : set 'b =
comprehension (\ y: 'b. exists x: 'a. mem x u /\ y = f x)

lemma map_def:
forall f: HO.func 'a 'b, u: set 'a.
forall x: 'a. mem x u -> mem (f x) (map f u)

end

```

## Finite sets

```theory Fset

use import int.Int
clone export SetGen

function cardinal (set 'a) : int

axiom cardinal_nonneg: forall s: set 'a. cardinal s >= 0

axiom cardinal_empty:
forall s: set 'a. cardinal s = 0 <-> is_empty s

forall x : 'a. forall s : set 'a.
not (mem x s) -> cardinal (add x s) = 1 + cardinal s

axiom cardinal_remove:
forall x : 'a. forall s : set 'a.
mem x s -> cardinal s = 1 + cardinal (remove x s)

axiom cardinal_subset:
forall s1 s2 : set 'a. subset s1 s2 -> cardinal s1 <= cardinal s2

lemma subset_eq:
forall s1 s2 : set 'a.
subset s1 s2 -> cardinal s1 = cardinal s2 -> s1 == s2

lemma cardinal1:
forall s: set 'a. cardinal s = 1 ->
forall x: 'a. mem x s -> x = choose s

end

```

## Finite Set Comprehension

```theory FsetComprehension

use export Fset
use import int.Int
use HighOrd as HO

```

{ x | x in U and p(x) }

```  function filter (p: HO.pred 'a) (u: set 'a) : set 'a

axiom filter_def:
forall p: HO.pred 'a, u: set 'a.
forall x: 'a. mem x (filter p u) <-> (p x /\ mem x u)

lemma filter_cardinal:
forall p: HO.pred 'a, u: set 'a. cardinal (filter p u) <= cardinal u

```

{ f x | x in U }

```  function map (f: HO.func 'a 'b) (u: set 'a) : set 'b

axiom map_def:
forall f: HO.func 'a 'b, u: set 'a.
forall y: 'b. mem y (map f u) <-> (exists x: 'a. mem x u /\ y = f x)

lemma map_def1:
forall f: HO.func 'a 'b, u: set 'a.
forall x: 'a. mem x u -> mem (f x) (map f u)

lemma map_cardinal:
forall f: HO.func 'a 'b, u: set 'a. cardinal (map f u) <= cardinal u

end

```

## N-th element of a finite set

```theory FsetNth

use import int.Int
use import Fset

function nth (i: int) (s: set 'a) : 'a

axiom nth_injective:
forall s: set 'a, i j: int.
0 <= i < cardinal s -> 0 <= j < cardinal s -> nth i s = nth j s -> i = j

axiom nth_surjective:
forall s: set 'a, x: 'a. mem x s ->
exists i: int. 0 <= i < cardinal s /\ x = nth i s

end

```

## Induction principle on finite sets

```theory FsetInduction

use import Fset

type t

predicate p (set t)

lemma Induction :
(forall s: set t. is_empty s -> p s) ->
(forall s: set t. p s -> forall t: t.
not (mem t s) -> p (add t s)) ->
forall s: set t. p s

end

```

## Finite sets of integers

```theory Fsetint

use export int.Int
use export Fset

function min_elt (set int) : int

axiom min_elt_def1:
forall s: set int. not (is_empty s) -> mem (min_elt s) s
axiom min_elt_def2:
forall s: set int. forall x: int. mem x s -> min_elt s <= x

function max_elt (set int) : int

axiom max_elt_def1:
forall s: set int. not (is_empty s) -> mem (max_elt s) s
axiom max_elt_def2:
forall s: set int. forall x: int. mem x s -> x <= max_elt s

function interval int int : set int

axiom interval_def: forall x l r: int. mem x (interval l r) <-> l <= x < r

lemma cardinal_interval:
forall l r: int. cardinal (interval l r) = if l <= r then r - l else 0

end

```

## Finite set iterators

```theory Min

use import Fset
use import int.Int

type param

type elt

function cost param elt : int

function min param (set elt) : int

axiom min_is_a_lower_bound:
forall p:param, s:set elt, x:elt. mem x s -> cost p x >= min p s

axiom min_appears_in_set:
forall p:param, s:set elt. not (is_empty s) ->
exists x:elt. mem x s /\ cost p x = min p s

end

```

sum on finite set

```theory FsetSum "Sum of a function over a finite set"

use import HighOrd
use import int.Int
use import Fset as S

function sum (set 'a) ('a -> int) : int
```

`sum s f` is the sum Sum_{S.mem x s} f x

```  axiom Sum_def_empty :
forall f. sum (S.empty: set 'a) f = 0

forall s: set 'a. forall f x.
not (mem x s) -> sum (S.add x s) f = sum s f + f x

lemma Sum_remove:
forall s: set 'a. forall f x.
mem x s -> sum (S.remove x s) f = sum s f - f x

lemma Sum_def_choose:
forall s: set 'a. forall f.
not (S.is_empty s) ->
let x = S.choose s in
sum s f = f x + sum (S.remove x s) f

lemma Sum_transitivity:
forall s1 s2: set 'a. forall f.
sum (S.union s1 s2) f = sum s1 f + sum s2 f - sum (S.inter s1 s2) f

lemma Sum_eq:
forall s: set 'a. forall f g.
(forall x. S.mem x s -> f x = g x) -> sum s f = sum s g

end

```

## Sets realized as maps

```theory SetMap

use import map.Map
use import map.Const
use import bool.Bool

type set 'a = map 'a bool

predicate mem (x:'a) (s:set 'a) = s[x] = True

constant empty : set 'a = const False

predicate is_empty (s : set 'a) = forall x : 'a. not (mem x s)

goal Empty_def1 : is_empty(empty : set 'a)

function add (x:'a) (s:set 'a) : set 'a = s[x <- True]

function remove (x:'a) (s:set 'a) : set 'a =  s[x <- False]

function union (set 'a) (set 'a) : set 'a

axiom Union_def :
forall s1 s2 : set 'a. forall x : 'a.
(union s1 s2)[x] = orb s1[x] s2[x]

function inter (set 'a) (set 'a) : set 'a

axiom Inter_def :
forall s1 s2 : set 'a. forall x : 'a.
(inter s1 s2)[x] = andb s1[x] s2[x]

function diff (set 'a) (set 'a) : set 'a

axiom Diff_def1 :
forall s1 s2 : set 'a. forall x : 'a.
(diff s1 s2)[x] = andb s1[x] (notb s2[x])

predicate equal(s1 s2 : set 'a) = forall x : 'a. s1[x] = s2[x]

(* dubious axiom: extensionality should be postulated on maps instead
axiom Equal_is_eq : forall s1 s2 : set 'a. equal s1 s2 -> s1 = s2
*)

predicate subset(s1 s2 : set 'a) = forall x : 'a. mem x s1 -> mem x s2

function complement (set 'a) : set 'a

axiom Complement_def :
forall s : set 'a. forall x : 'a.
(complement s)[x] = notb s[x]

end
```

Generated by why3doc 0.88.3