stdlib/int.mlw

   1
   2 (** {1 Theory of integers}
   3
   4 This file provides the basic theory of integers, and several additional
   5 theories for classical functions.
   6
   7 *)
   8
   9 (** {2 Integers and the basic operators} *)
  10
  11 module Int
  12
  13   let constant zero : int = 0
  14   let constant one  : int = 1
  15
  16   val (=) (x y : int) : bool ensures { result <-> x = y }
  17
  18   val function  (-_) int : int
  19   val function  (+)  int int : int
  20   val function  (*)  int int : int
  21   val predicate (<)  int int : bool
  22
  23   let function  (-)  (x y : int) = x + -y
  24   let predicate (>)  (x y : int) = y < x
  25   let predicate (<=) (x y : int) = x < y || x = y
  26   let predicate (>=) (x y : int) = y <= x
  27
  28   clone export algebra.OrderedUnitaryCommutativeRing with
  29     type t = int, constant zero = zero, constant one = one,
  30     function (-_) = (-_), function (+) = (+),
  31     function (*) = (*), predicate (<=) = (<=)
  32
  33   meta "remove_unused:keep" function (+)
  34   meta "remove_unused:keep" function (-)
  35 (* do not necessarily keep, to allow for linear arithmetic only
  36   meta "remove_unused:keep" function (*)
  37 *)
  38   meta "remove_unused:keep" function (-_)
  39   meta "remove_unused:keep" predicate (<)
  40   meta "remove_unused:keep" predicate (<=)
  41   meta "remove_unused:keep" predicate (>)
  42   meta "remove_unused:keep" predicate (>=)
  43
  44 end
  45
  46 (** {2 Absolute Value} *)
  47
  48 module Abs
  49
  50   use Int
  51
  52   let function abs (x:int) : int = if x >= 0 then x else -x
  53
  54   lemma Abs_le: forall x y:int. abs x <= y <-> -y <= x <= y
  55   meta "remove_unused:dependency" lemma Abs_le, function abs
  56
  57   lemma Abs_pos: forall x:int. abs x >= 0
  58   meta "remove_unused:dependency" lemma Abs_pos, function abs
  59
  60 (***
  61   lemma Abs_zero: forall x:int. abs x = 0 -> x = 0
  62 *)
  63
  64 end
  65
  66 (** {2 Minimum and Maximum} *)
  67
  68 module MinMax
  69
  70   use Int
  71
  72   clone export relations.MinMax with type t = int, predicate le = (<=), goal .
  73
  74   let min (x y : int) : int
  75     ensures { result = min x y }
  76   = if x <= y then x else y
  77
  78   let max (x y : int) : int
  79     ensures { result = max x y }
  80    = if x <= y then y else x
  81
  82
  83 end
  84
  85 (** {2 The Basic Well-Founded Order on Integers} *)
  86
  87 module Lex2
  88
  89   use Int
  90
  91   predicate lt_nat (x y: int) = 0 <= y /\ x < y
  92
  93   clone export relations.Lex with type t1 = int, type t2 = int,
  94     predicate rel1 = lt_nat, predicate rel2 = lt_nat
  95
  96 end
  97
  98 (** {2 Euclidean Division}
  99
 100 Division and modulo operators with the convention
 101 that modulo is always non-negative.
 102
 103 It implies that division rounds down when divisor is positive, and
 104 rounds up when divisor is negative.
 105
 106 *)
 107
 108 module EuclideanDivision
 109
 110   use Int
 111   use Abs
 112
 113   function div (x y: int) : int
 114   function mod (x y: int) : int
 115
 116   axiom Div_mod:
 117     forall x y:int. y <> 0 -> x = y * div x y + mod x y
 118
 119   axiom Mod_bound:
 120     forall x y:int. y <> 0 -> 0 <= mod x y < abs y
 121
 122   lemma Div_unique:
 123     forall x y q:int. y > 0 -> q * y <= x < q * y + y -> div x y = q
 124
 125   lemma Div_bound:
 126     forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x
 127
 128   lemma Mod_1: forall x:int. mod x 1 = 0
 129
 130   lemma Div_1: forall x:int. div x 1 = x
 131
 132   lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0
 133
 134   lemma Div_inf_neg: forall x y:int. 0 < x <= y -> div (-x) y = -1
 135
 136   lemma Mod_0: forall y:int. y <> 0 -> mod 0 y = 0
 137
 138   lemma Div_1_left: forall y:int. y > 1 -> div 1 y = 0
 139
 140   lemma Div_minus1_left: forall y:int. y > 1 -> div (-1) y = -1
 141
 142   lemma Mod_1_left: forall y:int. y > 1 -> mod 1 y = 1
 143
 144   lemma Mod_minus1_left: forall y:int. y > 1 -> mod (-1) y = y - 1
 145
 146   lemma Div_mult: forall x y z:int [div (x * y + z) x].
 147           x > 0 ->
 148           div (x * y + z) x = y + div z x
 149
 150   lemma Mod_mult: forall x y z:int [mod (x * y + z) x].
 151           x > 0 ->
 152           mod (x * y + z) x = mod z x
 153
 154   val div (x y:int) : int
 155     requires { y <> 0 }
 156     ensures { result = div x y }
 157
 158   val mod (x y:int) : int
 159     requires { y <> 0 }
 160     ensures { result = mod x y }
 161
 162
 163 end
 164
 165 (** {2 Division by 2}
 166
 167 The particular case of Euclidean division by 2
 168
 169 *)
 170
 171 module Div2
 172
 173   use Int
 174
 175   lemma div2:
 176     forall x: int. exists y: int. x = 2*y \/ x = 2*y+1
 177
 178 end
 179
 180 (** {2 Computer Division}
 181
 182 Division and modulo operators with the same conventions as mainstream
 183 programming language such as C, Java, OCaml, that is, division rounds
 184 towards zero, and thus `mod x y` has the same sign as `x`.
 185
 186 *)
 187
 188 module ComputerDivision
 189
 190   use Int
 191   use Abs
 192
 193   function div (x y: int) : int
 194   function mod (x y: int) : int
 195
 196   axiom Div_mod:
 197     forall x y:int. y <> 0 -> x = y * div x y + mod x y
 198   meta "remove_unused:dependency" axiom Div_mod, function div
 199   meta "remove_unused:dependency" axiom Div_mod, function mod
 200
 201   axiom Div_bound:
 202     forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x
 203   meta "remove_unused:dependency" axiom Div_bound, function div
 204   meta "remove_unused:dependency" axiom Div_bound, function mod
 205
 206   axiom Mod_bound:
 207     forall x y:int. y <> 0 -> - abs y < mod x y < abs y
 208   meta "remove_unused:dependency" axiom Mod_bound, function div
 209   meta "remove_unused:dependency" axiom Mod_bound, function mod
 210
 211   axiom Div_sign_pos:
 212     forall x y:int. x >= 0 /\ y > 0 -> div x y >= 0
 213   meta "remove_unused:dependency" axiom Div_sign_pos, function div
 214   meta "remove_unused:dependency" axiom Div_sign_pos, function mod
 215
 216   axiom Div_sign_neg:
 217     forall x y:int. x <= 0 /\ y > 0 -> div x y <= 0
 218   meta "remove_unused:dependency" axiom Div_sign_neg, function div
 219   meta "remove_unused:dependency" axiom Div_sign_neg, function mod
 220
 221   axiom Mod_sign_pos:
 222     forall x y:int. x >= 0 /\ y <> 0 -> mod x y >= 0
 223   meta "remove_unused:dependency" axiom Mod_sign_pos, function div
 224   meta "remove_unused:dependency" axiom Mod_sign_pos, function mod
 225
 226   axiom Mod_sign_neg:
 227     forall x y:int. x <= 0 /\ y <> 0 -> mod x y <= 0
 228   meta "remove_unused:dependency" axiom Mod_sign_neg, function div
 229   meta "remove_unused:dependency" axiom Mod_sign_neg, function mod
 230
 231   lemma Rounds_toward_zero:
 232     forall x y:int. y <> 0 -> abs (div x y * y) <= abs x
 233   meta "remove_unused:dependency" lemma Rounds_toward_zero, function div
 234   meta "remove_unused:dependency" lemma Rounds_toward_zero, function mod
 235
 236   lemma Div_1: forall x:int. div x 1 = x
 237   meta "remove_unused:dependency" lemma Div_1, function div
 238   meta "remove_unused:dependency" lemma Div_1, function mod
 239
 240   lemma Mod_1: forall x:int. mod x 1 = 0
 241   meta "remove_unused:dependency" lemma Mod_1, function div
 242   meta "remove_unused:dependency" lemma Mod_1, function mod
 243
 244   lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0
 245   meta "remove_unused:dependency" lemma Div_inf, function div
 246   meta "remove_unused:dependency" lemma Div_inf, function mod
 247
 248   lemma Mod_inf: forall x y:int. 0 <= x < y -> mod x y = x
 249   meta "remove_unused:dependency" lemma Mod_inf, function div
 250   meta "remove_unused:dependency" lemma Mod_inf, function mod
 251
 252   lemma Div_mult: forall x y z:int [div (x * y + z) x].
 253           x > 0 /\ y >= 0 /\ z >= 0 ->
 254           div (x * y + z) x = y + div z x
 255   meta "remove_unused:dependency" lemma Div_mult, function div
 256   meta "remove_unused:dependency" lemma Div_mult, function mod
 257
 258   lemma Mod_mult: forall x y z:int [mod (x * y + z) x].
 259           x > 0 /\ y >= 0 /\ z >= 0 ->
 260           mod (x * y + z) x = mod z x
 261   meta "remove_unused:dependency" lemma Mod_mult, function div
 262   meta "remove_unused:dependency" lemma Mod_mult, function mod
 263
 264   val div (x y:int) : int
 265     requires { y <> 0 }
 266     ensures { result = div x y }
 267
 268   val mod (x y:int) : int
 269     requires { y <> 0 }
 270     ensures { result = mod x y }
 271
 272 end
 273
 274 (** {2 Generic Exponentiation of something to an integer exponent} *)
 275
 276 module Exponentiation
 277
 278   use Int
 279
 280   type t
 281   constant one : t
 282   function (*) t t : t
 283
 284   clone export algebra.Monoid
 285     with type t = t, constant unit = one, function op = (*), axiom .
 286
 287   (* TODO: implement with let rec once let cloning is done *)
 288   function power t int : t
 289
 290   axiom Power_0 : forall x: t. power x 0 = one
 291
 292   axiom Power_s : forall x: t, n: int. n >= 0 -> power x (n+1) = x * power x n
 293
 294   lemma Power_s_alt: forall x: t, n: int. n > 0 -> power x n = x * power x (n-1)
 295
 296   lemma Power_1 : forall x : t. power x 1 = x
 297
 298   lemma Power_sum : forall x: t, n m: int. 0 <= n -> 0 <= m ->
 299     power x (n+m) = power x n * power x m
 300
 301   lemma Power_mult : forall x:t, n m : int. 0 <= n -> 0 <= m ->
 302     power x (Int.(*) n m) = power (power x n) m
 303
 304   lemma Power_comm1 : forall x y: t. x * y = y * x ->
 305     forall n:int. 0 <= n ->
 306     power x n * y = y * power x n
 307
 308   lemma Power_comm2 : forall x y: t. x * y = y * x ->
 309     forall n:int. 0 <= n ->
 310     power (x * y) n = power x n * power y n
 311
 312 (* TODO
 313
 314   use ComputerDivision
 315
 316   lemma Power_even : forall x:t, n:int. n >= 0 -> mod n 2 = 0 ->
 317     power x n = power (x*x) (div n 2)
 318
 319   lemma power_odd : forall x:t, n:int. n >= 0 -> mod n 2 <> 0 ->
 320     power x n = x * power (x*x) (div n 2)
 321 *)
 322
 323 end
 324
 325 (** {2 Power of an integer to an integer } *)
 326
 327 module Power
 328
 329   use Int
 330
 331   (* TODO: remove once power is implemented in Exponentiation *)
 332   val function power int int : int
 333
 334   clone export Exponentiation with
 335     type t = int, constant one = one,
 336     function (*) = (*), function power = power,
 337     goal Assoc, goal Unit_def_l, goal Unit_def_r,
 338     axiom Power_0, axiom Power_s
 339
 340   lemma Power_non_neg:
 341      forall x y. x >= 0 /\ y >= 0 -> power x y >= 0
 342
 343   lemma Power_pos:
 344      forall x y. x > 0 /\ y >= 0 -> power x y > 0
 345
 346   lemma Power_monotonic:
 347     forall x n m:int. 0 < x /\ 0 <= n <= m -> power x n <= power x m
 348
 349 end
 350
 351 (** {2 Number of integers satisfying a given predicate} *)
 352
 353 module NumOf
 354
 355   use Int
 356
 357   (** number of `n` such that `a <= n < b` and `p n` *)
 358   let rec function numof (p: int -> bool) (a b: int) : int
 359     variant { b - a }
 360   = if b <= a then 0 else
 361     if p (b - 1) then 1 + numof p a (b - 1)
 362                  else     numof p a (b - 1)
 363
 364   lemma Numof_bounds :
 365     forall p : int -> bool, a b : int. a < b -> 0 <= numof p a b <= b - a
 366     (* direct when a>=b, by induction on b when a <= b *)
 367
 368   lemma Numof_append :
 369     forall p : int -> bool, a b c : int.
 370     a <= b <= c -> numof p a c = numof p a b + numof p b c
 371     (* by induction on c *)
 372
 373   lemma Numof_left_no_add :
 374     forall p : int -> bool, a b : int.
 375     a < b -> not p a -> numof p a b = numof p (a+1) b
 376     (* by Numof_append *)
 377   lemma Numof_left_add :
 378     forall p : int -> bool, a b : int.
 379     a < b -> p a -> numof p a b = 1 + numof p (a+1) b
 380     (* by Numof_append *)
 381
 382   lemma Empty :
 383     forall p : int -> bool, a b : int.
 384     (forall n : int. a <= n < b -> not p n) -> numof p a b = 0
 385     (* by induction on b *)
 386
 387   lemma Full :
 388     forall p : int -> bool, a b : int. a <= b ->
 389     (forall n : int. a <= n < b -> p n) -> numof p a b = b - a
 390     (* by induction on b *)
 391
 392   lemma numof_increasing:
 393     forall p : int -> bool, i j k : int.
 394     i <= j <= k -> numof p i j <= numof p i k
 395     (* by Numof_append and Numof_non_negative *)
 396
 397   lemma numof_strictly_increasing:
 398     forall p: int -> bool, i j k l: int.
 399     i <= j <= k < l -> p k -> numof p i j < numof p i l
 400     (* by Numof_append and numof_increasing *)
 401
 402   lemma numof_change_any:
 403     forall p1 p2: int -> bool, a b: int.
 404     (forall j: int. a <= j < b -> p1 j -> p2 j) ->
 405     numof p2 a b >= numof p1 a b
 406
 407   lemma numof_change_some:
 408     forall p1 p2: int -> bool, a b i: int. a <= i < b ->
 409     (forall j: int. a <= j < b -> p1 j -> p2 j) ->
 410     not (p1 i) -> p2 i ->
 411     numof p2 a b > numof p1 a b
 412
 413   lemma numof_change_equiv:
 414     forall p1 p2: int -> bool, a b: int.
 415     (forall j: int. a <= j < b -> p1 j <-> p2 j) ->
 416     numof p2 a b = numof p1 a b
 417
 418 end
 419
 420 (** {2 Sum} *)
 421
 422 module Sum
 423
 424   use Int
 425
 426   (** sum of `f n` for `a <= n < b` *)
 427   let rec function sum (f: int -> int) (a b: int) : int
 428     variant { b - a }
 429   = if b <= a then 0 else sum f a (b - 1) + f (b - 1)
 430
 431   lemma sum_left:
 432     forall f: int -> int, a b: int.
 433     a < b -> sum f a b = f a + sum f (a + 1) b
 434
 435   lemma sum_ext:
 436     forall f g: int -> int, a b: int.
 437     (forall i. a <= i < b -> f i = g i) ->
 438     sum f a b = sum g a b
 439
 440   lemma sum_le:
 441     forall f g: int -> int, a b: int.
 442     (forall i. a <= i < b -> f i <= g i) ->
 443     sum f a b <= sum g a b
 444
 445   lemma sum_zero:
 446     forall f: int -> int, a b: int.
 447     (forall i. a <= i < b -> f i = 0) ->
 448     sum f a b = 0
 449
 450   lemma sum_nonneg:
 451     forall f: int -> int, a b: int.
 452     (forall i. a <= i < b -> 0 <= f i) ->
 453     0 <= sum f a b
 454
 455   lemma sum_decomp:
 456     forall f: int -> int, a b c: int. a <= b <= c ->
 457     sum f a c = sum f a b + sum f b c
 458
 459   let rec lemma shift_left (f g: int -> int) (a b c d: int)
 460     requires { b - a = d - c }
 461     requires { forall i. a <= i < b -> f i  = g (c + i - a) }
 462     variant  { b - a }
 463     ensures  { sum f a b = sum g c d }
 464   = if a < b then shift_left f g (a+1) b (c+1) d
 465
 466 end
 467
 468 (** A similar theory, but with a polymorphic parameter passed
 469     to function `f` and to function `sum`. *)
 470 module SumParam
 471
 472   use Int
 473
 474   (** sum of `f x n` for `a <= n < b` *)
 475   let rec function sum (f: 'a -> int -> int) (x: 'a) (a b: int) : int
 476     variant { b - a }
 477   = if b <= a then 0 else sum f x a (b - 1) + f x (b - 1)
 478
 479   lemma sum_left:
 480     forall f: 'a -> int -> int, x: 'a, a b: int.
 481     a < b -> sum f x a b = f x a + sum f x (a + 1) b
 482
 483   lemma sum_ext:
 484     forall f: 'a -> int -> int, x: 'a, g: 'b -> int -> int, y: 'b, a b: int.
 485     (forall i. a <= i < b -> f x i = g y i) ->
 486     sum f x a b = sum g y a b
 487
 488   lemma sum_le:
 489     forall f: 'a -> int -> int, x: 'a, g: 'b -> int -> int, y: 'b, a b: int.
 490     (forall i. a <= i < b -> f x i <= g y i) ->
 491     sum f x a b <= sum g y a b
 492
 493   lemma sum_zero:
 494     forall f: 'a -> int -> int, x: 'a, a b: int.
 495     (forall i. a <= i < b -> f x i = 0) ->
 496     sum f x a b = 0
 497
 498   lemma sum_nonneg:
 499     forall f: 'a -> int -> int, x: 'a, a b: int.
 500     (forall i. a <= i < b -> 0 <= f x i) ->
 501     0 <= sum f x a b
 502
 503   lemma sum_decomp:
 504     forall f: 'a -> int -> int, x: 'a, a b c: int. a <= b <= c ->
 505     sum f x a c = sum f x a b + sum f x b c
 506
 507   let rec lemma shift_left
 508     (f: 'a -> int -> int) (x: 'a)
 509     (g: 'b -> int -> int) (y: 'b) (a b c d: int)
 510     requires { b - a = d - c }
 511     requires { forall i. a <= i < b -> f x i  = g y (c + i - a) }
 512     variant  { b - a }
 513     ensures  { sum f x a b = sum g y c d }
 514   = if a < b then shift_left f x g y (a+1) b (c+1) d
 515
 516   let rec lemma sum_middle_change (f:'a -> int -> int) (c1 c2:'a) (i j l: int)
 517     requires { i <= l < j }
 518     ensures  { (forall k : int. i <= k < j -> k <> l -> f c1 k = f c2 k) ->
 519                sum f c1 i j - f c1 l = sum f c2 i j - f c2 l }
 520     variant  { j - l }
 521   = if l = (j-1) then () else sum_middle_change f c1 c2 i (j-1) l
 522
 523 end
 524
 525 (** {2 Factorial function} *)
 526
 527 module Fact
 528
 529   use Int
 530
 531   let rec function fact (n: int) : int
 532     requires { n >= 0 }
 533     variant  { n }
 534   = if n = 0 then 1 else n * fact (n-1)
 535
 536 end
 537
 538 (** {2 Generic iteration of a function} *)
 539
 540 module Iter
 541
 542   use Int
 543
 544   (** `iter k x` is `f^k(x)` *)
 545   let rec function iter (f: 'a -> 'a) (k: int) (x: 'a) : 'a
 546     requires { k >= 0 }
 547     variant  { k }
 548   = if k = 0 then x else iter f (k - 1) (f x)
 549
 550   lemma iter_1: forall f, x: 'a. iter f 1 x = f x
 551
 552   lemma iter_s: forall f, k, x: 'a. 0 < k -> iter f k x = f (iter f (k - 1) x)
 553
 554 end
 555
 556 (** {2 Integers extended with an infinite value} *)
 557
 558 module IntInf
 559
 560   use Int
 561
 562   type t = Finite int | Infinite
 563
 564   let function add (x: t) (y: t) : t =
 565     match x with
 566       | Infinite -> Infinite
 567       | Finite x ->
 568         match y with
 569           | Infinite -> Infinite
 570           | Finite y -> Finite (x + y)
 571         end
 572     end
 573
 574   let predicate eq (x y: t) =
 575     match x, y with
 576       | Infinite, Infinite -> true
 577       | Finite x, Finite y -> x = y
 578       | _, _ -> false
 579     end
 580
 581   let predicate lt (x y: t) =
 582     match x with
 583       | Infinite -> false
 584       | Finite x ->
 585         match y with
 586           | Infinite -> true
 587           | Finite y -> x < y
 588         end
 589     end
 590
 591   let predicate le (x y: t) = lt x y || eq x y
 592
 593   clone export relations.TotalOrder with type t = t, predicate rel = le,
 594     lemma Refl, lemma Antisymm, lemma Trans, lemma Total
 595
 596 end
 597
 598 (** {2 Induction principle on integers}
 599
 600 This theory can be cloned with the wanted predicate, to perform an
 601 induction, either on nonnegative integers, or more generally on
 602 integers greater or equal a given bound.
 603
 604 *)
 605
 606 module SimpleInduction
 607
 608   use Int
 609
 610   predicate p int
 611
 612   axiom base: p 0
 613
 614   axiom induction_step: forall n:int. 0 <= n -> p n -> p (n+1)
 615
 616   lemma SimpleInduction : forall n:int. 0 <= n -> p n
 617
 618 end
 619
 620 module Induction
 621
 622   use Int
 623
 624   predicate p int
 625
 626   lemma Induction :
 627     (forall n:int. 0 <= n -> (forall k:int. 0 <= k < n -> p k) -> p n) ->
 628     forall n:int. 0 <= n -> p n
 629
 630   constant bound : int
 631
 632   lemma Induction_bound :
 633     (forall n:int. bound <= n ->
 634       (forall k:int. bound <= k < n -> p k) -> p n) ->
 635     forall n:int. bound <= n -> p n
 636
 637 end
 638
 639 module HOInduction
 640
 641   use Int
 642
 643   let lemma induction (p: int -> bool)
 644     requires { p 0 }
 645     requires { forall n. 0 <= n >= 0 -> p n -> p (n+1) }
 646     ensures  { forall n. 0 <= n -> p n }
 647   = let rec lemma f (n: int) requires { n >= 0 } ensures  { p n } variant {n}
 648     = if n > 0 then f (n-1) in f 0
 649
 650 end
 651
 652 (** {2 Fibonacci numbers} *)
 653
 654 module Fibonacci
 655
 656   use Int
 657
 658   let rec function fib (n: int) : int
 659     requires { n >= 0 }
 660     variant  { n }
 661   = if n = 0 then 0 else
 662     if n = 1 then 1 else
 663     fib (n-1) + fib (n-2)
 664
 665 end
 666
 667 module WFltof
 668   use Int
 669   use relations.WellFounded
 670
 671   type t
 672   function f t : int
 673
 674   axiom f_nonneg: forall x. 0 <= f x
 675
 676   predicate ltof (x y: t) = f x < f y
 677
 678   let rec lemma acc_ltof (n: int)
 679     requires { 0 <= n }
 680     ensures  { forall x. f x < n -> acc ltof x }
 681     variant  { n }
 682   = if n > 0 then acc_ltof (n-1)
 683
 684   lemma wf_ltof: well_founded ltof
 685
 686 end