Mercurial > cpdt > repo
changeset 440:f923024bd284
Vertical spacing pass, through end of Subset
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 30 Jul 2012 16:50:02 -0400 |
| parents | 393b8ed99c2f |
| children | cbfd23b4364d |
| files | src/Coinductive.v src/Predicates.v src/Subset.v |
| diffstat | 3 files changed, 37 insertions(+), 51 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Coinductive.v Mon Jul 30 13:21:36 2012 -0400 +++ b/src/Coinductive.v Mon Jul 30 16:50:02 2012 -0400 @@ -29,7 +29,7 @@ Fixpoint bad (u : unit) : P := bad u. ]] -This would leave us with [bad tt] as a proof of [P]. +%\smallskip{}%This would leave us with [bad tt] as a proof of [P]. There are also algorithmic considerations that make universal termination very desirable. We have seen how tactics like [reflexivity] compare terms up to equivalence under computational rules. Calls to recursive, pattern-matching functions are simplified automatically, with no need for explicit proof steps. It would be very hard to hold onto that kind of benefit if it became possible to write non-terminating programs; we would be running smack into the halting problem. @@ -167,14 +167,13 @@ Variables A B : Type. Variable f : A -> B. (* begin thide *) - (** [[ + (** %\vspace{-.15in}%[[ CoFixpoint map' (s : stream A) : stream B := match s with | Cons h t => interleave (Cons (f h) (map' t)) (Cons (f h) (map' t)) end. ]] - - We get another error message about an unguarded recursive call. *) + %\vspace{-.15in}%We get another error message about an unguarded recursive call. *) End map'. @@ -378,9 +377,10 @@ Theorem ones_eq' : stream_eq ones ones'. cofix; crush. - (** [[ + (** %\vspace{-.25in}%[[ Guarded. ]] + %\vspace{-.25in}% *) Abort.
--- a/src/Predicates.v Mon Jul 30 13:21:36 2012 -0400 +++ b/src/Predicates.v Mon Jul 30 16:50:02 2012 -0400 @@ -35,18 +35,17 @@ (** The so-called %\index{Curry-Howard correspondence}``%#"#Curry-Howard correspondence#"#%''~\cite{Curry,Howard}% states a formal connection between functional programs and mathematical proofs. In the last chapter, we snuck in a first introduction to this subject in Coq. Witness the close similarity between the types [unit] and [True] from the standard library: *) Print unit. -(** [[ +(** %\vspace{-.15in}%[[ Inductive unit : Set := tt : unit ]] *) Print True. -(** [[ +(** %\vspace{-.15in}%[[ Inductive True : Prop := I : True ]] -*) -(** Recall that [unit] is the type with only one value, and [True] is the proposition that always holds. Despite this superficial difference between the two concepts, in both cases we can use the same inductive definition mechanism. The connection goes further than this. We see that we arrive at the definition of [True] by replacing [unit] by [True], [tt] by [I], and [Set] by [Prop]. The first two of these differences are superficial changes of names, while the third difference is the crucial one for separating programs from proofs. A term [T] of type [Set] is a type of programs, and a term of type [T] is a program. A term [T] of type [Prop] is a logical proposition, and its proofs are of type [T]. Chapter 12 goes into more detail about the theoretical differences between [Prop] and [Set]. For now, we will simply follow common intuitions about what a proof is. +%\smallskip{}%Recall that [unit] is the type with only one value, and [True] is the proposition that always holds. Despite this superficial difference between the two concepts, in both cases we can use the same inductive definition mechanism. The connection goes further than this. We see that we arrive at the definition of [True] by replacing [unit] by [True], [tt] by [I], and [Set] by [Prop]. The first two of these differences are superficial changes of names, while the third difference is the crucial one for separating programs from proofs. A term [T] of type [Set] is a type of programs, and a term of type [T] is a program. A term [T] of type [Prop] is a logical proposition, and its proofs are of type [T]. Chapter 12 goes into more detail about the theoretical differences between [Prop] and [Set]. For now, we will simply follow common intuitions about what a proof is. The type [unit] has one value, [tt]. The type [True] has one proof, [I]. Why distinguish between these two types? Many people who have read about Curry-Howard in an abstract context and not put it to use in proof engineering answer that the two types in fact _should not_ be distinguished. There is a certain aesthetic appeal to this point of view, but I want to argue that it is best to treat Curry-Howard very loosely in practical proving. There are Coq-specific reasons for preferring the distinction, involving efficient compilation and avoidance of paradoxes in the presence of classical math, but I will argue that there is a more general principle that should lead us to avoid conflating programming and proving. @@ -84,12 +83,11 @@ (** There is also a predicate [False], which is the Curry-Howard mirror image of [Empty_set] from the last chapter. *) Print False. - (** [[ + (** %\vspace{-.15in}%[[ Inductive False : Prop := - ]] - We can conclude anything from [False], doing case analysis on a proof of [False] in the same way we might do case analysis on, say, a natural number. Since there are no cases to consider, any such case analysis succeeds immediately in proving the goal. *) + %\smallskip{}%We can conclude anything from [False], doing case analysis on a proof of [False] in the same way we might do case analysis on, say, a natural number. Since there are no cases to consider, any such case analysis succeeds immediately in proving the goal. *) Theorem False_imp : False -> 2 + 2 = 5. (* begin thide *) @@ -129,10 +127,9 @@ (** %\vspace{-.15in}% [[ not = fun A : Prop => A -> False : Prop -> Prop - ]] - We see that [not] is just shorthand for implication of [False]. We can use that fact explicitly in proofs. The syntax [~ P] expands to [not P]. *) + %\smallskip{}%We see that [not] is just shorthand for implication of [False]. We can use that fact explicitly in proofs. The syntax [~ P] expands to [not P]. *) Theorem arith_neq' : ~ (2 + 2 = 5). (* begin thide *) @@ -150,12 +147,11 @@ (** We also have conjunction, which we introduced in the last chapter. *) Print and. -(** [[ +(** %\vspace{-.15in}%[[ Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> A /\ B - ]] - The interested reader can check that [and] has a Curry-Howard equivalent called %\index{Gallina terms!prod}%[prod], the type of pairs. However, it is generally most convenient to reason about conjunction using tactics. An explicit proof of commutativity of [and] illustrates the usual suspects for such tasks. The operator [/\] is an infix shorthand for [and]. *) + %\smallskip{}%The interested reader can check that [and] has a Curry-Howard equivalent called %\index{Gallina terms!prod}%[prod], the type of pairs. However, it is generally most convenient to reason about conjunction using tactics. An explicit proof of commutativity of [and] illustrates the usual suspects for such tasks. The operator [/\] is an infix shorthand for [and]. *) Theorem and_comm : P /\ Q -> Q /\ P. @@ -174,7 +170,8 @@ Every proof of a conjunction provides proofs for both conjuncts, so we get a single subgoal reflecting that. We can proceed by splitting this subgoal into a case for each conjunct of [Q /\ P].%\index{tactics!split}% *) split. -(** 2 subgoals +(** [[ +2 subgoals H : P H0 : Q @@ -197,13 +194,12 @@ (** Coq disjunction is called %\index{Gallina terms!or}%[or] and abbreviated with the infix operator [\/]. *) Print or. -(** [[ +(** %\vspace{-.15in}%[[ Inductive or (A : Prop) (B : Prop) : Prop := or_introl : A -> A \/ B | or_intror : B -> A \/ B - ]] -We see that there are two ways to prove a disjunction: prove the first disjunct or prove the second. The Curry-Howard analogue of this is the Coq %\index{Gallina terms!sum}%[sum] type. We can demonstrate the main tactics here with another proof of commutativity. *) +%\smallskip{}%We see that there are two ways to prov a disjunction: prove the first disjunct or prove the second. The Curry-Howard analogue of this is the Coq %\index{Gallina terms!sum}%[sum] type. We can demonstrate the main tactics here with another proof of commutativity. *) Theorem or_comm : P \/ Q -> Q \/ P. @@ -372,13 +368,12 @@ %\index{existential quantification}\index{Gallina terms!exists}\index{Gallina terms!ex}%Existential quantification is defined in the standard library. *) Print ex. -(** [[ +(** %\vspace{-.15in}%[[ Inductive ex (A : Type) (P : A -> Prop) : Prop := ex_intro : forall x : A, P x -> ex P - ]] - The family [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s. We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x]. As usual, there are tactics that save us from worrying about the low-level details most of the time. We use the equality operator [=], which, depending on the settings in which they learned logic, different people will say either is or is not part of first-order logic. For our purposes, it is. *) + %\smallskip{}%The family [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s. We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x]. As usual, there are tactics that save us from worrying about the low-level details most of the time. We use the equality operator [=], which, depending on the settings in which they learned logic, different people will say either is or is not part of first-order logic. For our purposes, it is. *) Theorem exist1 : exists x : nat, x + 1 = 2. (* begin thide *) @@ -464,12 +459,11 @@ For instance, our definition [isZero] makes the predicate provable only when the argument is [0]. We can see that the concept of equality is somehow implicit in the inductive definition mechanism. The way this is accomplished is similar to the way that logic variables are used in %\index{Prolog}%Prolog, and it is a very powerful mechanism that forms a foundation for formalizing all of mathematics. In fact, though it is natural to think of inductive types as folding in the functionality of equality, in Coq, the true situation is reversed, with equality defined as just another inductive type!%\index{Gallina terms!eq}\index{Gallina terms!refl\_equal}% *) Print eq. -(** [[ +(** %\vspace{-.15in}%[[ Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x - ]] - Behind the scenes, uses of infix [=] are expanded to instances of [eq]. We see that [eq] has both a parameter [x] that is fixed and an extra unnamed argument of the same type. The type of [eq] allows us to state any equalities, even those that are provably false. However, examining the type of equality's sole constructor [eq_refl], we see that we can only _prove_ equality when its two arguments are syntactically equal. This definition turns out to capture all of the basic properties of equality, and the equality-manipulating tactics that we have seen so far, like [reflexivity] and [rewrite], are implemented treating [eq] as just another inductive type with a well-chosen definition. Another way of stating that definition is: equality is defined as the least reflexive relation. + %\smallskip{}%Behind the scenes, uses of infix [=] are expanded to instances of [eq]. We see that [eq] has both a parameter [x] that is fixed and an extra unnamed argument of the same type. The type of [eq] allows us to state any equalities, even those that are provably false. However, examining the type of equality's sole constructor [eq_refl], we see that we can only _prove_ equality when its two arguments are syntactically equal. This definition turns out to capture all of the basic properties of equality, and the equality-manipulating tactics that we have seen so far, like [reflexivity] and [rewrite], are implemented treating [eq] as just another inductive type with a well-chosen definition. Another way of stating that definition is: equality is defined as the least reflexive relation. Returning to the example of [isZero], we can see how to work with hypotheses that use this predicate. *) @@ -535,10 +529,9 @@ (** %\vspace{-.15in}% [[ isZero_ind : forall P : nat -> Prop, P 0 -> forall n : nat, isZero n -> P n - ]] - In our last proof script, [destruct] chose to instantiate [P] as [fun n => S n + S n = S (S (S (S n)))]. You can verify for yourself that this specialization of the principle applies to the goal and that the hypothesis [P 0] then matches the subgoal we saw generated. If you are doing a proof and encounter a strange transmutation like this, there is a good chance that you should go back and replace a use of [destruct] with [inversion]. *) + %\smallskip{}%In our last proof script, [destruct] chose to instantiate [P] as [fun n => S n + S n = S (S (S (S n)))]. You can verify for yourself that this specialization of the principle applies to the goal and that the hypothesis [P 0] then matches the subgoal we saw generated. If you are doing a proof and encounter a strange transmutation like this, there is a good chance that you should go back and replace a use of [destruct] with [inversion]. *) (* begin hide *) @@ -685,6 +678,7 @@ [[ IHn : forall m : nat, even n -> even m -> even (n + m) + ]] Unfortunately, the goal mentions [n0] where it would need to mention [n] to match [IHn]. We could keep looking for a way to finish this proof from here, but it turns out that we can make our lives much easier by changing our basic strategy. Instead of inducting on the structure of [n], we should induct _on the structure of one of the [even] proofs_. This technique is commonly called%\index{rule induction}% _rule induction_ in programming language semantics. In the setting of Coq, we have already seen how predicates are defined using the same inductive type mechanism as datatypes, so the fundamental unity of rule induction with "normal" induction is apparent. @@ -788,8 +782,7 @@ At this point it is useful to use a theorem from the standard library, which we also proved with a different name in the last chapter. We can search for a theorem that allows us to rewrite terms of the form [x + S y]. *) SearchRewrite (_ + S _). - -(** [[ +(** %\vspace{-.15in}%[[ plus_n_Sm : forall n m : nat, S (n + m) = n + S m ]] *)
--- a/src/Subset.v Mon Jul 30 13:21:36 2012 -0400 +++ b/src/Subset.v Mon Jul 30 16:50:02 2012 -0400 @@ -83,12 +83,11 @@ (** %\vspace{-.15in}% [[ = 1 : nat - ]] -One aspect in particular of the definition of [pred_strong1] may be surprising. We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions. Let us see what happens if we write this function in the way that at first seems most natural. +%\smallskip{}%One aspect in particular of the definition of [pred_strong1] may be surprising. We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions. Let us see what happens if we write this function in the way that at first seems most natural. -[[ +%\vspace{-.15in}%[[ Definition pred_strong1' (n : nat) (pf : n > 0) : nat := match n with | O => match zgtz pf with end @@ -152,10 +151,9 @@ (** %\vspace{-.15in}% [[ Inductive sig (A : Type) (P : A -> Prop) : Type := exist : forall x : A, P x -> sig P - ]] -The family [sig] is a Curry-Howard twin of [ex], except that [sig] is in [Type], while [ex] is in [Prop]. That means that [sig] values can survive extraction, while [ex] proofs will always be erased. The actual details of extraction of [sig]s are more subtle, as we will see shortly. +%\smallskip{}%The family [sig] is a Curry-Howard twin of [ex], except that [sig] is in [Type], while [ex] is in [Prop]. That means that [sig] values can survive extraction, while [ex] proofs will always be erased. The actual details of extraction of [sig]s are more subtle, as we will see shortly. We rewrite [pred_strong1], using some syntactic sugar for subset types. *) @@ -301,10 +299,9 @@ exist (fun m : nat => S n' = S m) n' (eq_refl (S n')) end : forall n : nat, n > 0 -> {m : nat | n = S m} - ]] -We see the code we entered, with some proofs filled in. The first proof obligation, the second argument to [False_rec], is filled in with a nasty-looking proof term that we can be glad we did not enter by hand. The second proof obligation is a simple reflexivity proof. *) +%\smallskip{}%We see the code we entered, with some proofs filled in. The first proof obligation, the second argument to [False_rec], is filled in with a nasty-looking proof term that we can be glad we did not enter by hand. The second proof obligation is a simple reflexivity proof. *) Eval compute in pred_strong4 two_gt0. (** %\vspace{-.15in}% [[ @@ -312,7 +309,7 @@ : {m : nat | 2 = S m} ]] - A tactic modifier called %\index{tactics!abstract}%[abstract] can be helpful for producing shorter terms, by automatically abstracting subgoals into named lemmas. *) + %\smallskip{}%A tactic modifier called %\index{tactics!abstract}%[abstract] can be helpful for producing shorter terms, by automatically abstracting subgoals into named lemmas. *) (* begin thide *) Definition pred_strong4' : forall n : nat, n > 0 -> {m : nat | n = S m}. @@ -361,7 +358,7 @@ : {m : nat | 2 = S m} ]] - One other alternative is worth demonstrating. Recent Coq versions include a facility called %\index{Program}%[Program] that streamlines this style of definition. Here is a complete implementation using [Program].%\index{Vernacular commands!Obligation Tactic}\index{Vernacular commands!Program Definition}% *) + %\smallskip{}%One other alternative is worth demonstrating. Recent Coq versions include a facility called %\index{Program}%[Program] that streamlines this style of definition. Here is a complete implementation using [Program].%\index{Vernacular commands!Obligation Tactic}\index{Vernacular commands!Program Definition}% *) Obligation Tactic := crush. @@ -379,7 +376,7 @@ : {m : nat | 2 = S m} ]] -In this case, we see that the new definition yields the same computational behavior as before. *) +%\smallskip{}%In this case, we see that the new definition yields the same computational behavior as before. *) (** * Decidable Proposition Types *) @@ -423,9 +420,8 @@ = No : {2 = 3} + {2 <> 3} ]] - *) -(** Note that the %\coqdocnotation{%#<tt>#Yes#</tt>#%}% and %\coqdocnotation{%#<tt>#No#</tt>#%}% notations are hiding proofs establishing the correctness of the outputs. +%\smallskip{}%Note that the %\coqdocnotation{%#<tt>#Yes#</tt>#%}% and %\coqdocnotation{%#<tt>#No#</tt>#%}% notations are hiding proofs establishing the correctness of the outputs. Our definition extracts to reasonable OCaml code. *) @@ -532,9 +528,8 @@ = No : {In 3 (1 :: 2 :: nil)} + {~ In 3 (1 :: 2 :: nil)} ]] - *) -(** [In_dec] has a reasonable extraction to OCaml. *) +%\smallskip{}%[In_dec] has a reasonable extraction to OCaml. *) Extraction In_dec. (* end thide *) @@ -601,16 +596,15 @@ : {{m | 0 = S m}} ]] - Because we used [maybe], one valid implementation of the type we gave [pred_strong7] would return [??] in every case. We can strengthen the type to rule out such vacuous implementations, and the type family %\index{Gallina terms!sumor}%[sumor] from the standard library provides the easiest starting point. For type [A] and proposition [B], [A + {B}] desugars to [sumor A B], whose values are either values of [A] or proofs of [B]. *) + %\smallskip{}%Because we used [maybe], one valid implementation of the type we gave [pred_strong7] would return [??] in every case. We can strengthen the type to rule out such vacuous implementations, and the type family %\index{Gallina terms!sumor}%[sumor] from the standard library provides the easiest starting point. For type [A] and proposition [B], [A + {B}] desugars to [sumor A B], whose values are either values of [A] or proofs of [B]. *) Print sumor. (** %\vspace{-.15in}% [[ Inductive sumor (A : Type) (B : Prop) : Type := inleft : A -> A + {B} | inright : B -> A + {B} ]] -*) -(** We add notations for easy use of the [sumor] constructors. The second notation is specialized to [sumor]s whose [A] parameters are instantiated with regular subset types, since this is how we will use [sumor] below. *) +%\smallskip{}%We add notations for easy use of the [sumor] constructors. The second notation is specialized to [sumor]s whose [A] parameters are instantiated with regular subset types, since this is how we will use [sumor] below. *) Notation "!!" := (inright _ _). Notation "[|| x ||]" := (inleft _ [x]). @@ -781,9 +775,8 @@ = ?? : {{t | hasType (Plus (Nat 1) (Bool false)) t}} ]] - *) -(** The type checker also extracts to some reasonable OCaml code. *) +%\smallskip{}%The type checker also extracts to some reasonable OCaml code. *) Extraction typeCheck. @@ -936,4 +929,4 @@ {(forall t : type, ~ hasType (Plus (Nat 1) (Bool false)) t)} ]] -The results of simplifying calls to [typeCheck'] look deceptively similar to the results for [typeCheck], but now the types of the results provide more information. *) +%\smallskip{}%The results of simplifying calls to [typeCheck'] look deceptively similar to the results for [typeCheck], but now the types of the results provide more information. *)