(** {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 (** [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 (** {2 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 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) 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 *) 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} *) 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] (** {2 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 *)