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

addition

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

  axiom add_def1:
    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

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

  lemma remove_add:
    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

  axiom cardinal_add:
    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

  axiom Sum_add:
    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.87.3