stdlib/seq.mlw

   1
   2 (** {1 Sequences}
   3
   4     This file provides a basic theory of sequences.
   5 *)
   6
   7 (** {2 Sequences and basic operations} *)
   8
   9 module Seq
  10
  11   use int.Int
  12
  13   (** the polymorphic type of sequences *)
  14   type seq 'a
  15
  16   (** `seq 'a` is an infinite type *)
  17   meta "infinite_type" type seq
  18
  19   val function length (seq 'a) : int
  20
  21   axiom length_nonnegative:
  22     forall s: seq 'a. 0 <= length s
  23
  24   val function get (seq 'a) int : 'a
  25     (* FIXME requires { 0 <= i < length s } *)
  26   (** `get s i` is the `i+1`-th element of sequence `s`
  27       (the first element has index 0) *)
  28
  29   let function ([]) (s: seq 'a) (i: int) : 'a =
  30     get s i
  31
  32   (** equality is extensional *)
  33   val predicate (==) (s1 s2: seq 'a)
  34     ensures { result <-> length s1 = length s2 &&
  35               forall i: int. 0 <= i < length s1 -> s1[i] = s2[i] }
  36     ensures { result -> s1 = s2 }
  37
  38   (** sequence comprehension *)
  39   val function create (len: int) (f: int -> 'a) : seq 'a
  40     requires { 0 <= len }
  41     ensures { length result = len }
  42     ensures { forall i. 0 <= i < len -> result[i] = f i }
  43
  44   (*** FIXME: could be defined, but let constant does
  45      not accept spec. *)
  46   (*** let constant empty : seq 'a
  47     ensures { length result = 0 }
  48   = while false do variant { 0 } () done;
  49     create 0 (fun _ requires { false } -> absurd)
  50    *)
  51
  52   (** empty sequence *)
  53   val constant empty : seq 'a
  54     ensures { length result = 0 }
  55
  56   (** `set s i v` is a new sequence `u` such that
  57       `u[i] = v` and `u[j] = s[j]` otherwise *)
  58   let function set (s:seq 'a) (i:int) (v:'a) : seq 'a
  59     requires { 0 <= i < length s }
  60     ensures { length result = length s }
  61     ensures { result[i] = v }
  62     ensures { forall j. 0 <= j < length s /\ j <> i -> result[j] = s[j] }
  63   = while false do variant { 0 } () done;
  64     create s.length (fun j -> if j = i then v else s[j])
  65
  66   (* FIXME: not a real alias because of spec, but should be. *)
  67   let function ([<-]) (s: seq 'a) (i: int) (v: 'a) : seq 'a
  68     requires { 0 <= i < length s }
  69    = set s i v
  70
  71   (** singleton sequence *)
  72   let function singleton (v:'a) : seq 'a
  73     ensures { length result = 1 }
  74     ensures { result[0] = v }
  75   = while false do variant { 0 } () done;
  76     create 1 (fun _ -> v)
  77
  78   (** insertion of elements on both sides *)
  79   let function cons (x:'a) (s:seq 'a) : seq 'a
  80     ensures { length result = 1 + length s }
  81     ensures { result[0] = x }
  82     ensures { forall i. 0 < i <= length s -> result[i] = s[i-1] }
  83   = while false do variant { 0 } () done;
  84     create (1 + length s) (fun i -> if i = 0 then x else s[i-1])
  85
  86   let function snoc (s:seq 'a) (x:'a) : seq 'a
  87     ensures { length result = 1 + length s }
  88     ensures { result[length s] = x }
  89     ensures { forall i. 0 <= i < length s -> result[i] = s[i] }
  90   = while false do variant { 0 } () done;
  91     create (1 + length s) (fun i -> if i = length s then x else s[i])
  92
  93   (** `s[i..j]` is the sub-sequence of `s` from element `i` included
  94       to element `j` excluded *)
  95   let function ([..]) (s:seq 'a) (i:int) (j:int) : seq 'a
  96     requires { 0 <= i <= j <= length s }
  97     ensures { length result = j - i }
  98     ensures { forall k. 0 <= k < j - i -> result[k] = s[i + k] }
  99   = while false do variant { 0 } () done;
 100     create (j-i) (fun k -> s[i+k])
 101
 102   (* FIXME: spec/alias *)
 103   let function ([_..]) (s: seq 'a) (i: int) : seq 'a
 104     requires { 0 <= i <= length s }
 105   = s[i .. length s]
 106
 107   (* FIXME: spec/alias *)
 108   let function ([.._]) (s: seq 'a) (j: int) : seq 'a
 109     requires { 0 <= j <= length s }
 110   = s[0 .. j]
 111
 112   (** concatenation *)
 113   let function (++) (s1:seq 'a) (s2:seq 'a) : seq 'a
 114     ensures { length result = length s1 + length s2 }
 115     ensures { forall i. 0 <= i < length s1 -> result[i] = s1[i] }
 116     ensures { forall i. length s1 <= i < length result ->
 117       result[i] = s2[i - length s1] }
 118   = while false do variant { 0 } () done;
 119     let l = length s1 in
 120     create (l + length s2)
 121            (fun i -> if i < l then s1[i] else s2[i-l])
 122
 123 end
 124
 125 (** {2 Lemma library about algebraic interactions between
 126        `empty`/`singleton`/`cons`/`snoc`/`++`/`[ .. ]`} *)
 127
 128 module FreeMonoid
 129
 130   use int.Int
 131   use Seq
 132
 133   (* Monoidal properties/simplification. *)
 134
 135   let lemma associative (s1 s2 s3:seq 'a)
 136     ensures { s1 ++ (s2 ++ s3) = (s1 ++ s2) ++ s3 }
 137   = if not (s1 ++ s2) ++ s3 == s1 ++ (s2 ++ s3) then absurd
 138   meta rewrite axiom associative
 139
 140   let lemma left_neutral (s:seq 'a)
 141     ensures { empty ++ s = s }
 142   = if not empty ++ s == s then absurd
 143   meta rewrite axiom left_neutral
 144
 145   let lemma right_neutral (s:seq 'a)
 146     ensures { s ++ empty = s }
 147   = if not s ++ empty == s then absurd
 148   meta rewrite axiom right_neutral
 149
 150   let lemma cons_def (x:'a) (s:seq 'a)
 151     ensures { cons x s = singleton x ++ s }
 152   = if not cons x s == singleton x ++ s then absurd
 153   meta rewrite axiom cons_def
 154
 155   let lemma snoc_def (s:seq 'a) (x:'a)
 156     ensures { snoc s x = s ++ singleton x }
 157   = if not snoc s x == s ++ singleton x then absurd
 158   meta rewrite axiom snoc_def
 159
 160   let lemma double_sub_sequence (s:seq 'a) (i j k l:int)
 161     requires { 0 <= i <= j <= length s }
 162     requires { 0 <= k <= l <= j - i }
 163     ensures { s[i .. j][k .. l] = s[k+i .. l+i] }
 164   = if not s[i .. j][k .. l] == s[k+i .. l+i] then absurd
 165
 166   (* Inverting cons/snoc/catenation *)
 167
 168   let lemma cons_back (x:'a) (s:seq 'a)
 169     ensures { (cons x s)[1 ..] = s }
 170   = if not (cons x s)[1 ..] == s then absurd
 171
 172   let lemma snoc_back (s:seq 'a) (x:'a)
 173     ensures { (snoc s x)[.. length s] = s }
 174   = if not (snoc s x)[.. length s] == s then absurd
 175
 176   let lemma cat_back (s1 s2:seq 'a)
 177     ensures { (s1 ++ s2)[.. length s1] = s1 }
 178     ensures { (s1 ++ s2)[length s1 ..] = s2 }
 179   = let c = s1 ++ s2 in let l = length s1 in
 180     if not (c[.. l] == s1 || c[l ..] == s2) then absurd
 181
 182   (* Decomposing sequences as cons/snoc/catenation/empty/singleton *)
 183
 184   let lemma cons_dec (s:seq 'a)
 185     requires { length s >= 1 }
 186     ensures  { s = cons s[0] s[1 ..] }
 187   = if not s == cons s[0] s[1 ..] then absurd
 188
 189   let lemma snoc_dec (s:seq 'a)
 190     requires { length s >= 1 }
 191     ensures  { s = snoc s[.. length s - 1] s[length s - 1] }
 192   = if not s == snoc s[.. length s - 1] s[length s - 1] then absurd
 193
 194   let lemma cat_dec (s:seq 'a) (i:int)
 195     requires { 0 <= i <= length s }
 196     ensures  { s = s[.. i] ++ s[i ..] }
 197   = if not s == s[.. i] ++ s[i ..] then absurd
 198
 199   let lemma empty_dec (s:seq 'a)
 200     requires { length s = 0 }
 201     ensures  { s = empty }
 202   = if not s == empty then absurd
 203
 204   let lemma singleton_dec (s:seq 'a)
 205     requires { length s = 1 }
 206     ensures  { s = singleton s[0] }
 207   = if not s == singleton s[0] then absurd
 208
 209 end
 210
 211 module ToList
 212   use int.Int
 213   use Seq
 214   use list.List
 215
 216   val function to_list (a: seq 'a) : list 'a
 217
 218   axiom to_list_empty:
 219     to_list (empty: seq 'a) = (Nil: list 'a)
 220
 221   axiom to_list_cons:
 222     forall s: seq 'a. 0 < length s ->
 223     to_list s = Cons s[0] (to_list s[1 ..])
 224
 225   use list.Length as ListLength
 226
 227   lemma to_list_length:
 228     forall s: seq 'a. ListLength.length (to_list s) = length s
 229
 230   use list.Nth as ListNth
 231   use option.Option
 232
 233   lemma to_list_nth:
 234     forall s: seq 'a, i: int. 0 <= i < length s ->
 235     ListNth.nth i (to_list s) = Some s[i]
 236
 237   let rec lemma to_list_def_cons (s: seq 'a) (x: 'a)
 238     variant { length s }
 239     ensures { to_list (cons x s) = Cons x (to_list s) }
 240   = assert { (cons x s)[1 ..] == s }
 241
 242 end
 243
 244 module OfList
 245   use int.Int
 246   use option.Option
 247   use list.List
 248   use list.Length as L
 249   use list.Nth
 250   use Seq
 251   use list.Append
 252
 253   let rec function of_list (l: list 'a) : seq 'a = match l with
 254     | Nil -> empty
 255     | Cons x r -> cons x (of_list r)
 256     end
 257
 258   lemma length_of_list:
 259     forall l: list 'a. length (of_list l) = L.length l
 260
 261   predicate point_wise (s: seq 'a) (l: list 'a) =
 262     forall i. 0 <= i < L.length l -> Some (get s i) = nth i l
 263
 264   lemma elts_seq_of_list: forall l: list 'a.
 265     point_wise (of_list l) l
 266
 267   lemma is_of_list: forall l: list 'a, s: seq 'a.
 268     L.length l = length s -> point_wise s l -> s == of_list l
 269
 270   let rec lemma of_list_app (l1 l2: list 'a)
 271     ensures { of_list (l1 ++ l2) == Seq.(++) (of_list l1) (of_list l2) }
 272     variant { l1 }
 273   = match l1 with
 274     | Nil -> ()
 275     | Cons _ r -> of_list_app r l2
 276     end
 277
 278   lemma of_list_app_length: forall l1 [@induction] l2: list 'a.
 279     length (of_list (l1 ++ l2)) = L.length l1 + L.length l2
 280
 281   let rec lemma of_list_snoc (l: list 'a) (x: 'a)
 282     variant { l }
 283     ensures { of_list (l ++ Cons x Nil) == snoc (of_list l) x }
 284   = match l with
 285     | Nil -> assert { snoc empty x = cons x empty }
 286     | Cons _ r -> of_list_snoc r x;
 287     end
 288
 289   meta coercion function of_list
 290
 291   use ToList
 292
 293   lemma convolution_to_of_list: forall l: list 'a.
 294     to_list (of_list l) = l
 295
 296 end
 297
 298 module Mem
 299
 300   use int.Int
 301   use Seq
 302
 303   predicate mem (x: 'a) (s: seq 'a) =
 304     exists i: int. 0 <= i < length s && s[i] = x
 305
 306   lemma mem_append : forall x: 'a, s1 s2.
 307     mem x (s1 ++ s2) <-> mem x s1 \/ mem x s2
 308
 309   lemma mem_tail: forall x: 'a, s.
 310     length s > 0 ->
 311     mem x s <-> (x = s[0] \/ mem x s[1 .. ])
 312
 313 end
 314
 315 module Distinct
 316   use int.Int
 317   use Seq
 318
 319   predicate distinct (s : seq 'a) =
 320     forall i j. 0 <= i < length s -> 0 <= j < length s ->
 321     i <> j -> s[i] <> s[j]
 322
 323 end
 324
 325 module Reverse
 326
 327   use int.Int
 328   use Seq
 329
 330   let function reverse (s: seq 'a) : seq 'a =
 331     create (length s) (fun i -> s[length s - 1 - i])
 332
 333 end
 334
 335 module ToFset
 336   use int.Int
 337   use set.Fset
 338   use Mem
 339   use Seq
 340
 341   val function to_set (s: seq 'a) : fset 'a
 342
 343   axiom to_set_empty: to_set (empty: seq 'a) = (Fset.empty: fset 'a)
 344
 345   axiom to_set_add: forall s: seq 'a. length s > 0 ->
 346     to_set s = add s[0] (to_set s[1 ..])
 347
 348   lemma to_set_cardinal: forall s: seq 'a.
 349     cardinal (to_set s) <= length s
 350
 351   lemma to_set_mem: forall s: seq 'a, e: 'a.
 352     mem e s <-> Fset.mem e (to_set s)
 353
 354   lemma to_set_snoc: forall s: seq 'a, x: 'a.
 355     to_set (snoc s x) = add x (to_set s)
 356
 357   use Distinct
 358
 359   lemma to_set_cardinal_distinct: forall s: seq 'a. distinct s ->
 360     cardinal (to_set s) = length s
 361
 362 end
 363
 364 (** {2 Sorted Sequences} *)
 365
 366 module Sorted
 367
 368   use int.Int
 369   use Seq
 370
 371   type t
 372   predicate le t t
 373   clone relations.TotalPreOrder as TO with
 374     type t = t, predicate rel = le, axiom .
 375
 376   predicate sorted_sub (s: seq t) (l u: int) =
 377     forall i1 i2. l <= i1 <= i2 < u -> le s[i1] s[i2]
 378   (** `sorted_sub s l u` is true whenever the sub-sequence `s[l .. u-1]` is
 379       sorted  w.r.t. order relation `le` *)
 380
 381   predicate sorted (s: seq t) =
 382     sorted_sub s 0 (length s)
 383   (** `sorted s` is true whenever the sequence `s` is sorted w.r.t `le`  *)
 384
 385   lemma sorted_cons:
 386     forall x: t, s: seq t.
 387       (forall i: int. 0 <= i < length s -> le x s[i]) /\ sorted s <->
 388     sorted (cons x s)
 389
 390   lemma sorted_append:
 391     forall s1 s2: seq t.
 392     (sorted s1 /\ sorted s2 /\
 393       (forall i j: int. 0 <= i < length s1 /\ 0 <= j < length s2 ->
 394       le s1[i] s2[j])) <-> sorted (s1 ++ s2)
 395
 396   lemma sorted_snoc:
 397     forall x: t, s: seq t.
 398       (forall i: int. 0 <= i < length s -> le s[i] x) /\ sorted s <->
 399     sorted (snoc s x)
 400
 401 end
 402
 403 module SortedInt (** sorted sequences of integers *)
 404
 405   use int.Int
 406   clone export Sorted with type t = int, predicate le = (<=), goal .
 407
 408 end
 409
 410 module Sum
 411
 412   use int.Int
 413   use Seq
 414   use int.Sum as S
 415
 416   function sum (s: seq int) : int = S.sum (fun i -> s[i]) 0 (length s)
 417
 418   lemma sum_snoc:
 419     forall s x. sum (snoc s x) = sum s + x
 420   lemma sum_tail:
 421     forall s. length s >= 1 -> sum s = s[0] + sum s[1 .. ]
 422   lemma sum_tail_tail:
 423     forall s. length s >= 2 -> sum s = s[0] + s[1] + sum s[2 .. ]
 424
 425 end
 426
 427 (** {2 Number of occurrences in a sequence} *)
 428
 429 module Occ
 430
 431   use int.Int
 432   use int.NumOf as N
 433   use Seq
 434
 435   function iseq (x: 'a) (s: seq 'a) : int->bool = fun i -> s[i] = x
 436
 437   function occ (x: 'a) (s: seq 'a) (l u: int) : int = N.numof (iseq x s) l u
 438
 439   function occ_all (x: 'a) (s: seq 'a) : int =
 440     occ x s 0 (length s)
 441
 442   lemma occ_cons:
 443     forall k: 'a, s: seq 'a, x: 'a.
 444     (occ_all k (cons x s) =
 445     if k = x then 1 + occ_all k s else occ_all k s
 446     ) by (cons x s == (cons x empty) ++ s)
 447
 448   lemma occ_snoc:
 449     forall k: 'a, s: seq 'a, x: 'a.
 450     occ_all k (snoc s x) =
 451     if k = x then 1 + occ_all k s else occ_all k s
 452
 453   lemma occ_tail:
 454     forall k: 'a, s: seq 'a.
 455     length s > 0 ->
 456     (occ_all k s[1..] =
 457     if k = s[0] then (occ_all k s) - 1 else occ_all k s
 458     ) by (s == cons s[0] s[1..])
 459
 460   lemma append_num_occ:
 461     forall x: 'a, s1 s2: seq 'a.
 462     occ_all x (s1 ++ s2) =
 463     occ_all x s1 + occ_all x s2
 464
 465 end
 466
 467 (** {2 Sequences Equality} *)
 468
 469 module SeqEq
 470
 471   use int.Int
 472   use Seq
 473
 474   predicate seq_eq_sub (s1 s2: seq 'a) (l u: int) =
 475     forall i. l <= i < u -> s1[i] = s2[i]
 476
 477 end
 478
 479 module Exchange
 480
 481   use int.Int
 482   use Seq
 483
 484   predicate exchange (s1 s2: seq 'a) (i j: int) =
 485     length s1 = length s2 /\
 486     0 <= i < length s1 /\ 0 <= j < length s1 /\
 487     s1[i] = s2[j] /\ s1[j] = s2[i] /\
 488     (forall k:int. 0 <= k < length s1 -> k <> i -> k <> j -> s1[k] = s2[k])
 489
 490   lemma exchange_set :
 491     forall s: seq 'a, i j: int.
 492     0 <= i < length s -> 0 <= j < length s ->
 493     exchange s s[i <- s[j]][j <- s[i]] i j
 494
 495 end
 496
 497 (** {2 Permutation of sequences} *)
 498
 499 module Permut
 500
 501   use int.Int
 502   use Seq
 503   use Occ
 504   use SeqEq
 505   use export Exchange
 506
 507   predicate permut (s1 s2: seq 'a) (l u: int) =
 508     length s1 = length s2 /\
 509     0 <= l <= length s1 /\ 0 <= u <= length s1 /\
 510     forall v: 'a. occ v s1 l u = occ v s2 l u
 511   (** `permut s1 s2 l u` is true when the segment `s1[l..u-1]` is a
 512   permutation of the segment `s2[l..u-1]`. Values outside this range are
 513   ignored. *)
 514
 515   predicate permut_sub (s1 s2: seq 'a) (l u: int) =
 516     seq_eq_sub s1 s2 0 l /\
 517     permut s1 s2 l u /\
 518     seq_eq_sub s1 s2 u (length s1)
 519   (** `permut_sub s1 s2 l u` is true when the segment `s1[l..u-1]` is a
 520   permutation of the segment `s2[l..u-1]` and values outside this range
 521   are equal. *)
 522
 523   predicate permut_all (s1 s2: seq 'a) =
 524     length s1 = length s2 /\ permut s1 s2 0 (length s1)
 525   (** `permut_all s1 s2` is true when sequence `s1` is a permutation of
 526   sequence `s2` *)
 527
 528   lemma exchange_permut_sub:
 529     forall s1 s2: seq 'a, i j l u: int.
 530     exchange s1 s2 i j -> l <= i < u -> l <= j < u ->
 531     0 <= l -> u <= length s1 -> permut_sub s1 s2 l u
 532
 533   (** enlarge the interval *)
 534   lemma Permut_sub_weakening:
 535     forall s1 s2: seq 'a, l1 u1 l2 u2: int.
 536     permut_sub s1 s2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length s1 ->
 537     permut_sub s1 s2 l2 u2
 538
 539   (** {3 Lemmas about permut} *)
 540
 541   lemma permut_refl: forall s: seq 'a, l u: int.
 542     0 <= l <= length s -> 0 <= u <= length s ->
 543     permut s s l u
 544
 545   lemma permut_sym: forall s1 s2: seq 'a, l u: int.
 546     permut s1 s2 l u -> permut s2 s1 l u
 547
 548   lemma permut_trans:
 549     forall s1 s2 s3: seq 'a, l u: int.
 550     permut s1 s2 l u -> permut s2 s3 l u -> permut s1 s3 l u
 551
 552   lemma permut_exists:
 553     forall s1 s2: seq 'a, l u i: int.
 554     permut s1 s2 l u -> l <= i < u ->
 555     exists j: int. l <= j < u /\ s1[j] = s2[i]
 556
 557   (** {3 Lemmas about permut_all} *)
 558
 559   use Mem
 560
 561   lemma permut_all_mem: forall s1 s2: seq 'a. permut_all s1 s2 ->
 562     forall x. mem x s1 <-> mem x s2
 563
 564   lemma exchange_permut_all:
 565     forall s1 s2: seq 'a, i j: int.
 566     exchange s1 s2 i j -> permut_all s1 s2
 567
 568 end
 569
 570 module FoldLeft
 571
 572   use Seq
 573   use int.Int
 574
 575   (** `fold_left f a [b1; ...; bn]` is `f (... (f (f a b1) b2) ...) bn` *)
 576   let rec function fold_left (f: 'a -> 'b -> 'a) (acc: 'a) (s: seq 'b) : 'a
 577     variant { length s }
 578   = if length s = 0 then acc else fold_left f (f acc s[0]) s[1 ..]
 579
 580   lemma fold_left_ext: forall f: 'b -> 'a -> 'b, acc: 'b, s1 s2: seq 'a.
 581     s1 == s2 -> fold_left f acc s1 = fold_left f acc s2
 582
 583   lemma fold_left_cons: forall s: seq 'a, x: 'a, f: 'b -> 'a -> 'b, acc: 'b.
 584     fold_left f acc (cons x s) = fold_left f (f acc x) s
 585
 586   let rec lemma fold_left_app (s1 s2: seq 'a) (f: 'b -> 'a -> 'b) (acc: 'b)
 587     ensures { fold_left f acc (s1 ++ s2) = fold_left f (fold_left f acc s1) s2 }
 588     variant { Seq.length s1 }
 589   = if Seq.length s1 > 0 then fold_left_app s1[1 ..] s2 f (f acc (Seq.get s1 0))
 590
 591 end
 592
 593 module FoldRight
 594
 595   use Seq
 596   use int.Int
 597
 598   (** `fold_right f [a1; ...; an] b` is `f a1 (f a2 (... (f an b) ...))` *)
 599   let rec function fold_right (f: 'b -> 'a -> 'a) (s: seq 'b) (acc: 'a) : 'a
 600     variant { length s }
 601   = if length s = 0 then acc
 602     else let acc = f s[length s - 1] acc in fold_right f s[.. length s - 1] acc
 603
 604   lemma fold_right_ext: forall f: 'a -> 'b -> 'b, acc: 'b, s1 s2: seq 'a.
 605     s1 == s2 -> fold_right f s1 acc = fold_right f s2 acc
 606
 607   lemma fold_right_snoc: forall s: seq 'a, x: 'a, f: 'a -> 'b -> 'b, acc: 'b.
 608     fold_right f (snoc s x) acc = fold_right f s (f x acc)
 609
 610 end
 611
 612 (*** TODO / TO DISCUSS
 613
 614   - what about s[i..j] when i..j is not a valid range?
 615     left undefined? empty sequence?
 616
 617   - what about negative index e.g. s[-3..] for the last three elements?
 618
 619   - a syntax for cons and snoc?
 620
 621   - create: better name? move to a separate theory?
 622
 623   - UNPLEASANT: we cannot write s[1..] because 1. is recognized as a float
 624     so we have to write s[1 ..]
 625
 626   - UNPLEASANT: when using both arrays and sequences, the lack of overloading
 627     is a pain; see for instance vstte12_ring_buffer.mlw
 628
 629 *)