seq.why 9.82 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16

(** {1 Sequences}

    This file provides a basic theory of sequences.
*)

(** {2 Sequences and basic operations} *)

theory Seq

  use import int.Int

  (** the polymorphic type of sequences *)

  type seq 'a

17 18
  (** [seq 'a] is an infinite type *)
  meta "infinite_type" type seq
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35

  (** length *)

  function length (seq 'a) : int

  axiom length_nonnegative:
    forall s: seq 'a. 0 <= length s

  (** empty sequence *)

  constant empty : seq 'a

  axiom empty_length:
    length (empty: seq 'a) = 0

  (** n-th element *)

36 37
  function get (seq 'a) int : 'a
    (** [get s i] is the ([i]+1)-th element of sequence [s]
38 39
        (the first element has index 0) *)

40 41
  function ([]) (s: seq 'a) (i: int) : 'a =
    get s i
42

43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64
  (** update *)

  function set (seq 'a) int 'a : seq 'a
    (** [set s i v] is a new sequence [u] such that
        [u[i] = v] and [u[j] = s[j]] otherwise *)

  axiom set_def1:
    forall s: seq 'a, i: int, v: 'a. 0 <= i < length s ->
    length (set s i v) = length s

  axiom set_def2:
    forall s: seq 'a, i: int, v: 'a. 0 <= i < length s ->
    get (set s i v) i = v

  axiom set_def3:
    forall s: seq 'a, i: int, v: 'a. 0 <= i < length s ->
    forall j: int. 0 <= j < length s -> j <> i ->
    get (set s i v) j = get s j

  function ([<-]) (s: seq 'a) (i: int) (v: 'a) : seq 'a =
    set s i v

65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
  (** equality *)

  predicate (==) (s1 s2: seq 'a) =
    length s1 = length s2 &&
    forall i: int. 0 <= i < length s1 -> s1[i] = s2[i]

  axiom extensionality:
    forall s1 s2: seq 'a. s1 == s2 -> s1 = s2

  (** insertion of elements on both sides *)

  function cons 'a (seq 'a) : seq 'a

  axiom cons_length:
    forall x: 'a, s: seq 'a. length (cons x s) = 1 + length s

  axiom cons_get:
    forall x: 'a, s: seq 'a, i: int. 0 <= i <= length s ->
    (cons x s)[i] = if i = 0 then x else s[i-1]

  function snoc (seq 'a) 'a : seq 'a

  axiom snoc_length:
    forall s: seq 'a, x: 'a. length (snoc s x) = 1 + length s

  axiom snoc_get:
    forall s: seq 'a, x: 'a, i: int. 0 <= i <= length s ->
    (snoc s x)[i] = if i < length s then s[i] else x

94 95
  lemma snoc_last: forall s: seq 'a, x: 'a. (snoc s x)[length s] = x

96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
  (** sub-sequence *)

  function ([_.._]) (seq 'a) int int : seq 'a
    (** [s[i..j]] is the sub-sequence of [s] from element [i] included
        to element [j] excluded *)

  axiom sub_length:
    forall s: seq 'a, i j: int. 0 <= i <= j <= length s ->
    length s[i..j] = j - i

  axiom sub_get:
    forall s: seq 'a, i j: int. 0 <= i <= j <= length s ->
    forall k: int. 0 <= k < j - i -> s[i..j][k] = s[i + k]

  function ([_..]) (s: seq 'a) (i: int) : seq 'a =
    s[i .. length s]

  function ([.._]) (s: seq 'a) (j: int) : seq 'a =
    s[0 .. j]

  (** concatenation *)

  function (++) (seq 'a) (seq 'a) : seq 'a

  axiom concat_length:
    forall s1 s2: seq 'a. length (s1 ++ s2) = length s1 + length s2

  axiom concat_get1:
    forall s1 s2: seq 'a, i: int. 0 <= i < length s1 ->
    (s1 ++ s2)[i] = s1[i]

  axiom concat_get2:
    forall s1 s2: seq 'a, i: int. length s1 <= i < length s1 + length s2 ->
    (s1 ++ s2)[i] = s2[i - length s1]

  (** sequence comprehension *)

  use HighOrd

  function create (len: int) (f: int -> 'a) : seq 'a

  axiom create_length:
138 139
    forall len: int, f: int -> 'a.
    0 <= len -> length (create len f) = len
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174

  axiom create_get:
    forall len: int, f: int -> 'a, i: int. 0 <= i < len ->
    (create len f)[i] = f i

end

theory ToList
  use import int.Int
  use import Seq
  use import list.List

  function to_list (a: seq 'a) : list 'a

  axiom to_list_empty:
    to_list (empty: seq 'a) = (Nil: list 'a)

  axiom to_list_cons:
    forall s: seq 'a. 0 < length s ->
    to_list s = Cons s[0] (to_list s[1 ..])

  use list.Length as ListLength

  lemma to_list_length:
    forall s: seq 'a. ListLength.length (to_list s) = length s

  use list.Nth as ListNth
  use import option.Option

  lemma to_list_nth:
    forall s: seq 'a, i: int. 0 <= i < length s ->
    ListNth.nth i (to_list s) = Some s[i]

end

175 176 177 178 179 180 181 182 183 184
theory Mem

  use import int.Int
  use import Seq

  predicate mem (x: 'a) (s: seq 'a) =
    exists i: int. 0 <= i < length s /\ s[i] = x

end

185 186 187 188 189 190 191 192 193 194
theory Distinct
  use import int.Int
  use import Seq

  predicate distinct (s : seq 'a) =
    forall i j. 0 <= i < length s -> 0 <= j < length s ->
    i <> j -> s[i] <> s[j]

end

195 196 197 198 199 200 201 202 203 204
theory Reverse

  use import int.Int
  use import Seq

  function reverse (s: seq 'a) : seq 'a =
    create (length s) (\ i. s[length s - 1 - i])

end

205 206 207
theory ToFset
  use import int.Int
  use import Seq as S
208
  use import Mem as SM
209 210 211 212 213 214 215 216 217 218 219 220
  use import set.Fset

  function to_set (s: seq 'a) : set 'a

  axiom to_set_empty: to_set (S.empty: seq 'a) = (empty: set 'a)

  axiom to_set_add: forall s: seq 'a. length s > 0 ->
    to_set s = add s[0] (to_set s[1 ..])

  lemma to_set_cardinal: forall s: seq 'a.
    cardinal (to_set s) <= length s

221 222
  lemma to_set_mem: forall s: seq 'a, e: 'a.
    SM.mem e s <-> mem e (to_set s)
223 224 225 226 227 228 229 230 231 232 233

  lemma to_set_snoc: forall s: seq 'a, x: 'a.
    to_set (snoc s x) = add x (to_set s)

  use import Distinct

  lemma to_set_cardinal_distinct: forall s: seq 'a. distinct s ->
    cardinal (to_set s) = length s

end

234
(** {2 Sorted Sequences} *)
235

236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
theory Sorted

  use import Seq
  use import int.Int

  type t
  predicate le t t
  clone relations.TotalOrder with type t = t, predicate rel = le

  predicate sorted_sub (s: seq t) (l u: int) =
    forall i1 i2. l <= i1 <= i2 < u -> le s[i1] s[i2]

(** sorted_sub s l u is true whenever the sub-sequence s[l .. u-1] is
    sorted  w.r.t. order relation le *)

  predicate sorted (s: seq t) =
    sorted_sub s 0 (length s)

(** sorted s is true whenever the sequence s is sorted w.r.t le  *)

  lemma sorted_cons:
    forall x: t, s: seq t.
      (forall i: int. 0 <= i < length s -> le x s[i]) /\ sorted s <->
    sorted (cons x s)

  lemma sorted_append:
    forall s1 s2: seq t.
    (sorted s1 /\ sorted s2 /\
      (forall i j: int. 0 <= i < length s1 /\ 0 <= j < length s2 ->
      le s1[i] s2[i])) <-> sorted (s1 ++ s2)

  lemma sorted_snoc:
    forall x: t, s: seq t.
      (forall i: int. 0 <= i < length s -> le s[i] x) /\ sorted s <->
    sorted (snoc s x)

end

theory SortedInt (** sorted sequences of integers *)

  use import int.Int
  clone export Sorted with type t = int, predicate le = (<=)

end

(** {2 Number of occurences in a sequence} *)

theory Occ

  use import int.Int
  use  int.NumOf as N
  use import HighOrd
  use import Seq

  function occ (x: 'a) (s: seq 'a) (l u: int) : int =
    N.numof (\ i. s[i] = x) l u

  (* TODO: lemmas for cons, snoc, etc. *)

  lemma append_num_occ:
    forall x: 'a, s1 s2: seq 'a.
    let s = s1 ++ s2 in
      occ x s 0 (length s) =
      occ x s1 0 (length s1) + occ x s2 0 (length s2)
300

301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372
end

(** {2 Sequences Equality} *)

theory SeqEq

  use import int.Int
  use import Seq

  predicate seq_eq_sub (s1 s2: seq 'a) (l u: int) =
    forall i. l <= i < u -> s1[i] = s2[i]

end

theory Exchange

  use import int.Int
  use import Seq

  predicate exchange (s1 s2: seq 'a) (i j: int) =
    length s1 = length s2 /\
    0 <= i < length s1 /\ 0 <= j < length s1 /\
    s1[i] = s2[j] /\ s1[j] = s2[i] /\
    (forall k:int. 0 <= k < length s1 -> k <> i -> k <> j -> s1[k] = s2[k])

  lemma exchange_set :
    forall s: seq 'a, i j: int.
    0 <= i < length s -> 0 <= j < length s ->
    exchange s s[i <- s[j]][j <- s[i]] i j

end

(** {2 Permutation of sequences} *)

theory Permut

  use import int.Int
  use import Seq
  use import Occ
  use import SeqEq
  use export Exchange

  predicate permut (s1 s2: seq 'a) (l u: int) =
    length s1 = length s2 /\
    0 <= l <= length s1 /\ 0 <= u <= length s1 /\
    forall v: 'a. occ v s1 l u = occ v s2 l u

  (** permut s1 s2 l u is true when the segment s1[l..u-1] is a
  permutation of the segment s2[l..u-1]. Values outside this range are
  ignored. *)

  predicate permut_sub (s1 s2: seq 'a) (l u: int) =
    seq_eq_sub s1 s2 0 l /\
    permut s1 s2 l u /\
    seq_eq_sub s1 s2 u (length s1)

  (** permut_sub s1 s2 l u is true when the segment s1[l..u-1] is a
  permutation of the segment s2[l..u-1] and values outside this range
  are equal. *)

  predicate permut_all (s1 s2: seq 'a) =
    length s1 = length s2 /\ permut s1 s2 0 (length s1)

  (** permut_all s1 s2 is true when sequence s1 is a permutation of
  sequence s2 *)

  lemma exchange_permut_sub:
    forall s1 s2: seq 'a, i j l u: int.
    exchange s1 s2 i j -> l <= i < u -> l <= j < u ->
    0 <= l -> u <= length s1 -> permut_sub s1 s2 l u

  (** enlarge the interval *)
373

374 375 376 377 378 379 380
  lemma Permut_sub_weakening:
    forall s1 s2: seq 'a, l1 u1 l2 u2: int.
    permut_sub s1 s2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length s1 ->
    permut_sub s1 s2 l2 u2

  (** {2 Lemmas about permut} *)

381
  lemma permut_refl: forall s: seq 'a, l u: int.
382
    0 <= l <= length s -> 0 <= u <= length s ->
383 384 385 386 387
    permut s s l u

  lemma permut_sym: forall s1 s2: seq 'a, l u: int.
    permut s1 s2 l u -> permut s2 s1 l u

388
  lemma permut_trans:
389
    forall s1 s2 s3: seq 'a, l u: int.
390 391 392 393 394 395 396 397 398
    permut s1 s2 l u -> permut s2 s3 l u -> permut s1 s3 l u

  lemma permut_exists:
    forall s1 s2: seq 'a, l u i: int.
    permut s1 s2 l u -> l <= i < u ->
    exists j: int. l <= j < u /\ s1[j] = s2[i]

  (** {2 Lemmas about permut_all} *)

399 400 401 402 403
  use import Mem

  lemma permut_all_mem: forall s1 s2: seq 'a. permut_all s1 s2 ->
    forall x. mem x s1 <-> mem x s2

404 405 406 407 408 409 410
  lemma exchange_permut_all:
    forall s1 s2: seq 'a, i j: int.
    exchange s1 s2 i j -> permut_all s1 s2

end

(* TODO / TO DISCUSS
411

412 413
  - reverse

414 415 416 417 418 419 420 421 422 423 424 425
  - what about s[i..j] when i..j is not a valid range?
    left undefined? empty sequence?

  - what about negative index e.g. s[-3..] for the last three elements?

  - a syntax for cons and snoc?

  - create: better name? move to a separate theory?

  - UNPLEASANT: we cannot write s[1..] because 1. is recognized as a float
    so we have to write s[1 ..]

426 427 428
  - UNPLEASANT: when using both arrays and sequences, the lack of overloading
    is a pain; see for instance vstte12_ring_buffer.mlw

429
*)