Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 448:2740b8a23cce
Proofreading pass through Chapter 3
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 17 Aug 2012 14:19:59 -0400 |
parents | 89c67796754e |
children | 4320c1a967c2 |
comparison
equal
deleted
inserted
replaced
447:9e3333bd08a1 | 448:2740b8a23cce |
---|---|
102 [[ | 102 [[ |
103 tt = tt | 103 tt = tt |
104 ]] | 104 ]] |
105 *) | 105 *) |
106 | 106 |
107 (** ...which we can discharge trivially. *) | 107 (** %\noindent{}%...which we can discharge trivially. *) |
108 | 108 |
109 reflexivity. | 109 reflexivity. |
110 Qed. | 110 Qed. |
111 (* end thide *) | 111 (* end thide *) |
112 | 112 |
158 | 158 |
159 (** We employ [match] pattern matching as in the last chapter. Since we match on a value whose type has no constructors, there is no need to provide any branches. This idiom may look familiar; we employed it with proofs of [False] in the last section. In fact, [Empty_set] is the Curry-Howard equivalent of [False]. As for why [Empty_set] starts with a capital letter and not a lowercase letter like [unit] does, we must refer the reader to the authors of the Coq standard library, to which we try to be faithful. | 159 (** We employ [match] pattern matching as in the last chapter. Since we match on a value whose type has no constructors, there is no need to provide any branches. This idiom may look familiar; we employed it with proofs of [False] in the last section. In fact, [Empty_set] is the Curry-Howard equivalent of [False]. As for why [Empty_set] starts with a capital letter and not a lowercase letter like [unit] does, we must refer the reader to the authors of the Coq standard library, to which we try to be faithful. |
160 | 160 |
161 %\medskip% | 161 %\medskip% |
162 | 162 |
163 Moving up the ladder of complexity, we can define the booleans:%\index{Gallina terms!bool}\index{Gallina terms!true}\index{Gallina terms!false}% *) | 163 Moving up the ladder of complexity, we can define the Booleans:%\index{Gallina terms!bool}\index{Gallina terms!true}\index{Gallina terms!false}% *) |
164 | 164 |
165 Inductive bool : Set := | 165 Inductive bool : Set := |
166 | true | 166 | true |
167 | false. | 167 | false. |
168 | 168 |
169 (** We can use less vacuous pattern matching to define boolean negation.%\index{Gallina terms!negb}% *) | 169 (** We can use less vacuous pattern matching to define Boolean negation.%\index{Gallina terms!negb}% *) |
170 | 170 |
171 Definition negb (b : bool) : bool := | 171 Definition negb (b : bool) : bool := |
172 match b with | 172 match b with |
173 | true => false | 173 | true => false |
174 | false => true | 174 | false => true |
207 | 207 |
208 destruct b; reflexivity. | 208 destruct b; reflexivity. |
209 Qed. | 209 Qed. |
210 (* end thide *) | 210 (* end thide *) |
211 | 211 |
212 (** Another theorem about booleans illustrates another useful tactic.%\index{tactics!discriminate}% *) | 212 (** Another theorem about Booleans illustrates another useful tactic.%\index{tactics!discriminate}% *) |
213 | 213 |
214 Theorem negb_ineq : forall b : bool, negb b <> b. | 214 Theorem negb_ineq : forall b : bool, negb b <> b. |
215 (* begin thide *) | 215 (* begin thide *) |
216 destruct b; discriminate. | 216 destruct b; discriminate. |
217 Qed. | 217 Qed. |
218 (* end thide *) | 218 (* end thide *) |
219 | 219 |
220 (** [discriminate] is used to prove that two values of an inductive type are not equal, whenever the values are formed with different constructors. In this case, the different constructors are [true] and [false]. | 220 (** The [discriminate] tactic is used to prove that two values of an inductive type are not equal, whenever the values are formed with different constructors. In this case, the different constructors are [true] and [false]. |
221 | 221 |
222 At this point, it is probably not hard to guess what the underlying induction principle for [bool] is. *) | 222 At this point, it is probably not hard to guess what the underlying induction principle for [bool] is. *) |
223 | 223 |
224 Check bool_ind. | 224 Check bool_ind. |
225 (** [bool_ind : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b] *) | 225 (** [bool_ind : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b] *) |
303 | 303 |
304 (** Now the conclusion is [S (plus n O) = S n]. Using our inductive hypothesis: *) | 304 (** Now the conclusion is [S (plus n O) = S n]. Using our inductive hypothesis: *) |
305 | 305 |
306 rewrite IHn. | 306 rewrite IHn. |
307 | 307 |
308 (** ...we get a trivial conclusion [S n = S n]. *) | 308 (** %\noindent{}%...we get a trivial conclusion [S n = S n]. *) |
309 | 309 |
310 reflexivity. | 310 reflexivity. |
311 | 311 |
312 (** Not much really went on in this proof, so the [crush] tactic from the [CpdtTactics] module can prove this theorem automatically. *) | 312 (** Not much really went on in this proof, so the [crush] tactic from the [CpdtTactics] module can prove this theorem automatically. *) |
313 | 313 |
597 : forall (P : even_list -> Prop) (P0 : odd_list -> Prop), | 597 : forall (P : even_list -> Prop) (P0 : odd_list -> Prop), |
598 P ENil -> | 598 P ENil -> |
599 (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) -> | 599 (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) -> |
600 (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> | 600 (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> |
601 forall e : even_list, P e | 601 forall e : even_list, P e |
602 | |
603 ]] | 602 ]] |
604 | 603 |
605 This is the principle we wanted in the first place. There is one more wrinkle left in using it: the [induction] tactic will not apply it for us automatically. It will be helpful to look at how to prove one of our past examples without using [induction], so that we can then generalize the technique to mutual inductive types.%\index{tactics!apply}% *) | 604 This is the principle we wanted in the first place. There is one more wrinkle left in using it: the [induction] tactic will not apply it for us automatically. It will be helpful to look at how to prove one of our past examples without using [induction], so that we can then generalize the technique to mutual inductive types.%\index{tactics!apply}% *) |
606 | 605 |
607 Theorem n_plus_O' : forall n : nat, plus n O = n. | 606 Theorem n_plus_O' : forall n : nat, plus n O = n. |
633 Inductive pformula : Set := | 632 Inductive pformula : Set := |
634 | Truth : pformula | 633 | Truth : pformula |
635 | Falsehood : pformula | 634 | Falsehood : pformula |
636 | Conjunction : pformula -> pformula -> pformula. | 635 | Conjunction : pformula -> pformula -> pformula. |
637 | 636 |
638 (** A key distinction here is between, for instance, the _syntax_ [Truth] and its _semantics_ [True]. We can make the semantics explicit with a recursive function. This function uses the infix operator %\index{Gallina operators!/\textbackslash}%[/\], which desugars to uses of the type family %\index{Gallina terms!and}%[and] from the standard library. The family [and] implements conjunction, the [Prop] Curry-Howard analogue of the usual pair type from functional programming (which is the type family %\index{Gallina terms!prod}%[prod] in Coq's standard library). *) | 637 (* begin hide *) |
638 (* begin thide *) | |
639 Definition prod' := prod. | |
640 (* end thide *) | |
641 (* end hide *) | |
642 | |
643 (** A key distinction here is between, for instance, the _syntax_ [Truth] and its _semantics_ [True]. We can make the semantics explicit with a recursive function. This function uses the infix operator %\index{Gallina operators!/\textbackslash}%[/\], which desugared to uses of the type family %\index{Gallina terms!and}%[and] from the standard library. The family [and] implements conjunction, the [Prop] Curry-Howard analogue of the usual pair type from functional programming (which is the type family %\index{Gallina terms!prod}%[prod] in Coq's standard library). *) | |
639 | 644 |
640 Fixpoint pformulaDenote (f : pformula) : Prop := | 645 Fixpoint pformulaDenote (f : pformula) : Prop := |
641 match f with | 646 match f with |
642 | Truth => True | 647 | Truth => True |
643 | Falsehood => False | 648 | Falsehood => False |
987 | 992 |
988 In addition to the definition of [and] itself, we get information on %\index{implicit arguments}%implicit arguments (and some other information that we omit here). The implicit argument information tells us that we build a proof of a conjunction by calling the constructor [conj] on proofs of the conjuncts, with no need to include the types of those proofs as explicit arguments. | 993 In addition to the definition of [and] itself, we get information on %\index{implicit arguments}%implicit arguments (and some other information that we omit here). The implicit argument information tells us that we build a proof of a conjunction by calling the constructor [conj] on proofs of the conjuncts, with no need to include the types of those proofs as explicit arguments. |
989 | 994 |
990 %\medskip% | 995 %\medskip% |
991 | 996 |
992 Now we create a section for our induction principle, following the same basic plan as in the last section of this chapter. *) | 997 Now we create a section for our induction principle, following the same basic plan as in the previous section of this chapter. *) |
993 | 998 |
994 Section nat_tree_ind'. | 999 Section nat_tree_ind'. |
995 Variable P : nat_tree -> Prop. | 1000 Variable P : nat_tree -> Prop. |
996 | 1001 |
997 Hypothesis NLeaf'_case : P NLeaf'. | 1002 Hypothesis NLeaf'_case : P NLeaf'. |
1161 | 1166 |
1162 This is the point in the proof where we apply some creativity. We define a function whose utility will become clear soon. *) | 1167 This is the point in the proof where we apply some creativity. We define a function whose utility will become clear soon. *) |
1163 | 1168 |
1164 Definition toProp (b : bool) := if b then True else False. | 1169 Definition toProp (b : bool) := if b then True else False. |
1165 | 1170 |
1166 (** It is worth recalling the difference between the lowercase and uppercase versions of truth and falsehood: [True] and [False] are logical propositions, while [true] and [false] are boolean values that we can case-analyze. We have defined [toProp] such that our conclusion of [False] is computationally equivalent to [toProp false]. Thus, the %\index{tactics!change}%[change] tactic will let us change the conclusion to [toProp false]. The general form [change e] replaces the conclusion with [e], whenever Coq's built-in computation rules suffice to establish the equivalence of [e] with the original conclusion. *) | 1171 (** It is worth recalling the difference between the lowercase and uppercase versions of truth and falsehood: [True] and [False] are logical propositions, while [true] and [false] are Boolean values that we can case-analyze. We have defined [toProp] such that our conclusion of [False] is computationally equivalent to [toProp false]. Thus, the %\index{tactics!change}%[change] tactic will let us change the conclusion to [toProp false]. The general form [change e] replaces the conclusion with [e], whenever Coq's built-in computation rules suffice to establish the equivalence of [e] with the original conclusion. *) |
1167 | 1172 |
1168 change (toProp false). | 1173 change (toProp false). |
1169 (** %\vspace{-.15in}%[[ | 1174 (** %\vspace{-.15in}%[[ |
1170 H : true = false | 1175 H : true = false |
1171 ============================ | 1176 ============================ |
1172 toProp false | 1177 toProp false |
1173 ]] | 1178 ]] |
1174 | 1179 |
1175 Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite, using the notation [<-] to request to replace the righthand side the equality with the lefthand side.%\index{tactics!rewrite}% *) | 1180 Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite, using the notation [<-] to request to replace the righthand side of the equality with the lefthand side.%\index{tactics!rewrite}% *) |
1176 | 1181 |
1177 rewrite <- H. | 1182 rewrite <- H. |
1178 (** %\vspace{-.15in}%[[ | 1183 (** %\vspace{-.15in}%[[ |
1179 H : true = false | 1184 H : true = false |
1180 ============================ | 1185 ============================ |