Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 420:671a6e7e1f29
Pass through InductiveTypes, to incorporate new coqdoc features
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 25 Jul 2012 16:15:50 -0400 |
parents | 686cf945dd02 |
children | 8077352044b2 |
comparison
equal
deleted
inserted
replaced
419:686cf945dd02 | 420:671a6e7e1f29 |
---|---|
25 The last chapter took a deep dive into some of the more advanced Coq features, to highlight the unusual approach that I advocate in this book. However, from this point on, we will rewind and go back to basics, presenting the relevant features of Coq in a more bottom-up manner. A useful first step is a discussion of the differences and relationships between proofs and programs in Coq. *) | 25 The last chapter took a deep dive into some of the more advanced Coq features, to highlight the unusual approach that I advocate in this book. However, from this point on, we will rewind and go back to basics, presenting the relevant features of Coq in a more bottom-up manner. A useful first step is a discussion of the differences and relationships between proofs and programs in Coq. *) |
26 | 26 |
27 | 27 |
28 (** * Proof Terms *) | 28 (** * Proof Terms *) |
29 | 29 |
30 (** Mainstream presentations of mathematics treat proofs as objects that exist outside of the universe of mathematical objects. However, for a variety of reasoning, it is convenient to encode proofs, traditional mathematical objects, and programs within a single formal language. Validity checks on mathematical objects are useful in any setting, to catch typoes and other uninteresting errors. The benefits of static typing for programs are widely recognized, and Coq brings those benefits to both mathematical objects and programs via a uniform mechanism. In fact, from this point on, we will not bother to distinguish between programs and mathematical objects. Many mathematical formalisms are most easily encoded in terms of programs. | 30 (** Mainstream presentations of mathematics treat proofs as objects that exist outside of the universe of mathematical objects. However, for a variety of reasoning tasks, it is convenient to encode proofs, traditional mathematical objects, and programs within a single formal language. Validity checks on mathematical objects are useful in any setting, to catch typoes and other uninteresting errors. The benefits of static typing for programs are widely recognized, and Coq brings those benefits to both mathematical objects and programs via a uniform mechanism. In fact, from this point on, we will not bother to distinguish between programs and mathematical objects. Many mathematical formalisms are most easily encoded in terms of programs. |
31 | 31 |
32 Proofs are fundamentally different from programs, because any two proofs of a theorem are considered equivalent, from a formal standpoint if not from an engineering standpoint. However, we can use the same type-checking technology to check proofs as we use to validate our programs. This is the%\index{Curry-Howard correspondence}% _Curry-Howard correspondence_ %\cite{Curry,Howard}%, an approach for relating proofs and programs. We represent mathematical theorems as types, such that a theorem's proofs are exactly those programs that type-check at the corresponding type. | 32 Proofs are fundamentally different from programs, because any two proofs of a theorem are considered equivalent, from a formal standpoint if not from an engineering standpoint. However, we can use the same type-checking technology to check proofs as we use to validate our programs. This is the%\index{Curry-Howard correspondence}% _Curry-Howard correspondence_ %\cite{Curry,Howard}%, an approach for relating proofs and programs. We represent mathematical theorems as types, such that a theorem's proofs are exactly those programs that type-check at the corresponding type. |
33 | 33 |
34 The last chapter's example already snuck in an instance of Curry-Howard. We used the token [->] to stand for both function types and logical implications. One reasonable conclusion upon seeing this might be that some fancy overloading of notations is at work. In fact, functions and implications are precisely identical according to Curry-Howard! That is, they are just two ways of describing the same computational phenomenon. | 34 The last chapter's example already snuck in an instance of Curry-Howard. We used the token [->] to stand for both function types and logical implications. One reasonable conclusion upon seeing this might be that some fancy overloading of notations is at work. In fact, functions and implications are precisely identical according to Curry-Howard! That is, they are just two ways of describing the same computational phenomenon. |
35 | 35 |
63 (** In fact, [False] implies anything, and we can take advantage of this fact with an odd looking [match] expression that has no branches. Since there are no rules for deducing [False], there are no cases to consider! *) | 63 (** In fact, [False] implies anything, and we can take advantage of this fact with an odd looking [match] expression that has no branches. Since there are no rules for deducing [False], there are no cases to consider! *) |
64 | 64 |
65 Check (fun x : False => match x with end : True). | 65 Check (fun x : False => match x with end : True). |
66 (** [: False -> True] *) | 66 (** [: False -> True] *) |
67 | 67 |
68 (** Every one of these example programs whose type looks like a logical formula is a %\index{proof term}%_proof term_. We use that name for any Gallina term of a logical type, and we will elaborate shortly on what makes a type logical. | 68 (** Every one of these example programs whose type looks like a logical formula is a%\index{proof term}% _proof term_. We use that name for any Gallina term of a logical type, and we will elaborate shortly on what makes a type logical. |
69 | 69 |
70 In the rest of this chapter, we will introduce different ways of defining types. Every example type can be interpreted alternatively as a type of programs or %\index{proposition}%propositions (i.e., formulas or theorem statements). | 70 In the rest of this chapter, we will introduce different ways of defining types. Every example type can be interpreted alternatively as a type of programs or %\index{proposition}%propositions (i.e., formulas or theorem statements). |
71 | 71 |
72 One of the first types we introduce will be [bool], with constructors [true] and [false]. Newcomers to Coq often wonder about the distinction between [True] and [true] and the distinction between [False] and [false]. One glib answer is that [True] and [False] are types, but [true] and [false] are not. A more useful answer is that Coq's metatheory guarantees that any term of type [bool] _evaluates_ to either [true] or [false]. This means that we have an _algorithm_ for answering any question phrased as an expression of type [bool]. Conversely, most propositions do not evaluate to [True] or [False]; the language of inductively defined propositions is much richer than that. We ought to be glad that we have no algorithm for deciding mathematical truth, since otherwise it would be clear that we could not formalize undecidable properties, like most any properties of general-purpose programs. *) | 72 One of the first types we introduce will be [bool], with constructors [true] and [false]. Newcomers to Coq often wonder about the distinction between [True] and [true] and the distinction between [False] and [false]. One glib answer is that [True] and [False] are types, but [true] and [false] are not. A more useful answer is that Coq's metatheory guarantees that any term of type [bool] _evaluates_ to either [true] or [false]. This means that we have an _algorithm_ for answering any question phrased as an expression of type [bool]. Conversely, most propositions do not evaluate to [True] or [False]; the language of inductively defined propositions is much richer than that. We ought to be glad that we have no algorithm for deciding mathematical truth, since otherwise it would be clear that we could not formalize undecidable properties, like most any properties of general-purpose programs. *) |
73 | 73 |
114 | 114 |
115 destruct x. | 115 destruct x. |
116 | 116 |
117 ]] | 117 ]] |
118 | 118 |
119 %\noindent%...which corresponds to %``%#"#proof by case analysis#"#%''% in classical math. For non-recursive inductive types, the two tactics will always have identical behavior. Often case analysis is sufficient, even in proofs about recursive types, and it is nice to avoid introducing unneeded induction hypotheses. | 119 %\noindent%...which corresponds to "proof by case analysis" in classical math. For non-recursive inductive types, the two tactics will always have identical behavior. Often case analysis is sufficient, even in proofs about recursive types, and it is nice to avoid introducing unneeded induction hypotheses. |
120 | 120 |
121 What exactly _is_ the %\index{induction principles}%induction principle for [unit]? We can ask Coq: *) | 121 What exactly _is_ the %\index{induction principles}%induction principle for [unit]? We can ask Coq: *) |
122 | 122 |
123 Check unit_ind. | 123 Check unit_ind. |
124 (** [unit_ind : forall P : unit -> Prop, P tt -> forall u : unit, P u] *) | 124 (** [unit_ind : forall P : unit -> Prop, P tt -> forall u : unit, P u] *) |
384 forall n : nat_list, P n | 384 forall n : nat_list, P n |
385 ]] | 385 ]] |
386 | 386 |
387 %\medskip% | 387 %\medskip% |
388 | 388 |
389 In general, we can implement any %``%#"#tree#"#%''% types as inductive types. For example, here are binary trees of naturals. *) | 389 In general, we can implement any "tree" types as inductive types. For example, here are binary trees of naturals. *) |
390 | 390 |
391 Inductive nat_btree : Set := | 391 Inductive nat_btree : Set := |
392 | NLeaf : nat_btree | 392 | NLeaf : nat_btree |
393 | NNode : nat_btree -> nat -> nat_btree -> nat_btree. | 393 | NNode : nat_btree -> nat -> nat_btree -> nat_btree. |
394 | 394 |
459 (* begin thide *) | 459 (* begin thide *) |
460 induction ls1; crush. | 460 induction ls1; crush. |
461 Qed. | 461 Qed. |
462 (* end thide *) | 462 (* end thide *) |
463 | 463 |
464 (** There is a useful shorthand for writing many definitions that share the same parameter, based on Coq's %\index{sections}\index{Vernacular commands!Section}\index{Vernacular commands!Variable}%_section_ mechanism. The following block of code is equivalent to the above: *) | 464 (** There is a useful shorthand for writing many definitions that share the same parameter, based on Coq's%\index{sections}\index{Vernacular commands!Section}\index{Vernacular commands!Variable}% _section_ mechanism. The following block of code is equivalent to the above: *) |
465 | 465 |
466 (* begin hide *) | 466 (* begin hide *) |
467 Reset list. | 467 Reset list. |
468 (* end hide *) | 468 (* end hide *) |
469 | 469 |
656 Inductive formula : Set := | 656 Inductive formula : Set := |
657 | Eq : nat -> nat -> formula | 657 | Eq : nat -> nat -> formula |
658 | And : formula -> formula -> formula | 658 | And : formula -> formula -> formula |
659 | Forall : (nat -> formula) -> formula. | 659 | Forall : (nat -> formula) -> formula. |
660 | 660 |
661 (** Our kinds of formulas are equalities between naturals, conjunction, and universal quantification over natural numbers. We avoid needing to include a notion of %``%#"#variables#"#%''% in our type, by using Coq functions to encode quantification. For instance, here is the encoding of [forall x : nat, x = x]:%\index{Vernacular commands!Example}% *) | 661 (** Our kinds of formulas are equalities between naturals, conjunction, and universal quantification over natural numbers. We avoid needing to include a notion of "variables" in our type, by using Coq functions to encode quantification. For instance, here is the encoding of [forall x : nat, x = x]:%\index{Vernacular commands!Example}% *) |
662 | 662 |
663 Example forall_refl : formula := Forall (fun x => Eq x x). | 663 Example forall_refl : formula := Forall (fun x => Eq x x). |
664 | 664 |
665 (** We can write recursive functions over reflexive types quite naturally. Here is one translating our formulas into native Coq propositions. *) | 665 (** We can write recursive functions over reflexive types quite naturally. Here is one translating our formulas into native Coq propositions. *) |
666 | 666 |
711 | 711 |
712 Given our last example of an inductive type, many readers are probably eager to try encoding the syntax of %\index{lambda calculus}%lambda calculus. Indeed, the function-based representation technique that we just used, called%\index{higher-order abstract syntax}\index{HOAS|see{higher-order abstract syntax}}% _higher-order abstract syntax_ (HOAS)%~\cite{HOAS}%, is the representation of choice for lambda calculi in %\index{Twelf}%Twelf and in many applications implemented in Haskell and ML. Let us try to import that choice to Coq: *) | 712 Given our last example of an inductive type, many readers are probably eager to try encoding the syntax of %\index{lambda calculus}%lambda calculus. Indeed, the function-based representation technique that we just used, called%\index{higher-order abstract syntax}\index{HOAS|see{higher-order abstract syntax}}% _higher-order abstract syntax_ (HOAS)%~\cite{HOAS}%, is the representation of choice for lambda calculi in %\index{Twelf}%Twelf and in many applications implemented in Haskell and ML. Let us try to import that choice to Coq: *) |
713 (* begin hide *) | 713 (* begin hide *) |
714 Inductive term : Set := App | Abs. | 714 Inductive term : Set := App | Abs. |
715 Reset term. | 715 Reset term. |
716 Definition uhoh := O. | |
716 (* end hide *) | 717 (* end hide *) |
717 (** [[ | 718 (** [[ |
718 Inductive term : Set := | 719 Inductive term : Set := |
719 | App : term -> term -> term | 720 | App : term -> term -> term |
720 | Abs : (term -> term) -> term. | 721 | Abs : (term -> term) -> term. |
757 fun P : unit -> Prop => unit_rect P | 758 fun P : unit -> Prop => unit_rect P |
758 : forall P : unit -> Prop, P tt -> forall u : unit, P u | 759 : forall P : unit -> Prop, P tt -> forall u : unit, P u |
759 | 760 |
760 ]] | 761 ]] |
761 | 762 |
762 We see that this induction principle is defined in terms of a more general principle, [unit_rect]. The %\texttt{%#<tt>#rec#</tt>#%}% stands for %``%#"#recursion principle,#"#%''% and the %\texttt{%#<tt>#t#</tt>#%}% at the end stands for [Type]. *) | 763 We see that this induction principle is defined in terms of a more general principle, [unit_rect]. The <<rec>> stands for "recursion principle," and the <<t>> at the end stands for [Type]. *) |
763 | 764 |
764 Check unit_rect. | 765 Check unit_rect. |
765 (** %\vspace{-.15in}% [[ | 766 (** %\vspace{-.15in}% [[ |
766 unit_rect | 767 unit_rect |
767 : forall P : unit -> Type, P tt -> forall u : unit, P u | 768 : forall P : unit -> Type, P tt -> forall u : unit, P u |
815 | 816 |
816 Definition unit_rect' (P : unit -> Type) (f : P tt) (u : unit) := | 817 Definition unit_rect' (P : unit -> Type) (f : P tt) (u : unit) := |
817 match u with | 818 match u with |
818 | tt => f | 819 | tt => f |
819 end. | 820 end. |
821 | |
822 (* begin hide *) | |
823 Definition foo := nat_rect. | |
824 (* end hide *) | |
820 | 825 |
821 (** We rely on Coq's heuristics for inferring [match] annotations, which are not consulted in the pretty-printing of terms. | 826 (** We rely on Coq's heuristics for inferring [match] annotations, which are not consulted in the pretty-printing of terms. |
822 | 827 |
823 We can check the implementation [nat_rect] as well: *) | 828 We can check the implementation [nat_rect] as well: *) |
824 | 829 |
888 (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> | 893 (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> |
889 forall e : even_list, P e | 894 forall e : even_list, P e |
890 | 895 |
891 ]] | 896 ]] |
892 | 897 |
893 We see a mutually recursive [fix], with the different functions separated by %\index{Gallina terms!with}%[with] in the same way that they would be separated by %\texttt{%#<tt>#and#</tt>#%}% in ML. A final %\index{Gallina terms!for}%[for] clause identifies which of the mutually recursive functions should be the final value of the [fix] expression. Using this definition as a template, we can reimplement [even_list_mut] directly. *) | 898 We see a mutually recursive [fix], with the different functions separated by %\index{Gallina terms!with}%[with] in the same way that they would be separated by <<and>> in ML. A final %\index{Gallina terms!for}%[for] clause identifies which of the mutually recursive functions should be the final value of the [fix] expression. Using this definition as a template, we can reimplement [even_list_mut] directly. *) |
894 | 899 |
895 Section even_list_mut'. | 900 Section even_list_mut'. |
896 (** First, we need the properties that we are proving. *) | 901 (** First, we need the properties that we are proving. *) |
897 | 902 |
898 Variable Peven : even_list -> Prop. | 903 Variable Peven : even_list -> Prop. |
944 | 949 |
945 Inductive nat_tree : Set := | 950 Inductive nat_tree : Set := |
946 | NLeaf' : nat_tree | 951 | NLeaf' : nat_tree |
947 | NNode' : nat -> list nat_tree -> nat_tree. | 952 | NNode' : nat -> list nat_tree -> nat_tree. |
948 | 953 |
949 (** This is an example of a %\index{nested inductive type}%_nested_ inductive type definition, because we use the type we are defining as an argument to a parametrized type family. Coq will not allow all such definitions; it effectively pretends that we are defining [nat_tree] mutually with a version of [list] specialized to [nat_tree], checking that the resulting expanded definition satisfies the usual rules. For instance, if we replaced [list] with a type family that used its parameter as a function argument, then the definition would be rejected as violating the positivity restriction. | 954 (** This is an example of a%\index{nested inductive type}% _nested_ inductive type definition, because we use the type we are defining as an argument to a parametrized type family. Coq will not allow all such definitions; it effectively pretends that we are defining [nat_tree] mutually with a version of [list] specialized to [nat_tree], checking that the resulting expanded definition satisfies the usual rules. For instance, if we replaced [list] with a type family that used its parameter as a function argument, then the definition would be rejected as violating the positivity restriction. |
950 | 955 |
951 Like we encountered for mutual inductive types, we find that the automatically generated induction principle for [nat_tree] is too weak. *) | 956 Like we encountered for mutual inductive types, we find that the automatically generated induction principle for [nat_tree] is too weak. *) |
952 | 957 |
953 Check nat_tree_ind. | 958 Check nat_tree_ind. |
954 (** %\vspace{-.15in}% [[ | 959 (** %\vspace{-.15in}% [[ |
1012 | 1017 |
1013 Hypothesis NLeaf'_case : P NLeaf'. | 1018 Hypothesis NLeaf'_case : P NLeaf'. |
1014 Hypothesis NNode'_case : forall (n : nat) (ls : list nat_tree), | 1019 Hypothesis NNode'_case : forall (n : nat) (ls : list nat_tree), |
1015 All P ls -> P (NNode' n ls). | 1020 All P ls -> P (NNode' n ls). |
1016 | 1021 |
1022 (* begin hide *) | |
1023 Definition list_nat_tree_ind := O. | |
1024 (* end hide *) | |
1025 | |
1017 (** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions. | 1026 (** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions. |
1018 | 1027 |
1019 [[ | 1028 [[ |
1020 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := | 1029 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := |
1021 match tr with | 1030 match tr with |
1035 << | 1044 << |
1036 Recursive call to nat_tree_ind' has principal argument equal to "tr" | 1045 Recursive call to nat_tree_ind' has principal argument equal to "tr" |
1037 instead of rest. | 1046 instead of rest. |
1038 >> | 1047 >> |
1039 | 1048 |
1040 There is no deep theoretical reason why this program should be rejected; Coq applies incomplete termination-checking heuristics, and it is necessary to learn a few of the most important rules. The term %``%#"#nested inductive type#"#%''% hints at the solution to this particular problem. Just like true mutually inductive types require mutually recursive induction principles, nested types require nested recursion. *) | 1049 There is no deep theoretical reason why this program should be rejected; Coq applies incomplete termination-checking heuristics, and it is necessary to learn a few of the most important rules. The term "nested inductive type" hints at the solution to this particular problem. Just like true mutually inductive types require mutually recursive induction principles, nested types require nested recursion. *) |
1041 | 1050 |
1042 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := | 1051 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := |
1043 match tr with | 1052 match tr with |
1044 | NLeaf' => NLeaf'_case | 1053 | NLeaf' => NLeaf'_case |
1045 | NNode' n ls => NNode'_case n ls | 1054 | NNode' n ls => NNode'_case n ls |
1151 (** It can be useful to understand how tactics like %\index{tactics!discriminate}%[discriminate] and %\index{tactics!injection}%[injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *) | 1160 (** It can be useful to understand how tactics like %\index{tactics!discriminate}%[discriminate] and %\index{tactics!injection}%[injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *) |
1152 | 1161 |
1153 Theorem true_neq_false : true <> false. | 1162 Theorem true_neq_false : true <> false. |
1154 | 1163 |
1155 (* begin thide *) | 1164 (* begin thide *) |
1156 (** We begin with the tactic %\index{tactics!red}%[red], which is short for %``%#"#one step of reduction,#"#%''% to unfold the definition of logical negation. *) | 1165 (** We begin with the tactic %\index{tactics!red}%[red], which is short for "one step of reduction," to unfold the definition of logical negation. *) |
1157 | 1166 |
1158 red. | 1167 red. |
1159 (** [[ | 1168 (** [[ |
1160 ============================ | 1169 ============================ |
1161 true = false -> False | 1170 true = false -> False |