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

comparison src/DataStruct.v @ 443:97c60ffdb998

Vertical spacing pass for MoreDep and DataStruct

author	Adam Chlipala <adam@chlipala.net>
date	Wed, 01 Aug 2012 16:32:04 -0400
parents	8077352044b2
children	df0a45de158a

comparison

equal deleted inserted replaced

-:89c67796754e
+:97c60ffdb998
 | Next : forall n, fin n -> fin (S n).
 (** An instance of [fin] is essentially a more richly typed copy of the natural numbers.  Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected.  For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))].
 Now it is easy to pick a [Prop]-free type for a selection function.  As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time.
 [[
 Fixpoint get n (ls : ilist n) : fin n -> A :=
 match ls with
 | Nil => fun idx => ?
 | Cons _ x ls' => fun idx =>
 match idx with
 | First _ => x
 | Next _ idx' => get ls' idx'
 end
 end.
 ]]
+%\vspace{-.15in}%We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses.  This still leaves us with a quandary in each of the [match] cases.  First, we need to figure out how to take advantage of the contradiction in the [Nil] case.  Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case.  The solution we adopt is another case of [match]-within-[return].
-We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses.  This still leaves us with a quandary in each of the [match] cases.  First, we need to figure out how to take advantage of the contradiction in the [Nil] case.  Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case.  The solution we adopt is another case of [match]-within-[return].
 [[
 Fixpoint get n (ls : ilist n) : fin n -> A :=
 match ls with
 | Nil => fun idx =>
 match idx in fin n' return (match n' with
 match idx with
 | First _ => x
 | Next _ idx' => get ls' idx'
 end
 end.
 ]]
+%\vspace{-.15in}%Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls'].  In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic.  We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A].  We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically.  Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern.  As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be.
-Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls'].  In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic.  We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A].  We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically.  Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern.  As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be.
 We need to use [match] annotations to make the relationship explicit.  Unfortunately, the usual trick of postponing argument binding will not help us here.  We need to match on both [ls] and [idx]; one or the other must be matched first.  To get around this, we apply the convoy pattern that we met last chapter.  This application is a little more clever than those we saw before; we use the natural number predecessor function [pred] to express the relationship between the types of these variables.
 [[
 Fixpoint get n (ls : ilist n) : fin n -> A :=
 match ls with
 | Nil => fun idx =>
 match idx in fin n' return (match n' with
 match idx in fin n' return ilist (pred n') -> A with
 | First _ => fun _ => x
 | Next _ idx' => fun ls' => get ls' idx'
 end ls'
 end.
 ]]
+%\vspace{-.15in}%There is just one problem left with this implementation.  Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination.  We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *)
-There is just one problem left with this implementation.  Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination.  We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *)
 Fixpoint get n (ls : ilist n) : fin n -> A :=
 match ls with
 | Nil => fun idx =>
 match idx in fin n' return (match n' with
 (** We can also build indexed lists of pairs in this way. *)
 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
 MCons (1, 2) (MCons (true, false) MNil).
+(** There are many more useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *)
 (* end thide *)
 (** ** A Lambda Calculus Interpreter *)
 end%type.
 (** The definition of [fmember] follows the definition of [ffin].  Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail.  While for [ffin] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for.  We express that with a sum type whose left branch is the appropriate equality proposition.  Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type].
 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
 [[
 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
 match ls with
 | nil => fun _ idx => match idx with end
 | _ :: ls' => fun mls idx =>
 match idx with
 | inl _ => fst mls
 | inr idx' => fhget ls' (snd mls) idx'
 end
 end.
 ]]
+%\vspace{-.15in}%Only one problem remains.  The expression [fst mls] is not known to have the proper type.  To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *)
-Only one problem remains.  The expression [fst mls] is not known to have the proper type.  To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *)
 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
 match ls with
 | nil => fun _ idx => match idx with end
 | _ :: ls' => fun mls idx =>
 (* end hide *)
 Print eq.
 (** %\vspace{-.15in}% [[
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 ]]
 In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument.  The type of the constructor [eq_refl] shows that [y] can only ever be instantiated to [x].  Thus, within a pattern-match with [eq_refl], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *)
 (* end thide *)
 tree_ind
 : forall (A : Set) (P : tree A -> Prop),
 (forall a : A, P (Leaf a)) ->
 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
 forall t : tree A, P t
 ]]
 The automatically generated induction principle is too weak.  For the [Node] case, it gives us no inductive hypothesis.  We could write our own induction principle, as we did in Chapter 3, but there is an easier way, if we are willing to alter the definition of [tree]. *)
 Abort.
 Implicit Arguments cond [A n].
 (* end thide *)
 (** Now the expression interpreter is straightforward to write. *)
+(* begin thide *)
 Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
 match e with
 | NConst n => n
 | Plus e1 e2 => exp'Denote e1 + exp'Denote e2
 | Eq e1 e2 =>
 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
 | BConst b => b
 | Cond _ _ tests bodies default =>
-(* begin thide *)
 cond
 (exp'Denote default)
 (fun idx => exp'Denote (tests idx))
 (fun idx => exp'Denote (bodies idx))
-(* end thide *)
+end.
-end.
+(* begin hide *)
+Reset exp'Denote.
+(* end hide *)
+(* end thide *)
+(* begin hide *)
+Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
+match e with
+| NConst n => n
+| Plus e1 e2 => exp'Denote e1 + exp'Denote e2
+| Eq e1 e2 =>
+if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
+| BConst b => b
+| Cond _ _ tests bodies default =>
+(* begin thide *)
+cond
+(exp'Denote default)
+(fun idx => exp'Denote (tests idx))
+(fun idx => exp'Denote (bodies idx))
+(* end thide *)
+end.
+(* end hide *)
 (** We will implement a constant-folding function that optimizes conditionals, removing cases with known-[false] tests and cases that come after known-[true] tests.  A function [cfoldCond] implements the heart of this logic.  The convoy pattern is used again near the end of the implementation. *)
 (* begin thide *)
 Section cfoldCond.
 match goal with
 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] =>
 specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)))
 end;
 repeat (match goal with
-| [ |- context[match ?E with NConst _ => _ | _ => _ end] ] => dep_destruct E
+| [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>
+dep_destruct E
 | [ |- context[if ?B then _ else _] ] => destruct B
 end; crush).
 Qed.
 (** It is also useful to know that the result of a call to [cond] is not changed by substituting new tests and bodies functions, so long as the new functions have the same input-output behavior as the old.  It turns out that, in Coq, it is not possible to prove in general that functions related in this way are equal.  We treat this issue with our discussion of axioms in a later chapter.  For now, it suffices to prove that the particular function [cond] is _extensional_; that is, it is unaffected by substitution of functions with input-output equivalents. *)

Mercurial > cpdt > repo

comparison src/DataStruct.v @ 443:97c60ffdb998