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