Why3 Standard Library index
This file provides the basic theory of integers, and several additional theories for classical functions.
module Int let constant zero : int = 0 let constant one : int = 1 val (=) (x y : int) : bool ensures { result <-> x = y } val function (-_) int : int val function (+) int int : int val function (*) int int : int val predicate (<) int int : bool let function (-) (x y : int) = x + -y let predicate (>) (x y : int) = y < x let predicate (<=) (x y : int) = x < y || x = y let predicate (>=) (x y : int) = y <= x clone export algebra.OrderedUnitaryCommutativeRing with type t = int, constant zero = zero, constant one = one, function (-_) = (-_), function (+) = (+), function (*) = (*), predicate (<=) = (<=) meta "remove_unused:keep" function (+) meta "remove_unused:keep" function (-) (* do not necessarily keep, to allow for linear arithmetic only meta "remove_unused:keep" function (*) *) meta "remove_unused:keep" function (-_) meta "remove_unused:keep" predicate (<) meta "remove_unused:keep" predicate (<=) meta "remove_unused:keep" predicate (>) meta "remove_unused:keep" predicate (>=) end
module Abs use Int let function abs (x:int) : int = if x >= 0 then x else -x lemma Abs_le: forall x y:int. abs x <= y <-> -y <= x <= y meta "remove_unused:dependency" lemma Abs_le, function abs lemma Abs_pos: forall x:int. abs x >= 0 meta "remove_unused:dependency" lemma Abs_pos, function abs end
module MinMax use Int clone export relations.MinMax with type t = int, predicate le = (<=), goal . let min (x y : int) : int ensures { result = min x y } = if x <= y then x else y let max (x y : int) : int ensures { result = max x y } = if x <= y then y else x end
module Lex2 use Int predicate lt_nat (x y: int) = 0 <= y /\ x < y clone export relations.Lex with type t1 = int, type t2 = int, predicate rel1 = lt_nat, predicate rel2 = lt_nat end
Division and modulo operators with the convention that modulo is always non-negative.
It implies that division rounds down when divisor is positive, and rounds up when divisor is negative.
module EuclideanDivision use Int use Abs function div (x y: int) : int function mod (x y: int) : int axiom Div_mod: forall x y:int. y <> 0 -> x = y * div x y + mod x y meta "remove_unused:dependency" axiom Div_mod, function div meta "remove_unused:dependency" axiom Div_mod, function mod axiom Mod_bound: forall x y:int. y <> 0 -> 0 <= mod x y < abs y meta "remove_unused:dependency" axiom Mod_bound, function mod lemma Div_unique: forall x y q:int. y > 0 -> q * y <= x < q * y + y -> div x y = q meta "remove_unused:dependency" lemma Div_unique, function div lemma Div_bound: forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x meta "remove_unused:dependency" lemma Div_bound, function div lemma Mod_1: forall x:int. mod x 1 = 0 meta "remove_unused:dependency" lemma Mod_1, function mod lemma Div_1: forall x:int. div x 1 = x meta "remove_unused:dependency" lemma Div_1, function div lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0 meta "remove_unused:dependency" lemma Div_inf, function div lemma Div_inf_neg: forall x y:int. 0 < x <= y -> div (-x) y = -1 meta "remove_unused:dependency" lemma Div_inf_neg, function div lemma Mod_0: forall y:int. y <> 0 -> mod 0 y = 0 meta "remove_unused:dependency" lemma Mod_0, function mod lemma Div_1_left: forall y:int. y > 1 -> div 1 y = 0 meta "remove_unused:dependency" lemma Div_1_left, function div lemma Div_minus1_left: forall y:int. y > 1 -> div (-1) y = -1 meta "remove_unused:dependency" lemma Div_minus1_left, function div lemma Mod_1_left: forall y:int. y > 1 -> mod 1 y = 1 meta "remove_unused:dependency" lemma Mod_1_left, function mod lemma Mod_minus1_left: forall y:int. y > 1 -> mod (-1) y = y - 1 meta "remove_unused:dependency" lemma Mod_minus1_left, function mod lemma Div_mult: forall x y z:int [div (x * y + z) x]. x > 0 -> div (x * y + z) x = y + div z x meta "remove_unused:dependency" lemma Div_mult, function div lemma Mod_mult: forall x y z:int [mod (x * y + z) x]. x > 0 -> mod (x * y + z) x = mod z x meta "remove_unused:dependency" lemma Mod_mult, function mod val div (x y:int) : int requires { y <> 0 } ensures { result = div x y } val mod (x y:int) : int requires { y <> 0 } ensures { result = mod x y } end
The particular case of Euclidean division by 2
module Div2 use Int lemma div2: forall x: int. exists y: int. x = 2*y \/ x = 2*y+1 end
Division and modulo operators with the same conventions as mainstream
programming language such as C, Java, OCaml, that is, division rounds
towards zero, and thus mod x y has the same sign as x.
module ComputerDivision use Int use Abs function div (x y: int) : int function mod (x y: int) : int axiom Div_mod: forall x y:int. y <> 0 -> x = y * div x y + mod x y meta "remove_unused:dependency" axiom Div_mod, function div meta "remove_unused:dependency" axiom Div_mod, function mod axiom Div_bound: forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x meta "remove_unused:dependency" axiom Div_bound, function div meta "remove_unused:dependency" axiom Div_bound, function mod axiom Mod_bound: forall x y:int. y <> 0 -> - abs y < mod x y < abs y meta "remove_unused:dependency" axiom Mod_bound, function div meta "remove_unused:dependency" axiom Mod_bound, function mod axiom Div_sign_pos: forall x y:int. x >= 0 /\ y > 0 -> div x y >= 0 meta "remove_unused:dependency" axiom Div_sign_pos, function div meta "remove_unused:dependency" axiom Div_sign_pos, function mod axiom Div_sign_neg: forall x y:int. x <= 0 /\ y > 0 -> div x y <= 0 meta "remove_unused:dependency" axiom Div_sign_neg, function div meta "remove_unused:dependency" axiom Div_sign_neg, function mod axiom Mod_sign_pos: forall x y:int. x >= 0 /\ y <> 0 -> mod x y >= 0 meta "remove_unused:dependency" axiom Mod_sign_pos, function div meta "remove_unused:dependency" axiom Mod_sign_pos, function mod axiom Mod_sign_neg: forall x y:int. x <= 0 /\ y <> 0 -> mod x y <= 0 meta "remove_unused:dependency" axiom Mod_sign_neg, function div meta "remove_unused:dependency" axiom Mod_sign_neg, function mod lemma Rounds_toward_zero: forall x y:int. y <> 0 -> abs (div x y * y) <= abs x meta "remove_unused:dependency" lemma Rounds_toward_zero, function div meta "remove_unused:dependency" lemma Rounds_toward_zero, function mod lemma Div_1: forall x:int. div x 1 = x meta "remove_unused:dependency" lemma Div_1, function div meta "remove_unused:dependency" lemma Div_1, function mod lemma Mod_1: forall x:int. mod x 1 = 0 meta "remove_unused:dependency" lemma Mod_1, function div meta "remove_unused:dependency" lemma Mod_1, function mod lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0 meta "remove_unused:dependency" lemma Div_inf, function div meta "remove_unused:dependency" lemma Div_inf, function mod lemma Mod_inf: forall x y:int. 0 <= x < y -> mod x y = x meta "remove_unused:dependency" lemma Mod_inf, function div meta "remove_unused:dependency" lemma Mod_inf, function mod lemma Div_mult: forall x y z:int [div (x * y + z) x]. x > 0 /\ y >= 0 /\ z >= 0 -> div (x * y + z) x = y + div z x meta "remove_unused:dependency" lemma Div_mult, function div meta "remove_unused:dependency" lemma Div_mult, function mod lemma Mod_mult: forall x y z:int [mod (x * y + z) x]. x > 0 /\ y >= 0 /\ z >= 0 -> mod (x * y + z) x = mod z x meta "remove_unused:dependency" lemma Mod_mult, function div meta "remove_unused:dependency" lemma Mod_mult, function mod val div (x y:int) : int requires { y <> 0 } ensures { result = div x y } val mod (x y:int) : int requires { y <> 0 } ensures { result = mod x y } end
module Exponentiation use Int type t constant one : t function (*) t t : t clone export algebra.Monoid with type t = t, constant unit = one, function op = (*), axiom . (* TODO: implement with let rec once let cloning is done *) function power t int : t axiom Power_0 : forall x: t. power x 0 = one axiom Power_s : forall x: t, n: int. n >= 0 -> power x (n+1) = x * power x n lemma Power_s_alt: forall x: t, n: int. n > 0 -> power x n = x * power x (n-1) lemma Power_1 : forall x : t. power x 1 = x lemma Power_sum : forall x: t, n m: int. 0 <= n -> 0 <= m -> power x (n+m) = power x n * power x m lemma Power_mult : forall x:t, n m : int. 0 <= n -> 0 <= m -> power x (Int.(*) n m) = power (power x n) m lemma Power_comm1 : forall x y: t. x * y = y * x -> forall n:int. 0 <= n -> power x n * y = y * power x n lemma Power_comm2 : forall x y: t. x * y = y * x -> forall n:int. 0 <= n -> power (x * y) n = power x n * power y n (* TODO use ComputerDivision lemma Power_even : forall x:t, n:int. n >= 0 -> mod n 2 = 0 -> power x n = power (x*x) (div n 2) lemma power_odd : forall x:t, n:int. n >= 0 -> mod n 2 <> 0 -> power x n = x * power (x*x) (div n 2) *) end
module Power use Int (* TODO: remove once power is implemented in Exponentiation *) val function power int int : int clone export Exponentiation with type t = int, constant one = one, function (*) = (*), function power = power, goal Assoc, goal Unit_def_l, goal Unit_def_r, axiom Power_0, axiom Power_s lemma Power_non_neg: forall x y. x >= 0 /\ y >= 0 -> power x y >= 0 lemma Power_pos: forall x y. x > 0 /\ y >= 0 -> power x y > 0 lemma Power_monotonic: forall x n m:int. 0 < x /\ 0 <= n <= m -> power x n <= power x m end
module NumOf use Int let rec function numof (p: int -> bool) (a b: int) : int variant { b - a } = if b <= a then 0 else if p (b - 1) then 1 + numof p a (b - 1) else numof p a (b - 1)
number of n such that a <= n < b and p n
lemma Numof_bounds : forall p : int -> bool, a b : int. a < b -> 0 <= numof p a b <= b - a (* direct when a>=b, by induction on b when a <= b *) lemma Numof_append : forall p : int -> bool, a b c : int. a <= b <= c -> numof p a c = numof p a b + numof p b c (* by induction on c *) lemma Numof_left_no_add : forall p : int -> bool, a b : int. a < b -> not p a -> numof p a b = numof p (a+1) b (* by Numof_append *) lemma Numof_left_add : forall p : int -> bool, a b : int. a < b -> p a -> numof p a b = 1 + numof p (a+1) b (* by Numof_append *) lemma Empty : forall p : int -> bool, a b : int. (forall n : int. a <= n < b -> not p n) -> numof p a b = 0 (* by induction on b *) lemma Full : forall p : int -> bool, a b : int. a <= b -> (forall n : int. a <= n < b -> p n) -> numof p a b = b - a (* by induction on b *) lemma numof_increasing: forall p : int -> bool, i j k : int. i <= j <= k -> numof p i j <= numof p i k (* by Numof_append and Numof_non_negative *) lemma numof_strictly_increasing: forall p: int -> bool, i j k l: int. i <= j <= k < l -> p k -> numof p i j < numof p i l (* by Numof_append and numof_increasing *) lemma numof_change_any: forall p1 p2: int -> bool, a b: int. (forall j: int. a <= j < b -> p1 j -> p2 j) -> numof p2 a b >= numof p1 a b lemma numof_change_some: forall p1 p2: int -> bool, a b i: int. a <= i < b -> (forall j: int. a <= j < b -> p1 j -> p2 j) -> not (p1 i) -> p2 i -> numof p2 a b > numof p1 a b lemma numof_change_equiv: forall p1 p2: int -> bool, a b: int. (forall j: int. a <= j < b -> p1 j <-> p2 j) -> numof p2 a b = numof p1 a b end
module Sum use Int let rec function sum (f: int -> int) (a b: int) : int variant { b - a } = if b <= a then 0 else sum f a (b - 1) + f (b - 1)
sum of f n for a <= n < b
lemma sum_left: forall f: int -> int, a b: int. a < b -> sum f a b = f a + sum f (a + 1) b lemma sum_ext: forall f g: int -> int, a b: int. (forall i. a <= i < b -> f i = g i) -> sum f a b = sum g a b lemma sum_le: forall f g: int -> int, a b: int. (forall i. a <= i < b -> f i <= g i) -> sum f a b <= sum g a b lemma sum_zero: forall f: int -> int, a b: int. (forall i. a <= i < b -> f i = 0) -> sum f a b = 0 lemma sum_nonneg: forall f: int -> int, a b: int. (forall i. a <= i < b -> 0 <= f i) -> 0 <= sum f a b lemma sum_decomp: forall f: int -> int, a b c: int. a <= b <= c -> sum f a c = sum f a b + sum f b c let rec lemma shift_left (f g: int -> int) (a b c d: int) requires { b - a = d - c } requires { forall i. a <= i < b -> f i = g (c + i - a) } variant { b - a } ensures { sum f a b = sum g c d } = if a < b then shift_left f g (a+1) b (c+1) d end module SumParam
A similar theory, but with a polymorphic parameter passed
to function f and to function sum.
use Int let rec function sum (f: 'a -> int -> int) (x: 'a) (a b: int) : int variant { b - a } = if b <= a then 0 else sum f x a (b - 1) + f x (b - 1)
sum of f x n for a <= n < b
lemma sum_left: forall f: 'a -> int -> int, x: 'a, a b: int. a < b -> sum f x a b = f x a + sum f x (a + 1) b lemma sum_ext: forall f: 'a -> int -> int, x: 'a, g: 'b -> int -> int, y: 'b, a b: int. (forall i. a <= i < b -> f x i = g y i) -> sum f x a b = sum g y a b lemma sum_le: forall f: 'a -> int -> int, x: 'a, g: 'b -> int -> int, y: 'b, a b: int. (forall i. a <= i < b -> f x i <= g y i) -> sum f x a b <= sum g y a b lemma sum_zero: forall f: 'a -> int -> int, x: 'a, a b: int. (forall i. a <= i < b -> f x i = 0) -> sum f x a b = 0 lemma sum_nonneg: forall f: 'a -> int -> int, x: 'a, a b: int. (forall i. a <= i < b -> 0 <= f x i) -> 0 <= sum f x a b lemma sum_decomp: forall f: 'a -> int -> int, x: 'a, a b c: int. a <= b <= c -> sum f x a c = sum f x a b + sum f x b c let rec lemma shift_left (f: 'a -> int -> int) (x: 'a) (g: 'b -> int -> int) (y: 'b) (a b c d: int) requires { b - a = d - c } requires { forall i. a <= i < b -> f x i = g y (c + i - a) } variant { b - a } ensures { sum f x a b = sum g y c d } = if a < b then shift_left f x g y (a+1) b (c+1) d let rec lemma sum_middle_change (f:'a -> int -> int) (c1 c2:'a) (i j l: int) requires { i <= l < j } ensures { (forall k : int. i <= k < j -> k <> l -> f c1 k = f c2 k) -> sum f c1 i j - f c1 l = sum f c2 i j - f c2 l } variant { j - l } = if l = (j-1) then () else sum_middle_change f c1 c2 i (j-1) l end
module Fact use Int let rec function fact (n: int) : int requires { n >= 0 } variant { n } = if n = 0 then 1 else n * fact (n-1) end
module Iter use Int let rec function iter (f: 'a -> 'a) (k: int) (x: 'a) : 'a requires { k >= 0 } variant { k } = if k = 0 then x else iter f (k - 1) (f x)
iter k x is f^k(x)
lemma iter_1: forall f, x: 'a. iter f 1 x = f x lemma iter_s: forall f, k, x: 'a. 0 < k -> iter f k x = f (iter f (k - 1) x) end
module IntInf use Int type t = Finite int | Infinite let function add (x: t) (y: t) : t = match x with | Infinite -> Infinite | Finite x -> match y with | Infinite -> Infinite | Finite y -> Finite (x + y) end end let predicate eq (x y: t) = match x, y with | Infinite, Infinite -> true | Finite x, Finite y -> x = y | _, _ -> false end let predicate lt (x y: t) = match x with | Infinite -> false | Finite x -> match y with | Infinite -> true | Finite y -> x < y end end let predicate le (x y: t) = lt x y || eq x y clone export relations.TotalOrder with type t = t, predicate rel = le, lemma Refl, lemma Antisymm, lemma Trans, lemma Total end
This theory can be cloned with the wanted predicate, to perform an induction, either on nonnegative integers, or more generally on integers greater or equal a given bound.
module SimpleInduction use Int predicate p int axiom base: p 0 axiom induction_step: forall n:int. 0 <= n -> p n -> p (n+1) lemma SimpleInduction : forall n:int. 0 <= n -> p n end module Induction use Int predicate p int lemma Induction : (forall n:int. 0 <= n -> (forall k:int. 0 <= k < n -> p k) -> p n) -> forall n:int. 0 <= n -> p n constant bound : int lemma Induction_bound : (forall n:int. bound <= n -> (forall k:int. bound <= k < n -> p k) -> p n) -> forall n:int. bound <= n -> p n end module HOInduction use Int let lemma induction (p: int -> bool) requires { p 0 } requires { forall n. 0 <= n >= 0 -> p n -> p (n+1) } ensures { forall n. 0 <= n -> p n } = let rec lemma f (n: int) requires { n >= 0 } ensures { p n } variant {n} = if n > 0 then f (n-1) in f 0 end
module Fibonacci use Int let rec function fib (n: int) : int requires { n >= 0 } variant { n } = if n = 0 then 0 else if n = 1 then 1 else fib (n-1) + fib (n-2) end module WFltof use Int use relations.WellFounded type t function f t : int axiom f_nonneg: forall x. 0 <= f x predicate ltof (x y: t) = f x < f y let rec lemma acc_ltof (n: int) requires { 0 <= n } ensures { forall x. f x < n -> acc ltof x } variant { n } = if n > 0 then acc_ltof (n-1) lemma wf_ltof: well_founded ltof end
Generated by why3doc 1.8.0