Why3 Standard Library index

Theory of maps

Generic Maps

```theory Map

type map 'a 'b

```

if `'b` is an infinite type, then `map 'a 'b` is infinite

```  meta "material_type_arg" type map, 1

function get (map 'a ~'b) 'a : 'b
function set (map 'a ~'b) 'a 'b : map 'a 'b

```

syntactic sugar

```  function ([])   (a : map 'a 'b) (i : 'a) : 'b = get a i
function ([<-]) (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b = set a i v

axiom Select_eq :
forall m : map 'a 'b. forall a1 a2 : 'a.
forall b : 'b [m[a1 <- b][a2]].
a1 = a2 -> m[a1 <- b][a2]  = b

axiom Select_neq :
forall m : map 'a 'b. forall a1 a2 : 'a.
forall b : 'b [m[a1 <- b][a2]].
a1 <> a2 -> m[a1 <- b][a2] = m[a2]

end

theory Const

use import Map

function const ~'b : map 'a 'b

axiom Const : forall b:'b, a:'a. (const b)[a] = b

end

```

Sorted Maps (indexed by integers)

```theory MapSorted

use import int.Int
use import Map

type elt

predicate le elt elt

predicate sorted_sub (a : map int elt) (l u : int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]
```

`sorted_sub a l u` is true whenever the array segment `a(l..u-1)` is sorted w.r.t order relation `le`

```end

```

Maps Equality (indexed by integers)

```theory MapEq

use import int.Int
use import Map

predicate map_eq_sub (a1 a2 : map int 'a) (l u : int) =
forall i:int. l <= i < u -> a1[i] = a2[i]

end

theory MapExchange

use import int.Int
use import Map

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

```

Sum of elements of a map (indexed by integers)

```theory MapSum

use import int.Int
use export Map

```

`sum m l h` is the sum of `m[i]` for `l <= i < h`

```  type container = map int int
clone export sum.Sum with type container = container, function f = get

end

```

Number of occurrences

```(* TODO: we could define Occ using theory int.NumOf *)
theory Occ

use import int.Int
use import 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

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)

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 u 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 *)

lemma occ_exists:
forall v: 'a, m: map int 'a, l u: int.
occ v m l u > 0 -> exists i: int. l <= i < u /\ m[i] = v

lemma occ_pos:
forall m: map int 'a, l u i: int.
l <= i < u -> occ m[i] m l u > 0

lemma occ_eq:
forall v: 'a, m1 m2: map int 'a, l u: int.
(forall i: int. l <= i < u -> m1[i] = m2[i]) -> occ v m1 l u = occ v m2 l u
(* by induction on u *)

end

theory MapPermut

use import int.Int
use import Map
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

```

Injectivity and surjectivity for maps (indexed by integers)

```theory MapInjection

use import int.Int
use export Map

predicate injective (a: map int int) (n: int) =
forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
```

`injective a n` is true when `a` is an injection on the domain `(0..n-1)`

```  predicate surjective (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)
```

`surjective a n` is true when `a` is a surjection from `(0..n-1)` to `(0..n-1)`

```  predicate range (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n
```

`range a n` is true when `a` maps the domain `(0..n-1)` into `(0..n-1)`

```  lemma injective_surjective:
forall a: map int int, n: int.
injective a n -> range a n -> surjective a n
```

main lemma: an injection on `(0..n-1)` that ranges into `(0..n-1)` is also a surjection

```  use import Occ

lemma injection_occ:
forall m: map int int, n: int.
injective m n <-> forall v:int. (occ v m 0 n <= 1)

end

```

Parametric Maps

```(*
theory MapParam

type idx
type elt
type map

(** if ['b] is an infinite type, then [map 'a 'b] is infinite *)
meta "material_type_arg" type map, 1

function get (map 'a ~'b) 'a : 'b
function set (map 'a ~'b) 'a 'b : map 'a 'b

(** syntactic sugar *)
function ([])   (a : map 'a 'b) (i : 'a) : 'b = get a i
function ([<-]) (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b = set a i v

axiom Select_eq :
forall m : map 'a 'b. forall a1 a2 : 'a.
forall b : 'b [m[a1 <- b][a2]].
a1 = a2 -> m[a1 <- b][a2]  = b

axiom Select_neq :
forall m : map 'a 'b. forall a1 a2 : 'a.
forall b : 'b [m[a1 <- b][a2]].
a1 <> a2 -> m[a1 <- b][a2] = m[a2]

function const ~'b : map 'a 'b

axiom Const : forall b:'b, a:'a. (const b)[a] = b

end
*)
```

Generated by why3doc 0.87.3