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 ============================