## Mercurial > cpdt > repo

### comparison src/MoreDep.v @ 499:2d7ce9e011f4

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Pass through Chapter 8

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Fri, 01 Feb 2013 17:19:15 -0500 |

parents | 5025a401ad9e |

children | ed829eaa91b2 |

comparison

equal
deleted
inserted
replaced

498:e3b90f0279f6 | 499:2d7ce9e011f4 |
---|---|

253 We run again into the problem of not being able to specify non-variable arguments in [in] clauses. The problem would just be hopeless without a use of an [in] clause, though, since the result type of the [match] depends on an argument to [exp]. Our solution will be to use a more general type, as we did for [hd]. First, we define a type-valued function to use in assigning a type to [pairOut]. *) | 253 We run again into the problem of not being able to specify non-variable arguments in [in] clauses. The problem would just be hopeless without a use of an [in] clause, though, since the result type of the [match] depends on an argument to [exp]. Our solution will be to use a more general type, as we did for [hd]. First, we define a type-valued function to use in assigning a type to [pairOut]. *) |

254 | 254 |

255 (* EX: Define a function [pairOut : forall t1 t2, exp (Prod t1 t2) -> option (exp t1 * exp t2)] *) | 255 (* EX: Define a function [pairOut : forall t1 t2, exp (Prod t1 t2) -> option (exp t1 * exp t2)] *) |

256 | 256 |

257 (* begin thide *) | 257 (* begin thide *) |

258 Definition pairOutType (t : type) := | 258 Definition pairOutType (t : type) := option (match t with |

259 match t with | 259 | Prod t1 t2 => exp t1 * exp t2 |

260 | Prod t1 t2 => option (exp t1 * exp t2) | 260 | _ => unit |

261 | _ => unit | 261 end). |

262 end. | 262 |

263 | 263 (** When passed a type that is a product, [pairOutType] returns our final desired type. On any other input type, [pairOutType] returns the harmless [option unit], since we do not care about extracting components of non-pairs. Now [pairOut] is easy to write. *) |

264 (** When passed a type that is a product, [pairOutType] returns our final desired type. On any other input type, [pairOutType] returns [unit], since we do not care about extracting components of non-pairs. Now we can write another helper function to provide the default behavior of [pairOut], which we will apply for inputs that are not literal pairs. *) | |

265 | |

266 Definition pairOutDefault (t : type) := | |

267 match t return (pairOutType t) with | |

268 | Prod _ _ => None | |

269 | _ => tt | |

270 end. | |

271 | |

272 (** Now [pairOut] is deceptively easy to write. *) | |

273 | 264 |

274 Definition pairOut t (e : exp t) := | 265 Definition pairOut t (e : exp t) := |

275 match e in (exp t) return (pairOutType t) with | 266 match e in (exp t) return (pairOutType t) with |

276 | Pair _ _ e1 e2 => Some (e1, e2) | 267 | Pair _ _ e1 e2 => Some (e1, e2) |

277 | _ => pairOutDefault _ | 268 | _ => None |

278 end. | 269 end. |

279 (* end thide *) | 270 (* end thide *) |

280 | 271 |

281 (** There is one important subtlety in this definition. Coq allows us to use convenient ML-style pattern matching notation, but, internally and in proofs, we see that patterns are expanded out completely, matching one level of inductive structure at a time. Thus, the default case in the [match] above expands out to one case for each constructor of [exp] besides [Pair], and the underscore in [pairOutDefault _] is resolved differently in each case. From an ML or Haskell programmer's perspective, what we have here is type inference determining which code is run (returning either [None] or [tt]), which goes beyond what is possible with type inference guiding parametric polymorphism in Hindley-Milner languages%\index{Hindley-Milner}%, but is similar to what goes on with Haskell type classes%\index{type classes}%. | 272 (** With [pairOut] available, we can write [cfold] in a straightforward way. There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden. In some places, we see that Coq's [match] annotation inference is too smart for its own good, and we have to turn that inference off with explicit [return] clauses. *) |

282 | |

283 With [pairOut] available, we can write [cfold] in a straightforward way. There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden. In some places, we see that Coq's [match] annotation inference is too smart for its own good, and we have to turn that inference off with explicit [return] clauses. *) | |

284 | 273 |

285 Fixpoint cfold t (e : exp t) : exp t := | 274 Fixpoint cfold t (e : exp t) : exp t := |

286 match e with | 275 match e with |

287 | NConst n => NConst n | 276 | NConst n => NConst n |

288 | Plus e1 e2 => | 277 | Plus e1 e2 => |

376 User error: e1 is used in hypothesis e | 365 User error: e1 is used in hypothesis e |

377 >> | 366 >> |

378 | 367 |

379 Coq gives us another cryptic error message. Like so many others, this one basically means that Coq is not able to build some proof about dependent types. It is hard to generate helpful and specific error messages for problems like this, since that would require some kind of understanding of the dependency structure of a piece of code. We will encounter many examples of case-specific tricks for recovering from errors like this one. | 368 Coq gives us another cryptic error message. Like so many others, this one basically means that Coq is not able to build some proof about dependent types. It is hard to generate helpful and specific error messages for problems like this, since that would require some kind of understanding of the dependency structure of a piece of code. We will encounter many examples of case-specific tricks for recovering from errors like this one. |

380 | 369 |

381 For our current proof, we can use a tactic [dep_destruct]%\index{tactics!dep\_destruct}% defined in the book's [CpdtTactics] module. General elimination/inversion of dependently typed hypotheses is undecidable, as witnessed by a simple reduction to the known-undecidable problem of higher-order unification, which has come up a few times already. The tactic [dep_destruct] makes a best effort to handle some common cases, relying upon the more primitive %\index{tactics!dependent destruction}%[dependent destruction] tactic that comes with Coq. In a future chapter, we will learn about the explicit manipulation of equality proofs that is behind [dependent destruction]'s implementation, but for now, we treat it as a useful black box. (In Chapter 12, we will also see how [dependent destruction] forces us to make a larger philosophical commitment about our logic than we might like, and we will see some workarounds.) *) | 370 For our current proof, we can use a tactic [dep_destruct]%\index{tactics!dep\_destruct}% defined in the book's [CpdtTactics] module. General elimination/inversion of dependently typed hypotheses is undecidable, as witnessed by a simple reduction from the known-undecidable problem of higher-order unification, which has come up a few times already. The tactic [dep_destruct] makes a best effort to handle some common cases, relying upon the more primitive %\index{tactics!dependent destruction}%[dependent destruction] tactic that comes with Coq. In a future chapter, we will learn about the explicit manipulation of equality proofs that is behind [dependent destruction]'s implementation, but for now, we treat it as a useful black box. (In Chapter 12, we will also see how [dependent destruction] forces us to make a larger philosophical commitment about our logic than we might like, and we will see some workarounds.) *) |

382 | 371 |

383 dep_destruct (cfold e1). | 372 dep_destruct (cfold e1). |

384 | 373 |

385 (** This successfully breaks the subgoal into 5 new subgoals, one for each constructor of [exp] that could produce an [exp Nat]. Note that [dep_destruct] is successful in ruling out the other cases automatically, in effect automating some of the work that we have done manually in implementing functions like [hd] and [pairOut]. | 374 (** This successfully breaks the subgoal into 5 new subgoals, one for each constructor of [exp] that could produce an [exp Nat]. Note that [dep_destruct] is successful in ruling out the other cases automatically, in effect automating some of the work that we have done manually in implementing functions like [hd] and [pairOut]. |

386 | 375 |