Certified Programming with Dependent Types: src/MoreDep.v comparison

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

-:40a9a36844d6
+:f38a3af9dd17
 <<
 Error: Non exhaustive pattern-matching: no clause found for pattern Nil
 >>
-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.
+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.
 [[
 Definition hd n (ls : ilist (S n)) : A :=
 match ls in (ilist (S n)) with
 | Cons _ h _ => h
 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!
 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):
 [[
-match E in (T x1 ... xn) as y return U with
+match E as y in (T x1 ... xn) return U with
 | C z1 ... zm => B
 | ...
 end
 ]]
-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].
+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].
-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.
+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.
 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.
 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.
 User error: e1 is used in hypothesis e
 >>
 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.
-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.) *)
+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.) *)
 dep_destruct (cfold e1).
 (** 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].
-This is the only new trick we need to learn to complete the proof.  We can back up and give a short, automated proof. *)
+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). *)
 Restart.
 induction e; crush;
 repeat (match goal with
 P s1
 -> star s2
 -> star (s1 ++ s2).
 End star.
-(** 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.
+(** 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.
 [[
 Inductive regexp : (string -> Prop) -> Set :=
 | Char : forall ch : ascii,
 regexp (fun s => s = String ch "")
 | Concat : forall (P1 P2 : string -> Prop) (r1 : regexp P1) (r2 : regexp P2),
 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
 + {forall l', S l' <= l
 -> ~ P (substring n (S l') s)
 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)}.
 refine (fix F (l : nat) : {exists l', S l' <= l
 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
 + {forall l', S l' <= l
 -> ~ P (substring n (S l') s)
 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} :=
-match l return {exists l', S l' <= l
+match l with
-/\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
+| O => _
-+ {forall l', S l' <= l
+| S l' =>
--> ~ P (substring n (S l') s)
+(P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
-\/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} with
+|| F l'
-| O => _
+end); clear F; crush; eauto 7;
-| S l' =>
+match goal with
-(P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
+| [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
-|| F l'
+end.
-end); clear F; crush; eauto 7;
-match goal with
-| [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
-end.
 Defined.
 End dec_star''.
 (* begin hide *)
 Lemma star_length_contra : forall n,

Mercurial > cpdt > repo

comparison src/MoreDep.v @ 480:f38a3af9dd17