Mercurial > cpdt > repo
comparison src/Predicates.v @ 494:07f2fb4d9b36
Pass through Chapter 4
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 19 Jan 2013 10:45:04 -0500 |
| parents | 31258618ef73 |
| children | 8303abe4a61f |
comparison
equal
deleted
inserted
replaced
| 493:4a663981b699 | 494:07f2fb4d9b36 |
|---|---|
| 458 (* end thide *) | 458 (* end thide *) |
| 459 Qed. | 459 Qed. |
| 460 | 460 |
| 461 (** We can call [isZero] a%\index{judgment}% _judgment_, in the sense often used in the semantics of programming languages. Judgments are typically defined in the style of%\index{natural deduction}% _natural deduction_, where we write a number of%\index{inference rules}% _inference rules_ with premises appearing above a solid line and a conclusion appearing below the line. In this example, the sole constructor [IsZero] of [isZero] can be thought of as the single inference rule for deducing [isZero], with nothing above the line and [isZero 0] below it. The proof of [isZero_zero] demonstrates how we can apply an inference rule. (Readers not familiar with formal semantics should not worry about not following this paragraph!) | 461 (** We can call [isZero] a%\index{judgment}% _judgment_, in the sense often used in the semantics of programming languages. Judgments are typically defined in the style of%\index{natural deduction}% _natural deduction_, where we write a number of%\index{inference rules}% _inference rules_ with premises appearing above a solid line and a conclusion appearing below the line. In this example, the sole constructor [IsZero] of [isZero] can be thought of as the single inference rule for deducing [isZero], with nothing above the line and [isZero 0] below it. The proof of [isZero_zero] demonstrates how we can apply an inference rule. (Readers not familiar with formal semantics should not worry about not following this paragraph!) |
| 462 | 462 |
| 463 The definition of [isZero] differs in an important way from all of the other inductive definitions that we have seen in this and the previous chapter. Instead of writing just [Set] or [Prop] after the colon, here we write [nat -> Prop]. We saw examples of parameterized types like [list], but there the parameters appeared with names _before_ the colon. Every constructor of a parameterized inductive type must have a range type that uses the same parameter, whereas the form we use here enables us to use different arguments to the type for different constructors. | 463 The definition of [isZero] differs in an important way from all of the other inductive definitions that we have seen in this and the previous chapter. Instead of writing just [Set] or [Prop] after the colon, here we write [nat -> Prop]. We saw examples of parameterized types like [list], but there the parameters appeared with names _before_ the colon. Every constructor of a parameterized inductive type must have a range type that uses the same parameter, whereas the form we use here enables us to choose different arguments to the type for different constructors. |
| 464 | 464 |
| 465 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 (but worry not if not familiar with 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}% *) | 465 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 (but worry not if not familiar with 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}% *) |
| 466 | 466 |
| 467 Print eq. | 467 Print eq. |
| 468 (** %\vspace{-.15in}%[[ | 468 (** %\vspace{-.15in}%[[ |