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

comparison src/MoreDep.v @ 454:49bd155dfc52

Proofreading pass through Chapter 8

author	Adam Chlipala <adam@chlipala.net>
date	Mon, 27 Aug 2012 17:21:34 -0400
parents	2740b8a23cce
children	4320c1a967c2

comparison

equal deleted inserted replaced

-:e3fa35c750ac
+:49bd155dfc52
 Our [app] function could be typed in so-called%\index{stratified type systems}% _stratified_ type systems, which avoid true dependency.  That is, we could consider the length indices to lists to live in a separate, compile-time-only universe from the lists themselves.  This stratification between a compile-time universe and a run-time universe, with no references to the latter in the former, gives rise to the terminology "stratified."  Our next example would be harder to implement in a stratified system.  We write an injection function from regular lists to length-indexed lists.  A stratified implementation would need to duplicate the definition of lists across compile-time and run-time versions, and the run-time versions would need to be indexed by the compile-time versions. *)
 (* EX: Implement injection from normal lists *)
 (* begin thide *)
 Fixpoint inject (ls : list A) : ilist (length ls) :=
 match ls with
 | nil => Nil
 | h :: t => Cons h (inject t)
 end.
 (** We can define an inverse conversion and prove that it really is an inverse. *)
 Fixpoint unject n (ls : ilist n) : list A :=
 match ls with
 | Nil => nil
 | Cons _ h t => h :: unject t
 end.
 Theorem inject_inverse : forall ls, unject (inject ls) = ls.
 induction ls; crush.
 Qed.
 (* end thide *)
 (* EX: Implement statically checked "car"/"hd" *)
 (** Now let us attempt a function that is surprisingly tricky to write.  In ML, the list head function raises an exception when passed an empty list.  With length-indexed lists, we can rule out such invalid calls statically, and here is a first attempt at doing so.  We write [???] as a placeholder for a term that we do not know how to write, not for any real Coq notation like those introduced two chapters ago.
 [[
 Definition hd n (ls : ilist (S n)) : A :=
 match ls with
 | Nil => ???
 | Cons _ h _ => h
 end.
 ]]
 It is not clear what to write for the [Nil] case, so we are stuck before we even turn our function over to the type checker.  We could try omitting the [Nil] case:
 [[
 Definition hd n (ls : ilist (S n)) : A :=
 match ls with
 | Cons _ h _ => h
 end.
 ]]
 <<
 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 that encoding ourselves directly.  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
 end.
 ]]
 <<
 Error: The reference n was not found in the current environment
 >>
 In this and other cases, we feel like we want [in] clauses with type family arguments that are not variables.  Unfortunately, Coq only supports variables in those positions.  A completely general mechanism could only be supported with a solution to the problem of higher-order unification%~\cite{HOU}%, which is undecidable.  There _are_ useful heuristics for handling non-variable indices which are gradually making their way into Coq, but we will spend some time in this and the next few chapters on effective pattern matching on dependent types using only the primitive [match] annotations.
 Our final, working attempt at [hd] uses an auxiliary function and a surprising [return] annotation. *)
 (* begin thide *)
 Definition hd' n (ls : ilist n) :=
 match ls in (ilist n) return (match n with O => unit | S _ => A end) with
 | Nil => tt
 | Cons _ h _ => h
 end.
 Check hd'.
 (** %\vspace{-.15in}% [[
 hd'
 : forall n : nat, ilist n -> match n with
 | 0 => unit
 | S _ => A
 end
 ]]
 *)
 Definition hd n (ls : ilist (S n)) : A := hd' ls.
 (* end thide *)
 End ilist.
 (** We annotate our main [match] with a type that is itself a [match].  We write that the function [hd'] returns [unit] when the list is empty and returns the carried type [A] in all other cases.  In the definition of [hd], we just call [hd'].  Because the index of [ls] is known to be nonzero, the type checker reduces the [match] in the type of [hd'] to [A]. *)
 end.
 (* end thide *)
 (** 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}%.
-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 with explicit [return] clauses. *)
+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. *)
 Fixpoint cfold t (e : exp t) : exp t :=
 match e with
 | NConst n => NConst n
 | Plus e1 e2 =>
 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
 end
 ]]
-We would like to do a case analysis on [cfold e1], and we attempt that in the way that has worked so far.
+We would like to do a case analysis on [cfold e1], and we attempt to do so in the way that has worked so far.
 [[
 destruct (cfold e1).
 ]]
 <<
 present_insert.
 Qed.
 End present.
 End insert.
-(** We can generate executable OCaml code with the command %\index{Vernacular commands!Recursive Extraction}%[Recursive Extraction insert], which also automatically outputs the OCaml versions of all of [insert]'s dependencies.  In our previous extractions, we wound up with clean OCaml code.  Here, we find uses of %\index{Obj.magic}%<<Obj.magic>>, OCaml's unsafe cast operator for tweaking the apparent type of an expression in an arbitrary way.  Casts appear for this example because the return type of [insert] depends on the _value_ of the function's argument, a pattern which OCaml cannot handle.  Since Coq's type system is much more expressive than OCaml's, such casts are unavoidable in general.  Since the OCaml type-checker is no longer checking full safety of programs, we must rely on Coq's extractor to use casts only in provably safe ways. *)
+(** We can generate executable OCaml code with the command %\index{Vernacular commands!Recursive Extraction}%[Recursive Extraction insert], which also automatically outputs the OCaml versions of all of [insert]'s dependencies.  In our previous extractions, we wound up with clean OCaml code.  Here, we find uses of %\index{Obj.magic}%<<Obj.magic>>, OCaml's unsafe cast operator for tweaking the apparent type of an expression in an arbitrary way.  Casts appear for this example because the return type of [insert] depends on the _value_ of the function's argument, a pattern that OCaml cannot handle.  Since Coq's type system is much more expressive than OCaml's, such casts are unavoidable in general.  Since the OCaml type-checker is no longer checking full safety of programs, we must rely on Coq's extractor to use casts only in provably safe ways. *)
 (* begin hide *)
 Recursive Extraction insert.
 (* end hide *)
 <<
 User error: Large non-propositional inductive types must be in Type
 >>
-What is a %\index{large inductive types}%large inductive type?  In Coq, it is an inductive type that has a constructor which quantifies over some type of type [Type].  We have not worked with [Type] very much to this point.  Every term of CIC has a type, including [Set] and [Prop], which are assigned type [Type].  The type [string -> Prop] from the failed definition also has type [Type].
+What is a %\index{large inductive types}%large inductive type?  In Coq, it is an inductive type that has a constructor that quantifies over some type of type [Type].  We have not worked with [Type] very much to this point.  Every term of CIC has a type, including [Set] and [Prop], which are assigned type [Type].  The type [string -> Prop] from the failed definition also has type [Type].
 It turns out that allowing large inductive types in [Set] leads to contradictions when combined with certain kinds of classical logic reasoning.  Thus, by default, such types are ruled out.  There is a simple fix for our [regexp] definition, which is to place our new type in [Type].  While fixing the problem, we also expand the list of constructors to cover the remaining regular expression operators. *)
 Inductive regexp : (string -> Prop) -> Type :=
 | Char : forall ch : ascii,
 [[
 | S n' => fun _ => let n := S n' in
 (P1_dec (substring 0 n s)
 && P2_dec (substring n (length s - n) s))
 || F n' _
 ]]
 The [split] function itself is trivial to implement in terms of [split'].  We just ask [split'] to begin its search with [n = length s]. *)
 Definition split : {exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2}
 (** The function [dec_star''] implements a single iteration of the star.  That is, it tries to find a string prefix matching [P], and it calls a parameter function on the remainder of the string. *)
 Section dec_star''.
 Variable n : nat.
-(** [n] is the length of the prefix of [s] that we have already processed. *)
+(** Variable [n] is the length of the prefix of [s] that we have already processed. *)
 Variable P' : string -> Prop.
 Variable P'_dec : forall n' : nat, n' > n
 -> {P' (substring n' (length s - n') s)}
 + {~ P' (substring n' (length s - n') s)}.
 Eval hnf in matches a_b "a".
 Eval hnf in matches a_b "aa".
 Eval hnf in matches a_b "b".
 (* end hide *)
-(** Many regular expression matching problems are easy to test.  The reader may run each of the following queries to verify that it gives the correct answer.  We use evaluation strategy %\index{tactics!hnf}%[hnf] to reduce each term to%\index{head-normal form}% _head-normal form_, where the datatype constructor used to build its value is known. *)
+(** Many regular expression matching problems are easy to test.  The reader may run each of the following queries to verify that it gives the correct answer.  We use evaluation strategy %\index{tactics!hnf}%[hnf] to reduce each term to%\index{head-normal form}% _head-normal form_, where the datatype constructor used to build its value is known.  (Further reduction would involve wasteful simplification of proof terms justifying the answers of our procedures.) *)
 Example a_star := Star (Char "a"%char).
 Eval hnf in matches a_star "".
 Eval hnf in matches a_star "a".
 Eval hnf in matches a_star "b".

Mercurial > cpdt > repo

comparison src/MoreDep.v @ 454:49bd155dfc52