Demo_proof.v 17.4 KB
Newer Older
charguer's avatar
charguer committed
1
Set Implicit Arguments.
charguer's avatar
charguer committed
2
(* LibInt LibWf *)
charguer's avatar
charguer committed
3
Require Import CFLib.
charguer's avatar
charguer committed
4
Require Import Demo_ml.
charguer's avatar
ok    
charguer committed
5

charguer's avatar
charguer committed
6
Require Import Pervasives_ml. (* optional, improves display of, e.g. [incr] *)
charguer's avatar
charguer committed
7

charguer's avatar
charguer committed
8
(*Open Scope tag_scope.*)
charguer's avatar
charguer committed
9

charguer's avatar
xpat    
charguer committed
10
11
12



charguer's avatar
cp    
charguer committed
13
14
15
16
17
18
19
20








charguer's avatar
charguer committed
21
22
23
24
25
Lemma if_true_spec : 
  app if_true [tt] \[] \[= 1].
Proof using.
  xcf. xif. xret. xsimpl. auto.
Qed.
charguer's avatar
polylet    
charguer committed
26

charguer's avatar
charguer committed
27
28
29
30
31
32
Lemma if_term_spec :
  app if_term [tt] \[] \[= 1].
Proof using.
  xcf. xfun. xapp. xret. xextracts.
  xif. xrets~.
Qed.
charguer's avatar
charguer committed
33

charguer's avatar
charguer committed
34
35
36
37
38
39
Lemma if_else_if_spec : 
  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~.
charguer's avatar
charguer committed
40
41
42
Qed.


charguer's avatar
charguer committed
43
44
Definition Ref a (v:a) (l:loc) :=  (* TODO: change *)
  heap_is_single l v.
charguer's avatar
charguer committed
45

charguer's avatar
charguer committed
46
47
Notation "l '~~>' v" := (hdata (Ref v) l)
  (at level 32, no associativity) : heap_scope.
charguer's avatar
charguer committed
48

charguer's avatar
charguer committed
49
50
51
Notation "'app_keep' f xs H Q" :=
  (app f xs H%h (Q \*+ H))
  (at level 80, f at level 0, xs at level 0, H at level 0) : charac.
charguer's avatar
charguer committed
52
53
54



charguer's avatar
charguer committed
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
Parameter ref_spec : forall a (v:a),
  app ref [v] \[] (fun l => l ~~> v).

Parameter get_spec : forall a (v:a) l,
  app_keep get [l] (l ~~> v) \[= v].
(* Print get_spec. *)
(* keep (app get [l]) (l ~~> v) \[= v].*)

Parameter set_spec : forall a (v w:a) l,
  app set [l w] (l ~~> v) (# l ~~> w).

Parameter incr_spec : forall (n:int) l,
  app incr [l] (l ~~> n) (# l ~~> (n+1)).

Parameter decr_spec : forall (n:int) l,
  app decr [l] (l ~~> n) (# l ~~> (n+1)).


Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
Hint Extern 1 (RegisterSpec get) => Provide get_spec.
Hint Extern 1 (RegisterSpec set) => Provide set_spec.
Hint Extern 1 (RegisterSpec incr) => Provide incr_spec.
Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.





Notation "`! l" := (App infix_emark_ l;)
  (at level 69, no associativity, format "`! l") : machine_op_scope.


Lemma if_then_no_else_spec : forall (b:bool),
  app if_then_no_else [b] \[] \[= 1].
charguer's avatar
charguer committed
89
Proof using.
charguer's avatar
charguer committed
90
91
92
93
94
  xcf. xapp. dup 3.
  { xseq. xif. { xapp. } { xrets. skip. (* stuck *) } skip. } 
  { xseq....

  (* TODO: raise error message on xif *)
charguer's avatar
charguer committed
95
96
Qed.

charguer's avatar
charguer committed
97
98


charguer's avatar
xpat    
charguer committed
99
100
101
102
103
(********************************************************************)
(********************************************************************)
(********************************************************************)


charguer's avatar
charguer committed
104
105
(********************************************************************)
(* ** Top-level values *)
charguer's avatar
ok    
charguer committed
106

charguer's avatar
charguer committed
107
108
109
110
111
112
113
114
115
116
117
Lemma top_val_int_spec :
  top_val_int = 5.
Proof using.
  dup 5.
  xcf. auto.
  (* demos: *)
  xcf_show. skip.
  xcf_show top_val_int. skip. 
  xcf. skip.
  xcf top_val_int. skip.
Qed.
charguer's avatar
ok    
charguer committed
118

charguer's avatar
charguer committed
119
120
121
122
123
Lemma top_val_int_list_spec : 
  top_val_int_list = @nil int.
Proof using.
  xcf. auto.
Qed.
charguer's avatar
ok    
charguer committed
124

charguer's avatar
charguer committed
125
126
127
Lemma top_val_poly_list_spec : forall A,
  top_val_poly_list = @nil A.
Proof using. xcf*. Qed.
charguer's avatar
init  
charguer committed
128

charguer's avatar
charguer committed
129
130
131
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
132

charguer's avatar
init  
charguer committed
133

charguer's avatar
xpat    
charguer committed
134

charguer's avatar
charguer committed
135
(********************************************************************)
charguer's avatar
xpat    
charguer committed
136
(* ** Return *)
charguer's avatar
init  
charguer committed
137

charguer's avatar
xpat    
charguer committed
138
139
Lemma ret_unit_spec : 
  app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
charguer's avatar
charguer committed
140
Proof using.
charguer's avatar
xpat    
charguer committed
141
142
143
144
145
146
147
  xcf. dup 5.
  xret. xsimpl. auto.
  (* demos *)
  xrets. auto.
  xrets*.
  xret_no_gc. xsimpl. auto.
  xret_no_clean. xsimpl*. 
charguer's avatar
charguer committed
148
Qed.
charguer's avatar
ok    
charguer committed
149

charguer's avatar
xpat    
charguer committed
150
151
152
Lemma ret_int_spec : 
  app ret_int [tt] \[] \[= 3].
Proof using. xcf. xrets*. Qed.
charguer's avatar
ok    
charguer committed
153

charguer's avatar
xpat    
charguer committed
154
155
156
Lemma ret_int_pair_spec :
  app ret_int_pair [tt] \[] \[= (3,4)].
Proof using. xcf. xrets*. Qed.
charguer's avatar
ok    
charguer committed
157

charguer's avatar
xpat    
charguer committed
158
159
160
Lemma ret_poly_spec : forall A,
  app ret_poly [tt] \[] \[= @nil A].
Proof using. xcf. xrets*. Qed.
charguer's avatar
ok    
charguer committed
161
162


charguer's avatar
xlet    
charguer committed
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
(********************************************************************)
(* ** 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'.

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.
  dup 3. 
  { xapp3_no_apply. apply S. }
  { xapp3_no_simpl. }
  { xapp3. }
  dup 4.
  { xseq. xapp. xapp. xsimpl~. }
  { xapp. intro_subst. xapp. xsimpl~. }
  { xapps. xapps. xsimpl~. }
  { xapps. xapps~. }
Qed.


charguer's avatar
ok    
charguer committed
191

charguer's avatar
charguer committed
192
(********************************************************************)
charguer's avatar
xpat    
charguer committed
193
(* ** Let-value *)
charguer's avatar
init  
charguer committed
194

charguer's avatar
xpat    
charguer committed
195
196
Lemma let_val_int_spec : 
  app let_val_int [tt] \[] \[= 3].
charguer's avatar
charguer committed
197
Proof using.
charguer's avatar
xpat    
charguer committed
198
199
200
201
202
203
204
205
206
  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
207
208
Qed.

charguer's avatar
xpat    
charguer committed
209
210
211
212
213
214
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
215
Proof using.
charguer's avatar
xpat    
charguer committed
216
217
218
219
  xcf. dup 3.
  xval. xret. xsimpl. auto.
  xval as r. xrets~.
  xvals. xrets~.
charguer's avatar
charguer committed
220
Qed.
charguer's avatar
init  
charguer committed
221
222


charguer's avatar
xlet    
charguer committed
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
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
(********************************************************************)
(* ** Let-function *)

Lemma let_fun_const_spec : 
  app let_fun_const [tt] \[] \[= 3].
Proof using.
  xcf. dup 9.
  { xfun. apply Sf. xrets~. }
  { xfun as g. apply Sg. skip. }
  { xfun as g G. apply G. skip. }
  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]).
    { apply Sf. skip. } 
    { apply Sf. } }
  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h.
    { apply Sh. skip. } 
    { apply Sh. } }
  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h H.
    { apply H. skip. } 
    { apply H. } }
  { xfun (fun g => app g [tt] \[] \[=3]).
    { xrets~. } 
    { apply Sf. } }
  { xfun (fun g => app g [tt] \[] \[=3]) as h.
    { skip. } 
    { skip. } }
  { xfun (fun g => app g [tt] \[] \[=3]) as h H.
    { skip. } 
    { 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.
    dup 5. 
    { apply Spec. xret. }
    { xapp3_no_apply. Focus 2. apply S. xret. }
    { xapp3_no_simpl. xret. }
    { xapp3. xret. }
    { xapp. xret. xsimpl~. }
    xsimpl~.
Qed.

Lemma let_fun_poly_pair_homogeneous_spec : 
  app let_fun_poly_pair_homogeneous [tt] \[] \[= (3,3)].
Proof using.
  xcf. 
  xfun.
  xapp. 
  xret.
  xsimpl~.
Qed.

Lemma let_fun_on_the_fly_spec :
  app let_fun_on_the_fly [tt] \[] \[= 4].
Proof using.
  xcf.
  xfun.
  xfun.
  xapp. 
  xapp.
  xret.
  xsimpl~.
Qed.


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

Lemma let_term_nested_id_calls_spec :
  app let_term_nested_id_calls [tt] \[] \[= 2].
Proof using.
  xcf.
  xfun (fun f => forall (x:int), app f [x] \[] \[= x]). { xret~. }
  xapps. 
  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.
  xcf. 
  xfun (fun f => forall A B (x:A) (y:B), app f [x y] \[] \[= (x,y)]). { xret~. }
  xapps.
  xapps.
  xapps.
  xapps.
  xrets~.
Qed.

charguer's avatar
charguer committed
318
(********************************************************************)
charguer's avatar
xpat    
charguer committed
319
(* ** Pattern-matching *)
charguer's avatar
init  
charguer committed
320

charguer's avatar
xpat    
charguer committed
321
322
323
324
325
326
327
Lemma match_pair_as_spec : 
  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. }
charguer's avatar
charguer committed
328
329
330
331
  { xmatch_no_cases. dup 6. 
    { xmatch_case.
      { xrets~. } 
      { xmatch_case. } }
charguer's avatar
xpat    
charguer committed
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
    { xcase_no_simpl.
      { dup 3.
        { xalias. xalias. xret. xsimpl. xauto*. }
        { xalias as u U. 
          xalias as v. skip. }
        { xalias_subst. xalias_subst. skip. } }
      { xdone. } } 
    { xcase_no_simpl as E. skip. skip. }
    { xcase_no_intros. intros x y E. skip. intros F. skip. }
    { xcase. skip. skip. }
    { xcase as C. skip. skip. 
      (* note: inversion got rid of C *) 
    } }
  { xmatch_no_simpl_no_alias. skip. }
  { xmatch_no_simpl_subst_alias. skip. }
charguer's avatar
charguer committed
347
  { xmatch_no_intros. skip. }
charguer's avatar
xpat    
charguer committed
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
  { xmatch_no_simpl. inverts C. skip. } 
Qed.

Lemma match_nested_spec : 
  app match_nested [tt] \[] \[= (2,2)::nil].
Proof using.
  xcf. xval. dup 3.
  { xmatch_no_simpl.  
    { xrets~. } 
    { false. (* note: [xrets] would produce a ununified [hprop]. 
     caused by [tryfalse] in [hextract_cleanup]. TODO: avoid this. *) } }
  { xmatch.
    xrets~. 
    (* second case is killed by [xcase_post] *) }
  { xmatch_no_intros. skip. skip. }
charguer's avatar
charguer committed
363
Qed.
charguer's avatar
init  
charguer committed
364

charguer's avatar
demo    
charguer committed
365

charguer's avatar
charguer committed
366
367
368
369
370
371
372
373
374
375
376
377
(********************************************************************)
(* ** Let-pattern *)

Lemma let_pattern_pair_int_spec : 
  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
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
(********************************************************************)
(* ** Infix functions *)
 
Lemma infix_plus_plus_plus__spec : forall x y,
  app infix_plus_plus_plus_ [x y] \[] \[= x + y].
Proof using.
  xcf. xrets~.
Qed.

Hint Extern 1 (RegisterSpec infix_plus_plus_plus_) => Provide infix_plus_plus_plus__spec.

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.

Lemma infix_minus_minus_minus__spec : forall x y,
  app infix_minus_minus_minus_ [x y] \[] \[= x + y].
Proof using.
  intros. xcf_show as S. rewrite S. xapps~.
Qed.
charguer's avatar
charguer committed
402
403


charguer's avatar
charguer committed
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
(********************************************************************)
(* ** Inlined total functions *)

Lemma inlined_fun_arith_spec :
  app inlined_fun_arith [tt] \[] \[= 3].
Proof using.  
  xcf.
  xval.
  xlet.
  (* note: division by a possibly-null constant is not inlined *) 
  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
init  
charguer committed
427

charguer's avatar
charguer committed
428
(********************************************************************)
charguer's avatar
xpat    
charguer committed
429
430
(********************************************************************)
(********************************************************************)
charguer's avatar
init  
charguer committed
431

charguer's avatar
xpat    
charguer committed
432
(*
charguer's avatar
init  
charguer committed
433
434


charguer's avatar
charguer committed
435
436
(********************************************************************)
(* ** Partial applications *)
charguer's avatar
init  
charguer committed
437

charguer's avatar
charguer committed
438
439
440
441
442
443
Lemma app_partial_2_1 () =
   let f x y = (x,y) in
   f 3
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
444

charguer's avatar
charguer committed
445
446
447
448
449
450
Lemma app_partial_3_2 () =
   let f x y z = (x,z) in
   f 2 4
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
451

charguer's avatar
charguer committed
452
453
454
455
456
457
Lemma app_partial_add () =
  let add x y = x + y in
  let g = add 1 in g 2
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
458

charguer's avatar
charguer committed
459
460
461
462
463
464
465
Lemma app_partial_appto () =
  let appto x f = f x in
  let _r = appto 3 ((+) 1) in
  appto 3 (fun x -> x + 1)
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
466

charguer's avatar
charguer committed
467
468
469
470
471
472
473
474
475
Lemma test_partial_app_arities () =
   let func4 a b c d = a + b + c + d in
   let f1 = func4 1 in
   let f2 = func4 1 2 in
   let f3 = func4 1 2 3 in
   f1 2 3 4 + f2 3 4 + f3 4
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
476

charguer's avatar
charguer committed
477
478
479
480
481
Lemma app_partial_builtin () =
  let f = (+) 1 in
  f 2
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
482
483
484
Qed.


charguer's avatar
cp    
charguer committed
485
486
487
488
489
490
491
let app_partial_builtin_and () =
  let f = (&&) true in
  f false




charguer's avatar
charguer committed
492
493
494
495
496
497
498
499
(********************************************************************)
(* ** Over applications *)

Lemma app_over_id () =
   let f x = x in
   f f 3
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
500
501
502
503
Qed.



charguer's avatar
charguer committed
504
505
506
507
508
509
510
511
512
513

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



Lemma top_fun_poly_id : forall A (x:A),
  app top_fun_poly_id [x] \[] \[= x].  (* (fun r => \[r = x]). *)
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
514
515
Qed.

charguer's avatar
charguer committed
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
Lemma top_fun_poly_proj1 : forall A B (x:A) (y:B),
  app top_fun_poly_proj1 [(x,y)] \[] \[= x]
Proof using.
  xcf.
Qed.

Lemma top_fun_poly_proj1' : forall A B (p:A*B),
  app top_fun_poly_proj1 [p] \[] \[= fst x]. (* (fun r => \[r = fst x]).  *)
Proof using.
  xcf.
Qed.

Lemma top_fun_poly_pair_homogeneous : forall A (x y : A), 
  app top_fun_poly_pair_homogeneous [x y] \[] \[= (x,y)]. 
Proof using.
  xcf.
Qed.


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

Lemma let_poly_nil () = 
  let x = [] in x
Proof using.
  xcf.
Qed.

Lemma let_poly_nil_pair () = 
  let x = ([], []) in x
Proof using.
  xcf.
Qed.

Lemma let_poly_nil_pair_homogeneous () =
  let x : ('a list * 'a list) = ([], []) in x
Proof using.
  xcf.
Qed.

Lemma let_poly_nil_pair_heterogeneous () =
  let x : ('a list * int list) = ([], []) in x
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
561

charguer's avatar
charguer committed
562

charguer's avatar
demo    
charguer committed
563
*)
charguer's avatar
charguer committed
564

charguer's avatar
charguer committed
565
566
567
568
569
570
571

(********************************************************************)
(********************************************************************)
(********************************************************************)
(* TODO: xgc demo *)


charguer's avatar
charguer committed
572
573
574
(********************************************************************)
(********************************************************************)
(********************************************************************)
charguer's avatar
init  
charguer committed
575
576
(*

charguer's avatar
charguer committed
577
578
579

(********************************************************************)
(* ** Fatal Exceptions *)
charguer's avatar
init  
charguer committed
580

charguer's avatar
charguer committed
581
582
583
584
585
586
587
588
589
590
Lemma exn_assert_false () =
   assert false
Proof using.
  xcf.
Qed.

Lemma exn_failwith () =
   failwith "ok"
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
591
592
Qed.

charguer's avatar
charguer committed
593
exception My_exn 
charguer's avatar
init  
charguer committed
594

charguer's avatar
charguer committed
595
596
597
598
Lemma exn_raise () =
   raise My_exn
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
599
600
601
Qed.


charguer's avatar
charguer committed
602
603
(********************************************************************)
(* ** Assertions *)
charguer's avatar
init  
charguer committed
604

charguer's avatar
charguer committed
605
606
607
608
609
Lemma assert_true () =
  assert true; 3
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
610

charguer's avatar
charguer committed
611
612
613
614
615
Lemma assert_pos x =
  assert (x > 0); 3
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
616

charguer's avatar
charguer committed
617
618
619
620
621
Lemma assert_same (x:int) (y:int) =
  assert (x = y); 3
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
622
623
624



charguer's avatar
charguer committed
625
626
(********************************************************************)
(* ** Conditionals *)
charguer's avatar
init  
charguer committed
627
628
629



charguer's avatar
charguer committed
630
631
632
633
634
635
636
637
638
639
640
(********************************************************************)
(* ** Records *)

type 'a sitems = {
  mutable nb : int;
  mutable items : 'a list; }

Lemma sitems_build n =
  { nb = n; items = [] }
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
641
642
Qed.

charguer's avatar
charguer committed
643
644
645
646
647
Lemma sitems_get_nb r =
  r.nb
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
648

charguer's avatar
charguer committed
649
650
651
652
653
Lemma sitems_incr_nb r =
  r.nb <- r.nb + 1 
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
654

charguer's avatar
charguer committed
655
656
657
658
659
Lemma sitems_length_items r =
  List.length r.items
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
660

charguer's avatar
charguer committed
661
662
663
664
665
Lemma sitems_push x r =
  r.nb <- r.nb + 1;
  r.items <- x :: r.items
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
666
667
668
Qed.


charguer's avatar
charguer committed
669
670
(********************************************************************)
(* ** Arrays *)
charguer's avatar
init  
charguer committed
671

charguer's avatar
charguer committed
672
673
674
675
676
677
678
679
Lemma array_ops () =
  let t = Array.make 3 0 in
  let _x = t.(1) in
  t.(2) <- 4;
  let _y = t.(2) in
  let _z = t.(1) in
  Array.length t
Proof using.
charguer's avatar
init  
charguer committed
680
681
682
683
  xcf.
Qed.


charguer's avatar
charguer committed
684
685
(********************************************************************)
(* ** While loops *)
charguer's avatar
init  
charguer committed
686

charguer's avatar
charguer committed
687
688
689
690
691
692
693
694
695
Lemma while_decr () =
   let n = ref 3 in
   let c = ref 0 in
   while !n > 0 do 
      incr c;
      decr n;
   done;
   !c
Proof using.
charguer's avatar
init  
charguer committed
696
697
698
  xcf.
Qed.

charguer's avatar
charguer committed
699
700
701
702
703
Lemma while_false () =
   while false do () done
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
704
705


charguer's avatar
charguer committed
706
707
708
709
710
711
712
713
714
(********************************************************************)
(* ** For loops *)

Lemma for_incr () =
   let n = ref 0 in
   for i = 1 to 10 do
      incr n;
   done;
   !n
charguer's avatar
init  
charguer committed
715

charguer's avatar
charguer committed
716
717
718
719
(* "for .. down to" not yet supported *)
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
720
721


charguer's avatar
charguer committed
722
723
(********************************************************************)
(* ** Recursive function *)
charguer's avatar
init  
charguer committed
724

charguer's avatar
charguer committed
725
726
727
728
729
730
731
Lemma rec rec_partial_half x =
  if x = 0 then 0
  else if x = 1 then assert false
  else 1 + rec_partial_half(x-2)
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
732
733
734



charguer's avatar
cp    
charguer committed
735
736
737
738
let rec rec_mutual_f x =
  if x <= 0 then x else 1 + rec_mutual_g (x-2)
and rec rec_mutual g x =
  rec_mutual_f (x+1)
charguer's avatar
init  
charguer committed
739
740
741
*)


charguer's avatar
cp    
charguer committed
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
(********************************************************************)
(* ** Lazy binary operators 

let lazyop_val () =
  if true && (false || true) then 1 else 0

let lazyop_term () =
  let f x = (x = 0) in
  if f 1 || f 0 then 1 else 0

let lazyop_mixed () =
  let f x = (x = 0) in
  if true && (f 1 || (f 0 && true)) then 1 else 0

*)

charguer's avatar
init  
charguer committed
758

charguer's avatar
charguer committed
759
(* TODO: include demo of  xpost (fun r =>\[r = 3]). *)
charguer's avatar
init  
charguer committed
760
761


charguer's avatar
cp    
charguer committed
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
(********************************************************************)
(* ** Evaluation order 

let order_app () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  g() + f()

let order_constr () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  (g() :: f() :: nil)

let order_array () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  [| g() ; f() |]

let order_list () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  [ g() ; f() ]

let order_tuple () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  (g(), f())

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
init  
charguer committed
802
803


charguer's avatar
charguer committed
804
805
806
807
(*************************************************************************)
(*************************************************************************)
(*************************************************************************)
(** * Polymorphic let demos
charguer's avatar
init  
charguer committed
808
809


charguer's avatar
charguer committed
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
845
846
847
848
849
850
851
852
853
854
855
856
(** Demo top-level polymorphic let. *)

Lemma poly_top_spec : forall A,
  poly_top = @nil A.
Proof using. xcf. Qed.

(** Demo local polymorphic let. *)

Lemma poly_let_1_spec : forall A,
  Spec poly_let_1 () |B>>
    B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval. subst. xrets. auto. Qed.  

(** Demo [xval_st P] *)

Lemma poly_let_1_spec' : forall A,
  Spec poly_let_1 () |B>>
    B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval_st (fun a => a = @nil). extens~. xrets. subst~. Qed.

(** Demo [xval_st P as x Hx] *)

Lemma poly_let_1_spec'' : forall A,
  Spec poly_let_1 () |B>>
    B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval_st (fun a => a = @nil) as p Hp. extens~. xrets. subst~. Qed.

(** Demo for partially-polymorphic values. *)

Lemma poly_let_2_spec : forall A1 A2,
  Spec poly_let_2 () |B>>
    B \[] (fun '(x,y) : list A1 * list A2 => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xvals. xrets. auto. Qed.

Lemma poly_let_2_same_spec : forall A,
  Spec poly_let_2_same () |B>>
    B \[] (fun '(x,y) : list A * list A => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xvals. xrets. auto. Qed.

Lemma poly_let_2_partial_spec : forall A,
  Spec poly_let_2_partial () |B>>
    B \[] (fun '(x,y) : list A * list int => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xval as p Hp. subst p. xrets. auto. Qed.
 *)