Why3 Standard Library index

# Theory of integers

This file provides the basic theory of integers, and several additional theories for classical functions.

## Integers and the basic operators

```theory Int

constant zero : int = 0
constant one  : int = 1

predicate (< ) int int
predicate (> ) (x y : int) = y < x
predicate (<=) (x y : int) = x < y \/ x = y

clone export algebra.OrderedUnitaryCommutativeRing with type t = int,
constant zero = zero, constant one = one, predicate (<=) = (<=)

end

```

## Absolute Value

```theory Abs

use import Int

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

lemma Abs_pos: forall x:int. abs x >= 0

end

```

## Minimum and Maximum

```theory MinMax

use import Int
clone export relations.MinMax with type t = int, predicate le = (<=),
goal TotalOrder.Refl,
goal TotalOrder.Trans,
goal TotalOrder.Antisymm,
goal TotalOrder.Total

end

```

## The Basic Well-Founded Order on Integers

```theory Lex2

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

```

## Euclidean Division

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.

```theory EuclideanDivision

use import Int
use import Abs

function div int int : int
function mod int int : int

axiom Div_mod:
forall x y:int. y <> 0 -> x = y * div x y + mod x y

axiom Mod_bound:
forall x y:int. y <> 0 -> 0 <= mod x y < abs y

lemma Div_unique:
forall x y q:int. y > 0 -> q * y <= x < q * y + y -> div x y = q

lemma Div_bound:
forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x

lemma Mod_1: forall x:int. mod x 1 = 0

lemma Div_1: forall x:int. div x 1 = x

lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0

lemma Div_inf_neg: forall x y:int. 0 < x <= y -> div (-x) y = -1

lemma Mod_0: forall y:int. y <> 0 -> mod 0 y = 0

lemma Div_1_left: forall y:int. y > 1 -> div 1 y = 0

lemma Div_minus1_left: forall y:int. y > 1 -> div (-1) y = -1

lemma Mod_1_left: forall y:int. y > 1 -> mod 1 y = 1

lemma Mod_minus1_left: forall y:int. y > 1 -> mod (-1) y = y - 1

lemma Div_mult: forall x y z:int [div (x * y + z) x].
x > 0 ->
div (x * y + z) x = y + div z x

lemma Mod_mult: forall x y z:int [mod (x * y + z) x].
x > 0 ->
mod (x * y + z) x = mod z x

end

```

## Division by 2

The particular case of Euclidean division by 2

```theory Div2

use import Int

lemma div2:
forall x: int. exists y: int. x = 2*y \/ x = 2*y+1

end

```

## Computer Division

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

```theory ComputerDivision

use import Int
use import Abs

function div int int : int
function mod int int : int

axiom Div_mod:
forall x y:int. y <> 0 -> x = y * div x y + mod x y

axiom Div_bound:
forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x

axiom Mod_bound:
forall x y:int. y <> 0 -> - abs y < mod x y < abs y

axiom Div_sign_pos:
forall x y:int. x >= 0 /\ y > 0 -> div x y >= 0

axiom Div_sign_neg:
forall x y:int. x <= 0 /\ y > 0 -> div x y <= 0

axiom Mod_sign_pos:
forall x y:int. x >= 0 /\ y <> 0 -> mod x y >= 0

axiom Mod_sign_neg:
forall x y:int. x <= 0 /\ y <> 0 -> mod x y <= 0

lemma Rounds_toward_zero:
forall x y:int. y <> 0 -> abs (div x y * y) <= abs x

lemma Div_1: forall x:int. div x 1 = x

lemma Mod_1: forall x:int. mod x 1 = 0

lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0

lemma Mod_inf: forall x y:int. 0 <= x < y -> mod x y = x

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

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

end

```

## Generic Exponentiation of something to an integer exponent

```theory Exponentiation

use import Int

type t
constant one : t
function (*) t t : t
clone algebra.CommutativeMonoid
with type t = t, constant unit = one, function op = (*)

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_mult2 : forall x y: t, n: int. 0 <= n ->
power (x * y) n = power x n * power y n

(* TODO

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

```

## Power of an integer to an integer

```theory Power

use import Int

clone export Exponentiation with type t = int, constant one = one,
function (*) = (*), goal CommutativeMonoid.Assoc,
goal CommutativeMonoid.Unit_def_l, goal CommutativeMonoid.Unit_def_r,
goal CommutativeMonoid.Comm.Comm

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

```

## Number of integers satisfying a given predicate

```theory NumOf

use import Int
use HighOrd
use import Bool

function numof (p: int -> bool) (a b: int) : int
```

number of `n` such that `a <= n < b` and `p n`

```  axiom Numof_empty :
forall p: int -> bool, a b: int.
b <= a -> numof p a b = 0

forall p : int -> bool, a b : int.
a < b -> not (p (b-1)) -> numof p a b = numof p a (b-1)
forall p : int -> bool, a b : int.
a < b -> p (b-1) -> numof p a b = 1 + numof p a (b-1)

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 *)

forall p : int -> bool, a b : int.
a < b -> not p a -> numof p a b = numof p (a+1) b
(* by Numof_append *)
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

```

## Sum

```theory Sum

use import Int
use HighOrd

function sum (a b: int) (f: int -> int) : int
```

sum of `f n` for `a <= n < b`

```  axiom sum_def1:
forall f: int -> int, a b: int.
b <= a -> sum a b f = 0

axiom sum_def2:
forall f: int -> int, a b: int.
a < b -> sum a b f = sum a (b - 1) f + f (b - 1)

lemma sum_left:
forall f: int -> int, a b: int.
a < b -> sum a b f = f a + sum (a + 1) b f

lemma sum_ext:
forall f g: int -> int, a b: int.
(forall i. a <= i < b -> f i = g i) ->
sum a b f = sum a b g

lemma sum_le:
forall f g: int -> int, a b: int.
(forall i. a <= i < b -> f i <= g i) ->
sum a b f <= sum a b g

lemma sum_nonneg:
forall f: int -> int, a b: int.
(forall i. a <= i < b -> 0 <= f i) ->
0 <= sum a b f

lemma sum_decomp:
forall f: int -> int, a b c: int. a <= b <= c ->
sum a c f = sum a b f + sum b c f

lemma sum_zero:
forall f: int -> int, a b: int.
(forall i. a <= i < b -> f i = 0) ->
sum a b f = 0

end

```

## Factorial function

```theory Fact

use import Int

function fact int : int

axiom fact0: fact 0 = 1
axiom factn: forall n:int. n >= 1 -> fact n = n * fact (n-1)

(* in the new system it will be:

let rec function fact (n:int) : int =
requires { n >= 0 }
variant  { n }
= if n = 0 then 1 else n * fact (n-1)

with the semantics

function fact int : int
axiom fact_def : \forall n:int [fact n].
n >= 0 -> fact n = if n = 0 then 1 else n * fact (n-1)

*)

end

```

## Generic iteration of a function

```theory Iter

use import Int

type t
function f t : t

function iter int t : t
```

`iter k x` is `f^k(x)`

```  axiom iter_0: forall x: t. iter 0 x = x
axiom iter_s: forall k: int, x: t. 0 < k -> iter k x = iter (k-1) (f x)

lemma iter_1: forall x: t. iter 1 x = f x
lemma iter_s2: forall k: int, x: t. 0 < k -> iter k x = f (iter (k-1) x)

end

```

## Integers extended with an infinite value

```theory IntInf

use import Int

type t = Finite int | Infinite

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

predicate lt (x y: t) =
match x with
| Infinite -> false
| Finite x ->
match y with
| Infinite -> true
| Finite y -> x < y
end
end

predicate le (x y: t) = lt x y \/ x = y

clone export relations.TotalOrder with type t = t, predicate rel = le,
lemma Refl, lemma Antisymm, lemma Trans, lemma Total

end

```

## Induction principle on integers

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.

```theory SimpleInduction

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

theory Induction

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

theory Fibonacci "Fibonacci numbers"

use import Int

function fib int : int

axiom fib0: fib 0 = 0
axiom fib1: fib 1 = 1
axiom fibn: forall n:int. n >= 2 -> fib n = fib (n-1) + fib (n-2)

end
```

Generated by why3doc 0.87.2