Pervasives_proof.v 9.66 KB
Newer Older
charguer's avatar
cp  
charguer committed
1 2 3 4 5 6 7 8 9 10 11 12
Set Implicit Arguments.
Require Import CFLib.
Require Import Pervasives_ml.



(************************************************************)
(** Boolean *)

Lemma not_spec : forall (a:bool),
  app not [a] \[] \[= !a ].
Proof using.
charguer's avatar
charguer committed
13
  xcf. xgo*.
charguer's avatar
cp  
charguer committed
14 15 16 17 18 19 20 21 22
Qed.

Hint Extern 1 (RegisterSpec not) => Provide not_spec.


(************************************************************)
(** Physical equality *)

Parameter infix_eq_eq__spec : curried 2%nat infix_eq_eq_ /\
charguer's avatar
charguer committed
23
  forall (a b:loc),
charguer's avatar
cp  
charguer committed
24 25
  app infix_eq_eq_ [a b] \[] \[= isTrue (a = b) ].

charguer's avatar
charguer committed
26 27
Hint Extern 1 (RegisterSpec infix_eq_eq_) => Provide infix_eq_eq__spec.

charguer's avatar
cp  
charguer committed
28
Lemma infix_emark_eq__spec : curried 2%nat infix_emark_eq_ /\
charguer's avatar
charguer committed
29
  forall (a b:loc),
charguer's avatar
cp  
charguer committed
30 31
  app infix_emark_eq_ [a b] \[] \[= isTrue (a <> b) ].
Proof using.
charguer's avatar
charguer committed
32
  xcf. xgo*. rew_refl; xauto*.
charguer's avatar
cp  
charguer committed
33 34 35 36 37 38 39 40 41
Qed.

Hint Extern 1 (RegisterSpec infix_emark_eq_) => Provide infix_emark_eq__spec.


(************************************************************)
(** Comparison *)


charguer's avatar
charguer committed
42
Definition eq_spec_for (A:Type) := curried 2%nat infix_eq_ /\
charguer's avatar
cp  
charguer committed
43 44 45 46 47 48 49 50 51
  forall (a b:bool),
  app infix_eq_ [a b] \[] \[= isTrue (a = b) ].

Parameter eq_bool_spec : eq_spec_for bool.
Parameter eq_int_spec : eq_spec_for int.

Hint Extern 1 (RegisterSpec infix_eq_) => Provide eq_int_spec.
 (* TODO: register several specs *)

charguer's avatar
charguer committed
52
Definition neq_spec_for (A:Type) := curried 2%nat infix_lt_gt_ /\
charguer's avatar
cp  
charguer committed
53 54 55 56 57 58 59 60
  forall (a b:bool),
  app infix_lt_gt_ [a b] \[] \[= isTrue (a <> b) ].

Parameter neq_bool_spec : neq_spec_for bool.
Parameter neq_int_spec : neq_spec_for int.

Hint Extern 1 (RegisterSpec infix_lt_gt_) => Provide neq_int_spec.

charguer's avatar
array  
charguer committed
61
  (* LATER: give specification for partially applied comparison operators *)
charguer's avatar
cp  
charguer committed
62 63 64 65

Lemma min_spec : forall (n m:int),
  app min [n m] \[] \[= Coq.ZArith.BinInt.Zmin n m ].
Proof using.
charguer's avatar
charguer committed
66 67 68
  xcf. xgo*.
  { rewrite~ Z.min_l. }
  { rewrite~ Z.min_r. math. }
charguer's avatar
cp  
charguer committed
69 70 71 72 73
Qed.

Lemma max_spec : forall (n m:int),
  app max [n m] \[] \[= Coq.ZArith.BinInt.Zmax n m ].
Proof using.
charguer's avatar
charguer committed
74 75 76
  xcf. xgo*.
  { rewrite~ Z.max_l. }
  { rewrite~ Z.max_r. math. }
charguer's avatar
cp  
charguer committed
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
Qed.

Hint Extern 1 (RegisterSpec min) => Provide min_spec.
Hint Extern 1 (RegisterSpec max) => Provide max_spec.


(************************************************************)
(** Boolean *)

Parameter infix_bar_bar__spec : forall (a b:bool),
  app infix_bar_bar_ [a b] \[] \[= a && b ].

Parameter infix_amp_amp__spec : forall (a b:bool),
  app infix_amp_amp_ [a b] \[] \[= a || b ].

Hint Extern 1 (RegisterSpec infix_bar_bar_) => Provide infix_bar_bar__spec.
Hint Extern 1 (RegisterSpec infix_amp_amp_) => Provide infix_amp_amp__spec.


(************************************************************)
(** Integer *)

Parameter infix_tilde_minus__spec : curried 1%nat infix_tilde_minus_ /\
  forall (n:int),
  app infix_tilde_minus_ [n] \[] \[= Coq.ZArith.BinInt.Zopp n ].

Parameter infix_plus__spec : curried 2%nat infix_plus_ /\
  forall (n m:int),
  app infix_plus_ [n m] \[] \[= Coq.ZArith.BinInt.Zplus n m ].

Parameter infix_minus__spec : curried 2%nat infix_minus_ /\
  forall (n m:int),
  app infix_minus_ [n m] \[] \[= Coq.ZArith.BinInt.Zminus n m ].

Parameter infix_star__spec : curried 2%nat infix_star_ /\
  forall (n m:int),
  app infix_star_ [n m] \[] \[= Coq.ZArith.BinInt.Zmult n m ].

charguer's avatar
charguer committed
115
Parameter infix_slash__spec : curried 2%nat infix_slash_ /\
charguer's avatar
cp  
charguer committed
116 117
  forall (n m:int),
  m <> 0 ->
charguer's avatar
charguer committed
118
  app infix_slash_ [n m] \[] \[= CFML.CFHeader.int_div n m ].
charguer's avatar
cp  
charguer committed
119 120 121 122 123 124 125 126 127

Parameter infix_mod__spec : curried 2%nat infix_mod_ /\
  forall (n m:int),
  m <> 0 ->
  app infix_mod_ [n m] \[] \[= CFML.CFHeader.int_mod n m ].

Hint Extern 1 (RegisterSpec infix_tilde_minus_) => Provide infix_tilde_minus__spec.
Hint Extern 1 (RegisterSpec infix_plus_) => Provide infix_plus__spec.
Hint Extern 1 (RegisterSpec infix_minus_) => Provide infix_minus__spec.
charguer's avatar
charguer committed
128 129
Hint Extern 1 (RegisterSpec infix_star_) => Provide infix_star__spec.
Hint Extern 1 (RegisterSpec infix_slash_) => Provide infix_slash__spec.
charguer's avatar
cp  
charguer committed
130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149
Hint Extern 1 (RegisterSpec infix_mod_) => Provide infix_mod__spec.

(* NOT NEEDED
Notation "`~- n" := (App infix_tilde_minus_ n;)
  (at level 69, no associativity) : app_scope.
Notation "n `+ m" := (App infix_plus_ n m;)
  (at level 69, no associativity) : app_scope.
Notation "n `+ m" := (App infix_minus_ n m;)
  (at level 69, no associativity) : app_scope.
Notation "n `+ m" := (App infix_star_ n m;)
  (at level 69, no associativity) : app_scope.
Notation "n `+ m" := (App infix_div_ n m;)
  (at level 69, no associativity) : app_scope.
Notation "n `+ m" := (App infix_mod_ n m;)
  (at level 69, no associativity) : app_scope.
 *)

Lemma succ_spec : forall (n:int),
  app succ [n] \[] \[= n+1 ].
Proof using.
charguer's avatar
charguer committed
150
  xcf. xgo*.
charguer's avatar
cp  
charguer committed
151 152 153 154 155
Qed.

Lemma pred_spec : forall (n:int),
  app pred [n] \[] \[= n-1 ].
Proof using.
charguer's avatar
charguer committed
156
  xcf. xgo*.
charguer's avatar
cp  
charguer committed
157 158 159
Qed.

Lemma abs_spec : forall (n:int),
charguer's avatar
charguer committed
160
  app Pervasives_ml.abs [n] \[] \[= Coq.ZArith.BinInt.Zabs n ].
charguer's avatar
cp  
charguer committed
161
Proof using.
charguer's avatar
charguer committed
162 163 164
  xcf. xgo.
  { rewrite~ Z.abs_eq. }
  { rewrite~ Z.abs_neq. math. }
charguer's avatar
cp  
charguer committed
165 166 167 168 169 170 171 172 173 174 175
Qed.

Hint Extern 1 (RegisterSpec succ) => Provide succ_spec.
Hint Extern 1 (RegisterSpec pred) => Provide pred_spec.
Hint Extern 1 (RegisterSpec abs) => Provide abs_spec.



(************************************************************)
(** References *)

charguer's avatar
charguer committed
176 177
Definition Ref a (v:a) (r:loc) :=  
  r ~> `{ contents' := v }.
charguer's avatar
cp  
charguer committed
178

charguer's avatar
array  
charguer committed
179
Notation "r '~~>' v" := (hdata (Ref v) r)
charguer's avatar
cp  
charguer committed
180 181 182
  (at level 32, no associativity) : heap_scope.

Lemma ref_spec : forall a (v:a),
charguer's avatar
array  
charguer committed
183
  app ref [v] \[] (fun r => r ~~> v).
charguer's avatar
records  
charguer committed
184
Proof using. xcf_go~. Qed.
charguer's avatar
cp  
charguer committed
185

charguer's avatar
array  
charguer committed
186 187
Lemma infix_emark__spec : forall a (v:a) r,
  app_keep infix_emark_ [r] (r ~~> v) \[= v].
charguer's avatar
records  
charguer committed
188
Proof using. xunfold Ref. xcf_go~. Qed.
charguer's avatar
cp  
charguer committed
189

charguer's avatar
array  
charguer committed
190 191
Lemma infix_colon_eq__spec : forall a (v w:a) r,
  app infix_colon_eq_ [r w] (r ~~> v) (# r ~~> w).
charguer's avatar
records  
charguer committed
192
Proof using. xunfold Ref. xcf_go~. Qed.
charguer's avatar
cp  
charguer committed
193

charguer's avatar
charguer committed
194 195 196 197
Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
Hint Extern 1 (RegisterSpec infix_emark_) => Provide infix_emark__spec.
Hint Extern 1 (RegisterSpec infix_colon_eq_) => Provide infix_colon_eq__spec.

charguer's avatar
charguer committed
198 199 200 201 202 203 204 205
Notation "'App'' `! r" := (App infix_emark_ r;)
  (at level 69, no associativity, r at level 0,
   format "'App''  `! r") : charac.

Notation "'App'' r `:= x" := (App infix_colon_eq_ r x;)
  (at level 69, no associativity, r at level 0,
   format "'App''  r  `:=  x") : charac.

charguer's avatar
array  
charguer committed
206 207
Lemma incr_spec : forall (n:int) r,
  app incr [r] (r ~~> n) (# r ~~> (n+1)).
charguer's avatar
records  
charguer committed
208
Proof using. xcf_go~. Qed.
charguer's avatar
cp  
charguer committed
209

charguer's avatar
array  
charguer committed
210 211
Lemma decr_spec : forall (n:int) r,
  app decr [r] (r ~~> n) (# r ~~> (n-1)).
charguer's avatar
records  
charguer committed
212
Proof using. xcf_go~. Qed.
charguer's avatar
cp  
charguer committed
213 214 215 216 217 218 219 220 221

Hint Extern 1 (RegisterSpec incr) => Provide incr_spec.
Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.


(************************************************************)
(** Pairs *)

Lemma fst_spec : forall A B (x:A) (y:B),
charguer's avatar
charguer committed
222
  app fst [(x,y)] \[] \[= x].
charguer's avatar
records  
charguer committed
223
Proof using. xcf_go~. Qed.
charguer's avatar
cp  
charguer committed
224 225

Lemma snd_spec : forall A B (x:A) (y:B),
charguer's avatar
charguer committed
226
  app snd [(x,y)] \[] \[= y].
charguer's avatar
records  
charguer committed
227
Proof using. xcf_go~. Qed.
charguer's avatar
cp  
charguer committed
228 229 230 231 232 233 234 235 236 237

Hint Extern 1 (RegisterSpec fst) => Provide fst_spec.
Hint Extern 1 (RegisterSpec snd) => Provide snd_spec.


(************************************************************)
(** Unit *)

Lemma ignore_spec : 
  app ignore [tt] \[] \[= tt].
charguer's avatar
records  
charguer committed
238
Proof using. xcf_go~. Qed.
charguer's avatar
cp  
charguer committed
239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257

Hint Extern 1 (RegisterSpec ignore) => Provide ignore_spec.


(************************************************************)
(** Float *)

(* TODO *)





(************************************************************)
(************************************************************)
(************************************************************)

(* FUTURE

charguer's avatar
charguer committed
258 259 260 261

(*------------------------------------------------------------------*)
(* ** References *)

charguer's avatar
array  
charguer committed
262 263
Definition Ref a A (T:htype A a) (V:A) (r:loc) :=
  Hexists v, heap_is_single r v \* v ~> T V.
charguer's avatar
charguer committed
264 265 266 267 268 269 270 271 272 273 274 275 276 277 278

Instance Ref_Heapdata : forall a A (T:htype A a),
  (Heapdata (@Ref a A T)).
Proof using.
  intros. applys Heapdata_prove. intros x X1 X2.
  unfold Ref. hdata_simpl. hextract as x1 x2.
  hchange (@star_is_single_same_loc x). hsimpl. 
Qed.

Open Local Scope heap_scope_advanced.

Notation "'~~>' v" := (~> Ref (@Id _) v)
  (at level 32, no associativity) : heap_scope_advanced.

(*
charguer's avatar
array  
charguer committed
279
Notation "l '~~>' v" := (r ~> Ref (@Id _) v)
charguer's avatar
charguer committed
280 281
  (at level 32, no associativity) : heap_scope. 
*)
charguer's avatar
array  
charguer committed
282
Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) r)
charguer's avatar
charguer committed
283 284
  (at level 32, no associativity) : heap_scope.

charguer's avatar
array  
charguer committed
285 286
Lemma focus_ref : forall (r:loc) a A (T:htype A a) V,
  r ~> Ref T V ==> Hexists v, r ~~> v \* v ~> T V.
charguer's avatar
charguer committed
287 288
Proof. intros. unfold Ref, hdata. unfold Id. hsimpl~. Qed.

charguer's avatar
array  
charguer committed
289 290
Lemma unfocus_ref : forall (r:loc) a (v:a) A (T:htype A a) V,
  r ~~> v \* v ~> T V ==> r ~> Ref T V.
charguer's avatar
charguer committed
291 292
Proof. intros. unfold Ref. hdata_simpl. hsimpl. subst~. Qed.

charguer's avatar
array  
charguer committed
293 294
Lemma heap_is_single_impl_null : forall (r:loc) A (v:A),
  heap_is_single r v ==> heap_is_single r v \* \[r <> null].
charguer's avatar
charguer committed
295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317
Proof.
  intros. intros h Hh. forwards*: heap_is_single_null. exists___*.
Qed.

Lemma focus_ref_null : forall a A (T:htype A a) V,
  null ~> Ref T V ==> \[False].
Proof.
  intros. unfold Ref, hdata. hextract as v.
  hchanges (@heap_is_single_impl_null null).
Qed.

Global Opaque Ref.
Implicit Arguments focus_ref [a A].
Implicit Arguments unfocus_ref [a A].




(************************************************************)
(** Group of References *)

Parameter caml_ref_spec_group : forall a,
  Spec caml_ref (v:a) |R>> forall (M:map loc a),
charguer's avatar
array  
charguer committed
318 319
    R (Group (Ref Id) M) (fun (r:loc) => 
       Group (Ref Id) (M[r:=v]) \* \[r \notindom M]).
charguer's avatar
charguer committed
320 321

Lemma caml_get_spec_group : forall a,
charguer's avatar
array  
charguer committed
322 323 324
  Spec caml_get (r:loc) |R>> forall (M:map loc a), 
    forall `{Inhab a}, r \indom M ->
    keep R (Group (Ref Id) M) (fun x => \[x = M[r]]).
charguer's avatar
charguer committed
325
Proof.
charguer's avatar
array  
charguer committed
326 327
  intros. xweaken. intros r R LR HR M IA IlM. simpls.
  rewrite~ (Group_rem r M). xapply (HR (M[r])); hsimpl~. 
charguer's avatar
charguer committed
328 329 330
Qed.

Lemma caml_set_spec_group : forall a, 
charguer's avatar
array  
charguer committed
331 332 333
  Spec caml_set (r:loc) (v:a) |R>> forall (M:map loc a), 
    forall `{Inhab a}, r \indom M ->
    R (Group (Ref Id) M) (# Group (Ref Id) (M[r:=v])).
charguer's avatar
charguer committed
334
Proof.
charguer's avatar
array  
charguer committed
335 336 337 338
  intros. xweaken. intros r v R LR HR M IA IlM. simpls.
  rewrite~ (Group_rem r M).
  xapply (HR (M[r])). hsimpl.
  intros _. hchanges~ (Group_add' r M).
charguer's avatar
charguer committed
339 340 341
Qed.


charguer's avatar
cp  
charguer committed
342
*)