From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Strings/Ascii.v | 24 ++++++++++++------------ theories/Strings/String.v | 40 ++++++++++++++++++++-------------------- 2 files changed, 32 insertions(+), 32 deletions(-) (limited to 'theories/Strings') diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 5a2cc9695..6d3dc02a9 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -18,26 +18,26 @@ Declare ML Module "ascii_syntax_plugin". (** * Definition of ascii characters *) (** Definition of ascii character as a 8 bits constructor *) - + Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). Delimit Scope char_scope with char. Bind Scope char_scope with ascii. - + Definition zero := Ascii false false false false false false false false. - + Definition one := Ascii true false false false false false false false. - + Definition app1 (f : bool -> bool) (a : ascii) := match a with | Ascii a1 a2 a3 a4 a5 a6 a7 a8 => Ascii (f a1) (f a2) (f a3) (f a4) (f a5) (f a6) (f a7) (f a8) end. - + Definition app2 (f : bool -> bool -> bool) (a b : ascii) := match a, b with | Ascii a1 a2 a3 a4 a5 a6 a7 a8, Ascii b1 b2 b3 b4 b5 b6 b7 b8 => - Ascii (f a1 b1) (f a2 b2) (f a3 b3) (f a4 b4) + Ascii (f a1 b1) (f a2 b2) (f a3 b3) (f a4 b4) (f a5 b5) (f a6 b6) (f a7 b7) (f a8 b8) end. @@ -47,7 +47,7 @@ Definition shift (c : bool) (a : ascii) := end. (** Definition of a decidable function that is effective *) - + Definition ascii_dec : forall a b : ascii, {a = b} + {a <> b}. decide equality; apply bool_dec. Defined. @@ -57,7 +57,7 @@ Defined. (** Auxillary function that turns a positive into an ascii by looking at the last n bits, ie z mod 2^n *) -Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive) +Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive) (n : nat) {struct n} : ascii := match n with | O => res @@ -72,7 +72,7 @@ Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive) (** Function that turns a positive into an ascii by looking at the last 8 bits, ie a mod 8 *) - + Definition ascii_of_pos (a : positive) := ascii_of_pos_aux zero one a 8. (** Function that turns a Peano number into an ascii by converting it @@ -83,7 +83,7 @@ Definition ascii_of_nat (a : nat) := | O => zero | S a' => ascii_of_pos (P_of_succ_nat a') end. - + (** The opposite function *) Definition nat_of_ascii (a : ascii) : nat := @@ -103,7 +103,7 @@ Definition nat_of_ascii (a : ascii) : nat := + (if a2 then 1 else 0)) + (if a1 then 1 else 0). -Theorem ascii_nat_embedding : +Theorem ascii_nat_embedding : forall a : ascii, ascii_of_nat (nat_of_ascii a) = a. Proof. destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity. @@ -124,7 +124,7 @@ Qed. Notice that the ascii characters of code >= 128 do not denote stand-alone utf8 characters so that only the notation "nnn" is available for them (unless your terminal is able to represent them, - which is typically not the case in coqide). + which is typically not the case in coqide). *) Open Local Scope char_scope. 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 -- cgit v1.2.3