(** {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 (<=) = (<=)

  meta "remove_unused:keep" function (+)
  meta "remove_unused:keep" function (-)
(* do not necessarily keep, to allow for linear arithmetic only
  meta "remove_unused:keep" function (*)
*)
  meta "remove_unused:keep" function (-_)
  meta "remove_unused:keep" predicate (<)
  meta "remove_unused:keep" predicate (<=)
  meta "remove_unused:keep" predicate (>)
  meta "remove_unused:keep" 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
  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

(***
  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
  meta "remove_unused:dependency" axiom Div_mod, function div
  meta "remove_unused:dependency" axiom Div_mod, function mod

  axiom Mod_bound:
    forall x y:int. y <> 0 -> 0 <= mod x y < abs y
  meta "remove_unused:dependency" axiom Mod_bound, function mod

  lemma Div_unique:
    forall x y q:int. y > 0 -> q * y <= x < q * y + y -> div x y = q
  meta "remove_unused:dependency" lemma Div_unique, function div

  lemma Div_bound:
    forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x
  meta "remove_unused:dependency" lemma Div_bound, function div

  lemma Mod_1: forall x:int. mod x 1 = 0
  meta "remove_unused:dependency" lemma Mod_1, function mod

  lemma Div_1: forall x:int. div x 1 = x
  meta "remove_unused:dependency" lemma Div_1, function div

  lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0
  meta "remove_unused:dependency" lemma Div_inf, function div

  lemma Div_inf_neg: forall x y:int. 0 < x <= y -> div (-x) y = -1
  meta "remove_unused:dependency" lemma Div_inf_neg, function div

  lemma Mod_0: forall y:int. y <> 0 -> mod 0 y = 0
  meta "remove_unused:dependency" lemma Mod_0, function mod

  lemma Div_1_left: forall y:int. y > 1 -> div 1 y = 0
  meta "remove_unused:dependency" lemma Div_1_left, function div

  lemma Div_minus1_left: forall y:int. y > 1 -> div (-1) y = -1
  meta "remove_unused:dependency" lemma Div_minus1_left, function div

  lemma Mod_1_left: forall y:int. y > 1 -> mod 1 y = 1
  meta "remove_unused:dependency" lemma Mod_1_left, function mod

  lemma Mod_minus1_left: forall y:int. y > 1 -> mod (-1) y = y - 1
  meta "remove_unused:dependency" lemma Mod_minus1_left, function mod

  lemma Div_mult: forall x y z:int [div (x * y + z) x].
          x > 0 ->
          div (x * y + z) x = y + div z x
  meta "remove_unused:dependency" lemma Div_mult, function div

  lemma Mod_mult: forall x y z:int [mod (x * y + z) x].
          x > 0 ->
          mod (x * y + z) x = mod z x
  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

(** {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
  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

(** {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

(** A similar theory, but with a polymorphic parameter passed
    to function `f` and to function `sum`. *)
module SumParam

  use Int

  (** sum of `f x n` for `a <= n < b` *)
  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

(** {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