Demo_proof.v 39.2 KB
Newer Older
charguer's avatar
charguer committed
1
Set Implicit Arguments.
2
Require Import CFML.CFLib.
charguer's avatar
xwhile  
charguer committed
3 4
Require Import Demo_ml.
Require Import Stdlib.
charguer's avatar
charguer committed
5
Require LibListZ.
charguer's avatar
charguer committed
6
Import ZsubNoSimpl.
charguer's avatar
charguer committed
7 8
Open Scope tag_scope.

charguer's avatar
charguer committed
9 10


charguer's avatar
polylet  
charguer committed
11 12 13
(********************************************************************)
(********************************************************************)

charguer's avatar
charguer committed
14 15 16 17 18
(********************************************************************)
(* ** Notation for PRE/INV/POST *)


Lemma notation_inv_post_spec_pre : forall (r:loc) (n:int),
POTTIER Francois's avatar
POTTIER Francois committed
19 20
  app notation_inv_post [r]
    PRE (r ~~> n)
charguer's avatar
charguer committed
21 22 23 24
    POST (fun x => \[x = n] \* r ~~> n).
Proof using. xcf. xapp. Qed.

Lemma notation_inv_post_spec_inv : forall (r:loc) (n:int),
POTTIER Francois's avatar
POTTIER Francois committed
25 26
  app notation_inv_post [r]
    INV (r ~~> n)
charguer's avatar
charguer committed
27 28 29 30
    POST \[= n].
Proof using. xcf. xapp. Qed.

Lemma notation_pre_inv_post_spec_pre : forall (r s:loc) (n m:int),
POTTIER Francois's avatar
POTTIER Francois committed
31 32
  app notation_pre_inv_post [r s]
    PRE (r ~~> n \* s ~~> m)
charguer's avatar
charguer committed
33 34 35 36
    POST (fun x => \[x = m] \* r ~~> (n+1) \* s ~~> m).
Proof using. xcf. xapp. xapp. xsimpl*. Qed.

Lemma notation_pre_inv_post_spec_inv : forall (r s:loc) (n m:int),
POTTIER Francois's avatar
POTTIER Francois committed
37 38 39
  app notation_pre_inv_post [r s]
    PRE' (r ~~> n)
    INV' (s ~~> m)
charguer's avatar
charguer committed
40 41 42 43 44
    POST (fun x => \[x = m] \* r ~~> (n+1)).
Proof using. xcf. xapp. xapp. xsimpl*. Qed.



charguer's avatar
charguer committed
45 46 47 48 49 50
(********************************************************************)
(* ** Encoding of names *)

Lemma renaming_types : True.
Proof using.
  pose renaming_t'_.
POTTIER Francois's avatar
POTTIER Francois committed
51 52
  pose renaming_t2_. pose C'.
  pose renaming_t3_.
charguer's avatar
charguer committed
53 54
  pose renaming_t4_.
  auto.
POTTIER Francois's avatar
POTTIER Francois committed
55
Qed.
charguer's avatar
charguer committed
56

POTTIER Francois's avatar
POTTIER Francois committed
57
Lemma renaming_demo_spec :
charguer's avatar
charguer committed
58 59 60 61 62 63 64 65 66
  app renaming_demo [tt] \[] \[= tt].
Proof using.
  xcf.
  xval.
  xval.
  xval.
  xval.
  xval.
  xrets.
POTTIER Francois's avatar
POTTIER Francois committed
67
  auto.
charguer's avatar
charguer committed
68
Qed.
charguer's avatar
polylet  
charguer committed
69 70


charguer's avatar
charguer committed
71 72 73
(********************************************************************)
(* ** Polymorphic let bindings and value restriction *)

POTTIER Francois's avatar
POTTIER Francois committed
74
Lemma let_poly_p0_spec :
charguer's avatar
polylet  
charguer committed
75 76 77 78 79
  app let_poly_p0 [tt] \[] \[= tt].
Proof using.
  xcf. xlet_poly_keep (= true). xapp_skip. intro_subst. xrets~.
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
80
Lemma let_poly_p1_spec :
charguer's avatar
polylet  
charguer committed
81 82 83 84 85 86 87
  app let_poly_p1 [tt] \[] \[= tt].
Proof using.
  xcf. xfun. xlet_poly_keep (fun B (r:option B) => r = None).
  { xapps. xrets. }
  { intros Hr. xrets~. }
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
88
Lemma let_poly_p2_spec :
charguer's avatar
polylet  
charguer committed
89 90 91 92 93 94
  app let_poly_p2 [tt] \[] \[= tt].
Proof using.
  xcf. xfun. xlet.
  { xlet_poly_keep (fun B (r:option B) => r = None).
    { xapps. xrets. }
    { intros Hr. xrets~. } }
POTTIER Francois's avatar
POTTIER Francois committed
95
  { xrets~. }
charguer's avatar
polylet  
charguer committed
96 97
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
98
Lemma let_poly_p3_spec :
charguer's avatar
polylet  
charguer committed
99 100
  app let_poly_p3 [tt] \[] \[= tt].
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
101
  xcf.
charguer's avatar
polylet  
charguer committed
102 103 104 105
  xlet_poly_keep (= true). { xapp_skip. } intro_subst.
  xapp_skip.
  xlet_poly_keep (= false). { xapp_skip. } intro_subst.
  xapp_skip.
POTTIER Francois's avatar
POTTIER Francois committed
106
  xrets~.
charguer's avatar
polylet  
charguer committed
107 108
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
109
Lemma let_poly_f0_spec : forall A,
charguer's avatar
polylet  
charguer committed
110 111 112 113 114
  app let_poly_f0 [tt] \[] \[= @nil A].
Proof using.
  xcf. xapps. xapps. xsimpl~.
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
115
Lemma let_poly_f1_spec : forall A,
charguer's avatar
polylet  
charguer committed
116 117 118 119 120
  app let_poly_f1 [tt] \[] \[= @nil A].
Proof using.
  xcf. xapps. xapps. xsimpl~.
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
121
Lemma let_poly_f2_spec : forall A,
charguer's avatar
polylet  
charguer committed
122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
  app let_poly_f2 [tt] \[] \[= @nil A].
Proof using.
  xcf. xapps. xapps. xsimpl~.
Qed.

Lemma let_poly_f3_spec :
  app let_poly_f3 [tt] \[] \[= @nil int].
Proof using.
  xcf. xapps. xapps. xsimpl~.
Qed.

Lemma let_poly_f4_spec :
  app let_poly_f4 [tt] \[] \[= @nil int].
Proof using.
  xcf. xapps. xapps. xsimpl~.
Qed.

Lemma let_poly_g1_spec :
  app let_poly_g1 [tt] \[] \[= 5::nil].
Proof using.
  xcf. xapps. xapps. xapps. xsimpl~.
Qed.

Lemma let_poly_g2_spec :
  app let_poly_g2 [tt] \[] \[= 4::nil].
Proof using.
  xcf. xapps. xapps. xapps. xsimpl~.
Qed.

charguer's avatar
charguer committed
151 152
Lemma let_poly_h0_spec : forall A,
  app let_poly_h0 [tt] \[] (fun (r:loc) => r ~~> (@nil A)).
charguer's avatar
polylet  
charguer committed
153
Proof using.
charguer's avatar
charguer committed
154
  xcf. xapps. xret~.
charguer's avatar
polylet  
charguer committed
155 156
Qed.

charguer's avatar
charguer committed
157 158 159 160
Lemma let_poly_h1_spec : forall A,
  app let_poly_h1 [tt] \[] (fun (f:func) =>
    \[ app f [tt] \[] (fun (r:loc) => r ~~> (@nil A)) ]).
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
161
  xcf. xlet (fun g => \[ app g [tt] \[] (fun (r:loc) => r ~~> (@nil A)) ]).
charguer's avatar
charguer committed
162 163 164
  { xfun. xrets. xapps. xapps. }
  intros Hg. xrets. xapps.
Qed.
charguer's avatar
xgc  
charguer committed
165

charguer's avatar
charguer committed
166 167 168 169 170 171
Lemma let_poly_h2_spec : forall A,
  app let_poly_h2 [tt] \[] (fun (f:func) =>
    \[ app f [tt] \[] (fun (r:loc) => r ~~> (@nil A)) ]).
Proof using.
  xcf. xfun. xrets. xapps. xapps.
Qed.
charguer's avatar
recfun  
charguer committed
172

charguer's avatar
charguer committed
173 174 175 176 177
Lemma let_poly_h3_spec : forall A,
  app let_poly_h3 [tt] \[] (fun (r:loc) => r ~~> (@nil A)).
Proof using.
  xcf. xfun. xapps. xapps.
Qed.
charguer's avatar
xpat  
charguer committed
178

charguer's avatar
charguer committed
179 180 181 182 183
Lemma let_poly_k1_spec : forall A,
  app let_poly_k1 [tt] \[] \[= @nil A].
Proof using.
  xcf. xrets~.
Qed.
charguer's avatar
xpat  
charguer committed
184

charguer's avatar
charguer committed
185 186 187 188 189
Lemma let_poly_k2_spec : forall A,
  app let_poly_k2 [tt] \[] (fun (r:loc) => r ~~> (@nil A)).
Proof using.
  xcf. xapps.
Qed.
charguer's avatar
charguer committed
190

POTTIER Francois's avatar
POTTIER Francois committed
191
Lemma let_poly_r1_spec :
charguer's avatar
charguer committed
192 193 194 195 196
  app let_poly_r1 [tt] \[] \[= tt].
Proof using.
  xcf. xapps. xrets~.
  Unshelve. solve_type.
Qed.
charguer's avatar
charguer committed
197

charguer's avatar
charguer committed
198 199
Lemma let_poly_r2_spec : forall A,
  app let_poly_r2 [tt] \[] \[= @nil A].
charguer's avatar
charguer committed
200
Proof using.
charguer's avatar
charguer committed
201 202 203 204 205
  xcf. xapps. dup 2.
  { xval. xrets~. }
  { xvals. xrets~. }
  Unshelve. solve_type.
Qed.
charguer's avatar
charguer committed
206

charguer's avatar
charguer committed
207 208 209

Lemma let_poly_r3_spec : forall A,
  app let_poly_r3 [tt] \[] \[= @nil A].
charguer's avatar
charguer committed
210
Proof using.
charguer's avatar
charguer committed
211 212 213
  xcf. xlet_poly_keep (fun A (r:list A) => r = nil).
  { xapps. xrets~. }
  intros Hr. xrets. auto.
charguer's avatar
charguer committed
214 215 216
Qed.


charguer's avatar
charguer committed
217

charguer's avatar
charguer committed
218 219
(********************************************************************)
(* ** Top-level values *)
charguer's avatar
ok  
charguer committed
220

charguer's avatar
charguer committed
221 222 223 224 225 226 227
Lemma top_val_int_spec :
  top_val_int = 5.
Proof using.
  dup 5.
  xcf. auto.
  (* demos: *)
  xcf_show. skip.
POTTIER Francois's avatar
POTTIER Francois committed
228
  xcf_show top_val_int. skip.
charguer's avatar
PRE  
charguer committed
229
  xcf_show top_val_int as M. skip.
charguer's avatar
charguer committed
230 231
  xcf. skip.
Qed.
charguer's avatar
ok  
charguer committed
232

POTTIER Francois's avatar
POTTIER Francois committed
233
Lemma top_val_int_list_spec :
charguer's avatar
charguer committed
234 235 236 237
  top_val_int_list = @nil int.
Proof using.
  xcf. auto.
Qed.
charguer's avatar
ok  
charguer committed
238

charguer's avatar
charguer committed
239 240 241
Lemma top_val_poly_list_spec : forall A,
  top_val_poly_list = @nil A.
Proof using. xcf*. Qed.
charguer's avatar
init  
charguer committed
242

charguer's avatar
charguer committed
243 244 245
Lemma top_val_poly_list_pair_spec : forall A B,
  top_val_poly_list_pair = (@nil A, @nil B).
Proof using. xcf*. Qed.
charguer's avatar
ok  
charguer committed
246

charguer's avatar
init  
charguer committed
247

charguer's avatar
xpat  
charguer committed
248

charguer's avatar
charguer committed
249
(********************************************************************)
charguer's avatar
xpat  
charguer committed
250
(* ** Return *)
charguer's avatar
init  
charguer committed
251

POTTIER Francois's avatar
POTTIER Francois committed
252
Lemma ret_unit_spec :
charguer's avatar
xpat  
charguer committed
253
  app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
charguer's avatar
charguer committed
254
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
255
  xcf. dup 8.
charguer's avatar
charguer committed
256 257 258 259 260 261 262 263 264 265
  { xret. xsimpl. auto. }
  { xrets. auto. }
  { xrets*. }
  { xret_no_gc. xsimpl. auto. }
  { xret_no_clean. xsimpl*. } (* differs only on nontrivial goals *)
  { xret_no_pull. xsimpl*. } (* differs only on a let binding *)
  { try xret (fun r => \[r = tt /\ True]).
    xpost. xret (fun r => \[r = tt /\ True]). xsimpl. auto. xsimpl. auto. }
  { try xrets (fun r => \[r = tt /\ True]).
    xpost. xrets (fun r => \[r = tt /\ True]). auto. xsimpl. auto. }
charguer's avatar
charguer committed
266
Qed.
charguer's avatar
ok  
charguer committed
267

POTTIER Francois's avatar
POTTIER Francois committed
268
Lemma ret_int_spec :
charguer's avatar
xpat  
charguer committed
269 270
  app ret_int [tt] \[] \[= 3].
Proof using. xcf. xrets*. Qed.
charguer's avatar
ok  
charguer committed
271

charguer's avatar
xpat  
charguer committed
272 273
Lemma ret_int_pair_spec :
  app ret_int_pair [tt] \[] \[= (3,4)].
charguer's avatar
xwhile  
charguer committed
274
Proof using. xcf_go*. Qed.
charguer's avatar
ok  
charguer committed
275

charguer's avatar
xpat  
charguer committed
276 277
Lemma ret_poly_spec : forall A,
  app ret_poly [tt] \[] \[= @nil A].
charguer's avatar
xwhile  
charguer committed
278
Proof using. xcf. xgo*. Qed.
charguer's avatar
ok  
charguer committed
279 280


charguer's avatar
xlet  
charguer committed
281 282 283 284 285 286 287 288
(********************************************************************)
(* ** Sequence *)

Axiom ret_unit_spec' : forall A (x:A),
  app ret_unit [x] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)

Hint Extern 1 (RegisterSpec ret_unit) => Provide ret_unit_spec'.

charguer's avatar
PRE  
charguer committed
289

charguer's avatar
xlet  
charguer committed
290 291 292 293 294 295 296 297
Lemma seq_ret_unit_spec :
  app seq_ret_unit [tt] \[] \[= tt].
Proof using.
  xcf.
  (* xlet. -- make sure we get a good error here *)
  xseq.
  xapp1.
  xapp2.
POTTIER Francois's avatar
POTTIER Francois committed
298
  dup 3.
charguer's avatar
xlet  
charguer committed
299
  { xapp3_no_apply. apply S. }
charguer's avatar
charguer committed
300
  { xapp3_no_simpl. skip. skip. }
charguer's avatar
xlet  
charguer committed
301 302
  { xapp3. }
  dup 4.
charguer's avatar
PRE  
charguer committed
303
  { xseq. xapp. xapp. xsimpl. auto. }
charguer's avatar
demo1  
charguer committed
304 305
  { xapp. intro_subst. xapp. }
  { xapps. xapps. }
charguer's avatar
xlet  
charguer committed
306
  { xapps. xapps~. }
charguer's avatar
charguer committed
307
Abort.
charguer's avatar
xlet  
charguer committed
308 309


charguer's avatar
ok  
charguer committed
310

charguer's avatar
charguer committed
311
(********************************************************************)
charguer's avatar
xpat  
charguer committed
312
(* ** Let-value *)
charguer's avatar
init  
charguer committed
313

POTTIER Francois's avatar
POTTIER Francois committed
314
Lemma let_val_int_spec :
charguer's avatar
xpat  
charguer committed
315
  app let_val_int [tt] \[] \[= 3].
charguer's avatar
charguer committed
316
Proof using.
charguer's avatar
xpat  
charguer committed
317 318 319 320 321 322 323 324 325
  xcf. dup 7.
  xval. xrets~.
  (* demos *)
  xval as r. xrets~.
  xval as r Er. xrets~.
  xvals. xrets~.
  xval_st (= 3). auto. xrets~.
  xval_st (= 3) as r. auto. xrets~.
  xval_st (= 3) as r Er. auto. xrets~.
charguer's avatar
init  
charguer committed
326 327
Qed.

charguer's avatar
xpat  
charguer committed
328 329 330 331 332 333
Lemma let_val_pair_int_spec :
  app let_val_pair_int [tt] \[] \[= (3,4)].
Proof using. xcf. xvals. xrets*. Qed.

Lemma let_val_poly_spec :
  app let_val_poly [tt] \[] \[= 3].
charguer's avatar
charguer committed
334
Proof using.
charguer's avatar
xpat  
charguer committed
335
  xcf. dup 3.
charguer's avatar
demo1  
charguer committed
336
  { xval. xret. xsimpl. auto. }
POTTIER Francois's avatar
POTTIER Francois committed
337
  { xval as r. xrets~. }
charguer's avatar
demo1  
charguer committed
338
  { xvals. xrets~. }
charguer's avatar
charguer committed
339
Qed.
charguer's avatar
init  
charguer committed
340 341


charguer's avatar
xlet  
charguer committed
342 343 344
(********************************************************************)
(* ** Let-function *)

POTTIER Francois's avatar
POTTIER Francois committed
345
Lemma let_fun_const_spec :
charguer's avatar
xlet  
charguer committed
346 347
  app let_fun_const [tt] \[] \[= 3].
Proof using.
charguer's avatar
PRE  
charguer committed
348
  xcf. dup 10.
charguer's avatar
charguer committed
349
  { xfun. apply Sf. xtag_pre_post. xrets~. }
charguer's avatar
xlet  
charguer committed
350
  { xfun as g. apply Sg. skip. }
charguer's avatar
PRE  
charguer committed
351
  { xfun as g. xapp. xret. skip. }
charguer's avatar
xlet  
charguer committed
352 353
  { xfun as g G. apply G. skip. }
  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]).
POTTIER Francois's avatar
POTTIER Francois committed
354
    { xapp. skip. }
charguer's avatar
xlet  
charguer committed
355 356
    { apply Sf. } }
  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h.
POTTIER Francois's avatar
POTTIER Francois committed
357
    { apply Sh. skip. }
charguer's avatar
xlet  
charguer committed
358 359
    { apply Sh. } }
  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h H.
POTTIER Francois's avatar
POTTIER Francois committed
360
    { xapp. skip. }
charguer's avatar
PRE  
charguer committed
361
    { xapp. } }
charguer's avatar
xlet  
charguer committed
362
  { xfun (fun g => app g [tt] \[] \[=3]).
POTTIER Francois's avatar
POTTIER Francois committed
363
    { xrets~. }
charguer's avatar
xlet  
charguer committed
364 365
    { apply Sf. } }
  { xfun (fun g => app g [tt] \[] \[=3]) as h.
POTTIER Francois's avatar
POTTIER Francois committed
366
    { skip. }
charguer's avatar
xlet  
charguer committed
367 368
    { skip. } }
  { xfun (fun g => app g [tt] \[] \[=3]) as h H.
POTTIER Francois's avatar
POTTIER Francois committed
369
    { skip. }
charguer's avatar
xlet  
charguer committed
370 371 372 373 374 375 376 377 378 379
    { skip. } }
Qed.

Lemma let_fun_poly_id_spec :
  app let_fun_poly_id [tt] \[] \[= 3].
Proof using.
  xcf. xfun. dup 2.
  { xapp. xret. xsimpl~. }
  { xapp1.
    xapp2.
POTTIER Francois's avatar
POTTIER Francois committed
380
    dup 5.
charguer's avatar
demo1  
charguer committed
381 382
    { apply Spec. xrets. auto. }
    { xapp3_no_apply. Focus 2. apply S. xrets. auto. }
charguer's avatar
charguer committed
383
    { xapp3_no_simpl. xrets~. skip. skip. }
charguer's avatar
demo1  
charguer committed
384 385
    { xapp3. xrets~. }
    { xapp. xret. xsimpl~. } }
charguer's avatar
charguer committed
386
Abort.
charguer's avatar
xlet  
charguer committed
387

POTTIER Francois's avatar
POTTIER Francois committed
388
Lemma let_fun_poly_pair_homogeneous_spec :
charguer's avatar
xlet  
charguer committed
389 390
  app let_fun_poly_pair_homogeneous [tt] \[] \[= (3,3)].
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
391
  xcf.
charguer's avatar
xlet  
charguer committed
392
  xfun.
POTTIER Francois's avatar
POTTIER Francois committed
393
  xapp.
charguer's avatar
xlet  
charguer committed
394 395 396 397 398 399 400 401 402 403
  xret.
  xsimpl~.
Qed.

Lemma let_fun_on_the_fly_spec :
  app let_fun_on_the_fly [tt] \[] \[= 4].
Proof using.
  xcf.
  xfun.
  xfun.
POTTIER Francois's avatar
POTTIER Francois committed
404
  xapp.
charguer's avatar
xlet  
charguer committed
405 406 407 408 409
  xapp.
  xret.
  xsimpl~.
Qed.

charguer's avatar
demo1  
charguer committed
410
Lemma let_fun_in_let_spec :
POTTIER Francois's avatar
POTTIER Francois committed
411
  app let_fun_in_let [tt] \[]
charguer's avatar
demo1  
charguer committed
412 413 414
    (fun g => \[ forall A (x:A), app g [x] \[] \[= x] ]).
Proof using.
  xcf. xlet (fun g => \[ forall A (x:A), app g [x] \[] \[= x] ]).
charguer's avatar
charguer committed
415
    (* TODO: use [xpush] *)
charguer's avatar
demo1  
charguer committed
416 417 418
  { xassert. { xret. }
    xfun. xrets. =>>. xapp. xrets~. }
  { =>> M. xrets~. }
POTTIER Francois's avatar
POTTIER Francois committed
419
Qed.
charguer's avatar
cp  
charguer committed
420

charguer's avatar
PRE  
charguer committed
421
Lemma let_fun_in_let_spec' :
POTTIER Francois's avatar
POTTIER Francois committed
422 423
  app let_fun_in_let [tt]
  PRE \[]
charguer's avatar
xwhile  
charguer committed
424 425 426 427 428 429
  POST (fun g => \[ forall A (x:A), app g [x] \[] \[= x] ]).
Proof using.
  xcf.
Abort.


charguer's avatar
xlet  
charguer committed
430 431 432 433 434 435 436 437

(********************************************************************)
(* ** Let-term *)

Lemma let_term_nested_id_calls_spec :
  app let_term_nested_id_calls [tt] \[] \[= 2].
Proof using.
  xcf.
charguer's avatar
demo1  
charguer committed
438
  xfun (fun f => forall (x:int), app f [x] \[] \[= x]). { xrets~. }
POTTIER Francois's avatar
POTTIER Francois committed
439
  xapps.
charguer's avatar
xlet  
charguer committed
440 441 442 443 444 445 446 447
  xapps.
  xapps.
  xrets~.
Qed.

Lemma let_term_nested_pairs_calls_spec :
  app let_term_nested_pairs_calls [tt] \[] \[= ((1,2),(3,(4,5))) ].
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
448
  xcf.
charguer's avatar
demo1  
charguer committed
449
  xfun (fun f => forall A B (x:A) (y:B), app f [x y] \[] \[= (x,y)]). { xrets~. }
charguer's avatar
xlet  
charguer committed
450 451 452 453 454 455 456
  xapps.
  xapps.
  xapps.
  xapps.
  xrets~.
Qed.

charguer's avatar
charguer committed
457
(********************************************************************)
charguer's avatar
xpat  
charguer committed
458
(* ** Pattern-matching *)
charguer's avatar
init  
charguer committed
459

POTTIER Francois's avatar
POTTIER Francois committed
460
Lemma match_pair_as_spec :
charguer's avatar
xpat  
charguer committed
461 462 463 464 465 466
  app match_pair_as [tt] \[] \[= (4,(3,4))].
Proof using.
  xcf. dup 8.
  { xmatch. xrets*. }
  { xmatch_subst_alias. xrets*. }
  { xmatch_no_alias. xalias. xalias as L. skip. }
POTTIER Francois's avatar
POTTIER Francois committed
467
  { xmatch_no_cases. dup 6.
charguer's avatar
charguer committed
468
    { xmatch_case.
POTTIER Francois's avatar
POTTIER Francois committed
469
      { xrets*. }
charguer's avatar
charguer committed
470
      { xmatch_case. } }
charguer's avatar
xpat  
charguer committed
471 472 473
    { xcase_no_simpl.
      { dup 3.
        { xalias. xalias. xret. xsimpl. xauto*. }
POTTIER Francois's avatar
POTTIER Francois committed
474
        { xalias as u U.
charguer's avatar
xpat  
charguer committed
475 476
          xalias as v. skip. }
        { xalias_subst. xalias_subst. skip. } }
POTTIER Francois's avatar
POTTIER Francois committed
477
      { xdone. } }
charguer's avatar
xpat  
charguer committed
478 479 480
    { xcase_no_simpl as E. skip. skip. }
    { xcase_no_intros. intros x y E. skip. intros F. skip. }
    { xcase. skip. skip. }
POTTIER Francois's avatar
POTTIER Francois committed
481 482
    { xcase as C. skip. skip.
      (* note: inversion got rid of C *)
charguer's avatar
xpat  
charguer committed
483 484 485
    } }
  { xmatch_no_simpl_no_alias. skip. }
  { xmatch_no_simpl_subst_alias. skip. }
charguer's avatar
charguer committed
486
  { xmatch_no_intros. skip. }
POTTIER Francois's avatar
POTTIER Francois committed
487
  { xmatch_no_simpl. inverts C. skip. }
charguer's avatar
xpat  
charguer committed
488 489
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
490
Lemma match_nested_spec :
charguer's avatar
xpat  
charguer committed
491 492 493
  app match_nested [tt] \[] \[= (2,2)::nil].
Proof using.
  xcf. xval. dup 3.
POTTIER Francois's avatar
POTTIER Francois committed
494 495 496
  { xmatch_no_simpl.
    { xrets*. }
    { false. (* note: [xrets] would produce a ununified [hprop].
charguer's avatar
xpat  
charguer committed
497 498
     caused by [tryfalse] in [hextract_cleanup]. TODO: avoid this. *) } }
  { xmatch.
POTTIER Francois's avatar
POTTIER Francois committed
499
    xrets*.
charguer's avatar
xpat  
charguer committed
500 501
    (* second case is killed by [xcase_post] *) }
  { xmatch_no_intros. skip. skip. }
charguer's avatar
charguer committed
502
Qed.
charguer's avatar
init  
charguer committed
503

charguer's avatar
demo  
charguer committed
504

charguer's avatar
charguer committed
505 506 507
(********************************************************************)
(* ** Let-pattern *)

POTTIER Francois's avatar
POTTIER Francois committed
508
Lemma let_pattern_pair_int_spec :
charguer's avatar
charguer committed
509 510 511 512 513 514 515 516
  app let_pattern_pair_int [tt] \[] \[= 3].
Proof using. xcf. xmatch. xrets~. Qed.

Lemma let_pattern_pair_int_wildcard_spec :
  app let_pattern_pair_int_wildcard [tt] \[] \[= 3].
Proof using. xcf. xmatch. xrets~. Qed.


charguer's avatar
charguer committed
517 518
(********************************************************************)
(* ** Infix functions *)
POTTIER Francois's avatar
POTTIER Francois committed
519

charguer's avatar
charguer committed
520 521
Lemma infix_plus_plus_plus_spec : forall x y,
  app infix_plus_plus_plus__ [x y] \[] \[= x + y].
charguer's avatar
charguer committed
522
Proof using.
charguer's avatar
xwhile  
charguer committed
523
  xcf_go~.
charguer's avatar
charguer committed
524 525
Qed.

charguer's avatar
charguer committed
526
Hint Extern 1 (RegisterSpec infix_plus_plus_plus__) => Provide infix_plus_plus_plus_spec.
charguer's avatar
charguer committed
527 528 529 530 531 532 533 534 535

Lemma infix_aux_spec : forall x y,
  app infix_aux [x y] \[] \[= x + y].
Proof using.
  xcf. xapps~.
Qed.

Hint Extern 1 (RegisterSpec infix_aux) => Provide infix_aux_spec.

charguer's avatar
charguer committed
536 537
Lemma infix_minus_minus_minus_spec : forall x y,
  app infix_minus_minus_minus__ [x y] \[] \[= x + y].
charguer's avatar
charguer committed
538 539 540
Proof using.
  intros. xcf_show as S. rewrite S. xapps~.
Qed.
charguer's avatar
charguer committed
541 542


charguer's avatar
charguer committed
543

charguer's avatar
charguer committed
544 545 546
(********************************************************************)
(* ** Lazy binary operators *)

POTTIER Francois's avatar
POTTIER Francois committed
547
Lemma lazyop_val_spec :
charguer's avatar
charguer committed
548 549 550 551 552 553 554 555 556
  app lazyop_val [tt] \[] \[= 1].
Proof using.
  xcf. xif. xrets~.
Qed.

(*
Ltac xauto_tilde ::= xauto_tilde_default ltac:(fun _ => auto_tilde).
*)

POTTIER Francois's avatar
POTTIER Francois committed
557
Lemma lazyop_term_spec :
charguer's avatar
charguer committed
558 559
  app lazyop_term [tt] \[] \[= 1].
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
560 561
  xcf. xfun (fun f => forall (x:int),
    app f [x] \[] \[= isTrue (x = 0)]).
charguer's avatar
charguer committed
562 563
  { xrets*. }
  xapps.
POTTIER Francois's avatar
POTTIER Francois committed
564
  xlet \[=true].
charguer's avatar
charguer committed
565 566 567
  { dup 10.
    { xors. xapps. xsimpl~. subst. xclean. xauto*. }
    { xors \[=true]. xapps. xsimpl~. skip. }
charguer's avatar
stable  
charguer committed
568
    { xor \[=true]. hsimpl. xapps. xsimpl. skip. }
charguer's avatar
charguer committed
569 570
    { xif_no_simpl. skip. skip. }
    { xpost. xif_no_simpl \[= true]. skip. skip. skip. }
POTTIER Francois's avatar
POTTIER Francois committed
571
    { xpost. xif_no_simpl \[=true] as R.
charguer's avatar
charguer committed
572
      { xclean. false. }
POTTIER Francois's avatar
POTTIER Francois committed
573
      { xapps. xsimpl. subst. xclean. xauto*. }
charguer's avatar
charguer committed
574
     xsimpl~. }
charguer's avatar
stable  
charguer committed
575
    { xpost. xif_no_intros \[=true]. intros R. skip. skip. skip. }
charguer's avatar
charguer committed
576
    { xpost. xif_no_simpl_no_intros \[=true]. intros R. skip. skip. skip. }
charguer's avatar
stable  
charguer committed
577
    { xif. xrets. xapps. xsimpl. skip. }
charguer's avatar
charguer committed
578 579 580 581 582 583 584
    { xgo*. subst. xclean. auto. }
      (* todo: maybe extend [xauto_common] with [logics]? or would it be too slow? *)
  }
  intro_subst. xif. xrets~.
Qed.


POTTIER Francois's avatar
POTTIER Francois committed
585
Lemma lazyop_mixed_spec :
charguer's avatar
charguer committed
586 587 588
  app lazyop_mixed [tt] \[] \[= 1].
Proof using.
  xcf.
POTTIER Francois's avatar
POTTIER Francois committed
589 590
  xfun (fun f => forall (x:int),
    app f [x] \[] \[= isTrue (x = 0)]).
charguer's avatar
charguer committed
591 592
  { xrets*. }
  xlet \[= true].
charguer's avatar
stable  
charguer committed
593
  { xif. xapps. xors. xapps. xrets. autos*. }
charguer's avatar
charguer committed
594 595 596 597 598 599
  { intro_subst. xif. xrets~. }
Qed.




charguer's avatar
charguer committed
600 601 602
(********************************************************************)
(* ** Comparison operators *)

POTTIER Francois's avatar
POTTIER Francois committed
603
Lemma compare_poly_spec :
charguer's avatar
charguer committed
604 605 606
  app compare_poly [tt] \[] \[= tt].
Proof using.
  xcf.
charguer's avatar
charguer committed
607
  xlet_poly_keep (= true).
charguer's avatar
stable  
charguer committed
608
  { xapps. xpolymorphic_eq. xsimpl. subst r. rew_bool_eq~. }
charguer's avatar
charguer committed
609 610 611
  intro_subst.
  xapp. xpolymorphic_eq. intro_subst.
  xlet_poly_keep (= true).
charguer's avatar
stable  
charguer committed
612
  { xapps. xpolymorphic_eq. xsimpl. subst r. rew_bool_eq~. }
charguer's avatar
charguer committed
613 614
  intro_subst.
  xapp. xpolymorphic_eq. intro_subst.
charguer's avatar
charguer committed
615
  xrets~.
POTTIER Francois's avatar
POTTIER Francois committed
616
Qed.
charguer's avatar
charguer committed
617

POTTIER Francois's avatar
POTTIER Francois committed
618
Lemma compare_poly_custom_spec : forall (A:Type),
charguer's avatar
charguer committed
619 620 621 622 623 624 625 626 627 628 629
  forall (x:compare_poly_type_ A) (y : compare_poly_type_ int),
  app compare_poly_custom [x y] \[] \[=tt].
Proof using.
  xcf.
  xapp. xpolymorphic_eq. intro_subst.
  xapp. xpolymorphic_eq. intro_subst.
  xapp. xpolymorphic_eq. intro_subst.
  xapp. xpolymorphic_eq. intro_subst.
  xrets~.
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
630
Lemma compare_physical_loc_func_spec :
charguer's avatar
charguer committed
631 632
  app compare_physical_loc_func [tt] \[] \[= tt].
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
633
  xcf. xapps. xapps.
charguer's avatar
charguer committed
634 635 636 637 638 639 640 641 642 643 644 645 646 647
  xapp. intro_subst.
  xapp. intro_subst.
  xfun.
  xapp_spec infix_eq_eq_gen_spec. intros.
  xlet (\[=1]).
    xif.
      xapps. xrets~.
      xrets~.
    intro_subst. xrets~.
Qed.

Fixpoint list_update (k:int) (v:int) (l:list (int*int)) :=
  match l with
  | nil => nil
POTTIER Francois's avatar
POTTIER Francois committed
648
  | (k2,v2)::t2 =>
charguer's avatar
charguer committed
649 650 651 652 653
     let t := (list_update k v t2) in
     let v' := (If k = k2 then v else v2) in
     (k2,v')::t
  end.

POTTIER Francois's avatar
POTTIER Francois committed
654
Lemma compare_physical_algebraic_spec :
charguer's avatar
charguer committed
655 656 657
  app compare_physical_algebraic [tt] \[] \[= (1,9)::(4,2)::(2,5)::nil ].
Proof using.
  xcf. xfun_ind (@list_sub (int*int)) (fun f =>
POTTIER Francois's avatar
POTTIER Francois committed
658
     forall (l:list (int*int)) (k:int) (v:int),
charguer's avatar
charguer committed
659
     app f [k v l] \[] \[= list_update k v l ]).
POTTIER Francois's avatar
POTTIER Francois committed
660
  { xmatch.
charguer's avatar
charguer committed
661
    { xrets~. }
charguer's avatar
charguer committed
662
    { xapps~. xrets. xif.
charguer's avatar
stable  
charguer committed
663
      { xrets. cases_if. auto. }
charguer's avatar
charguer committed
664 665 666 667
      { xapp_spec infix_emark_eq_gen_spec. intros M. xif.
        { xrets. case_if~. }
        { xrets. case_if~. rewrite~ M. } } } }
   { xapps. xsimpl. subst r. simpl. do 3 case_if. auto. }
POTTIER Francois's avatar
POTTIER Francois committed
668 669
Qed.

charguer's avatar
charguer committed
670 671


charguer's avatar
charguer committed
672 673 674 675 676
(********************************************************************)
(* ** Inlined total functions *)

Lemma inlined_fun_arith_spec :
  app inlined_fun_arith [tt] \[] \[= 3].
POTTIER Francois's avatar
POTTIER Francois committed
677
Proof using.
charguer's avatar
charguer committed
678 679 680
  xcf.
  xval.
  xlet.
POTTIER Francois's avatar
POTTIER Francois committed
681
  (* note: division by a possibly-null constant is not inlined *)
charguer's avatar
charguer committed
682 683 684 685 686 687 688 689 690 691 692 693
  xapp_skip.
  xrets.
  skip.
Qed.

Lemma inlined_fun_other_spec : forall (n:int),
  app inlined_fun_others [n] \[] \[= n+1].
Proof using.
  xcf. xret. xsimpl. simpl. auto.
Qed.


charguer's avatar
demo2  
charguer committed
694 695 696 697 698 699
(********************************************************************)
(* ** Type annotations *)

Lemma annot_let_spec :
  app annot_let [tt] \[] \[= 3].
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
700
  xcf_show.
charguer's avatar
demo2  
charguer committed
701 702 703 704 705 706
  xcf. xval. xrets~.
Qed.

Lemma annot_tuple_arg_spec :
  app annot_tuple_arg [tt] \[] \[= (3, @nil int)].
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
707
  xcf_show.
charguer's avatar
demo2  
charguer committed
708 709 710 711 712 713 714 715 716 717 718 719 720
  xcf. xrets~.
Qed.

Lemma annot_pattern_var_spec : forall (x:list int),
  app annot_pattern_var [x] \[] \[= If x = nil then 1 else 0].
Proof using.
  xcf_show.
  xcf. xmatch; xrets; case_if~.
Qed.

Lemma annot_pattern_constr_spec :
  app annot_pattern_constr [tt] \[] \[= 1].
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
721
  xcf_show.
charguer's avatar
demo2  
charguer committed
722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741
  xcf. xmatch; xrets~.
Qed.


(********************************************************************)
(* ** Polymorphic functions *)

Lemma top_fun_poly_id_spec : forall A (x:A),
  app top_fun_poly_id [x] \[] \[= x].  (* (fun r => \[r = x]). *)
Proof using.
  xcf. xrets~.
Qed.

Lemma top_fun_poly_proj1_spec : forall A B (x:A) (y:B),
  app top_fun_poly_proj1 [(x,y)] \[] \[= x].
Proof using.
  xcf. xmatch. xrets~.
Qed.

Lemma top_fun_poly_proj1' : forall A B (p:A*B),
POTTIER Francois's avatar
POTTIER Francois committed
742
  app top_fun_poly_proj1 [p] \[] \[= Datatypes.fst p].
charguer's avatar
demo2  
charguer committed
743 744 745 746 747 748
  (* TODO: maybe it's better if [fst] remains the one from Datatypes
     rather than the one from Pervasives? *)
Proof using.
  xcf. xmatch. xrets~.
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
749 750
Lemma top_fun_poly_pair_homogeneous_spec : forall A (x y : A),
  app top_fun_poly_pair_homogeneous [x y] \[] \[= (x,y)].
charguer's avatar
demo2  
charguer committed
751 752 753 754 755 756 757 758 759 760 761 762 763
Proof using.
  xcf. xrets~.
Qed.


(********************************************************************)
(* ** Polymorphic let bindings *)

Lemma let_poly_nil_spec : forall A,
  app let_poly_nil [tt] \[] \[= @nil A].
Proof using.
  xcf. dup 2.
  { xval. xrets. subst x. auto. }
POTTIER Francois's avatar
POTTIER Francois committed
764
  { xvals. xrets~. }
charguer's avatar
demo2  
charguer committed
765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786
Qed.

Lemma let_poly_nil_pair_spec : forall A B,
  app let_poly_nil_pair [tt] \[] \[= (@nil A, @nil B)].
Proof using.
  xcf. xvals. xrets~.
Qed.

Lemma let_poly_nil_pair_homogeneous_spec : forall A,
  app let_poly_nil_pair_homogeneous [tt] \[] \[= (@nil A, @nil A)].
Proof using.
  xcf. xvals. xrets~.
Qed.

Lemma let_poly_nil_pair_heterogeneous_spec : forall A,
  app let_poly_nil_pair_heterogeneous [tt] \[] \[= (@nil A, @nil int)].
Proof using.
  xcf. xvals. xrets~.
Qed.



charguer's avatar
demo3  
charguer committed
787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844
(********************************************************************)
(* ** Fatal Exceptions *)

Lemma exn_assert_false_spec : False ->
  app exn_assert_false [tt] \[] \[= tt].
Proof using.
  xcf. xfail. auto.
Qed.

Lemma exn_failwith_spec : False ->
  app exn_failwith [tt] \[] \[= tt].
Proof using.
  xcf. xfail. auto.
Qed.

Lemma exn_raise_spec : False ->
  app exn_raise [tt] \[] \[= tt].
Proof using.
  xcf. xfail. auto.
Qed.


(********************************************************************)
(* ** Assertions *)

Lemma assert_true_spec :
  app assert_true [tt] \[] \[= 3].
Proof using.
  dup 2.
  { xcf. xassert. { xrets~. } xrets~. }
  { xcf_go~. }
Qed.

Lemma assert_pos_spec : forall (x:int),
  x > 0 ->
  app assert_pos [x] \[] \[= 3].
Proof using.
  dup 2.
  { xcf. xassert. { xrets~. } xrets~. }
  { xcf_go~. }
Qed.

Lemma assert_same_spec : forall (x:int),
  app assert_same [x x] \[] \[= 3].
Proof using.
  dup 2.
  { xcf. xassert. { xrets~. } xrets~. }
  { xcf_go~. }
Qed.

Lemma assert_let_spec :
  app assert_let [tt] \[] \[= 3].
Proof using.
  dup 2.
  { xcf. xassert. { xvals. xrets~. } xrets~. }
  { xcf_go~. }
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
845
Lemma assert_seq_spec :
charguer's avatar
demo3  
charguer committed
846 847 848 849 850
  app assert_seq [tt] \[] \[= 1].
Proof using.
  xcf. xapp. xassert.
    xapp. xrets.
  (* assert cannot do visible side effects,
POTTIER Francois's avatar
POTTIER Francois committed
851
     otherwise the semantics could change with -noassert *)
charguer's avatar
demo3  
charguer committed
852 853
Abort.

POTTIER Francois's avatar
POTTIER Francois committed
854
Lemma assert_in_seq_spec :
charguer's avatar
demo3  
charguer committed
855 856
  app assert_in_seq [tt] \[] \[= 4].
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
857
  xcf. xlet. xassert. { xrets. } xrets.
charguer's avatar
toutbon  
charguer committed
858
  xpulls. xrets~.
charguer's avatar
demo3  
charguer committed
859 860 861 862 863 864
Qed.


(********************************************************************)
(* ** Conditionals *)

POTTIER Francois's avatar
POTTIER Francois committed
865
Lemma if_true_spec :
charguer's avatar
demo3  
charguer committed
866 867 868 869 870 871 872 873
  app if_true [tt] \[] \[= 1].
Proof using.
  xcf. xif. xret. xsimpl. auto.
Qed.

Lemma if_term_spec :
  app if_term [tt] \[] \[= 1].
Proof using.
charguer's avatar
toutbon  
charguer committed
874
  xcf. xfun. xapp. xret. xpulls.
charguer's avatar
demo3  
charguer committed
875 876 877
  xif. xrets~.
Qed.

POTTIER Francois's avatar
POTTIER Francois committed
878
Lemma if_else_if_spec :
charguer's avatar
demo3  
charguer committed
879 880 881 882 883 884 885 886 887 888
  app if_else_if [tt] \[] \[= 0].
Proof using.
  xcf. xfun (fun f => forall (x:int), app f [x] \[] \[= false]).
    { xrets~. }
  xapps. xif. xapps. xif. xrets~.
Qed.

Lemma if_then_no_else_spec : forall (b:bool),
  app if_then_no_else [b] \[] (fun x => \[ x >= 0]).
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
889
  xcf. xapp.
charguer's avatar
demo3  
charguer committed
890 891 892
  xseq. xif (Hexists n, \[n >= 0] \* r ~~> n).
   { xapp. xsimpl. math. }
   { xrets. math. }
charguer's avatar
toutbon  
charguer committed
893
   { (*xclean.*) xpull ;=>> P. xapp. xpulls. xsimpl. math. }
charguer's avatar
demo3  
charguer committed
894 895 896
Qed.


charguer's avatar
charguer committed
897 898


charguer's avatar
charguer committed
899
(********************************************************************)
charguer's avatar
charguer committed
900
(* ** Evaluation order *)
charguer's avatar
charguer committed
901

POTTIER Francois's avatar
POTTIER Francois committed
902 903
Lemma order_app_spec :
  app order_app [tt] \[] \[= 2].
charguer's avatar
charguer committed
904
Proof using.
POTTIER Francois's avatar
POTTIER Francois committed
905
  dup 2.
charguer's avatar
charguer committed
906 907 908 909
    {
    xcf. xapps. xfun. xfun. xfun.
    xapps. { xapps. xrets~. } xpulls.
    xapps. { xassert. xapps. xrets~. xapps. xrets~. } xpulls.
POTTIER Francois's avatar
POTTIER Francois committed
910
    xapps. { xassert. xapps. xrets~. xfun.
charguer's avatar
charguer committed
911
      xrets~ (fun f => \[AppCurried f [a b] := (Ret (a + b)%I)] \* r ~~> 2). eauto. }
POTTIER Francois's avatar
POTTIER Francois committed
912
      xpull ;=> Hf.
charguer's avatar
charguer committed
913
    xapp. xrets~.
POTTIER Francois's avatar
POTTIER Francois committed
914
     (* TODO: can we make xret guess the post?
charguer's avatar
charguer committed
915 916 917 918 919 920
        The idea is to have [(Ret f) H ?Q] where [f:func] and [f] has a spec in hyps
        to instantiate Q with [fun f => H \* \[spec of f]].
        Then, the proof should just be [xgo~]. *)
  }
  { xcf_go*. skip. (* TODO *) }
Qed.
charguer's avatar
charguer committed
921

POTTIER Francois's avatar
POTTIER Francois committed
922 923
Lemma order_constr_spec :
  app order_constr [tt] \[] \[= 1::1::nil].
charguer's avatar
charguer committed
924 925 926 927 928 929 930 931 932
Proof using.
  xcf_go*.
Qed.
  (* Details:
  xcf. xapps. xfun. xfun.
  xapps. { xapps. xrets~. } xpulls.
  xapps. { xassert. xapps. xrets~. xrets~. } xpulls.
  xrets~.
  *)
charguer's avatar
charguer committed
933 934


POTTIER Francois's avatar
POTTIER Francois committed
935 936
Lemma order_list_spec :
  app order_list [tt] \[] \[= 1::1::nil].
charguer's avatar
charguer committed
937
Proof using. xcf_go*. Qed.
POTTIER Francois's avatar
POTTIER Francois committed
938 939 940

Lemma order_tuple_spec :
  app order_tuple [tt] \[] \[= (1,1)].
charguer's avatar
charguer committed
941
Proof using. xcf_go*. Qed.
charguer's avatar
charguer committed
942

charguer's avatar
charguer committed
943 944
(* TODO:
let order_array () =
charguer's avatar
charguer committed
945

charguer's avatar
charguer committed
946 947 948 949 950 951
let order_record () =
  let r = ref 0 in
  let g () = incr r; [] in
  let f () = assert (!r = 1); 1 in
  { nb = f(); items = g() }
*)
charguer's avatar
charguer committed
952 953 954 955




charguer's avatar
charguer committed
956 957
(********************************************************************)
(* ** While loops *)
charguer's avatar
charguer committed
958

charguer's avatar
charguer committed
959

POTTIER Francois's avatar
POTTIER Francois committed
960
Lemma while_decr_spec :
charguer's avatar
charguer committed
961 962 963
  app while_decr [tt] \[] \[= 3].
Proof using.
  xcf. xapps. xapps. dup 9.
POTTIER Francois's avatar
POTTIER Francois committed
964
  { xwhile. intros R LR HR.
charguer's avatar
charguer committed
965 966 967
    cuts PR: (forall k, k >= 0 ->
      R (n ~~> k \* c ~~> (3-k)) (# n ~~> 0 \* c ~~> 3)).
    { xapplys PR. math. }
POTTIER Francois's avatar
POTTIER Francois committed
968 969
    intros k. induction_wf IH: (downto 0) k; intros Hk.
    applys (rm HR). xlet.
charguer's avatar
charguer committed
970
    { xapps. xrets. }
POTTIER Francois's avatar
POTTIER Francois committed
971 972 973
    { xpulls. xif.
      { xseq. xapps. xapps. simpl. xapplys IH. math. math. math. }
      { xrets. math. math. } }
charguer's avatar
charguer committed
974 975 976
    xapps. xsimpl~. }
  { xwhile as R. skip. skip. }
  { xwhile_inv (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
POTTIER Francois's avatar
POTTIER Francois committed
977
                         \* n ~~> k \* c ~~> (3-k)) (downto 0).
charguer's avatar
charguer committed
978
    { xsimpl*. math. }
POTTIER Francois's avatar
POTTIER Francois committed
979
    { intros S LS b k FS. xpull. intros. xlet.
charguer's avatar
charguer committed
980
      { xapps. xrets. }
POTTIER Francois's avatar
POTTIER Francois committed
981
      { xpulls. xif.
charguer's avatar
charguer committed
982
        { xseq. xapps. xapps. simpl. xapplys FS.
charguer's avatar
charguer committed
983
            hnf. math. math. eauto. math. eauto. eauto. }
charguer's avatar
charguer committed
984
        { xret. xsimpl. math. math. } } }
charguer's avatar
charguer committed
985
    { intros. xapps. xsimpl. math. } }
charguer's avatar
charguer committed
986 987 988
  { xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
                         \* n ~~> k \* c ~~> (3-k)) (downto 0).
    { xsimpl*. math. }
charguer's avatar
toutbon  
charguer committed
989
    { intros b k. xpull ;=> Hk Hb. xapps. xrets. xauto*. math. }
POTTIER Francois's avatar
POTTIER Francois committed
990
    { intros k. xpull ;=> Hk Hb. xapps. xapps. xsimpl. math. eauto. math. math. }
charguer's avatar
charguer committed
991
    { => k Hk Hb. xapp. xsimpl. math. } }
charguer's avatar
charguer committed
992 993 994 995 996
  { (* using a measure [fun k => abs k] *)
    xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
                         \* n ~~> k \* c ~~> (3-k)) (abs).
    skip. skip. skip. skip. }
  { (* defining the measure externally *)
POTTIER Francois's avatar
POTTIER Francois committed
997
    xwhile_inv_basic_measure (fun b m => Hexists k,
charguer's avatar
charguer committed
998 999 1000 1001
         \[m = k] \* \[k >= 0] \* \[b = isTrue (k > 0)]
                         \* n ~~> k \* c ~~> (3-k)).
    skip. skip. skip. skip. }
  { (* defining the measure externally, downwards *)
POTTIER Francois's avatar
POTTIER Francois committed
1002
    xwhile_inv_basic_measure (fun b m => Hexists i,
charguer's avatar
charguer committed
1003 1004 1005 1006
         \[m = 3-i] \* \[i <= 3] \* \[b = isTrue (i <= 3)]
                    \* n ~~> (3-i) \* c ~~> i).
    skip. skip. skip. skip. }
  { xwhile_inv_skip (fun b => Hexists k, \[k >= 0] \* \[b = isTrue (k > 0)]
POTTIER Francois's avatar
POTTIER Francois committed
1007
                         \* n ~~> k \* c ~~> (3-k)).
charguer's avatar
charguer committed
1008 1009
    skip. skip. skip. }
  { xwhile_inv_basic_skip (fun b => Hexists k, \[k >= 0] \* \[b = isTrue (k > 0)]
POTTIER Francois's avatar
POTTIER Francois committed
1010
                         \* n ~~> k \* c ~~> (3-k)).