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

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

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)

  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

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)

  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

  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)

  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)

  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