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

```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 (<=) = (<=)

end

```

## Absolute Value

```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

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

end

```

## Minimum and Maximum

```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

```

## The Basic Well-Founded Order on Integers

```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

```

## 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.

```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

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

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

```

## Division by 2

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

```

## 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`.

```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

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

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

```

## Generic Exponentiation of something to an integer exponent

```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

```

## Power of an integer to an integer

```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

```

## Number of integers satisfying a given predicate

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

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

```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

```

## Factorial function

```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

```

## Generic iteration of a function

```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

```

## Integers extended with an infinite value

```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

```

## 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.

```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

```

## Fibonacci numbers

```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.4.0