map.mlw 6.17 KB
Newer Older
1

2

MARCHE Claude's avatar
MARCHE Claude committed
3 4 5 6
(** {1 Theory of maps} *)

(** {2 Generic Maps} *)

7
module Map
8

Andrei Paskevich's avatar
Andrei Paskevich committed
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 =
Andrei Paskevich's avatar
Andrei Paskevich committed
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

MARCHE Claude's avatar
MARCHE Claude committed
20
end
21

22
module Const
MARCHE Claude's avatar
MARCHE Claude committed
23

24
  use Map
MARCHE Claude's avatar
MARCHE Claude committed
25

26
  let function const (v: 'b) : map 'a 'b = fun _ -> v
27 28 29

end

30
module MapExt
31 32 33

  predicate (==) (m1 m2: 'a -> 'b) = forall x: 'a. m1 x = m2 x

34
  lemma extensionality:
35
    forall m1 m2: 'a -> 'b. m1 == m2 -> m1 = m2
36 37
  (* This lemma is actually provable in Why3, because of how
     eliminate_epsilon handles equality to a lambda-term. *)
38 39 40

end

MARCHE Claude's avatar
MARCHE Claude committed
41 42
(** {2 Sorted Maps (indexed by integers)} *)

43
module MapSorted
44

45 46
  use int.Int
  use Map
47 48 49

  type elt

Andrei Paskevich's avatar
Andrei Paskevich committed
50
  predicate le elt elt
51

Andrei Paskevich's avatar
Andrei Paskevich committed
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 55
  (** `sorted_sub a l u` is true whenever the array segment `a(l..u-1)`
      is sorted w.r.t order relation `le` *)
56 57 58

end

MARCHE Claude's avatar
MARCHE Claude committed
59
(** {2 Maps Equality (indexed by integers)} *)
60

61
module MapEq
62

63 64
  use int.Int
  use Map
65

Andrei Paskevich's avatar
Andrei Paskevich committed
66
  predicate map_eq_sub (a1 a2 : map int 'a) (l u : int) =
67 68 69 70
    forall i:int. l <= i < u -> a1[i] = a2[i]

end

71
module MapExchange
72

73 74
  use int.Int
  use Map
75

76 77 78 79 80
  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])

81 82 83 84 85 86 87
  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

MARCHE Claude's avatar
MARCHE Claude committed
88
(** {2 Sum of elements of a map (indexed by integers)} *)
89

90
module MapSum
91

92
  use int.Int
93 94
  use export Map

95
  (** `sum m l h` is the sum of `m[i]` for `l <= i < h` *)
96 97

  type container = map int int
98 99
  clone export sum.Sum with
    type container = container, function f = get, axiom .
100 101 102

end

103 104
(** {2 Number of occurrences} *)

105
(* TODO: we could define Occ using theory int.NumOf *)
106
module Occ
107

108 109
  use int.Int
  use Map
110 111

  function occ (v: 'a) (m: map int 'a) (l u: int) : int
112
    (** number of occurrences of `v` in `m` between `l` included and `u` excluded *)
113 114 115 116 117 118 119 120 121 122 123 124 125

  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)

126 127 128 129 130 131 132 133
  lemma occ_left_no_add:
    forall v: 'a, m: map int 'a, l u: int.
    l < u -> m[l] <> v -> occ v m l u = occ v m (l+1) u

  lemma occ_left_add:
    forall v: 'a, m: map int 'a, l u: int.
    l < u -> m[l] = v -> occ v m l u = 1 + occ v m (l+1) u

134 135
  lemma occ_bounds:
    forall v: 'a, m: map int 'a, l u: int.
136
    l <= u -> 0 <= occ v m l u <= u - l
137
    (* direct when l>=u, by induction on u when l <= u *)
138 139 140 141 142 143 144 145 146 147 148

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

149 150 151 152 153 154 155 156
  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

157 158 159 160 161
  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 *)

162 163
  lemma occ_exchange :
    forall m: map int 'a, l u i j: int, x y z: 'a.
164
    l <= i < u -> l <= j < u -> i <> j ->
165 166 167
    occ z m[i <- x][j <- y] l u =
    occ z m[i <- y][j <- x] l u

168 169
end

170
module MapPermut
171

172 173 174
  use int.Int
  use Map
  use Occ
175 176 177 178 179 180 181 182 183 184 185 186 187 188

  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
189 190 191


(** {2 Injectivity and surjectivity for maps (indexed by integers)} *)
192

193
module MapInjection
194

195
  use int.Int
196 197 198 199
  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]
200 201
  (** `injective a n` is true when `a` is an injection
      on the domain `(0..n-1)` *)
202 203 204

  predicate surjective (a: map int int) (n: int) =
    forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)
205 206
  (** `surjective a n` is true when `a` is a surjection
      from `(0..n-1)` to `(0..n-1)` *)
207

208
  predicate range (a: map int int) (n: int) =
209
    forall i: int. 0 <= i < n -> 0 <= a[i] < n
210 211
  (** `range a n` is true when `a` maps the domain
      `(0..n-1)` into `(0..n-1)` *)
212 213 214

  lemma injective_surjective:
    forall a: map int int, n: int.
215
    injective a n -> range a n -> surjective a n
216 217
  (** main lemma: an injection on `(0..n-1)` that
      ranges into `(0..n-1)` is also a surjection *)
218

219
  use Occ
220 221 222 223 224 225 226

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

end

227
(***
228 229 230

(** {2 Parametric Maps} *)

231
module MapParam
232 233 234 235 236

  type idx
  type elt
  type map

237
  (** if `'b` is an infinite type, then `map 'a 'b` is infinite *)
238 239
  meta "material_type_arg" type map, 1

240 241
  function get (map 'a 'b) 'a : 'b
  function set (map 'a 'b) 'a 'b : map 'a 'b
242 243 244 245 246 247 248 249 250 251 252 253 254 255 256

  (** 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]

257
  function const 'b : map 'a 'b
258 259 260 261 262

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

end
*)