Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 465:4320c1a967c2
Spell check
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 29 Aug 2012 18:26:26 -0400 |
parents | 2740b8a23cce |
children | b36876d4611e |
comparison
equal
deleted
inserted
replaced
464:e53d051681b0 | 465:4320c1a967c2 |
---|---|
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 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. | 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 typos 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 |
934 | 934 |
935 Inductive nat_tree : Set := | 935 Inductive nat_tree : Set := |
936 | NLeaf' : nat_tree | 936 | NLeaf' : nat_tree |
937 | NNode' : nat -> list nat_tree -> nat_tree. | 937 | NNode' : nat -> list nat_tree -> nat_tree. |
938 | 938 |
939 (** 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. | 939 (** 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 parameterized 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. |
940 | 940 |
941 Like we encountered for mutual inductive types, we find that the automatically generated induction principle for [nat_tree] is too weak. *) | 941 Like we encountered for mutual inductive types, we find that the automatically generated induction principle for [nat_tree] is too weak. *) |
942 | 942 |
943 Check nat_tree_ind. | 943 Check nat_tree_ind. |
944 (** %\vspace{-.15in}% [[ | 944 (** %\vspace{-.15in}% [[ |