Mercurial > cpdt > repo
comparison src/MoreDep.v @ 480:f38a3af9dd17
Batch of changes based on proofreader feedback
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 30 Nov 2012 11:57:55 -0500 |
parents | 40a9a36844d6 |
children | 5025a401ad9e |
comparison
equal
deleted
inserted
replaced
479:40a9a36844d6 | 480:f38a3af9dd17 |
---|---|
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 such an encoding for ourselves. 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; the error message above was generated by an older Coq version. It is educational to discover for ourselves the encoding that the most recent Coq versions use. 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 |
156 | 156 |
157 When exactly will Coq accept a dependent pattern match as well-typed? Some other dependently typed languages employ fancy decision procedures to determine when programs satisfy their very expressive types. The situation in Coq is just the opposite. Only very straightforward symbolic rules are applied. Such a design choice has its drawbacks, as it forces programmers to do more work to convince the type checker of program validity. However, the great advantage of a simple type checking algorithm is that its action on _invalid_ programs is easier to understand! | 157 When exactly will Coq accept a dependent pattern match as well-typed? Some other dependently typed languages employ fancy decision procedures to determine when programs satisfy their very expressive types. The situation in Coq is just the opposite. Only very straightforward symbolic rules are applied. Such a design choice has its drawbacks, as it forces programmers to do more work to convince the type checker of program validity. However, the great advantage of a simple type checking algorithm is that its action on _invalid_ programs is easier to understand! |
158 | 158 |
159 We come now to the one rule of dependent pattern matching in Coq. A general dependent pattern match assumes this form (with unnecessary parentheses included to make the syntax easier to parse): | 159 We come now to the one rule of dependent pattern matching in Coq. A general dependent pattern match assumes this form (with unnecessary parentheses included to make the syntax easier to parse): |
160 [[ | 160 [[ |
161 match E in (T x1 ... xn) as y return U with | 161 match E as y in (T x1 ... xn) return U with |
162 | C z1 ... zm => B | 162 | C z1 ... zm => B |
163 | ... | 163 | ... |
164 end | 164 end |
165 ]] | 165 ]] |
166 | 166 |
167 The discriminee is a term [E], a value in some inductive type family [T], which takes [n] arguments. An %\index{in clause}%[in] clause binds an explicit name [xi] for the [i]th argument passed to [T] in the type of [E]. An %\index{as clause}%[as] clause binds the name [y] to refer to the discriminee [E]. | 167 The discriminee is a term [E], a value in some inductive type family [T], which takes [n] arguments. An %\index{as clause}%[as] clause binds the name [y] to refer to the discriminee [E]. An %\index{in clause}%[in] clause binds an explicit name [xi] for the [i]th argument passed to [T] in the type of [E]. |
168 | 168 |
169 We bind these new variables [xi] and [y] so that they may be referred to in [U], a type given in the %\index{return clause}%[return] clause. The overall type of the [match] will be [U], with [E] substituted for [y], and with each [xi] substituted by the actual argument appearing in that position within [E]'s type. | 169 We bind these new variables [y] and [xi] so that they may be referred to in [U], a type given in the %\index{return clause}%[return] clause. The overall type of the [match] will be [U], with [E] substituted for [y], and with each [xi] substituted by the actual argument appearing in that position within [E]'s type. |
170 | 170 |
171 In general, each case of a [match] may have a pattern built up in several layers from the constructors of various inductive type families. To keep this exposition simple, we will focus on patterns that are just single applications of inductive type constructors to lists of variables. Coq actually compiles the more general kind of pattern matching into this more restricted kind automatically, so understanding the typing of [match] requires understanding the typing of [match]es lowered to match one constructor at a time. | 171 In general, each case of a [match] may have a pattern built up in several layers from the constructors of various inductive type families. To keep this exposition simple, we will focus on patterns that are just single applications of inductive type constructors to lists of variables. Coq actually compiles the more general kind of pattern matching into this more restricted kind automatically, so understanding the typing of [match] requires understanding the typing of [match]es lowered to match one constructor at a time. |
172 | 172 |
173 The last piece of the typing rule tells how to type-check a [match] case. A generic constructor application [C z1 ... zm] has some type [T x1' ... xn'], an application of the type family used in [E]'s type, probably with occurrences of the [zi] variables. From here, a simple recipe determines what type we will require for the case body [B]. The type of [B] should be [U] with the following two substitutions applied: we replace [y] (the [as] clause variable) with [C z1 ... zm], and we replace each [xi] (the [in] clause variables) with [xi']. In other words, we specialize the result type based on what we learn based on which pattern has matched the discriminee. | 173 The last piece of the typing rule tells how to type-check a [match] case. A generic constructor application [C z1 ... zm] has some type [T x1' ... xn'], an application of the type family used in [E]'s type, probably with occurrences of the [zi] variables. From here, a simple recipe determines what type we will require for the case body [B]. The type of [B] should be [U] with the following two substitutions applied: we replace [y] (the [as] clause variable) with [C z1 ... zm], and we replace each [xi] (the [in] clause variables) with [xi']. In other words, we specialize the result type based on what we learn based on which pattern has matched the discriminee. |
174 | 174 |
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'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.) *) | 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.) *) |
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 |
387 This is the only new trick we need to learn to complete the proof. We can back up and give a short, automated proof. *) | 387 This is the only new trick we need to learn to complete the proof. We can back up and give a short, automated proof (which again is safe to skip and uses Ltac features not introduced yet). *) |
388 | 388 |
389 Restart. | 389 Restart. |
390 | 390 |
391 induction e; crush; | 391 induction e; crush; |
392 repeat (match goal with | 392 repeat (match goal with |
784 P s1 | 784 P s1 |
785 -> star s2 | 785 -> star s2 |
786 -> star (s1 ++ s2). | 786 -> star (s1 ++ s2). |
787 End star. | 787 End star. |
788 | 788 |
789 (** Now we can make our first attempt at defining a [regexp] type that is indexed by predicates on strings. Here is a reasonable-looking definition that is restricted to constant characters and concatenation. We use the constructor [String], which is the analogue of list cons for the type [string], where [""] is like list nil. | 789 (** Now we can make our first attempt at defining a [regexp] type that is indexed by predicates on strings, such that the index of a [regexp] tells us which language (string predicate) it recognizes. Here is a reasonable-looking definition that is restricted to constant characters and concatenation. We use the constructor [String], which is the analogue of list cons for the type [string], where [""] is like list nil. |
790 [[ | 790 [[ |
791 Inductive regexp : (string -> Prop) -> Set := | 791 Inductive regexp : (string -> Prop) -> Set := |
792 | Char : forall ch : ascii, | 792 | Char : forall ch : ascii, |
793 regexp (fun s => s = String ch "") | 793 regexp (fun s => s = String ch "") |
794 | Concat : forall (P1 P2 : string -> Prop) (r1 : regexp P1) (r2 : regexp P2), | 794 | Concat : forall (P1 P2 : string -> Prop) (r1 : regexp P1) (r2 : regexp P2), |
1113 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)} | 1113 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)} |
1114 + {forall l', S l' <= l | 1114 + {forall l', S l' <= l |
1115 -> ~ P (substring n (S l') s) | 1115 -> ~ P (substring n (S l') s) |
1116 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)}. | 1116 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)}. |
1117 refine (fix F (l : nat) : {exists l', S l' <= l | 1117 refine (fix F (l : nat) : {exists l', S l' <= l |
1118 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)} | 1118 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)} |
1119 + {forall l', S l' <= l | 1119 + {forall l', S l' <= l |
1120 -> ~ P (substring n (S l') s) | 1120 -> ~ P (substring n (S l') s) |
1121 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} := | 1121 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} := |
1122 match l return {exists l', S l' <= l | 1122 match l with |
1123 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)} | 1123 | O => _ |
1124 + {forall l', S l' <= l | 1124 | S l' => |
1125 -> ~ P (substring n (S l') s) | 1125 (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _) |
1126 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} with | 1126 || F l' |
1127 | O => _ | 1127 end); clear F; crush; eauto 7; |
1128 | S l' => | 1128 match goal with |
1129 (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _) | 1129 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush |
1130 || F l' | 1130 end. |
1131 end); clear F; crush; eauto 7; | |
1132 match goal with | |
1133 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush | |
1134 end. | |
1135 Defined. | 1131 Defined. |
1136 End dec_star''. | 1132 End dec_star''. |
1137 | 1133 |
1138 (* begin hide *) | 1134 (* begin hide *) |
1139 Lemma star_length_contra : forall n, | 1135 Lemma star_length_contra : forall n, |