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