int.mlw 13 KB
Newer Older
1

2
(** {1 Theory of integers}
MARCHE Claude's avatar
MARCHE Claude committed
3

4
This file provides the basic theory of integers, and several additional
5
theories for classical functions.
MARCHE Claude's avatar
MARCHE Claude committed
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

MARCHE Claude's avatar
MARCHE Claude committed
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

MARCHE Claude's avatar
MARCHE Claude committed
47
(***
48
  lemma Abs_zero: forall x:int. abs x = 0 -> x = 0
49
*)
50

51 52
end

MARCHE Claude's avatar
MARCHE Claude committed
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

MARCHE Claude's avatar
MARCHE Claude committed
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

MARCHE Claude's avatar
MARCHE Claude committed
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.
MARCHE Claude's avatar
MARCHE Claude committed
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

MARCHE Claude's avatar
MARCHE Claude committed
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

MARCHE Claude's avatar
MARCHE Claude committed
152 153
(** {2 Division by 2}

154
The particular case of Euclidean division by 2
MARCHE Claude's avatar
MARCHE Claude committed
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

MARCHE Claude's avatar
MARCHE Claude committed
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`.
MARCHE Claude's avatar
MARCHE Claude committed
172 173 174

*)

175
module ComputerDivision
MARCHE Claude's avatar
MARCHE Claude committed
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

MARCHE Claude's avatar
MARCHE Claude committed
192
  axiom Div_sign_pos:
193
    forall x y:int. x >= 0 /\ y > 0 -> div x y >= 0
MARCHE Claude's avatar
MARCHE Claude committed
194 195

  axiom Div_sign_neg:
196
    forall x y:int. x <= 0 /\ y > 0 -> div x y <= 0
MARCHE Claude's avatar
MARCHE Claude committed
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
Andrei Paskevich's avatar
Andrei Paskevich committed
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 *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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)

MARCHE Claude's avatar
MARCHE Claude committed
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 ->
MARCHE Claude's avatar
MARCHE Claude committed
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
MARCHE Claude's avatar
MARCHE Claude committed
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

MARCHE Claude's avatar
MARCHE Claude committed
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

302 303 304
  lemma Power_monotonic:
    forall x n m:int. 0 < x /\ 0 <= n <= m -> power x n <= power x m

305 306
end

307
(** {2 Number of integers satisfying a given predicate} *)
MARCHE Claude's avatar
MARCHE Claude committed
308

309
module NumOf
310

311
  use Int
312

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

320
  lemma Numof_bounds :
321
    forall p : int -> bool, a b : int. a < b -> 0 <= numof p a b <= b - a
MARCHE Claude's avatar
MARCHE Claude committed
322 323
    (* direct when a>=b, by induction on b when a <= b *)

324
  lemma Numof_append :
325
    forall p : int -> bool, a b c : int.
326
    a <= b <= c -> numof p a c = numof p a b + numof p b c
MARCHE Claude's avatar
MARCHE Claude committed
327
    (* by induction on c *)
328

329
  lemma Numof_left_no_add :
330
    forall p : int -> bool, a b : int.
331 332 333
    a < b -> not p a -> numof p a b = numof p (a+1) b
    (* by Numof_append *)
  lemma Numof_left_add :
334
    forall p : int -> bool, a b : int.
335 336
    a < b -> p a -> numof p a b = 1 + numof p (a+1) b
    (* by Numof_append *)
MARCHE Claude's avatar
MARCHE Claude committed
337 338

  lemma Empty :
339
    forall p : int -> bool, a b : int.
340
    (forall n : int. a <= n < b -> not p n) -> numof p a b = 0
MARCHE Claude's avatar
MARCHE Claude committed
341 342
    (* by induction on b *)

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

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

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

358
  lemma numof_change_any:
359
    forall p1 p2: int -> bool, a b: int.
360 361
    (forall j: int. a <= j < b -> p1 j -> p2 j) ->
    numof p2 a b >= numof p1 a b
362

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

369 370 371 372 373
  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

374
end
375

376 377
(** {2 Sum} *)

378
module Sum
379

380
  use Int
381

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

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

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

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

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

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

415 416 417 418 419 420 421
  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

422 423
end

MARCHE Claude's avatar
MARCHE Claude committed
424 425
(** {2 Factorial function} *)

426
module Fact
427

428
  use Int
429

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

435 436
end

MARCHE Claude's avatar
MARCHE Claude committed
437 438
(** {2 Generic iteration of a function} *)

439
module Iter
440

441
  use Int
442

443
  (** `iter k x` is `f^k(x)` *)
444 445 446 447
  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)
448

449
  lemma iter_1: forall f, x: 'a. iter f 1 x = f x
450

451
  lemma iter_s: forall f, k, x: 'a. 0 < k -> iter f k x = f (iter f (k - 1) x)
452 453 454

end

MARCHE Claude's avatar
MARCHE Claude committed
455
(** {2 Integers extended with an infinite value} *)
456

457
module IntInf
458

459
  use Int
460 461 462

  type t = Finite int | Infinite

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

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

490
  let predicate le (x y: t) = lt x y || eq x y
491 492 493 494 495 496

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

end

MARCHE Claude's avatar
MARCHE Claude committed
497 498
(** {2 Induction principle on integers}

499
This theory can be cloned with the wanted predicate, to perform an
500
induction, either on nonnegative integers, or more generally on
501
integers greater or equal a given bound.
MARCHE Claude's avatar
MARCHE Claude committed
502

503
*)
504

505
module SimpleInduction
506

507
  use Int
508 509 510 511 512 513 514 515 516 517 518

  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

519
module Induction
520

521
  use Int
522

Andrei Paskevich's avatar
Andrei Paskevich committed
523
  predicate p int
524

525
  lemma Induction :
526 527 528
    (forall n:int. 0 <= n -> (forall k:int. 0 <= k < n -> p k) -> p n) ->
    forall n:int. 0 <= n -> p n

529
  constant bound : int
530 531

  lemma Induction_bound :
532
    (forall n:int. bound <= n ->
533 534 535
      (forall k:int. bound <= k < n -> p k) -> p n) ->
    forall n:int. bound <= n -> p n

536
end
537

538 539
module HOInduction

540
  use Int
541 542 543 544 545 546 547 548 549 550

  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

551 552 553
(** {2 Fibonacci numbers} *)

module Fibonacci
554

555
  use Int
556

557 558 559 560 561 562
  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)
563 564

end
565 566

module WFltof
567 568
  use Int
  use relations.WellFounded
569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585

  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