stdlib/map.mlw

   1
   2
   3 (** {1 Theory of maps} *)
   4
   5 (** {2 Generic Maps} *)
   6
   7 module Map
   8
   9   type map 'a 'b = 'a -> 'b
  10
  11   let function get (f: map 'a 'b) (x: 'a) : 'b = f x
  12
  13   let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
  14     fun y -> if pure {y = x} then v else f y
  15
  16   (** syntactic sugar *)
  17   let function ([]) (f: map 'a 'b) (x: 'a) : 'b = f x
  18   let ghost function ([<-]) (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b = set f x v
  19
  20 end
  21
  22 module Const
  23
  24   use Map
  25
  26   let function const (v: 'b) : map 'a 'b = fun _ -> v
  27
  28 end
  29
  30 module MapExt
  31
  32   predicate (==) (m1 m2: 'a -> 'b) = forall x: 'a. m1 x = m2 x
  33
  34   lemma extensionality:
  35     forall m1 m2: 'a -> 'b. m1 == m2 -> m1 = m2
  36   (* This lemma is actually provable in Why3, because of how
  37      eliminate_epsilon handles equality to a lambda-term. *)
  38
  39 end
  40
  41 (** {2 Sorted Maps (indexed by integers)} *)
  42
  43 module MapSorted
  44
  45   use int.Int
  46   use Map
  47
  48   type elt
  49
  50   predicate le elt elt
  51
  52   predicate sorted_sub (a : map int elt) (l u : int) =
  53     forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]
  54   (** `sorted_sub a l u` is true whenever the array segment `a(l..u-1)`
  55       is sorted w.r.t order relation `le` *)
  56
  57 end
  58
  59 (** {2 Maps Equality (indexed by integers)} *)
  60
  61 module MapEq
  62
  63   use int.Int
  64   use Map
  65
  66   predicate map_eq_sub (a1 a2 : map int 'a) (l u : int) =
  67     forall i:int. l <= i < u -> a1[i] = a2[i]
  68
  69 end
  70
  71 module MapExchange
  72
  73   use int.Int
  74   use Map
  75
  76   predicate exchange (a1 a2: map int 'a) (l u i j: int) =
  77     l <= i < u /\ l <= j < u /\
  78     a1[i] = a2[j] /\ a1[j] = a2[i] /\
  79     (forall k:int. l <= k < u -> k <> i -> k <> j -> a1[k] = a2[k])
  80
  81   lemma exchange_set :
  82     forall a: map int 'a, l u i j: int.
  83     l <= i < u -> l <= j < u ->
  84     exchange a a[i <- a[j]][j <- a[i]] l u i j
  85
  86 end
  87
  88 (** {2 Sum of elements of a map (indexed by integers)} *)
  89
  90 module MapSum
  91
  92   use int.Int
  93   use int.Sum as S
  94   use Map
  95
  96   (** `sum m l h` is the sum of `m[i]` for `l <= i < h` *)
  97   function sum (m: map int int) (l h: int) : int = S.sum (get m) l h
  98
  99 end
 100
 101 (** {2 Number of occurrences} *)
 102
 103 (* TODO: we could define Occ using theory int.NumOf *)
 104 module Occ
 105
 106   use int.Int
 107   use Map
 108
 109   function occ (v: 'a) (m: map int 'a) (l u: int) : int
 110     (** number of occurrences of `v` in `m` between `l` included and `u` excluded *)
 111
 112   axiom occ_empty:
 113     forall v: 'a, m: map int 'a, l u: int.
 114     u <= l -> occ v m l u = 0
 115
 116   axiom occ_right_no_add:
 117     forall v: 'a, m: map int 'a, l u: int.
 118     l < u -> m[u-1] <> v -> occ v m l u = occ v m l (u-1)
 119
 120   axiom occ_right_add:
 121     forall v: 'a, m: map int 'a, l u: int.
 122     l < u -> m[u-1] = v -> occ v m l u = 1 + occ v m l (u-1)
 123
 124   lemma occ_left_no_add:
 125     forall v: 'a, m: map int 'a, l u: int.
 126     l < u -> m[l] <> v -> occ v m l u = occ v m (l+1) u
 127
 128   lemma occ_left_add:
 129     forall v: 'a, m: map int 'a, l u: int.
 130     l < u -> m[l] = v -> occ v m l u = 1 + occ v m (l+1) u
 131
 132   lemma occ_bounds:
 133     forall v: 'a, m: map int 'a, l u: int.
 134     l <= u -> 0 <= occ v m l u <= u - l
 135     (* direct when l>=u, by induction on u when l <= u *)
 136
 137   lemma occ_append:
 138     forall v: 'a, m: map int 'a, l mid u: int.
 139     l <= mid <= u -> occ v m l u = occ v m l mid + occ v m mid u
 140     (* by induction on u *)
 141
 142   lemma occ_neq:
 143     forall v: 'a, m: map int 'a, l u: int.
 144     (forall i: int. l <= i < u -> m[i] <> v) -> occ v m l u = 0
 145     (* by induction on u *)
 146
 147   lemma occ_exists:
 148     forall v: 'a, m: map int 'a, l u: int.
 149     occ v m l u > 0 -> exists i: int. l <= i < u /\ m[i] = v
 150
 151   lemma occ_pos:
 152     forall m: map int 'a, l u i: int.
 153     l <= i < u -> occ m[i] m l u > 0
 154
 155   lemma occ_eq:
 156     forall v: 'a, m1 m2: map int 'a, l u: int.
 157     (forall i: int. l <= i < u -> m1[i] = m2[i]) -> occ v m1 l u = occ v m2 l u
 158     (* by induction on u *)
 159
 160   lemma occ_exchange :
 161     forall m: map int 'a, l u i j: int, x y z: 'a.
 162     l <= i < u -> l <= j < u -> i <> j ->
 163     occ z m[i <- x][j <- y] l u =
 164     occ z m[i <- y][j <- x] l u
 165
 166 end
 167
 168 module MapPermut
 169
 170   use int.Int
 171   use Map
 172   use Occ
 173
 174   predicate permut (m1 m2: map int 'a) (l u: int) =
 175     forall v: 'a. occ v m1 l u = occ v m2 l u
 176
 177   lemma permut_trans: (* provable, yet useful *)
 178     forall a1 a2 a3 : map int 'a. forall l u : int.
 179     permut a1 a2 l u -> permut a2 a3 l u -> permut a1 a3 l u
 180
 181   lemma permut_exists :
 182     forall a1 a2: map int 'a, l u i: int.
 183     permut a1 a2 l u -> l <= i < u ->
 184     exists j: int. l <= j < u /\ a1[j] = a2[i]
 185
 186 end
 187
 188
 189 (** {2 Injectivity and surjectivity for maps (indexed by integers)} *)
 190
 191 module MapInjection
 192
 193   use int.Int
 194   use export Map
 195
 196   predicate injective (a: map int int) (n: int) =
 197     forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
 198   (** `injective a n` is true when `a` is an injection
 199       on the domain `(0..n-1)` *)
 200
 201   predicate surjective (a: map int int) (n: int) =
 202     forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)
 203   (** `surjective a n` is true when `a` is a surjection
 204       from `(0..n-1)` to `(0..n-1)` *)
 205
 206   predicate range (a: map int int) (n: int) =
 207     forall i: int. 0 <= i < n -> 0 <= a[i] < n
 208   (** `range a n` is true when `a` maps the domain
 209       `(0..n-1)` into `(0..n-1)` *)
 210
 211   lemma injective_surjective:
 212     forall a: map int int, n: int.
 213     injective a n -> range a n -> surjective a n
 214   (** main lemma: an injection on `(0..n-1)` that
 215       ranges into `(0..n-1)` is also a surjection *)
 216
 217   use Occ
 218
 219   lemma injection_occ:
 220     forall m: map int int, n: int.
 221     injective m n <-> forall v:int. (occ v m 0 n <= 1)
 222
 223 end
 224