map.why 5.87 KB
Newer Older
1

2

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

(** {2 Generic Maps} *)

theory Map
8 9 10

  type map 'a 'b

Andrei Paskevich's avatar
Andrei Paskevich committed
11
  (** if ['b] is an infinite type, then [map 'a 'b] is infinite *)
12 13
  meta "material_type_arg" type map, 1

14 15
  function get (map 'a ~'b) 'a : 'b
  function set (map 'a ~'b) 'a 'b : map 'a 'b
16

17
  (** syntactic sugar *)
Andrei Paskevich's avatar
Andrei Paskevich committed
18 19
  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
20 21 22 23 24 25 26 27 28 29 30

  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]

MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34 35 36 37
end


theory Const

  use import Map

38
  function const ~'b : map 'a 'b
39

40
  axiom Const : forall b:'b, a:'a. (const b)[a] = b
41 42 43

end

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

46 47 48 49 50 51 52
theory MapSorted

  use import int.Int
  use import Map

  type elt

Andrei Paskevich's avatar
Andrei Paskevich committed
53
  predicate le elt elt
54

Andrei Paskevich's avatar
Andrei Paskevich committed
55
  predicate sorted_sub (a : map int elt) (l u : int) =
56
    forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]
57 58
  (** [sorted_sub a l u] is true whenever the array segment [a(l..u-1)]
      is sorted w.r.t order relation [le] *)
59 60 61

end

MARCHE Claude's avatar
MARCHE Claude committed
62
(** {2 Maps Equality (indexed by integers)} *)
63 64 65
theory MapEq

  use import int.Int
66
  use import Map
67

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

end

73
theory MapExchange
74 75

  use import int.Int
76
  use import Map
77

78 79 80 81 82
  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])

83 84 85 86 87 88 89
  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
90
(** {2 Sum of elements of a map (indexed by integers)} *)
91 92 93 94 95
theory MapSum

  use import int.Int
  use export Map

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

  type container = map int int
Andrei Paskevich's avatar
Andrei Paskevich committed
99
  clone export sum.Sum with type container = container, function f = get
100 101 102

end

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

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

  use import int.Int
109
  use import Map
110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127

  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.
128
    l <= u -> 0 <= occ v m l u <= u - l
129
    (* direct when l>=u, by induction on u when l <= u *)
130 131 132 133 134 135 136 137 138 139 140

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

141 142 143 144 145 146 147 148
  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

149 150 151 152 153
  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 *)

154 155
end

156
theory MapPermut
157 158

  use import int.Int
159
  use import Map
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
  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
175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211


(** {2 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

212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248


(** {2 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
*)