Certified Programming with Dependent Types: src/InductiveTypes.v comparison

comparison src/InductiveTypes.v @ 469:b36876d4611e

Batch of changes based on proofreader feedback

author	Adam Chlipala <adam@chlipala.net>
date	Wed, 26 Sep 2012 16:35:35 -0400
parents	4320c1a967c2
children	0df6dde807ab

comparison

equal deleted inserted replaced

-:62475ab7570b
+:b36876d4611e
 (** %\smallskip{}%No proofs of %\index{Gallina terms!False}%[False] exist in the top-level context, but the implication-as-function analogy gives us an easy way to, for example, show that [False] implies itself. *)
 Check (fun x : False => x).
 (** [: False -> False] *)
-(** %\smallskip{}%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! *)
-Check (fun x : False => match x with end : True).
-(** [: False -> True] *)
 (** %\smallskip{}%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.
-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).
+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 proofs.
-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. *)
+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 almost any interesting property of general-purpose programs. *)
 (** * Enumerations *)
 (** Coq inductive types generalize the %\index{algebraic datatypes}%algebraic datatypes found in %\index{Haskell}%Haskell and %\index{ML}%ML.  Confusingly enough, inductive types also generalize %\index{generalized algebraic datatypes}%generalized algebraic datatypes (GADTs), by adding the possibility for type dependency.  Even so, it is worth backing up from the examples of the last chapter and going over basic, algebraic datatype uses of inductive datatypes, because the chance to prove things about the values of these types adds new wrinkles beyond usual practice in Haskell and ML.
 match n with
 | O => O
 | S n' => n'
 end.
-(** We can prove theorems by case analysis: *)
+(** We can prove theorems by case analysis with [destruct] as for simpler inductive types, but we can also now get into genuine inductive theorems.  First, we will need a recursive function, to make things interesting.%\index{Gallina terms!plus}% *)
-Theorem S_isZero : forall n : nat, isZero (pred (S (S n))) = false.
-(* begin thide *)
-destruct n; reflexivity.
-Qed.
-(* end thide *)
-(** We can also now get into genuine inductive theorems.  First, we will need a recursive function, to make things interesting.%\index{Gallina terms!plus}% *)
 Fixpoint plus (n m : nat) : nat :=
 match n with
 | O => m
 | S n' => S (plus n' m)
 (** Our first subgoal is [plus O O = O], which _is_ trivial by computation. *)
 reflexivity.
-(** Our second subgoal is more work and also demonstrates our first inductive hypothesis.
+(** Our second subgoal requires more work and also demonstrates our first inductive hypothesis.
 [[
 n : nat
 IHn : plus n O = n
 ============================
 induction ls1; crush.
 Qed.
 (* end thide *)
 End list.
-(* begin hide *)
 Implicit Arguments Nil [T].
-(* end hide *)
+(** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed.  With an [Implicit Arguments]%~\index{Vernacular commands!Implicit Arguments}% command, we ask that [T] be inferred when we use [Nil]; Coq's heuristics already decided to apply a similar policy to [Cons], because of the [Set Implicit Arguments]%~\index{Vernacular commands!Set Implicit Arguments}% command elided at the beginning of this chapter.  We verify that our definitions have been saved properly using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)
-(** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed.  We verify that this has happened using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)
 Print list.
 (** %\vspace{-.15in}% [[
 Inductive list (T : Set) : Set :=
 Nil : list T | Cons : T -> list T -> list T
 (** We simply need to specify two predicates, one for each of the mutually inductive types.  In general, it would not be a good idea to assume that a proof assistant could infer extra predicates, so this way of applying mutual induction is about as straightforward as we could hope for. *)
 (** * Reflexive Types *)
-(** A kind of inductive type called a _reflexive type_ is defined in terms of functions that have the type being defined as their range.  One very useful class of examples is in modeling variable binders.  Our example will be an encoding of the syntax of first-order logic.  Since the idea of syntactic encodings of logic may require a bit of acclimation, let us first consider a simpler formula type for a subset of propositional logic. *)
+(** A kind of inductive type called a _reflexive type_ includes at least one constructor that takes as an argument _a function returning the same type we are defining_.  One very useful class of examples is in modeling variable binders.  Our example will be an encoding of the syntax of first-order logic.  Since the idea of syntactic encodings of logic may require a bit of acclimation, let us first consider a simpler formula type for a subset of propositional logic.  We are not yet using a reflexive type, but later we will extend the example reflexively. *)
 Inductive pformula : Set :=
 | Truth : pformula
 | Falsehood : pformula
 | Conjunction : pformula -> pformula -> pformula.
 Focusing on the [Forall] case, which comes third, we see that we are allowed to assume that the theorem holds _for any application of the argument function [f1]_.  That is, Coq induction principles do not follow a simple rule that the textual representations of induction variables must get shorter in appeals to induction hypotheses.  Luckily for us, the people behind the metatheory of Coq have verified that this flexibility does not introduce unsoundness.
 %\medskip%
-Up to this point, we have seen how to encode in Coq more and more of what is possible with algebraic datatypes in %\index{Haskell}%Haskell and %\index{ML}%ML.  This may have given the inaccurate impression that inductive types are a strict extension of algebraic datatypes.  In fact, Coq must rule out some types allowed by Haskell and ML, for reasons of soundness.  Reflexive types provide our first good example of such a case.
+Up to this point, we have seen how to encode in Coq more and more of what is possible with algebraic datatypes in %\index{Haskell}%Haskell and %\index{ML}%ML.  This may have given the inaccurate impression that inductive types are a strict extension of algebraic datatypes.  In fact, Coq must rule out some types allowed by Haskell and ML, for reasons of soundness.  Reflexive types provide our first good example of such a case; only some of them are legal.
 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: *)
 (* begin hide *)
 (* begin thide *)
 Inductive term : Set := App | Abs.
 %\index{type inference}%Type inference for dependent pattern matching is undecidable, which can be proved by reduction from %\index{higher-order unification}%higher-order unification%~\cite{HOU}%.  Thus, we often find ourselves needing to annotate our programs in a way that explains dependencies to the type checker.  In the example of [unit_rect], we have an %\index{Gallina terms!as}%[as] clause, which binds a name for the discriminee; and a %\index{Gallina terms!return}%[return] clause, which gives a way to compute the [match] result type as a function of the discriminee.
 To prove that [unit_rect] is nothing special, we can reimplement it manually. *)
 Definition unit_rect' (P : unit -> Type) (f : P tt) (u : unit) :=
-match u with
+match u return P u with
 | tt => f
 end.
 (* begin hide *)
 (* begin thide *)
 Definition foo := nat_rect.
 (* end thide *)
 (* end hide *)
-(** We rely on Coq's heuristics for inferring [match] annotations, which are not consulted in the pretty-printing of terms.
+(** We can check the implementation [nat_rect] as well: *)
-We can check the implementation [nat_rect] as well: *)
 Print nat_rect.
 (** %\vspace{-.15in}% [[
 nat_rect =
 fun (P : nat -> Type) (f : P O) (f0 : forall n : nat, P n -> P (S n)) =>

Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 469:b36876d4611e