Mercurial > cpdt > repo
changeset 93:a08e82c646a5
Comment regexp matcher
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 07 Oct 2008 16:50:46 -0400 |
parents | 41392e5acbf5 |
children | affdf00759d8 |
files | src/MoreDep.v |
diffstat | 1 files changed, 82 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/src/MoreDep.v Tue Oct 07 16:08:58 2008 -0400 +++ b/src/MoreDep.v Tue Oct 07 16:50:46 2008 -0400 @@ -346,6 +346,10 @@ (** * A Certified Regular Expression Matcher *) +(** Another interesting example is regular expressions with dependent types that express which predicates over strings particular regexps implement. We can then assign a dependent type to a regular expression matching function, guaranteeing that it always decides the string property that we expect it to decide. + + Before defining the syntax of expressions, it is helpful to define an inductive type capturing the meaning of the Kleene star. We use Coq's string support, which comes through a combination of the [Strings] library and some parsing notations built into Coq. Operators like [++] and functions like [length] that we know from lists are defined again for strings. Notation scopes help us control which versions we want to use in particular contexts. *) + Require Import Ascii String. Open Scope string_scope. @@ -360,6 +364,23 @@ -> 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. + +[[ +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), + regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2). + +[[ +User error: Large non-propositional inductive types must be in Type +]] + +What is a 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]. + +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, regexp (fun s => s = String ch "") @@ -370,6 +391,9 @@ | Star : forall P (r : regexp P), regexp (star P). +(** Many theorems about strings are useful for implementing a certified regexp matcher, and few of them are in the [Strings] library. The book source includes statements, proofs, and hint commands for a handful of such omittted theorems. Since they are orthogonal to our use of dependent types, we hide them in the rendered versions of this book. *) + +(* begin hide *) Open Scope specif_scope. Lemma length_emp : length "" <= 0. @@ -397,7 +421,7 @@ Qed. Lemma substring_none : forall s n, - substring n 0 s = EmptyString. + substring n 0 s = "". induction s; substring. Qed. @@ -430,13 +454,20 @@ Qed. Hint Rewrite substring_app_fst substring_app_snd using (trivial; fail) : cpdt. +(* end hide *) + +(** A few auxiliary functions help us in our final matcher definition. The function [split] will be used to implement the regexp concatenation case. *) Section split. Variables P1 P2 : string -> Prop. Variable P1_dec : forall s, {P1 s} + { ~P1 s}. Variable P2_dec : forall s, {P2 s} + { ~P2 s}. + (** We require a choice of two arbitrary string predicates and functions for deciding them. *) Variable s : string. + (** Our computation will take place relative to a single fixed string, so it is easiest to make it a [Variable], rather than an explicit argument to our functions. *) + + (** [split'] is the workhorse behind [split]. It searches through the possible ways of splitting [s] into two pieces, checking the two predicates against each such pair. [split'] progresses right-to-left, from splitting all of [s] into the first piece to splitting all of [s] into the second piece. It takes an extra argument, [n], which specifies how far along we are in this search process. *) Definition split' (n : nat) : n <= length s -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2} @@ -448,7 +479,8 @@ -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2} + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~P1 s1 \/ ~P2 s2} with | O => fun _ => Reduce (P1_dec "" && P2_dec s) - | S n' => fun _ => (P1_dec (substring 0 (S n') s) && P2_dec (substring (S n') (length s - S n') s)) + | S n' => fun _ => (P1_dec (substring 0 (S n') s) + && P2_dec (substring (S n') (length s - S n') s)) || F n' _ end); clear F; crush; eauto 7; match goal with @@ -458,6 +490,18 @@ end; crush. Defined. + (** There is one subtle point in the [split'] code that is worth mentioning. The main body of the function is a [match] on [n]. In the case where [n] is known to be [S n'], we write [S n'] in several places where we might be tempted to write [n]. However, without further work to craft proper [match] annotations, the type-checker does not use the equality between [n] and [S n']. Thus, it is common to see patterns repeated in [match] case bodies in dependently-typed Coq code. We can at least use a [let] expression to avoid copying the pattern more than once, replacing the first case body with: + + [[ + + | S n' => fun _ => let n := S n' in + (P1_dec (substring 0 n s) + && P2_dec (substring n (length s - n) s)) + || F n' _ + ]] + + [split] 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} + {forall s1 s2, s = s1 ++ s2 -> ~P1 s1 \/ ~P2 s2}. refine (Reduce (split' (n := length s) _)); crush; eauto. @@ -466,6 +510,7 @@ Implicit Arguments split [P1 P2]. +(* begin hide *) Lemma app_empty_end : forall s, s ++ "" = s. induction s; crush. Qed. @@ -557,11 +602,17 @@ Qed. Hint Rewrite minus_minus using omega : cpdt. +(* end hide *) + +(** One more helper function will come in handy: [dec_star], for implementing another linear search through ways of splitting a string, this time for implementing the Kleene star. *) Section dec_star. Variable P : string -> Prop. Variable P_dec : forall s, {P s} + { ~P s}. + (** Some new lemmas and hints about the [star] type family are useful here. We omit them here; they are included in the book source at this point. *) + + (* begin hide *) Hint Constructors star. Lemma star_empty : forall s, @@ -623,28 +674,38 @@ | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto end. Qed. + (* end hide *) + + (** 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 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)}. + (** When we use [dec_star''], we will instantiate [P'_dec] with a function for continuing the search for more instances of [P] in [s]. *) + + (** Now we come to [dec_star''] itself. It takes as an input a natural [l] that records how much of the string has been searched so far, as we did for [split']. The return type expresses that [dec_star''] is looking for an index into [s] that splits [s] into a nonempty prefix and a suffix, such that the prefix satisfies [P] and the suffix satisfies [P']. *) Definition dec_star'' (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)}. + -> ~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)} := + -> ~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 /\ 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 + ~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') _) @@ -656,6 +717,7 @@ Defined. End dec_star''. + (* begin hide *) Lemma star_length_contra : forall n, length s > n -> n >= length s @@ -671,16 +733,19 @@ Qed. Hint Resolve star_length_contra star_length_flip substring_suffix_emp. + (* end hide *) + (** The work of [dec_star''] is nested inside another linear search by [dec_star'], which provides the final functionality we need, but for arbitrary suffixes of [s], rather than just for [s] overall. *) + Definition dec_star' (n n' : nat) : length s - n' <= n -> {star P (substring n' (length s - n') s)} - + {~star P (substring n' (length s - n') s)}. + + { ~star P (substring n' (length s - n') s)}. refine (fix F (n n' : nat) {struct n} : length s - n' <= n -> {star P (substring n' (length s - n') s)} - + {~star P (substring n' (length s - n') s)} := + + { ~star P (substring n' (length s - n') s)} := match n return length s - n' <= n -> {star P (substring n' (length s - n') s)} - + {~star P (substring n' (length s - n') s)} with + + { ~star P (substring n' (length s - n') s)} with | O => fun _ => Yes | S n'' => fun _ => le_gt_dec (length s) n' @@ -695,6 +760,8 @@ 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. *) + Definition dec_star : {star P s} + { ~star P s}. refine (match s with | "" => Reduce (dec_star' (n := length s) 0 _) @@ -703,6 +770,7 @@ Defined. End dec_star. +(* begin hide *) Lemma app_cong : forall x1 y1 x2 y2, x1 = x2 -> y1 = y2 @@ -711,6 +779,9 @@ Qed. Hint Resolve app_cong. +(* end hide *) + +(** With these helper functions completed, the implementation of our [matches] function is refreshingly straightforward. We only need one small piece of specific tactic work beyond what [crush] does for us. *) Definition matches P (r : regexp P) s : {P s} + { ~P s}. refine (fix F P (r : regexp P) s : {P s} + { ~P s} := @@ -722,10 +793,10 @@ end); crush; match goal with | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _)) - end; - tauto. + end; tauto. Defined. +(* begin hide *) Example hi := Concat (Char "h"%char) (Char "i"%char). Eval simpl in matches hi "hi". Eval simpl in matches hi "bye". @@ -741,3 +812,4 @@ Eval simpl in matches a_star "a". Eval simpl in matches a_star "b". Eval simpl in matches a_star "aa". +(* end hide *)