Mercurial > cpdt > repo
comparison src/MoreDep.v @ 448:2740b8a23cce
Proofreading pass through Chapter 3
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 17 Aug 2012 14:19:59 -0400 |
| parents | 97c60ffdb998 |
| children | 49bd155dfc52 |
comparison
equal
deleted
inserted
replaced
| 447:9e3333bd08a1 | 448:2740b8a23cce |
|---|---|
| 197 | 197 |
| 198 | Pair : forall t1 t2, exp t1 -> exp t2 -> exp (Prod t1 t2) | 198 | Pair : forall t1 t2, exp t1 -> exp t2 -> exp (Prod t1 t2) |
| 199 | Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1 | 199 | Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1 |
| 200 | Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2. | 200 | Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2. |
| 201 | 201 |
| 202 (** We have a standard algebraic datatype [type], defining a type language of naturals, booleans, and product (pair) types. Then we have the indexed inductive type [exp], where the argument to [exp] tells us the encoded type of an expression. In effect, we are defining the typing rules for expressions simultaneously with the syntax. | 202 (** We have a standard algebraic datatype [type], defining a type language of naturals, Booleans, and product (pair) types. Then we have the indexed inductive type [exp], where the argument to [exp] tells us the encoded type of an expression. In effect, we are defining the typing rules for expressions simultaneously with the syntax. |
| 203 | 203 |
| 204 We can give types and expressions semantics in a new style, based critically on the chance for _type-level computation_. *) | 204 We can give types and expressions semantics in a new style, based critically on the chance for _type-level computation_. *) |
| 205 | 205 |
| 206 Fixpoint typeDenote (t : type) : Set := | 206 Fixpoint typeDenote (t : type) : Set := |
| 207 match t with | 207 match t with |
| 233 (* begin thide *) | 233 (* begin thide *) |
| 234 Definition sumboool := sumbool. | 234 Definition sumboool := sumbool. |
| 235 (* end thide *) | 235 (* end thide *) |
| 236 (* end hide *) | 236 (* end hide *) |
| 237 | 237 |
| 238 (** Despite the fancy type, the function definition is routine. In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype. The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case. Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type. Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns. | 238 (** Despite the fancy type, the function definition is routine. In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype. The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case. Remember that [eq_nat_dec] has a rich dependent type, rather than a simple Boolean type. Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple Boolean from the [sumbool] that [eq_nat_dec] returns. |
| 239 | 239 |
| 240 We can implement our old favorite, a constant folding function, and prove it correct. It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so. Unsurprisingly, a first attempt leads to a type error. | 240 We can implement our old favorite, a constant folding function, and prove it correct. It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so. Unsurprisingly, a first attempt leads to a type error. |
| 241 [[ | 241 [[ |
| 242 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) := | 242 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) := |
| 243 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with | 243 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with |