Mercurial > cpdt > repo
changeset 100:070f4de92311
Templatize MoreDep
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 08 Oct 2008 10:01:26 -0400 |
parents | 8c7d9b82a4a4 |
children | bc12662ae895 |
files | src/MoreDep.v |
diffstat | 1 files changed, 31 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/src/MoreDep.v Wed Oct 08 09:41:50 2008 -0400 +++ b/src/MoreDep.v Wed Oct 08 10:01:26 2008 -0400 @@ -56,11 +56,15 @@ We see the return of a problem we have considered before. Without explicit annotations, Coq does not enrich our typing assumptions in the branches of a [match] expression. It is clear that the unification variable [?14] should be resolved to 0 in this context, so that we have [0 + n2] reducing to [n2], but Coq does not realize that. We cannot fix the problem using just the simple [return] clauses we applied in the last chapter. We need to combine a [return] clause with a new kind of annotation, an [in] clause. *) +(* EX: Implement concatenation *) + +(* begin thide *) Fixpoint app n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) {struct ls1} : ilist (n1 + n2) := match ls1 in (ilist n1) return (ilist (n1 + n2)) with | Nil => ls2 | Cons _ x ls1' => Cons x (app ls1' ls2) end. +(* end thide *) (** This version of [app] passes the type checker. Using [return] alone allowed us to express a dependency of the [match] result type on the %\textit{%#<i>#value#</i>#%}% of the discriminee. What [in] adds to our arsenal is a way of expressing a dependency on the %\textit{%#<i>#type#</i>#%}% of the discriminee. Specifically, the [n1] in the [in] clause above is a %\textit{%#<i>#binding occurrence#</i>#%}% whose scope is the [return] clause. @@ -68,6 +72,9 @@ Our [app] function could be typed in so-called %\textit{%#<i>#stratified#</i>#%}% type systems, which avoid true dependency. We could consider the length indices to lists to live in a separate, compile-time-only universe from the lists themselves. 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 return (ilist (length ls)) with | nil => Nil @@ -85,6 +92,9 @@ 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. @@ -123,6 +133,7 @@ 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 @@ -130,6 +141,7 @@ end. Definition hd n (ls : ilist (S n)) : A := hd' ls. +(* end thide *) (** 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]. *) @@ -205,6 +217,9 @@ We run again into the problem of not being able to specify non-variable arguments in [in] clauses. The problem would just be hopeless without a use of an [in] clause, though, since the result type of the [match] depends on an argument to [exp]. Our solution will be to use a more general type, as we did for [hd]. First, we define a type-valued function to use in assigning a type to [pairOut]. *) +(* EX: Define a function [pairOut : forall t1 t2, exp (Prod t1 t2) -> option (exp t1 * exp t2)] *) + +(* begin thide *) Definition pairOutType (t : type) := match t with | Prod t1 t2 => option (exp t1 * exp t2) @@ -226,6 +241,7 @@ | Pair _ _ e1 e2 => Some (e1, e2) | _ => pairOutDefault _ 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, but is similar to what goes on with Haskell type classes. @@ -283,6 +299,7 @@ (** The correctness theorem for [cfold] turns out to be easy to prove, once we get over one serious hurdle. *) Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e). +(* begin thide *) induction e; crush. (** The first remaining subgoal is: @@ -342,10 +359,13 @@ | [ |- (if ?E then _ else _) = _ ] => destruct E end; crush). Qed. +(* end thide *) (** Dependently-Typed Red-Black Trees *) +(** TODO: Add commentary for this section. *) + Inductive color : Set := Red | Black. Inductive rbtree : color -> nat -> Set := @@ -353,6 +373,9 @@ | RedNode : forall n, rbtree Black n -> nat-> rbtree Black n -> rbtree Red n | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n). +(* EX: Prove that every [rbtree] is balanced. *) + +(* begin thide *) Require Import Max Min. Section depth. @@ -380,10 +403,10 @@ induction t; crush; match goal with | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y) - end; crush. - - destruct c1; crush. - destruct c2; crush. + end; crush; + repeat (match goal with + | [ H : context[match ?C with Red => _ | Black => _ end] |- _ ] => destruct C + end; crush). Qed. Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1. @@ -393,6 +416,7 @@ Theorem balanced : forall c n (t : rbtree c n), 2 * depth min t + 1 >= depth max t. intros; generalize (depth_min t); generalize (depth_max t); crush. Qed. +(* end thide *) Inductive rtree : nat -> Set := @@ -414,6 +438,9 @@ end. End present. +Locate "{ _ : _ & _ }". +Print sigT. + Notation "{< x >}" := (existT _ _ x). Definition balance1 n (a : rtree n) (data : nat) c2 :=