(** {1 Theory of integers} This file provides the basic theory of integers, and several additional theories for classical functions. *) (** {2 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 (** {2 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 (*** lemma Abs_zero: forall x:int. abs x = 0 -> x = 0 *) end (** {2 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 (** {2 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 (** {2 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 (** {2 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 (** {2 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 (** {2 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 (** {2 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 (** {2 Number of integers satisfying a given predicate} *) module NumOf use Int (** number of `n` such that `a <= n < b` and `p n` *) 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 (** {2 Sum} *) module Sum use Int (** sum of `f n` for `a <= n < b` *) 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 (** {2 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 (** {2 Generic iteration of a function} *) module Iter use Int (** `iter k x` is `f^k(x)` *) 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 (** {2 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 (** {2 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 (** {2 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