[library] new libraries map.MapExchange and array.ArrayExchange

(used to be in Permut libraries)
new library array.ArrayPermut2, similar to ArrayPermut, but using
number of occurrences
parent f00d1747
......@@ -142,15 +142,11 @@ module ArrayEq
end
(** {2 Permutation} *)
module ArrayPermut
module ArrayExchange
use import int.Int
use import Array
use import map.MapPermut as M
use import map.MapEq
use import ArrayEq
use import map.MapExchange as M
predicate exchange (a1 a2: array 'a) (i j: int) =
a1.length = a2.length /\
......@@ -158,6 +154,19 @@ module ArrayPermut
(** [exchange a1 a2 i j] means that arrays [a1] and [a2] only differ
by the swapping of elements at indices [i] and [j] *)
end
(** {2 Permutation} *)
module ArrayPermut
use import int.Int
use import Array
use import map.MapPermut as M
use import map.MapEq
use export ArrayExchange
use import ArrayEq
predicate permut (a1 a2: array 'a) (l u: int) =
a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\
M.permut a1.elts a2.elts l u
......@@ -187,12 +196,6 @@ module ArrayPermut
forall a: array 'a, l u: int.
0 <= l <= u <= length a -> permut_sub a a l u
(*
lemma permut_sub_sym:
forall a1 a2: array 'a, l u: int.
permut_sub a1 a2 l u -> permut_sub a2 a1 l u
*)
lemma permut_sub_trans:
forall a1 a2 a3: array 'a, l u: int.
permut_sub a1 a2 l u -> permut_sub a2 a3 l u -> permut_sub a1 a3 l u
......@@ -222,18 +225,9 @@ module ArrayPermut
(** {3 lemmas about [permut_all]} *)
(** permut_all is reflexive, symmetric, transitive and contains
transpositions *)
lemma permut_all_refl:
forall a: array 'a. permut_all a a
(*
lemma permut_all_sym:
forall a1 a2: array 'a.
permut_all a1 a2 -> permut_all a2 a1
*)
lemma permut_all_trans:
forall a1 a2 a3: array 'a.
permut_all a1 a2 -> permut_all a2 a3 -> permut_all a1 a3
......@@ -256,11 +250,82 @@ module ArrayPermut
end
(** alternative definition using number of occurrences *)
module ArrayPermut2
use import int.Int
use import Array
use import map.MapPermut2 as M
use import map.MapEq
use import ArrayEq
use export ArrayExchange
predicate permut (a1 a2: array 'a) (l u: int) =
a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\
M.permut a1.elts a2.elts l u
(** [permut a1 a2 l u] is true when the segment
[a1(l..u-1)] is a permutation of the segment [a2(l..u-1)].
Values outside of the interval (l..u-1) are ignored. *)
predicate permut_sub (a1 a2: array 'a) (l u: int) =
map_eq_sub a1.elts a2.elts 0 l /\
permut a1 a2 l u /\
map_eq_sub a1.elts a2.elts u (length a1)
(** [permut_sub a1 a2 l u] is true when the segment
[a1(l..u-1)] is a permutation of the segment [a2(l..u-1)]
and values outside of the interval (l..u-1) are equal. *)
predicate permut_all (a1 a2: array 'a) =
a1.length = a2.length /\ M.permut a1.elts a2.elts 0 a1.length
(** [permut_all a1 a2 l u] is true when array [a1] is a permutation
of array [a2]. *)
lemma exchange_permut_sub:
forall a1 a2: array 'a, i j l u: int.
exchange a1 a2 i j -> l <= i < u -> l <= j < u ->
0 <= l -> u <= length a1 -> permut_sub a1 a2 l u
(** we can always enlarge the interval *)
lemma permut_sub_weakening:
forall a1 a2: array 'a, l1 u1 l2 u2: int.
permut_sub a1 a2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length a1 ->
permut_sub a1 a2 l2 u2
lemma permut_sub_compose:
forall a1 a2 a3: array 'a, l1 u1 l2 u2: int. u1 <= l2 ->
permut_sub a1 a2 l1 u1 ->
permut_sub a2 a3 l2 u2 ->
permut_sub a1 a3 l1 u2
(** {3 lemmas about [permut_all]} *)
lemma exchange_permut_all:
forall a1 a2: array 'a, i j: int.
exchange a1 a2 i j -> permut_all a1 a2
(***
(** identical arrays *)
lemma array_eq_permut_all:
forall a1 a2: array 'a.
array_eq a1 a2 -> permut_all a1 a2
(** permutation on a sub-interval *)
lemma permut_sub_permut_all:
forall a1 a2: array 'a, l u: int.
permut_sub a1 a2 l u -> permut_all a1 a2
***)
end
module ArraySwap
use import int.Int
use import Array
use import ArrayPermut
use export ArrayExchange
let swap (a:array 'a) (i:int) (j:int) : unit
requires { 0 <= i < length a /\ 0 <= j < length a }
......
......@@ -91,18 +91,31 @@ theory MapInjection
end
(** {2 Map Permutation (indexed by integers)} *)
theory MapPermut
theory MapExchange
use import int.Int
use import Map
use import MapEq
predicate exchange (a1 a2: map int 'a) (l u i j: int) =
l <= i < u /\ l <= j < u /\
a1[i] = a2[j] /\ a1[j] = a2[i] /\
(forall k:int. l <= k < u -> k <> i -> k <> j -> a1[k] = a2[k])
lemma exchange_set :
forall a: map int 'a, l u i j: int.
l <= i < u -> l <= j < u ->
exchange a a[i <- a[j]][j <- a[i]] l u i j
end
(** {2 Map Permutation (indexed by integers)} *)
theory MapPermut
use import int.Int
use import Map
use import MapExchange
use import MapEq
inductive permut (map int 'a) (map int 'a) int int =
| permut_refl : (* a1[l..u[ and a2[l..u[ are identical *)
forall a1 a2 : map int 'a. forall l u : int.
......@@ -127,11 +140,6 @@ theory MapPermut
permut a1 a2 l u -> permut a2 a1 l u
*)
lemma exchange_set :
forall a: map int 'a, l u i j: int.
l <= i < u -> l <= j < u ->
exchange a a[i <- a[j]][j <- a[i]] l u i j
lemma permut_exists :
forall a1 a2: map int 'a, l u i: int.
permut a1 a2 l u -> l <= i < u ->
......@@ -228,3 +236,62 @@ theory BV32
clone export BitVector with constant size = size
end
(** {2 Number of occurrences} *)
theory Occ
use import int.Int
use export Map
function occ (v: 'a) (m: map int 'a) (l u: int) : int
(** number of occurrences of v in m between l included and u excluded *)
axiom occ_empty:
forall v: 'a, m: map int 'a, l u: int.
u <= l -> occ v m l u = 0
axiom occ_right_no_add:
forall v: 'a, m: map int 'a, l u: int.
l < u -> m[u-1] <> v -> occ v m l u = occ v m l (u-1)
axiom occ_right_add:
forall v: 'a, m: map int 'a, l u: int.
l < u -> m[u-1] = v -> occ v m l u = 1 + occ v m l (u-1)
lemma occ_bounds:
forall v: 'a, m: map int 'a, l u: int.
l < u -> 0 <= occ v m l u <= u - l
(* direct when l>=u, by induction on b when l <= u *)
lemma occ_append:
forall v: 'a, m: map int 'a, l mid u: int.
l <= mid <= u -> occ v m l u = occ v m l mid + occ v m mid u
(* by induction on u *)
lemma occ_neq:
forall v: 'a, m: map int 'a, l u: int.
(forall i: int. l <= i < u -> m[i] <> v) -> occ v m l u = 0
(* by induction on u *)
end
theory MapPermut2
use import int.Int
use import Occ
predicate permut (m1 m2: map int 'a) (l u: int) =
forall v: 'a. occ v m1 l u = occ v m2 l u
lemma permut_trans: (* provable, yet useful *)
forall a1 a2 a3 : map int 'a. forall l u : int.
permut a1 a2 l u -> permut a2 a3 l u -> permut a1 a3 l u
lemma permut_exists :
forall a1 a2: map int 'a, l u i: int.
permut a1 a2 l u -> l <= i < u ->
exists j: int. l <= j < u /\ a1[j] = a2[i]
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment