(** {1 A library for Set theory} this library provides a few Why3 theories that formalize the set theory as it is defined in the B-book. Reference: {h Discharging Proof Obligations from Atelier B using Multiple Automated Provers} *) (** {2 Interval} interval of integers, seen as sets *) theory Interval use export int.Int use export set.Set function integer : set int axiom mem_integer: forall x:int.mem x integer function natural : set int axiom mem_natural: forall x:int. mem x natural <-> x >= 0 function mk int int : set int axiom mem_interval: forall x a b : int [mem x (mk a b)]. mem x (mk a b) <-> a <= x <= b lemma interval_empty : forall a b:int. a > b -> mk a b = empty lemma interval_add : forall a b:int. a <= b -> (mk a b) = add b (mk a (b-1)) end (** {2 Power set} the power set of some set S, i.e the set of subsets of S *) theory PowerSet use export set.Set function power (set 'a) : set (set 'a) axiom mem_power : forall x y:set 'a [mem x (power y)]. mem x (power y) <-> subset x y end (** {2 Relations} Relations between two sets *) theory Relation use export set.Set type rel 'a 'b = set ('a , 'b) end (** {2 Image} Image by a relation *) theory Image use export Relation function image (r : rel 'a 'b) (dom : set 'a) : set 'b axiom mem_image: forall r : rel 'a 'b, dom : set 'a, y : 'b [mem y (image r dom)]. mem y (image r dom) <-> exists x: 'a. mem x dom /\ mem (x,y) r lemma image_union: forall r : rel 'a 'b, s t: set 'a. image r (union s t) = union (image r s) (image r t) lemma image_add: forall r : rel 'a 'b, dom : set 'a, x:'a. image r (add x dom) = union (image r (singleton x)) (image r dom) end (** {2 Domain, Range, Inverse} Domain, Range and inverse of a relation *) theory InverseDomRan use export Relation function inverse (rel 'a 'b) : rel 'b 'a axiom Inverse_def: forall r : rel 'a 'b. forall x : 'a, y : 'b. mem (y,x) (inverse r) <-> mem (x,y) r function dom (rel 'a 'b) : set 'a axiom dom_def: forall r : rel 'a 'b. forall x : 'a. mem x (dom r) <-> exists y : 'b. mem (x,y) r function ran (rel 'a 'b) : set 'b axiom ran_def: forall r : rel 'a 'b. forall y : 'b. mem y (ran r) <-> exists x : 'a. mem (x,y) r end (** {2 Functions} Partial functions as relations *) theory Function use export Relation (** operator A +-> B : set of partial functions from A to B, seen as a relation *) function (+->) (s:set 'a) (t:set 'b) : set (rel 'a 'b) axiom mem_function: forall f:rel 'a 'b, s:set 'a, t:set 'b. mem f (s +-> t) <-> (forall x:'a, y:'b. mem (x,y) f -> mem x s /\ mem y t) /\ (forall x:'a, y1 y2:'b. mem (x,y1) f /\ mem (x,y2) f -> y1=y2) lemma domain_function: forall f:rel 'a 'b, s:set 'a, t:set 'b, x:'a, y:'b. mem f (s +-> t) -> mem (x,y) f -> mem x s lemma range_function: forall f:rel 'a 'b, s:set 'a, t:set 'b, x:'a, y:'b. mem f (s +-> t) -> mem (x,y) f -> mem y t lemma function_extend_range: forall f:rel 'a 'b, s:set 'a, t u:set 'b. subset t u -> mem f (s +-> t) -> mem f (s +-> u) lemma function_reduce_range: forall f:rel 'a 'b, s:set 'a, t u:set 'b. subset u t -> mem f (s +-> t) -> (forall x:'a, y:'b. mem (x,y) f -> mem y u) -> mem f (s +-> u) use import InverseDomRan function (-->) (s:set 'a) (t:set 'b) : set (rel 'a 'b) axiom mem_total_functions: forall f:rel 'a 'b, s:set 'a, t:set 'b. mem f (s --> t) <-> mem f (s +-> t) /\ dom f == s lemma total_function_is_function: forall f:rel 'a 'b, s:set 'a, t:set 'b. mem f (s --> t) -> mem f (s +-> t) function apply (rel 'a 'b) 'a : 'b axiom apply_def1: forall f:rel 'a 'b, s:set 'a, t:set 'b, a:'a. mem a s /\ mem f (s --> t) -> mem (a, apply f a) f axiom apply_def2: forall f:rel 'a 'b, s:set 'a, t:set 'b, a:'a, b:'b. mem f (s --> t) /\ mem (a,b) f -> b = apply f a lemma injection: forall f:rel 'a 'b, s:set 'a, t:set 'b. forall x y:'a. mem f (s --> t) -> mem (inverse f) (t +-> s) -> mem x s -> mem y s -> (apply f x) = (apply f y) -> x=y end (** {2 Identity} *) theory Identity use export Function function id (set 'a) : rel 'a 'a axiom id_def: forall x y:'a, s:set 'a. mem (x,y) (id s) <-> mem x s /\ x=y use import InverseDomRan lemma id_dom: forall s:set 'a. dom (id s) = s lemma id_ran: forall s:set 'a. ran (id s) = s lemma id_fun: forall s:set 'a. mem (id s) (s +-> s) lemma id_total_fun: forall s:set 'a. mem (id s) (s --> s) end (** {2 Sequences} Finite sequences as total functions on domain 1..n *) theory Sequence use import Function use import Interval use import Identity function seq_length (n:int) (s : set 'a) : set (rel int 'a) = (mk 1 n) --> s function seq (set 'a) : set (rel int 'a) function size (rel int 'a) : int axiom mem_seq : forall s:set 'a, r:rel int 'a. mem r (seq s) <-> size r >= 0 /\ mem r (seq_length (size r) s) lemma seq_as_total_function : forall s:set 'a, r:rel int 'a. mem r (seq s) -> mem r ((mk 1 (size r)) --> s) axiom size_def : forall n: int, r: rel int 'a. size r = n <-> exists s: set 'a. mem r (seq_length n s) goal Test1: mem (id (mk 1 21)) (seq_length 21 (mk 1 21)) goal ValuesLemmas_2: mem (id (mk 1 21)) (seq (mk 1 21)) goal ValuesLemmas_8: (* proven only by z3 *) size (id (mk 1 21)) = 21 goal Test_wrong_size: not(size (id (mk 1 21)) = 22) end theory IsFinite (* cas ou F est utilisÃ© uniquement a droite de appartient: on definit inductivement le predicat "in F(s)" *) use import set.Set inductive is_finite_subset (s1:set 'a) (s2:set 'a) = | Empty: forall s:set 'a. is_finite_subset empty s | Add: forall x:'a, s1 s2:set 'a. is_finite_subset s1 s2 -> is_finite_subset (add x s1) s2 use Interval lemma finite_interval : forall a b:int. is_finite_subset (Interval.mk a b) Interval.integer (* cas general *) function finite_subsets (s:set 'a) : set (set 'a) axiom finite_Empty : forall s: set 'a. mem empty (finite_subsets s) axiom finite_Add: forall x:'a, s1 s2:set 'a. mem s1 (finite_subsets s2) -> mem (add x s1) (finite_subsets s2) axiom finite_inversion: forall s1 s2:set 'a. mem s1 (finite_subsets s2) -> s1 == empty \/ exists x:'a, s3:set 'a. s1 == add x s3 /\ mem s3 (finite_subsets s2) end theory PowerRelation use export Relation use export PowerSet function times (set 'a) (set 'b) : rel 'a 'b axiom times_def: forall a : set 'a, b : set 'b, x : 'a, y : 'b. mem (x,y) (times a b) <-> mem x a /\ mem y b (* relations u v: Set of relations between sets u /\ v *) function relations (u: set 'a) (v: set 'b) : set (rel 'a 'b) = power(times u v) (* following lemmas are needed to type relations *) lemma break_mem_in_add: forall c : ('a, 'b), s : rel 'a 'b, x: 'a, y : 'b. mem c (add (x,y) s) <-> c = (x, y) \/ mem c s lemma break_power_times: forall r : rel 'a 'b, u : set 'a, v : set 'b. mem r (power (times u v)) <-> subset r (times u v) lemma subset_of_times: forall r: rel 'a 'b, u: set 'a, v: set 'b. subset r (times u v) <-> forall x: 'a, y: 'b. mem (x,y) r -> mem x u /\ mem y v end