Mercurial > cpdt > repo
comparison src/MoreDep.v @ 475:1fd4109f7b31
Batch of changes based on proofreader feedback
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 22 Oct 2012 14:23:52 -0400 |
| parents | 4320c1a967c2 |
| children | 417450ccceda |
comparison
equal
deleted
inserted
replaced
| 474:d9e1fb184672 | 475:1fd4109f7b31 |
|---|---|
| 104 | 104 |
| 105 << | 105 << |
| 106 Error: Non exhaustive pattern-matching: no clause found for pattern Nil | 106 Error: Non exhaustive pattern-matching: no clause found for pattern Nil |
| 107 >> | 107 >> |
| 108 | 108 |
| 109 Unlike in ML, we cannot use inexhaustive pattern matching, because there is no conception of a <<Match>> exception to be thrown. In fact, recent versions of Coq _do_ allow this, by implicit translation to a [match] that considers all constructors. It is educational to discover that encoding ourselves directly. We might try using an [in] clause somehow. | 109 Unlike in ML, we cannot use inexhaustive pattern matching, because there is no conception of a <<Match>> exception to be thrown. In fact, recent versions of Coq _do_ allow this, by implicit translation to a [match] that considers all constructors. It is educational to discover such an encoding for ourselves. We might try using an [in] clause somehow. |
| 110 | 110 |
| 111 [[ | 111 [[ |
| 112 Definition hd n (ls : ilist (S n)) : A := | 112 Definition hd n (ls : ilist (S n)) : A := |
| 113 match ls in (ilist (S n)) with | 113 match ls in (ilist (S n)) with |
| 114 | Cons _ h _ => h | 114 | Cons _ h _ => h |
| 376 User error: e1 is used in hypothesis e | 376 User error: e1 is used in hypothesis e |
| 377 >> | 377 >> |
| 378 | 378 |
| 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. | 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. |
| 380 | 380 |
| 381 For our current proof, we can use a tactic [dep_destruct]%\index{tactics!dep\_destruct}% defined in the book [CpdtTactics] module. General elimination/inversion of dependently typed hypotheses is undecidable, since it must be implemented with [match] expressions that have the restriction on [in] clauses that we have already discussed. 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 [dep_destruct]'s implementation in Ltac, 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.) *) | 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, since it must be implemented with [match] expressions that have the restriction on [in] clauses that we have already discussed. 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 [dep_destruct]'s implementation in Ltac, 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 | 382 |
| 383 dep_destruct (cfold e1). | 383 dep_destruct (cfold e1). |
| 384 | 384 |
| 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]. | 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]. |
| 386 | 386 |
| 403 (** With this example, we get a first taste of how to build automated proofs that adapt automatically to changes in function definitions. *) | 403 (** With this example, we get a first taste of how to build automated proofs that adapt automatically to changes in function definitions. *) |
| 404 | 404 |
| 405 | 405 |
| 406 (** * Dependently Typed Red-Black Trees *) | 406 (** * Dependently Typed Red-Black Trees *) |
| 407 | 407 |
| 408 (** Red-black trees are a favorite purely functional data structure with an interesting invariant. We can use dependent types to enforce that operations on red-black trees preserve the invariant. For simplicity, we specialize our red-black trees to represent sets of [nat]s. *) | 408 (** Red-black trees are a favorite purely functional data structure with an interesting invariant. We can use dependent types to guarantee that operations on red-black trees preserve the invariant. For simplicity, we specialize our red-black trees to represent sets of [nat]s. *) |
| 409 | 409 |
| 410 Inductive color : Set := Red | Black. | 410 Inductive color : Set := Red | Black. |
| 411 | 411 |
| 412 Inductive rbtree : color -> nat -> Set := | 412 Inductive rbtree : color -> nat -> Set := |
| 413 | Leaf : rbtree Black 0 | 413 | Leaf : rbtree Black 0 |
| 1101 | 1101 |
| 1102 Variable P' : string -> Prop. | 1102 Variable P' : string -> Prop. |
| 1103 Variable P'_dec : forall n' : nat, n' > n | 1103 Variable P'_dec : forall n' : nat, n' > n |
| 1104 -> {P' (substring n' (length s - n') s)} | 1104 -> {P' (substring n' (length s - n') s)} |
| 1105 + {~ P' (substring n' (length s - n') s)}. | 1105 + {~ P' (substring n' (length s - n') s)}. |
| 1106 | |
| 1106 (** When we use [dec_star''], we will instantiate [P'_dec] with a function for continuing the search for more instances of [P] in [s]. *) | 1107 (** When we use [dec_star''], we will instantiate [P'_dec] with a function for continuing the search for more instances of [P] in [s]. *) |
| 1107 | 1108 |
| 1108 (** Now we come to [dec_star''] itself. It takes as an input a natural [l] that records how much of the string has been searched so far, as we did for [split']. The return type expresses that [dec_star''] is looking for an index into [s] that splits [s] into a nonempty prefix and a suffix, such that the prefix satisfies [P] and the suffix satisfies [P']. *) | 1109 (** Now we come to [dec_star''] itself. It takes as an input a natural [l] that records how much of the string has been searched so far, as we did for [split']. The return type expresses that [dec_star''] is looking for an index into [s] that splits [s] into a nonempty prefix and a suffix, such that the prefix satisfies [P] and the suffix satisfies [P']. *) |
| 1109 | 1110 |
| 1110 Definition dec_star'' : forall l : nat, | 1111 Definition dec_star'' : forall l : nat, |