Commit 3ee891f7 by Mário Pereira

### new theories seq.{Mem,Occ,Exchange,Sorted,Permut}

`new operation set on sequences (with syntax [<-])`
parent 02ee6a9d
 ... ... @@ -40,6 +40,28 @@ theory Seq 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) = ... ... @@ -148,11 +170,180 @@ theory ToList end (* TODO / TO DISCUSS 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 (** {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) - add set 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 *) s[i <- v] = s when i < 0 || i >= length s? 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_trans: forall s1 s2 s3: seq 'a. forall 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} *) 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 ... ... @@ -172,4 +363,3 @@ end is a pain; see for instance vstte12_ring_buffer.mlw *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!