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

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

  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

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| Infinitelt "keyword1">m"w  axine export with
  pan class="keyword1">type Infinitegoadicate le| goama goama goama goama umTotal>

  end

Integtion on principle b *igers ex2>

The pihe sa

theory use import Int

  typdicate axiom *: axiom forall n:int. n <= n -> 0 Nump> int> 0 Nump> inta href="int.html#infix.20.2B_86">+1) =  lemma forall x ynt. n <= n -> 0 Nump> int> end

theory egtion on>

  use import Int

  typdicate axima egtion on>

     forall n : t. n <= n -> 0 forall n :kt. n <= n -a href="int.html#infix.20.3C_16">< l -> 0 -

intk> notall x ynt. n <= n -> 0 -

intn axintant axima egtion on_nd: in forall n : t. n : ihref="int.html#infix.20.3C.3D_18"><= n -> 0 forall n :kt. n : ihref="int.html#infix.20.3C.3D_18"><= n -a href="int.html#infix.20.3C_16">< l -> 0 -

intk> notall x ynt. n : ihref="int.html#infix.20.3C.3D_18"><= n -> 0 -

intn end theory use import Int typction axiom int00 axiom int11 axiom forall n:int. n >= 1 -2 inta href="int.html#infix.20-_100">-1) < href="int.html#infix.20.2B_86">+ -1) 2end

v>Irp>Theeric aerdeby why3doc 0.87.p>