Mercurial > cpdt > repo

comparison src/Subset.v @ 337:4186722d329b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hide some more Subset code in template
author Adam Chlipala <adam@chlipala.net>
date Thu, 06 Oct 2011 12:04:55 -0400
parents 1f57a8d0ed3d
children c7faf3551c5d
comparison
equal deleted inserted replaced
336:a45c07b97ab0 337:4186722d329b
482 482
483 (** %\smallskip% 483 (** %\smallskip%
484 484
485 We can build %``%#"#smart#"#%''% versions of the usual boolean operators and put them to good use in certified programming. For instance, here is a [sumbool] version of boolean %``%#"#or.#"#%''% *) 485 We can build %``%#"#smart#"#%''% versions of the usual boolean operators and put them to good use in certified programming. For instance, here is a [sumbool] version of boolean %``%#"#or.#"#%''% *)
486 486
487 (* EX: Write a function that decides if an element belongs to a list. *)
488
487 (* begin thide *) 489 (* begin thide *)
488 Notation "x || y" := (if x then Yes else Reduce y). 490 Notation "x || y" := (if x then Yes else Reduce y).
489 491
490 (** Let us use it for building a function that decides list membership. We need to assume the existence of an equality decision procedure for the type of list elements. *) 492 (** Let us use it for building a function that decides list membership. We need to assume the existence of an equality decision procedure for the type of list elements. *)
491 493
636 638
637 (** The meaning of [x <- e1; e2] is: First run [e1]. If it fails to find an answer, then announce failure for our derived computation, too. If [e1] %\textit{%#<i>#does#</i>#%}% find an answer, pass that answer on to [e2] to find the final result. The variable [x] can be considered bound in [e2]. 639 (** The meaning of [x <- e1; e2] is: First run [e1]. If it fails to find an answer, then announce failure for our derived computation, too. If [e1] %\textit{%#<i>#does#</i>#%}% find an answer, pass that answer on to [e2] to find the final result. The variable [x] can be considered bound in [e2].
638 640
639 This notation is very helpful for composing richly typed procedures. For instance, here is a very simple implementation of a function to take the predecessors of two naturals at once. *) 641 This notation is very helpful for composing richly typed procedures. For instance, here is a very simple implementation of a function to take the predecessors of two naturals at once. *)
640 642
643 (* EX: Write a function that tries to compute predecessors of two [nat]s at once. *)
644
645 (* begin thide *)
641 Definition doublePred : forall n1 n2 : nat, {{p | n1 = S (fst p) /\ n2 = S (snd p)}}. 646 Definition doublePred : forall n1 n2 : nat, {{p | n1 = S (fst p) /\ n2 = S (snd p)}}.
642 refine (fun n1 n2 => 647 refine (fun n1 n2 =>
643 m1 <- pred_strong7 n1; 648 m1 <- pred_strong7 n1;
644 m2 <- pred_strong7 n2; 649 m2 <- pred_strong7 n2;
645 [|(m1, m2)|]); tauto. 650 [|(m1, m2)|]); tauto.
646 Defined. 651 Defined.
652 (* end thide *)
647 653
648 (** We can build a [sumor] version of the %``%#"#bind#"#%''% notation and use it to write a similarly straightforward version of this function. *) 654 (** We can build a [sumor] version of the %``%#"#bind#"#%''% notation and use it to write a similarly straightforward version of this function. *)
649 655
650 (** printing <-- $\longleftarrow$ *) 656 (** printing <-- $\longleftarrow$ *)
651 657
655 end) 661 end)
656 (right associativity, at level 60). 662 (right associativity, at level 60).
657 663
658 (** printing * $\times$ *) 664 (** printing * $\times$ *)
659 665
666 (* EX: Write a more expressively typed version of the last exercise. *)
667
668 (* begin thide *)
660 Definition doublePred' : forall n1 n2 : nat, 669 Definition doublePred' : forall n1 n2 : nat,
661 {p : nat * nat | n1 = S (fst p) /\ n2 = S (snd p)} 670 {p : nat * nat | n1 = S (fst p) /\ n2 = S (snd p)}
662 + {n1 = 0 \/ n2 = 0}. 671 + {n1 = 0 \/ n2 = 0}.
663 refine (fun n1 n2 => 672 refine (fun n1 n2 =>
664 m1 <-- pred_strong8 n1; 673 m1 <-- pred_strong8 n1;
665 m2 <-- pred_strong8 n2; 674 m2 <-- pred_strong8 n2;
666 [||(m1, m2)||]); tauto. 675 [||(m1, m2)||]); tauto.
667 Defined. 676 Defined.
677 (* end thide *)
668 678
669 679
670 (** * A Type-Checking Example *) 680 (** * A Type-Checking Example *)
671 681
672 (** We can apply these specification types to build a certified type checker for a simple expression language. *) 682 (** We can apply these specification types to build a certified type checker for a simple expression language. *)