int.mlw 13 KB
Newer Older
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 10

*)

(** {2 Integers and the basic operators} *)

11
module Int
12

Mário Pereira's avatar
Mário Pereira committed
13 14
  let constant zero : int = 0
  let constant one  : int = 1
MARCHE Claude's avatar
MARCHE Claude committed
15

16
  val (=) (x y : int) : bool ensures { result <-> x = y }
17

18 19 20 21 22 23 24 25 26 27 28 29 30
  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 (+) = (+),
31
    function (*) = (*), predicate (<=) = (<=)
32

33
end
34

35 36
(** {2 Absolute Value} *)

37
module Abs
38

39
  use Int
40

41
  let function abs (x:int) : int = if x >= 0 then x else -x
42

43 44
  lemma Abs_le: forall x y:int. abs x <= y <-> -y <= x <= y

45
  lemma Abs_pos: forall x:int. abs x >= 0
MARCHE Claude's avatar
MARCHE Claude committed
46

47
(***
48
  lemma Abs_zero: forall x:int. abs x = 0 -> x = 0
49
*)
50

51 52
end

53 54
(** {2 Minimum and Maximum} *)

55
module MinMax
56

57
  use Int
58

59
  clone export relations.MinMax with type t = int, predicate le = (<=), goal .
60

61 62 63 64 65 66 67 68 69
  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


70 71
end

72 73
(** {2 The Basic Well-Founded Order on Integers} *)

74
module Lex2
75

76
  use Int
77 78 79 80 81 82 83 84

  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

85 86
(** {2 Euclidean Division}

87
Division and modulo operators with the convention
88 89 90 91
that modulo is always non-negative.

It implies that division rounds down when divisor is positive, and
rounds up when divisor is negative.
92 93 94

*)

95
module EuclideanDivision
MARCHE Claude's avatar
MARCHE Claude committed
96

97 98
  use Int
  use Abs
MARCHE Claude's avatar
MARCHE Claude committed
99

100 101
  function div (x y: int) : int
  function mod (x y: int) : int
MARCHE Claude's avatar
MARCHE Claude committed
102

MARCHE Claude's avatar
MARCHE Claude committed
103
  axiom Div_mod:
104
    forall x y:int. y <> 0 -> x = y * div x y + mod x y
MARCHE Claude's avatar
MARCHE Claude committed
105

MARCHE Claude's avatar
MARCHE Claude committed
106
  axiom Mod_bound:
107
    forall x y:int. y <> 0 -> 0 <= mod x y < abs y
MARCHE Claude's avatar
MARCHE Claude committed
108

109 110 111 112 113 114
  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

115
  lemma Mod_1: forall x:int. mod x 1 = 0
MARCHE Claude's avatar
MARCHE Claude committed
116

117
  lemma Div_1: forall x:int. div x 1 = x
MARCHE Claude's avatar
MARCHE Claude committed
118

MARCHE Claude's avatar
MARCHE Claude committed
119 120
  lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0

121 122
  lemma Div_inf_neg: forall x y:int. 0 < x <= y -> div (-x) y = -1

MARCHE Claude's avatar
MARCHE Claude committed
123 124
  lemma Mod_0: forall y:int. y <> 0 -> mod 0 y = 0

125 126 127 128 129 130 131 132
  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

133 134 135 136 137 138 139
  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
140

141 142 143 144 145 146 147 148 149
  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 }


150 151
end

152 153
(** {2 Division by 2}

154
The particular case of Euclidean division by 2
155 156

*)
157

158
module Div2
159

160
  use Int
161 162 163 164 165 166

  lemma div2:
    forall x: int. exists y: int. x = 2*y \/ x = 2*y+1

end

167
(** {2 Computer Division}
MARCHE Claude's avatar
MARCHE Claude committed
168

169
Division and modulo operators with the same conventions as mainstream
170
programming language such as C, Java, OCaml, that is, division rounds
171
towards zero, and thus `mod x y` has the same sign as `x`.
172 173 174

*)

175
module ComputerDivision
176

177 178
  use Int
  use Abs
MARCHE Claude's avatar
MARCHE Claude committed
179

180 181
  function div (x y: int) : int
  function mod (x y: int) : int
MARCHE Claude's avatar
MARCHE Claude committed
182

MARCHE Claude's avatar
MARCHE Claude committed
183
  axiom Div_mod:
184
    forall x y:int. y <> 0 -> x = y * div x y + mod x y
MARCHE Claude's avatar
MARCHE Claude committed
185

MARCHE Claude's avatar
MARCHE Claude committed
186
  axiom Div_bound:
187
    forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x
MARCHE Claude's avatar
MARCHE Claude committed
188 189

  axiom Mod_bound:
190 191
    forall x y:int. y <> 0 -> - abs y < mod x y < abs y

192
  axiom Div_sign_pos:
193
    forall x y:int. x >= 0 /\ y > 0 -> div x y >= 0
194 195

  axiom Div_sign_neg:
196
    forall x y:int. x <= 0 /\ y > 0 -> div x y <= 0
197

198
  axiom Mod_sign_pos:
199
    forall x y:int. x >= 0 /\ y <> 0 -> mod x y >= 0
200 201

  axiom Mod_sign_neg:
202
    forall x y:int. x <= 0 /\ y <> 0 -> mod x y <= 0
203 204 205

  lemma Rounds_toward_zero:
    forall x y:int. y <> 0 -> abs (div x y * y) <= abs x
MARCHE Claude's avatar
MARCHE Claude committed
206

MARCHE Claude's avatar
MARCHE Claude committed
207 208
  lemma Div_1: forall x:int. div x 1 = x

209
  lemma Mod_1: forall x:int. mod x 1 = 0
MARCHE Claude's avatar
MARCHE Claude committed
210

MARCHE Claude's avatar
MARCHE Claude committed
211 212 213 214
  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

215
  lemma Div_mult: forall x y z:int [div (x * y + z) x].
216
          x > 0 /\ y >= 0 /\ z >= 0 ->
MARCHE Claude's avatar
MARCHE Claude committed
217 218
          div (x * y + z) x = y + div z x

219
  lemma Mod_mult: forall x y z:int [mod (x * y + z) x].
220
          x > 0 /\ y >= 0 /\ z >= 0 ->
MARCHE Claude's avatar
MARCHE Claude committed
221
          mod (x * y + z) x = mod z x
MARCHE Claude's avatar
MARCHE Claude committed
222

223 224 225 226 227 228 229 230
  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 }

231 232
end

233
(** {2 Generic Exponentiation of something to an integer exponent} *)
234

235
module Exponentiation
236

237
  use Int
238

239
  type t
240
  constant one : t
241
  function (*) t t : t
Andrei Paskevich's avatar
Andrei Paskevich committed
242

243
  clone export algebra.Monoid
244
    with type t = t, constant unit = one, function op = (*), axiom .
245

Andrei Paskevich's avatar
Andrei Paskevich committed
246
  (* TODO: implement with let rec once let cloning is done *)
247
  function power t int : t
248 249 250 251

  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
252

253 254
  lemma Power_s_alt: forall x: t, n: int. n > 0 -> power x n = x * power x (n-1)

255 256
  lemma Power_1 : forall x : t. power x 1 = x

257
  lemma Power_sum : forall x: t, n m: int. 0 <= n -> 0 <= m ->
258 259 260
    power x (n+m) = power x n * power x m

  lemma Power_mult : forall x:t, n m : int. 0 <= n -> 0 <= m ->
Andrei Paskevich's avatar
Andrei Paskevich committed
261
    power x (Int.(*) n m) = power (power x n) m
262

263 264 265 266 267 268
  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 ->
269 270
    power (x * y) n = power x n * power y n

MARCHE Claude's avatar
MARCHE Claude committed
271 272
(* TODO

273
  use ComputerDivision
MARCHE Claude's avatar
MARCHE Claude committed
274 275 276 277 278 279 280 281

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

282 283
end

284
(** {2 Power of an integer to an integer } *)
285

286
module Power
287

288
  use Int
289

Andrei Paskevich's avatar
Andrei Paskevich committed
290 291 292 293 294 295
  (* 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,
296 297
    goal Assoc, goal Unit_def_l, goal Unit_def_r,
    axiom Power_0, axiom Power_s
298

299 300 301
  lemma Power_non_neg:
     forall x y. x >= 0 /\ y >= 0 -> power x y >= 0

DAILLER Sylvain's avatar
DAILLER Sylvain committed
302 303 304
  lemma Power_pos:
     forall x y. x > 0 /\ y >= 0 -> power x y > 0

305 306 307
  lemma Power_monotonic:
    forall x n m:int. 0 < x /\ 0 <= n <= m -> power x n <= power x m

308 309
end

310
(** {2 Number of integers satisfying a given predicate} *)
311

312
module NumOf
313

314
  use Int
315

316
  (** number of `n` such that `a <= n < b` and `p n` *)
Andrei Paskevich's avatar
Andrei Paskevich committed
317 318 319
  let rec function numof (p: int -> bool) (a b: int) : int
    variant { b - a }
  = if b <= a then 0 else
320 321
    if p (b - 1) then 1 + numof p a (b - 1)
                 else     numof p a (b - 1)
322

323
  lemma Numof_bounds :
324
    forall p : int -> bool, a b : int. a < b -> 0 <= numof p a b <= b - a
325 326
    (* direct when a>=b, by induction on b when a <= b *)

327
  lemma Numof_append :
328
    forall p : int -> bool, a b c : int.
329
    a <= b <= c -> numof p a c = numof p a b + numof p b c
330
    (* by induction on c *)
331

332
  lemma Numof_left_no_add :
333
    forall p : int -> bool, a b : int.
334 335 336
    a < b -> not p a -> numof p a b = numof p (a+1) b
    (* by Numof_append *)
  lemma Numof_left_add :
337
    forall p : int -> bool, a b : int.
338 339
    a < b -> p a -> numof p a b = 1 + numof p (a+1) b
    (* by Numof_append *)
340 341

  lemma Empty :
342
    forall p : int -> bool, a b : int.
343
    (forall n : int. a <= n < b -> not p n) -> numof p a b = 0
344 345
    (* by induction on b *)

346
  lemma Full :
347
    forall p : int -> bool, a b : int. a <= b ->
348
    (forall n : int. a <= n < b -> p n) -> numof p a b = b - a
349 350
    (* by induction on b *)

351
  lemma numof_increasing:
352
    forall p : int -> bool, i j k : int.
353 354
    i <= j <= k -> numof p i j <= numof p i k
    (* by Numof_append and Numof_non_negative *)
355

356
  lemma numof_strictly_increasing:
357
    forall p: int -> bool, i j k l: int.
358 359
    i <= j <= k < l -> p k -> numof p i j < numof p i l
    (* by Numof_append and numof_increasing *)
360

361
  lemma numof_change_any:
362
    forall p1 p2: int -> bool, a b: int.
363 364
    (forall j: int. a <= j < b -> p1 j -> p2 j) ->
    numof p2 a b >= numof p1 a b
365

366
  lemma numof_change_some:
367
    forall p1 p2: int -> bool, a b i: int. a <= i < b ->
368 369 370
    (forall j: int. a <= j < b -> p1 j -> p2 j) ->
    not (p1 i) -> p2 i ->
    numof p2 a b > numof p1 a b
371

372 373 374 375 376
  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

377
end
378

379 380
(** {2 Sum} *)

381
module Sum
382

383
  use Int
384

385
  (** sum of `f n` for `a <= n < b` *)
Andrei Paskevich's avatar
Andrei Paskevich committed
386 387 388
  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)
389 390 391

  lemma sum_left:
    forall f: int -> int, a b: int.
Andrei Paskevich's avatar
Andrei Paskevich committed
392
    a < b -> sum f a b = f a + sum f (a + 1) b
393 394 395

  lemma sum_ext:
    forall f g: int -> int, a b: int.
Andrei Paskevich's avatar
Andrei Paskevich committed
396 397
    (forall i. a <= i < b -> f i = g i) ->
    sum f a b = sum g a b
398

399 400
  lemma sum_le:
    forall f g: int -> int, a b: int.
Andrei Paskevich's avatar
Andrei Paskevich committed
401 402 403 404 405 406 407
    (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
408

409 410
  lemma sum_nonneg:
    forall f: int -> int, a b: int.
Andrei Paskevich's avatar
Andrei Paskevich committed
411 412
    (forall i. a <= i < b -> 0 <= f i) ->
    0 <= sum f a b
413 414 415

  lemma sum_decomp:
    forall f: int -> int, a b c: int. a <= b <= c ->
Andrei Paskevich's avatar
Andrei Paskevich committed
416
    sum f a c = sum f a b + sum f b c
417

418 419 420 421 422 423 424
  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

425 426
end

427 428
(** {2 Factorial function} *)

429
module Fact
430

431
  use Int
432

433
  let rec function fact (n: int) : int
434 435 436 437
    requires { n >= 0 }
    variant  { n }
  = if n = 0 then 1 else n * fact (n-1)

438 439
end

440 441
(** {2 Generic iteration of a function} *)

442
module Iter
443

444
  use Int
445

446
  (** `iter k x` is `f^k(x)` *)
447 448 449 450
  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)
451

452
  lemma iter_1: forall f, x: 'a. iter f 1 x = f x
453

454
  lemma iter_s: forall f, k, x: 'a. 0 < k -> iter f k x = f (iter f (k - 1) x)
455 456 457

end

458
(** {2 Integers extended with an infinite value} *)
459

460
module IntInf
461

462
  use Int
463 464 465

  type t = Finite int | Infinite

466
  let function add (x: t) (y: t) : t =
467 468 469 470 471 472 473 474 475
    match x with
      | Infinite -> Infinite
      | Finite x ->
        match y with
          | Infinite -> Infinite
          | Finite y -> Finite (x + y)
        end
    end

476 477 478 479 480 481 482 483
  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) =
484 485 486 487 488 489 490 491 492
    match x with
      | Infinite -> false
      | Finite x ->
        match y with
          | Infinite -> true
          | Finite y -> x < y
        end
    end

493
  let predicate le (x y: t) = lt x y || eq x y
494 495 496 497 498 499

  clone export relations.TotalOrder with type t = t, predicate rel = le,
    lemma Refl, lemma Antisymm, lemma Trans, lemma Total

end

500 501
(** {2 Induction principle on integers}

502
This theory can be cloned with the wanted predicate, to perform an
503
induction, either on nonnegative integers, or more generally on
504
integers greater or equal a given bound.
505

506
*)
507

508
module SimpleInduction
509

510
  use Int
511 512 513 514 515 516 517 518 519 520 521

  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

522
module Induction
523

524
  use Int
525

526
  predicate p int
527

528
  lemma Induction :
529 530 531
    (forall n:int. 0 <= n -> (forall k:int. 0 <= k < n -> p k) -> p n) ->
    forall n:int. 0 <= n -> p n

532
  constant bound : int
533 534

  lemma Induction_bound :
535
    (forall n:int. bound <= n ->
536 537 538
      (forall k:int. bound <= k < n -> p k) -> p n) ->
    forall n:int. bound <= n -> p n

539
end
540

541 542
module HOInduction

543
  use Int
544 545 546 547 548 549 550 551 552 553

  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

554 555 556
(** {2 Fibonacci numbers} *)

module Fibonacci
557

558
  use Int
559

560 561 562 563 564 565
  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)
566 567

end
568 569

module WFltof
570 571
  use Int
  use relations.WellFounded
572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588

  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