seq.why 9.82 KB
 Jean-Christophe Filliatre committed Mar 21, 2015 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 `````` Martin Clochard committed Apr 15, 2015 17 18 `````` (** [seq 'a] is an infinite type *) meta "infinite_type" type seq `````` Jean-Christophe Filliatre committed Mar 21, 2015 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 *) `````` Jean-Christophe Filliatre committed May 20, 2015 36 37 `````` function get (seq 'a) int : 'a (** [get s i] is the ([i]+1)-th element of sequence [s] `````` Jean-Christophe Filliatre committed Mar 21, 2015 38 39 `````` (the first element has index 0) *) `````` Jean-Christophe Filliatre committed May 20, 2015 40 41 `````` function ([]) (s: seq 'a) (i: int) : 'a = get s i `````` Jean-Christophe Filliatre committed May 20, 2015 42 `````` `````` Mário Pereira committed Jun 16, 2015 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 `````` Jean-Christophe Filliatre committed Mar 21, 2015 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 `````` Mário Pereira committed Jul 09, 2015 94 95 `````` lemma snoc_last: forall s: seq 'a, x: 'a. (snoc s x)[length s] = x `````` Jean-Christophe Filliatre committed Mar 21, 2015 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: `````` Jean-Christophe Filliatre committed Apr 12, 2015 138 139 `````` forall len: int, f: int -> 'a. 0 <= len -> length (create len f) = len `````` Jean-Christophe Filliatre committed Mar 21, 2015 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 `````` Mário Pereira committed Jun 16, 2015 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 `````` Mário Pereira committed Sep 20, 2015 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 `````` Jean-Christophe Filliatre committed Jan 12, 2016 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 `````` Mário Pereira committed Sep 20, 2015 205 206 207 ``````theory ToFset use import int.Int use import Seq as S `````` 208 `````` use import Mem as SM `````` Mário Pereira committed Sep 20, 2015 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) `````` Mário Pereira committed Sep 20, 2015 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 `````` Mário Pereira committed Jun 16, 2015 234 ``````(** {2 Sorted Sequences} *) `````` Mário Pereira committed Sep 20, 2015 235 `````` `````` Mário Pereira committed Jun 16, 2015 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) `````` Jean-Christophe Filliatre committed Mar 21, 2015 300 `````` `````` Mário Pereira committed Jun 16, 2015 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 *) `````` Jean-Christophe Filliatre committed Apr 17, 2015 373 `````` `````` Mário Pereira committed Jun 16, 2015 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} *) `````` Mário Pereira committed Jul 21, 2015 381 `````` lemma permut_refl: forall s: seq 'a, l u: int. `````` Mário Pereira committed Oct 26, 2015 382 `````` 0 <= l <= length s -> 0 <= u <= length s -> `````` Mário Pereira committed Jul 21, 2015 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 `````` Mário Pereira committed Jun 16, 2015 388 `````` lemma permut_trans: `````` Mário Pereira committed Jul 21, 2015 389 `````` forall s1 s2 s3: seq 'a, l u: int. `````` Mário Pereira committed Jun 16, 2015 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} *) `````` Mário Pereira committed Jul 21, 2015 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 `````` Mário Pereira committed Jun 16, 2015 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 `````` Jean-Christophe Filliatre committed Apr 17, 2015 411 `````` `````` Jean-Christophe Filliatre committed Apr 17, 2015 412 413 `````` - reverse `````` Jean-Christophe Filliatre committed Mar 21, 2015 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 ..] `````` Jean-Christophe Filliatre committed Apr 27, 2015 426 427 428 `````` - UNPLEASANT: when using both arrays and sequences, the lack of overloading is a pain; see for instance vstte12_ring_buffer.mlw `````` Jean-Christophe Filliatre committed Mar 21, 2015 429 ``*)``