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

comparison src/MoreDep.v @ 380:31fa03bc0f18

Get it to build with Coq 8.4

author	Adam Chlipala <adam@chlipala.net>
date	Thu, 29 Mar 2012 18:10:52 -0400
parents	d1276004eec9
children	b911d0df5eee

comparison

equal deleted inserted replaced

-:e23d41ae63be
+:31fa03bc0f18
 A quick word of encouragement: After writing this code, even I do not understand the precise details of how balancing works!  I consulted Chris Okasaki's paper %``%#"#Red-Black Trees in a Functional Setting#"#%''~\cite{Okasaki}% and transcribed the code to use dependent types.  Luckily, the details are not so important here; types alone will tell us that insertion preserves balanced-ness, and we will prove that insertion produces trees containing the right keys.*)
 Definition balance1 n (a : rtree n) (data : nat) c2 :=
 match a in rtree n return rbtree c2 n
 -> { c : color & rbtree c (S n) } with
-| RedNode' _ _ _ t1 y t2 =>
+| RedNode' _ c0 _ t1 y t2 =>
-match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
+match t1 in rbtree c n return rbtree c0 n -> rbtree c2 n
 -> { c : color & rbtree c (S n) } with
 | RedNode _ a x b => fun c d =>
 {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
 | t1' => fun t2 =>
-match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
+match t2 in rbtree c n return rbtree Black n -> rbtree c2 n
 -> { c : color & rbtree c (S n) } with
 | RedNode _ b x c => fun a d =>
 {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
 | b => fun a t => {<BlackNode (RedNode a y b) data t>}
 end t1'
 Here is the symmetric function [balance2], for cases where the possibly invalid tree appears on the right rather than on the left. *)
 Definition balance2 n (a : rtree n) (data : nat) c2 :=
 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
-| RedNode' _ _ _ t1 z t2 =>
+| RedNode' _ c0 _ t1 z t2 =>
-match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
+match t1 in rbtree c n return rbtree c0 n -> rbtree c2 n
 -> { c : color & rbtree c (S n) } with
 | RedNode _ b y c => fun d a =>
 {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
 | t1' => fun t2 =>
-match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
+match t2 in rbtree c n return rbtree Black n -> rbtree c2 n
 -> { c : color & rbtree c (S n) } with
 | RedNode _ c z' d => fun b a =>
 {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
 | b => fun a t => {<BlackNode t data (RedNode a z b)>}
 end t1'
 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 with
+match l return {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)} with
 | O => _
 | S l' =>
 (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
 || F l'
 end); clear F; crush; eauto 7;
 | [ H1 : _ < _ - _, H2 : forall l' : nat, _ <= _ - _ -> _ |- _ ] =>
 generalize (H2 _ (lt_le_S _ _ H1)); tauto
 end.
 Defined.
-(** Finally, we have [dec_star].  It has a straightforward implementation.  We introduce a spurious match on [s] so that [simpl] will know to reduce calls to [dec_star].  The heuristic that [simpl] uses is only to unfold identifier definitions when doing so would simplify some [match] expression. *)
+(** Finally, we have [dec_star], defined by straightforward reduction from [dec_star']. *)
 Definition dec_star : {star P s} + {~ star P s}.
-refine (match s return _ with
+refine (Reduce (dec_star' (n := length s) 0 _)); crush.
-| "" => Reduce (dec_star' (n := length s) 0 _)
-| _ => Reduce (dec_star' (n := length s) 0 _)
-end); crush.
 Defined.
 End dec_star.
 (* begin hide *)
 Lemma app_cong : forall x1 y1 x2 y2,
 (** It is interesting to pause briefly to consider alternate implementations of [matches].  Dependent types give us much latitude in how specific correctness properties may be encoded with types.  For instance, we could have made [regexp] a non-indexed inductive type, along the lines of what is possible in traditional ML and Haskell.  We could then have implemented a recursive function to map [regexp]s to their intended meanings, much as we have done with types and programs in other examples.  That style is compatible with the [refine]-based approach that we have used here, and it might be an interesting exercise to redo the code from this subsection in that alternate style or some further encoding of the reader's choice.  The main advantage of indexed inductive types is that they generally lead to the smallest amount of code. *)
 (* begin hide *)
 Example hi := Concat (Char "h"%char) (Char "i"%char).
-Eval simpl in matches hi "hi".
+Eval hnf in matches hi "hi".
-Eval simpl in matches hi "bye".
+Eval hnf in matches hi "bye".
 Example a_b := Or (Char "a"%char) (Char "b"%char).
-Eval simpl in matches a_b "".
+Eval hnf in matches a_b "".
-Eval simpl in matches a_b "a".
+Eval hnf in matches a_b "a".
-Eval simpl in matches a_b "aa".
+Eval hnf in matches a_b "aa".
-Eval simpl in matches a_b "b".
+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. *)
+(** 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}\emph{%#<i>#head-normal form#</i>#%}%, where the datatype constructor used to build its value is known. *)
 Example a_star := Star (Char "a"%char).
-Eval simpl in matches a_star "".
+Eval hnf in matches a_star "".
-Eval simpl in matches a_star "a".
+Eval hnf in matches a_star "a".
-Eval simpl in matches a_star "b".
+Eval hnf in matches a_star "b".
-Eval simpl in matches a_star "aa".
+Eval hnf in matches a_star "aa".
 (** Evaluation inside Coq does not scale very well, so it is easy to build other tests that run for hours or more.  Such cases are better suited to execution with the extracted OCaml code. *)

Mercurial > cpdt > repo

comparison src/MoreDep.v @ 380:31fa03bc0f18