Mercurial > cpdt > repo

comparison src/MoreDep.v @ 297:b441010125d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Everything compiles in Coq 8.3pl1
author Adam Chlipala <adam@chlipala.net>
date Fri, 14 Jan 2011 14:39:12 -0500
parents 559ec7328410
children 7b38729be069
comparison
equal deleted inserted replaced
296:559ec7328410 297:b441010125d4
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2011, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
873 Variable s : string. 873 Variable s : string.
874 (** 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. *) 874 (** 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. *)
875 875
876 (** [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. *) 876 (** [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. *)
877 877
878 Definition split' (n : nat) : n <= length s 878 Definition split' : forall n : nat, n <= length s
879 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2} 879 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
880 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2}. 880 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2}.
881 refine (fix F (n : nat) : n <= length s 881 refine (fix F (n : nat) : n <= length s
882 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2} 882 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
883 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2} := 883 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2} :=
1092 + {~ P' (substring n' (length s - n') s)}. 1092 + {~ P' (substring n' (length s - n') s)}.
1093 (** When we use [dec_star''], we will instantiate [P'_dec] with a function for continuing the search for more instances of [P] in [s]. *) 1093 (** When we use [dec_star''], we will instantiate [P'_dec] with a function for continuing the search for more instances of [P] in [s]. *)
1094 1094
1095 (** 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']. *) 1095 (** 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']. *)
1096 1096
1097 Definition dec_star'' (l : nat) 1097 Definition dec_star'' : forall l : nat,
1098 : {exists l', S l' <= l 1098 {exists l', S l' <= l
1099 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)} 1099 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
1100 + {forall l', S l' <= l 1100 + {forall l', S l' <= l
1101 -> ~ P (substring n (S l') s) 1101 -> ~ P (substring n (S l') s)
1102 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)}. 1102 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)}.
1103 refine (fix F (l : nat) : {exists l', S l' <= l 1103 refine (fix F (l : nat) : {exists l', S l' <= l
1135 Hint Resolve star_length_contra star_length_flip substring_suffix_emp. 1135 Hint Resolve star_length_contra star_length_flip substring_suffix_emp.
1136 (* end hide *) 1136 (* end hide *)
1137 1137
1138 (** 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. *) 1138 (** 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. *)
1139 1139
1140 Definition dec_star' (n n' : nat) : length s - n' <= n 1140 Definition dec_star' : forall n n' : nat, length s - n' <= n
1141 -> {star P (substring n' (length s - n') s)} 1141 -> {star P (substring n' (length s - n') s)}
1142 + {~ star P (substring n' (length s - n') s)}. 1142 + {~ star P (substring n' (length s - n') s)}.
1143 refine (fix F (n n' : nat) : length s - n' <= n 1143 refine (fix F (n n' : nat) : length s - n' <= n
1144 -> {star P (substring n' (length s - n') s)} 1144 -> {star P (substring n' (length s - n') s)}
1145 + {~ star P (substring n' (length s - n') s)} := 1145 + {~ star P (substring n' (length s - n') s)} :=
1179 Hint Resolve app_cong. 1179 Hint Resolve app_cong.
1180 (* end hide *) 1180 (* end hide *)
1181 1181
1182 (** 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. *) 1182 (** 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. *)
1183 1183
1184 Definition matches P (r : regexp P) s : {P s} + {~ P s}. 1184 Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}.
1185 refine (fix F P (r : regexp P) s : {P s} + {~ P s} := 1185 refine (fix F P (r : regexp P) s : {P s} + {~ P s} :=
1186 match r with 1186 match r with
1187 | Char ch => string_dec s (String ch "") 1187 | Char ch => string_dec s (String ch "")
1188 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s) 1188 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
1189 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s 1189 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s