Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 352:ab60b10890ed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Non-termination monad
author Adam Chlipala <adam@chlipala.net>
date Wed, 26 Oct 2011 16:57:11 -0400
parents bb1a470c1757
children 3322367e955d
comparison
equal deleted inserted replaced
351:bb1a470c1757 352:ab60b10890ed
273 (forall x : A, (forall y : A, R y x -> P y) -> P x) -> 273 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
274 forall a : A, P a 274 forall a : A, P a
275 ]] 275 ]]
276 276
277 Some more recent Coq features provide more convenient syntax for defining recursive functions. Interested readers can consult the Coq manual about the commands %\index{Function}%[Function] and %\index{Program Fixpoint}%[Program Fixpoint]. *) 277 Some more recent Coq features provide more convenient syntax for defining recursive functions. Interested readers can consult the Coq manual about the commands %\index{Function}%[Function] and %\index{Program Fixpoint}%[Program Fixpoint]. *)
278
279
280 (** * A Non-Termination Monad *)
281
282 Section computation.
283 Variable A : Type.
284
285 Definition computation :=
286 {f : nat -> option A
287 | forall (n : nat) (v : A),
288 f n = Some v
289 -> forall (n' : nat), n' >= n
290 -> f n' = Some v}.
291
292 Definition runTo (m : computation) (n : nat) (v : A) :=
293 proj1_sig m n = Some v.
294
295 Definition run (m : computation) (v : A) :=
296 exists n, runTo m n v.
297 End computation.
298
299 Hint Unfold runTo.
300
301 Ltac run' := unfold run, runTo in *; try red; crush;
302 repeat (match goal with
303 | [ _ : proj1_sig ?E _ = _ |- _ ] =>
304 match goal with
305 | [ x : _ |- _ ] =>
306 match x with
307 | E => destruct E
308 end
309 end
310 | [ |- context[match ?M with exist _ _ => _ end] ] => let Heq := fresh "Heq" in
311 case_eq M; intros ? ? Heq; try rewrite Heq in *; try subst
312 | [ _ : context[match ?M with exist _ _ => _ end] |- _ ] => let Heq := fresh "Heq" in
313 case_eq M; intros ? ? Heq; try rewrite Heq in *; subst
314 | [ H : forall n v, ?E n = Some v -> _,
315 _ : context[match ?E ?N with Some _ => _ | None => _ end] |- _ ] =>
316 specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate
317 | [ H : forall n v, ?E n = Some v -> _, H' : ?E _ = Some _ |- _ ] => rewrite (H _ _ H') by auto
318 end; simpl in *); eauto 7.
319
320 Ltac run := run'; repeat (match goal with
321 | [ H : forall n v, ?E n = Some v -> _
322 |- context[match ?E ?N with Some _ => _ | None => _ end] ] =>
323 specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate
324 end; run').
325
326 Lemma ex_irrelevant : forall P : Prop, P -> exists n : nat, P.
327 exists 0; auto.
328 Qed.
329
330 Hint Resolve ex_irrelevant.
331
332 Require Import Max.
333
334 Ltac max := intros n m; generalize (max_spec_le n m); crush.
335
336 Lemma max_1 : forall n m, max n m >= n.
337 max.
338 Qed.
339
340 Lemma max_2 : forall n m, max n m >= m.
341 max.
342 Qed.
343
344 Hint Resolve max_1 max_2.
345
346 Lemma ge_refl : forall n, n >= n.
347 crush.
348 Qed.
349
350 Hint Resolve ge_refl.
351
352 Hint Extern 1 => match goal with
353 | [ H : _ = exist _ _ _ |- _ ] => rewrite H
354 end.
355
356 Section Bottom.
357 Variable A : Type.
358
359 Definition Bottom : computation A.
360 exists (fun _ : nat => @None A); abstract run.
361 Defined.
362
363 Theorem run_Bottom : forall v, ~run Bottom v.
364 run.
365 Qed.
366 End Bottom.
367
368 Section Return.
369 Variable A : Type.
370 Variable v : A.
371
372 Definition Return : computation A.
373 intros; exists (fun _ : nat => Some v); abstract run.
374 Defined.
375
376 Theorem run_Return : run Return v.
377 run.
378 Qed.
379
380 Theorem run_Return_inv : forall x, run Return x -> x = v.
381 run.
382 Qed.
383 End Return.
384
385 Hint Resolve run_Return.
386
387 Section Bind.
388 Variables A B : Type.
389 Variable m1 : computation A.
390 Variable m2 : A -> computation B.
391
392 Definition Bind : computation B.
393 exists (fun n =>
394 let (f1, Hf1) := m1 in
395 match f1 n with
396 | None => None
397 | Some v =>
398 let (f2, Hf2) := m2 v in
399 f2 n
400 end); abstract run.
401 Defined.
402
403 Require Import Max.
404
405 Theorem run_Bind : forall (v1 : A) (v2 : B),
406 run m1 v1
407 -> run (m2 v1) v2
408 -> run Bind v2.
409 run; match goal with
410 | [ x : nat, y : nat |- _ ] => exists (max x y)
411 end; run.
412 Qed.
413
414 Theorem run_Bind_inv : forall (v2 : B),
415 run Bind v2
416 -> exists v1 : A,
417 run m1 v1
418 /\ run (m2 v1) v2.
419 run.
420 Qed.
421 End Bind.
422
423 Hint Resolve run_Bind.
424
425 Notation "x <- m1 ; m2" :=
426 (Bind m1 (fun x => m2)) (right associativity, at level 70).
427
428 Definition meq A (m1 m2 : computation A) := forall n, proj1_sig m1 n = proj1_sig m2 n.
429
430 Theorem left_identity : forall A B (a : A) (f : A -> computation B),
431 meq (Bind (Return a) f) (f a).
432 run.
433 Qed.
434
435 Theorem right_identity : forall A (m : computation A),
436 meq (Bind m (@Return _)) m.
437 run.
438 Qed.
439
440 Theorem associativity : forall A B C (m : computation A) (f : A -> computation B) (g : B -> computation C),
441 meq (Bind (Bind m f) g) (Bind m (fun x => Bind (f x) g)).
442 run.
443 Qed.
444
445 Section monotone_runTo.
446 Variable A : Type.
447 Variable c : computation A.
448 Variable v : A.
449
450 Theorem monotone_runTo : forall (n1 : nat),
451 runTo c n1 v
452 -> forall n2, n2 >= n1
453 -> runTo c n2 v.
454 run.
455 Qed.
456 End monotone_runTo.
457
458 Hint Resolve monotone_runTo.
459
460 Section lattice.
461 Variable A : Type.
462
463 Definition leq (x y : option A) :=
464 forall v, x = Some v -> y = Some v.
465 End lattice.
466
467 Hint Unfold leq.
468
469 Section Fix.
470 Variables A B : Type.
471 Variable f : (A -> computation B) -> (A -> computation B).
472
473 Hypothesis f_continuous : forall n v v1 x,
474 runTo (f v1 x) n v
475 -> forall (v2 : A -> computation B),
476 (forall x, leq (proj1_sig (v1 x) n) (proj1_sig (v2 x) n))
477 -> runTo (f v2 x) n v.
478
479 Fixpoint Fix' (n : nat) (x : A) : computation B :=
480 match n with
481 | O => Bottom _
482 | S n' => f (Fix' n') x
483 end.
484
485 Hint Extern 1 (_ >= _) => omega.
486 Hint Unfold leq.
487
488 Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v
489 -> forall n', n' >= n
490 -> proj1_sig (Fix' n' x) steps = Some v.
491 unfold runTo in *; induction n; crush;
492 match goal with
493 | [ H : _ >= _ |- _ ] => inversion H; crush; eauto
494 end.
495 Qed.
496
497 Hint Resolve Fix'_ok.
498
499 Hint Extern 1 (proj1_sig _ _ = _) => simpl;
500 match goal with
501 | [ |- proj1_sig ?E _ = _ ] => eapply (proj2_sig E)
502 end.
503
504 Definition Fix : A -> computation B.
505 intro x; exists (fun n => proj1_sig (Fix' n x) n); abstract run.
506 Defined.
507
508 Definition extensional (f : (A -> computation B) -> (A -> computation B)) :=
509 forall g1 g2 n,
510 (forall x, proj1_sig (g1 x) n = proj1_sig (g2 x) n)
511 -> forall x, proj1_sig (f g1 x) n = proj1_sig (f g2 x) n.
512
513 Hypothesis f_extensional : extensional f.
514
515 Theorem run_Fix : forall x v,
516 run (f Fix x) v
517 -> run (Fix x) v.
518 run; match goal with
519 | [ n : nat |- _ ] => exists (S n); eauto
520 end.
521 Qed.
522 End Fix.
523
524 Hint Resolve run_Fix.
525
526 Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y)
527 -> x = y.
528 intros ? ? ? H; generalize (H _ (refl_equal _)); crush.
529 Qed.
530
531 Lemma leq_None : forall A (x y : A), leq (Some x) None
532 -> False.
533 intros ? ? ? H; generalize (H _ (refl_equal _)); crush.
534 Qed.
535
536 Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A).
537 refine (fun A le => Fix
538 (fun (mergeSort : list A -> computation (list A))
539 (ls : list A) =>
540 if le_lt_dec 2 (length ls)
541 then let lss := partition ls in
542 ls1 <- mergeSort (fst lss);
543 ls2 <- mergeSort (snd lss);
544 Return (merge le ls1 ls2)
545 else Return ls) _); abstract (run;
546 repeat (match goal with
547 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
548 end; run);
549 repeat match goal with
550 | [ H : forall x, leq (proj1_sig (?f x) _) (proj1_sig (?g x) _) |- _ ] =>
551 match goal with
552 | [ H1 : f ?arg = _, H2 : g ?arg = _ |- _ ] =>
553 generalize (H arg); rewrite H1; rewrite H2; clear H1 H2; simpl; intro
554 end
555 end; run; repeat match goal with
556 | [ H : _ |- _ ] => (apply leq_None in H; tauto) || (apply leq_Some in H; subst)
557 end; auto).
558 Defined.
559
560 Print mergeSort'.
561
562 Lemma test_mergeSort' : run (mergeSort' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
563 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
564 exists 4; reflexivity.
565 Qed.
566
567 Definition looper : bool -> computation unit.
568 refine (Fix (fun looper (b : bool) =>
569 if b then Return tt else looper b) _);
570 abstract (unfold leq in *; run;
571 repeat match goal with
572 | [ x : unit |- _ ] => destruct x
573 | [ x : bool |- _ ] => destruct x
574 end; auto).
575 Defined.
576
577 Lemma test_looper : run (looper true) tt.
578 exists 1; reflexivity.
579 Qed.