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

charguer's avatar
charguer committed
6 7


charguer's avatar
xpat  
charguer committed
8 9 10 11
Open Scope tag_scope.



charguer's avatar
charguer committed
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33


Ltac xapp3_common args cont :=
  let Sf := get_last_hyp tt in
  let K := xapp_instantiate Sf args in 
  forwards_nounfold_then K cont.

Ltac xapp3_core args ::=
  let Sfi := fresh "S" in 
  xapp3_common args ltac:(fun R => 
    generalize R; intros Sfi).

Ltac xapp4_core args ::=
  xapp3_common args ltac:(fun R => 
    xapply_core R ltac:(fun _ => idtac) ltac:(fun _ => idtac)).

Ltac xapp5_core args ::=
  xapp3_common args ltac:(fun R => 
    xapply_core R ltac:(fun _ => hsimpl) ltac:(fun _ => try xok)).



charguer's avatar
charguer committed
34 35
(********************************************************************)
(* ** Let-function *)
charguer's avatar
xpat  
charguer committed
36 37


charguer's avatar
charguer committed
38 39 40
Lemma let_fun_poly_id_spec :
  app let_fun_poly_id [tt] \[] \[= 3].
Proof using.
charguer's avatar
charguer committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
  xcf. xfun.
  xapp1.
  xapp2.
  dup 3. 
  { xapp3. Focus 2. apply S. xret. }
  { xapp3. Focus 2. xapply S. 
(* TODO . xsimpl. xsimpl. 

apply S. xret. }

  { xapp4.  

let args := constr:(>>) in
  let Sf := get_last_hyp tt in
  let Sfi := fresh "SpecI" in
  let K := xapp_instantiate Sf args in 
  pose K.
forwards R: K.

  xapp3.
*)
charguer's avatar
charguer committed
62
Qed.
charguer's avatar
xpat  
charguer committed
63

charguer's avatar
charguer committed
64 65 66
Lemma let_fun_poly_pair_homogeneous () =
  let f (x:'a) (y:'a) = (x,y) in
  f 3 3
charguer's avatar
charguer committed
67
Proof using.
charguer's avatar
xpat  
charguer committed
68
  xcf.
charguer's avatar
charguer committed
69
Qed.
charguer's avatar
polylet  
charguer committed
70

charguer's avatar
charguer committed
71 72
Lemma let_fun_on_the_fly () =
  (fun x f -> f x) 3 (fun x -> x+1) 
charguer's avatar
xpat  
charguer committed
73 74 75
Proof using.
  xcf.
Qed.
charguer's avatar
polylet  
charguer committed
76 77


charguer's avatar
charguer committed
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
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.




charguer's avatar
charguer committed
108

charguer's avatar
xpat  
charguer committed
109 110
(********************************************************************)
(* ** Let-term *)
charguer's avatar
charguer committed
111

charguer's avatar
xpat  
charguer committed
112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
Lemma let_term_nested_id_calls () =
   let f x = x in
   let a = f (f (f 2)) in
   a
Proof using.
  xcf.
Qed.

Lemma let_term_nested_pairs_calls () =
   let f x y = (x,y) in
   let a = f (f 1 2) (f 3 (f 4 5)) in
   a
Proof using.
  xcf.
Qed.
charguer's avatar
polylet  
charguer committed
127 128


charguer's avatar
xpat  
charguer committed
129 130 131 132 133 134 135







charguer's avatar
charguer committed
136
(********************************************************************)
charguer's avatar
xpat  
charguer committed
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
(* ** Sequence *)


Axiom ret_unit_spec : 
  app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Proof using.


Lemma seq_noop_spec :
  app seq_noop [tt] \[] \[= tt].
Proof using.
  xcf. 
  xfun.
  xret.


Qed.

charguer's avatar
polylet  
charguer committed
155 156 157



charguer's avatar
xpat  
charguer committed
158 159 160 161 162
(********************************************************************)
(********************************************************************)
(********************************************************************)


charguer's avatar
charguer committed
163 164
(********************************************************************)
(* ** Top-level values *)
charguer's avatar
ok  
charguer committed
165

charguer's avatar
charguer committed
166 167 168 169 170 171 172 173 174 175 176
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
177

charguer's avatar
charguer committed
178 179 180 181 182
Lemma top_val_int_list_spec : 
  top_val_int_list = @nil int.
Proof using.
  xcf. auto.
Qed.
charguer's avatar
ok  
charguer committed
183

charguer's avatar
charguer committed
184 185 186
Lemma top_val_poly_list_spec : forall A,
  top_val_poly_list = @nil A.
Proof using. xcf*. Qed.
charguer's avatar
init  
charguer committed
187

charguer's avatar
charguer committed
188 189 190
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
191

charguer's avatar
init  
charguer committed
192

charguer's avatar
xpat  
charguer committed
193

charguer's avatar
charguer committed
194
(********************************************************************)
charguer's avatar
xpat  
charguer committed
195
(* ** Return *)
charguer's avatar
init  
charguer committed
196

charguer's avatar
xpat  
charguer committed
197 198
Lemma ret_unit_spec : 
  app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
charguer's avatar
charguer committed
199
Proof using.
charguer's avatar
xpat  
charguer committed
200 201 202 203 204 205 206
  xcf. dup 5.
  xret. xsimpl. auto.
  (* demos *)
  xrets. auto.
  xrets*.
  xret_no_gc. xsimpl. auto.
  xret_no_clean. xsimpl*. 
charguer's avatar
charguer committed
207
Qed.
charguer's avatar
ok  
charguer committed
208

charguer's avatar
xpat  
charguer committed
209 210 211
Lemma ret_int_spec : 
  app ret_int [tt] \[] \[= 3].
Proof using. xcf. xrets*. Qed.
charguer's avatar
ok  
charguer committed
212

charguer's avatar
xpat  
charguer committed
213 214 215
Lemma ret_int_pair_spec :
  app ret_int_pair [tt] \[] \[= (3,4)].
Proof using. xcf. xrets*. Qed.
charguer's avatar
ok  
charguer committed
216

charguer's avatar
xpat  
charguer committed
217 218 219
Lemma ret_poly_spec : forall A,
  app ret_poly [tt] \[] \[= @nil A].
Proof using. xcf. xrets*. Qed.
charguer's avatar
ok  
charguer committed
220 221 222



charguer's avatar
charguer committed
223
(********************************************************************)
charguer's avatar
xpat  
charguer committed
224
(* ** Let-value *)
charguer's avatar
init  
charguer committed
225

charguer's avatar
xpat  
charguer committed
226 227
Lemma let_val_int_spec : 
  app let_val_int [tt] \[] \[= 3].
charguer's avatar
charguer committed
228
Proof using.
charguer's avatar
xpat  
charguer committed
229 230 231 232 233 234 235 236 237
  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
238 239
Qed.

charguer's avatar
xpat  
charguer committed
240 241 242 243 244 245
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
246
Proof using.
charguer's avatar
xpat  
charguer committed
247 248 249 250
  xcf. dup 3.
  xval. xret. xsimpl. auto.
  xval as r. xrets~.
  xvals. xrets~.
charguer's avatar
charguer committed
251
Qed.
charguer's avatar
init  
charguer committed
252 253


charguer's avatar
charguer committed
254
(********************************************************************)
charguer's avatar
xpat  
charguer committed
255
(* ** Pattern-matching *)
charguer's avatar
init  
charguer committed
256

charguer's avatar
xpat  
charguer committed
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
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. }
  { xmatch_no_cases. dup 5.
    { 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. }
  { xmatch_no_intros. skip. skip. }
  { 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
297
Qed.
charguer's avatar
init  
charguer committed
298

charguer's avatar
demo  
charguer committed
299

charguer's avatar
charguer committed
300 301 302 303 304 305 306 307 308 309 310 311 312 313
(********************************************************************)
(* ** 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
init  
charguer committed
314

charguer's avatar
charguer committed
315
(********************************************************************)
charguer's avatar
xpat  
charguer committed
316 317
(********************************************************************)
(********************************************************************)
charguer's avatar
init  
charguer committed
318

charguer's avatar
xpat  
charguer committed
319
(*
charguer's avatar
init  
charguer committed
320 321 322 323 324





charguer's avatar
charguer committed
325 326
(********************************************************************)
(* ** Partial applications *)
charguer's avatar
init  
charguer committed
327

charguer's avatar
charguer committed
328 329 330 331 332 333
Lemma app_partial_2_1 () =
   let f x y = (x,y) in
   f 3
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
334

charguer's avatar
charguer committed
335 336 337 338 339 340
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
341

charguer's avatar
charguer committed
342 343 344 345 346 347
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
348

charguer's avatar
charguer committed
349 350 351 352 353 354 355
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
356

charguer's avatar
charguer committed
357 358 359 360 361 362 363 364 365
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
366

charguer's avatar
charguer committed
367 368 369 370 371
Lemma app_partial_builtin () =
  let f = (+) 1 in
  f 2
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
372 373 374 375
Qed.



charguer's avatar
charguer committed
376 377 378 379 380 381 382 383
(********************************************************************)
(* ** Over applications *)

Lemma app_over_id () =
   let f x = x in
   f f 3
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
384 385
Qed.

charguer's avatar
charguer committed
386 387 388 389 390 391 392
(********************************************************************)
(* ** Infix functions *)

Lemma (+++) x y = x + y  
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
393

charguer's avatar
charguer committed
394 395 396 397
Lemma infix_aux x y = x + y
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
398

charguer's avatar
charguer committed
399 400 401 402
Lemma (---) = infix_aux
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
403 404


charguer's avatar
charguer committed
405 406 407 408 409 410 411 412

(********************************************************************)
(* ** Inlined total functions *)

Lemma f () =
   1 - 1/(-1) + (2 / 2) mod 3
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
413 414 415
Qed.


charguer's avatar
charguer committed
416 417 418 419 420 421 422 423 424 425

(********************************************************************)
(* ** 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
426 427
Qed.

charguer's avatar
charguer committed
428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472
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
473

charguer's avatar
charguer committed
474

charguer's avatar
demo  
charguer committed
475
*)
charguer's avatar
charguer committed
476

charguer's avatar
charguer committed
477 478 479 480 481 482 483

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


charguer's avatar
charguer committed
484 485 486
(********************************************************************)
(********************************************************************)
(********************************************************************)
charguer's avatar
init  
charguer committed
487 488
(*

charguer's avatar
charguer committed
489 490 491

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

charguer's avatar
charguer committed
493 494 495 496 497 498 499 500 501 502
Lemma exn_assert_false () =
   assert false
Proof using.
  xcf.
Qed.

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

charguer's avatar
charguer committed
505
exception My_exn 
charguer's avatar
init  
charguer committed
506

charguer's avatar
charguer committed
507 508 509 510
Lemma exn_raise () =
   raise My_exn
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
511 512 513
Qed.


charguer's avatar
charguer committed
514 515
(********************************************************************)
(* ** Assertions *)
charguer's avatar
init  
charguer committed
516

charguer's avatar
charguer committed
517 518 519 520 521
Lemma assert_true () =
  assert true; 3
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
522

charguer's avatar
charguer committed
523 524 525 526 527
Lemma assert_pos x =
  assert (x > 0); 3
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
528

charguer's avatar
charguer committed
529 530 531 532 533
Lemma assert_same (x:int) (y:int) =
  assert (x = y); 3
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
534 535 536



charguer's avatar
charguer committed
537 538
(********************************************************************)
(* ** Conditionals *)
charguer's avatar
init  
charguer committed
539

charguer's avatar
charguer committed
540 541 542 543 544
Lemma if_true () =
   if true then 1 else 0
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
545

charguer's avatar
charguer committed
546 547 548 549 550 551
Lemma if_term () =
   let f x = true in
   if f 0 then 1 else 0
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
552

charguer's avatar
charguer committed
553 554 555 556 557 558 559
Lemma if_else_if () =
   let f x = false in
   if f 0 then 1 
   else if f 1 then 2
   else 0
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
560 561
Qed.

charguer's avatar
charguer committed
562 563 564 565 566 567 568 569
Lemma if_then_no_else b =
  let r = ref 0 in
  if b
     then incr r; 
  !r
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
570 571


charguer's avatar
charguer committed
572 573 574 575 576 577 578 579 580 581 582
(********************************************************************)
(* ** 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
583 584
Qed.

charguer's avatar
charguer committed
585 586 587 588 589
Lemma sitems_get_nb r =
  r.nb
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
590

charguer's avatar
charguer committed
591 592 593 594 595
Lemma sitems_incr_nb r =
  r.nb <- r.nb + 1 
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
596

charguer's avatar
charguer committed
597 598 599 600 601
Lemma sitems_length_items r =
  List.length r.items
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
602

charguer's avatar
charguer committed
603 604 605 606 607
Lemma sitems_push x r =
  r.nb <- r.nb + 1;
  r.items <- x :: r.items
Proof using.
  xcf.
charguer's avatar
init  
charguer committed
608 609 610
Qed.


charguer's avatar
charguer committed
611 612
(********************************************************************)
(* ** Arrays *)
charguer's avatar
init  
charguer committed
613

charguer's avatar
charguer committed
614 615 616 617 618 619 620 621
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
622 623 624 625
  xcf.
Qed.


charguer's avatar
charguer committed
626 627
(********************************************************************)
(* ** While loops *)
charguer's avatar
init  
charguer committed
628

charguer's avatar
charguer committed
629 630 631 632 633 634 635 636 637
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
638 639 640
  xcf.
Qed.

charguer's avatar
charguer committed
641 642 643 644 645
Lemma while_false () =
   while false do () done
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
646 647


charguer's avatar
charguer committed
648 649 650 651 652 653 654 655 656
(********************************************************************)
(* ** 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
657

charguer's avatar
charguer committed
658 659 660 661
(* "for .. down to" not yet supported *)
Proof using.
  xcf.
Qed.
charguer's avatar
init  
charguer committed
662 663


charguer's avatar
charguer committed
664 665
(********************************************************************)
(* ** Recursive function *)
charguer's avatar
init  
charguer committed
666

charguer's avatar
charguer committed
667 668 669 670 671 672 673
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
674 675 676 677 678 679 680 681 682 683 684 685 686




*)








charguer's avatar
charguer committed
687 688 689 690
(*************************************************************************)
(*************************************************************************)
(*************************************************************************)
(** * Polymorphic let demos
charguer's avatar
init  
charguer committed
691 692


charguer's avatar
charguer committed
693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739
(** 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.
 *)



charguer's avatar
charguer committed
740 741 742