diff options
Diffstat (limited to 'theories/Strings/String.v')
-rw-r--r-- | theories/Strings/String.v | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 7d6696b78..82a60c189 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -18,7 +18,7 @@ Declare ML Module "string_syntax_plugin". (** *** Definition of strings *) (** Implementation of string as list of ascii characters *) - + Inductive string : Set := | EmptyString : string | String : ascii -> string -> string. @@ -48,7 +48,7 @@ where "s1 ++ s2" := (append s1 s2) : string_scope. (******************************) (** Length *) (******************************) - + Fixpoint length (s : string) : nat := match s with | EmptyString => 0 @@ -58,7 +58,7 @@ Fixpoint length (s : string) : nat := (******************************) (** Nth character of a string *) (******************************) - + Fixpoint get (n : nat) (s : string) {struct s} : option ascii := match s with | EmptyString => None @@ -69,7 +69,7 @@ Fixpoint get (n : nat) (s : string) {struct s} : option ascii := end. (** Two lists that are identical through get are syntactically equal *) - + Theorem get_correct : forall s1 s2 : string, (forall n : nat, get n s1 = get n s2) <-> s1 = s2. Proof. @@ -90,7 +90,7 @@ rewrite H1; auto. Qed. (** The first elements of [s1 ++ s2] are the ones of [s1] *) - + Theorem append_correct1 : forall (s1 s2 : string) (n : nat), n < length s1 -> get n s1 = get n (s1 ++ s2). @@ -103,7 +103,7 @@ apply lt_S_n; auto. Qed. (** The last elements of [s1 ++ s2] are the ones of [s2] *) - + Theorem append_correct2 : forall (s1 s2 : string) (n : nat), get n s2 = get (n + length s1) (s1 ++ s2). @@ -120,7 +120,7 @@ Qed. (** [substring n m s] returns the substring of [s] that starts at position [n] and of length [m]; if this does not make sense it returns [""] *) - + Fixpoint substring (n m : nat) (s : string) {struct s} : string := match n, m, s with | 0, 0, _ => EmptyString @@ -131,7 +131,7 @@ Fixpoint substring (n m : nat) (s : string) {struct s} : string := end. (** The substring is included in the initial string *) - + Theorem substring_correct1 : forall (s : string) (n m p : nat), p < m -> get p (substring n m s) = get (p + n) s. @@ -149,7 +149,7 @@ intros n' m p H; rewrite <- Plus.plus_Snm_nSm; simpl in |- *; auto. Qed. (** The substring has at most [m] elements *) - + Theorem substring_correct2 : forall (s : string) (n m p : nat), m <= p -> get p (substring n m s) = None. Proof. @@ -167,7 +167,7 @@ Qed. (** *** Test functions *) (** Test if [s1] is a prefix of [s2] *) - + Fixpoint prefix (s1 s2 : string) {struct s2} : bool := match s1 with | EmptyString => true @@ -184,7 +184,7 @@ Fixpoint prefix (s1 s2 : string) {struct s2} : bool := (** If [s1] is a prefix of [s2], it is the [substring] of length [length s1] starting at position [O] of [s2] *) - + Theorem prefix_correct : forall s1 s2 : string, prefix s1 s2 = true <-> substring 0 (length s1) s2 = s1. @@ -203,7 +203,7 @@ Qed. (** Test if, starting at position [n], [s1] occurs in [s2]; if so it returns the position *) - + Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat := match s2, n with | EmptyString, 0 => @@ -212,7 +212,7 @@ Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat := | String a s1' => None end | EmptyString, S n' => None - | String b s2', 0 => + | String b s2', 0 => if prefix s1 s2 then Some 0 else match index 0 s1 s2' with @@ -230,7 +230,7 @@ Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat := Opaque prefix. (** If the result of [index] is [Some m], [s1] in [s2] at position [m] *) - + Theorem index_correct1 : forall (n m : nat) (s1 s2 : string), index n s1 s2 = Some m -> substring m (length s1) s2 = s1. @@ -260,9 +260,9 @@ intros x H H1; apply H; injection H1; intros H2; injection H2; auto. intros; discriminate. Qed. -(** If the result of [index] is [Some m], +(** If the result of [index] is [Some m], [s1] does not occur in [s2] before [m] *) - + Theorem index_correct2 : forall (n m : nat) (s1 s2 : string), index n s1 s2 = Some m -> @@ -305,9 +305,9 @@ apply Lt.lt_S_n; auto. intros; discriminate. Qed. -(** If the result of [index] is [None], [s1] does not occur in [s2] +(** If the result of [index] is [None], [s1] does not occur in [s2] after [n] *) - + Theorem index_correct3 : forall (n m : nat) (s1 s2 : string), index n s1 s2 = None -> @@ -349,7 +349,7 @@ Transparent prefix. (** If we are searching for the [Empty] string and the answer is no this means that [n] is greater than the size of [s] *) - + Theorem index_correct4 : forall (n : nat) (s : string), index n EmptyString s = None -> length s < n. @@ -368,7 +368,7 @@ Qed. (** Same as [index] but with no optional type, we return [0] when it does not occur *) - + Definition findex n s1 s2 := match index n s1 s2 with | Some n => n |