Why3 Standard Library index



Sequences

This file provides a basic theory of sequences.


Sequences and basic operations

theory Seq

  use import int.Int

the polymorphic type of sequences

  type seq 'a

seq 'a is an infinite type

  meta "infinite_type" type seq

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

  function get (seq 'a) int : 'a

get s i is the (i+1)-th element of sequence s (the first element has index 0)

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

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

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

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

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:
    forall len: int, f: int -> 'a.
    0 <= len -> length (create len f) = len

  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

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

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

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

theory ToFset
  use import int.Int
  use import Seq as S
  use import Mem as SM
  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

  lemma to_set_mem: forall s: seq 'a, e: 'a.
    SM.mem e s <-> mem e (to_set s)

  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

Sorted Sequences

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 sl .. 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

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)

end

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

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 s1l..u-1 is a permutation of the segment s2l..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 s1l..u-1 is a permutation of the segment s2l..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

  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

Lemmas about permut

  lemma permut_refl: forall s: seq 'a, l u: int.
    0 <= l <= length s -> 0 <= u <= length s ->
    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

  lemma permut_trans:
    forall s1 s2 s3: seq 'a, l u: int.
    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]

Lemmas about permut_all

  use import Mem

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

  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

  - reverse

  - 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 ..]

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

*)

Generated by why3doc 0.87.3