Ajout bibliothèque String de Laurent Théry

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8009 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 513 insertions, 0 deletions

diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
new file mode 100644
index 000000000..18aaa2c0b
--- /dev/null
+++ b/theories/Strings/Ascii.v
@@ -0,0 +1,123 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(* Contributed by Laurent Théry (INRIA);
+   Adapted to Coq V8 by the Coq Development Team *)
+
+Require Import Bool.
+Require Import BinPos.
+
+(***********************************)
+(** 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) 
+        (f a5 b5) (f a6 b6) (f a7 b7) (f a8 b8)
+  end.
+
+Definition shift (c : bool) (a : ascii) :=
+  match a with
+  | Ascii a1 a2 a3 a4 a5 a6 a7 a8 => Ascii c a1 a2 a3 a4 a5 a6 a7
+  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.
+
+(***********************************************************************)
+(** Conversion between natural numbers modulo 256 and ascii characters *)
+(***********************************************************************)
+
+(* 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) 
+ (n : nat) {struct n} : ascii :=
+  match n with
+  | O => res
+  | S n1 =>
+      match z with
+      | xH => app2 orb res acc
+      | xI z' => ascii_of_pos_aux (app2 orb res acc) (shift false acc) z' n1
+      | xO z' => ascii_of_pos_aux res (shift false acc) z' n1
+      end
+  end.
+
+
+(* 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
+   to positive *)
+
+Definition ascii_of_nat (a : nat) :=
+  match a with
+  | O => zero
+  | S a' => ascii_of_pos (P_of_succ_nat a')
+  end.
+ 
+(* The opposite function *)
+
+Definition nat_of_ascii (a : ascii) : nat :=
+  let (a1, a2, a3, a4, a5, a6, a7, a8) := a in
+      2 *
+      (2 *
+       (2 *
+        (2 *
+         (2 *
+          (2 *
+           (2 * (if a8 then 1 else 0)
+            + (if a7 then 1 else 0))
+           + (if a6 then 1 else 0))
+          + (if a5 then 1 else 0))
+         + (if a4 then 1 else 0))
+        + (if a3 then 1 else 0))
+       + (if a2 then 1 else 0))
+      + (if a1 then 1 else 0).
+
+Theorem ascii_nat_embedding : 
+  forall a : ascii, ascii_of_nat (nat_of_ascii a) = a.
+Proof.
+  destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity.
+Abort.
+
+(********************************)
+(** Examples of concrete syntax *)
+(********************************)
+
+Open Local Scope char_scope.
+
+Example Space := " ".
+Example DoubleQuote := """".
+Example Beep := "007".
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
new file mode 100644
index 000000000..82da318c5
--- /dev/null
+++ b/theories/Strings/String.v
@@ -0,0 +1,390 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(** Contributed by Laurent Théry (INRIA);
+    Adapted to Coq V8 by the Coq Development Team *)
+
+Require Import Arith.
+Require Import Ascii.
+
+(******************************)
+(** Definition of strings     *)
+(******************************)
+
+(** Implementation of string as list of ascii characters *)
+ 
+Inductive string : Set :=
+  | EmptyString : string
+  | String : ascii -> string -> string.
+
+Delimit Scope string_scope with string.
+Bind Scope string_scope with string.
+Open Local Scope string_scope.
+
+(** Equality is decidable *)
+
+Definition string_dec : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}.
+ decide equality; apply ascii_dec.
+Defined.
+
+(******************************)
+(** Concatenation of strings  *)
+(******************************)
+
+Reserved Notation "x ++ y" (right associativity, at level 60).
+
+Fixpoint append (s1 s2 : string) {struct s1} : string :=
+  match s1 with
+  | EmptyString => s2
+  | String c s1' => String c (s1' ++ s2)
+  end
+
+where "s1 ++ s2" := (append s1 s2) : string_scope.
+
+(******************************)
+(** Length                    *)
+(******************************)
+ 
+Fixpoint length (s : string) : nat :=
+  match s with
+  | EmptyString => 0
+  | String c s' => S (length s')
+  end.
+
+(******************************)
+(** Nth character of a string *)
+(******************************)
+ 
+Fixpoint get (n : nat) (s : string) {struct s} : option ascii :=
+  match s with
+  | EmptyString => None
+  | String c s' => match n with
+                   | O => Some c
+                   | S n' => get n' s'
+                   end
+  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.
+intros s1; elim s1; simpl in |- *.
+intros s2; case s2; simpl in |- *; split; auto.
+intros H; generalize (H 0); intros H1; inversion H1.
+intros; discriminate.
+intros a s1' Rec s2; case s2; simpl in |- *; split; auto.
+intros H; generalize (H 0); intros H1; inversion H1.
+intros; discriminate.
+intros H; generalize (H 0); simpl in |- *; intros H1; inversion H1.
+case (Rec s).
+intros H0; rewrite H0; auto.
+intros n; exact (H (S n)).
+intros H; injection H; intros H1 H2 n; case n; auto.
+rewrite H2; trivial.
+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).
+Proof.
+intros s1; elim s1; simpl in |- *; auto.
+intros s2 n H; inversion H.
+intros a s1' Rec s2 n; case n; simpl in |- *; auto.
+intros n0 H; apply Rec; auto.
+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).
+Proof.
+intros s1; elim s1; simpl in |- *; auto.
+intros s2 n; rewrite plus_comm; simpl in |- *; auto.
+intros a s1' Rec s2 n; case n; simpl in |- *; auto.
+generalize (Rec s2 0); simpl in |- *; auto.
+intros n0; rewrite <- Plus.plus_Snm_nSm; auto.
+Qed.
+
+(******************************)
+(** Substrings                *)
+(******************************)
+
+(** [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
+  | 0, S m', EmptyString => s
+  | 0, S m', String c s' => String c (substring 0 m' s')
+  | S n', _, EmptyString => s
+  | S n', _, String c s' => substring n' m s'
+  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.
+Proof.
+intros s; elim s; simpl in |- *; auto.
+intros n; case n; simpl in |- *; auto.
+intros m; case m; simpl in |- *; auto.
+intros a s' Rec; intros n; case n; simpl in |- *; auto.
+intros m; case m; simpl in |- *; auto.
+intros p H; inversion H.
+intros m' p; case p; simpl in |- *; auto.
+intros n0 H; apply Rec; simpl in |- *; auto.
+apply Lt.lt_S_n; auto.
+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.
+intros s; elim s; simpl in |- *; auto.
+intros n; case n; simpl in |- *; auto.
+intros m; case m; simpl in |- *; auto.
+intros a s' Rec; intros n; case n; simpl in |- *; auto.
+intros m; case m; simpl in |- *; auto.
+intros m' p; case p; simpl in |- *; auto.
+intros H; inversion H.
+intros n0 H; apply Rec; simpl in |- *; auto.
+apply Le.le_S_n; auto.
+Qed.
+
+(******************************)
+(** Test functions            *)
+(******************************)
+
+(** Test if [s1] is a prefix of [s2] *)
+ 
+Fixpoint prefix (s1 s2 : string) {struct s2} : bool :=
+  match s1 with
+  | EmptyString => true
+  | String a s1' =>
+      match s2 with
+      | EmptyString => false
+      | String b s2' =>
+          match ascii_dec a b with
+          | left _ => prefix s1' s2'
+          | right _ => false
+          end
+      end
+  end.
+
+(** 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.
+Proof.
+intros s1; elim s1; simpl in |- *; auto.
+intros s2; case s2; simpl in |- *; split; auto.
+intros a s1' Rec s2; case s2; simpl in |- *; auto.
+split; intros; discriminate.
+intros b s2'; case (ascii_dec a b); simpl in |- *; auto.
+intros e; case (Rec s2'); intros H1 H2; split; intros H3; auto.
+rewrite e; rewrite H1; auto.
+apply H2; injection H3; auto.
+intros n; split; intros; try discriminate.
+case n; injection H; auto.
+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 =>
+      match s1 with
+      | EmptyString => Some 0
+      | String a s1' => None
+      end
+  | EmptyString, S n' => None
+  | String b s2', 0 => 
+      if prefix s1 s2 then Some 0
+      else
+        match index 0 s1 s2' with
+        | Some n => Some (S n)
+        | None => None
+        end
+   | String b s2', S n' =>
+      match index n' s1 s2' with
+      | Some n => Some (S n)
+      | None => None
+      end
+  end.
+
+(* Dirty trick to evaluate locally that prefix reduces itself *)
+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.
+Proof.
+intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl in |- *;
+ auto.
+intros n; case n; simpl in |- *; auto.
+intros m s1; case s1; simpl in |- *; auto.
+intros H; injection H; intros H1; rewrite <- H1; auto.
+intros; discriminate.
+intros; discriminate.
+intros b s2' Rec n m s1.
+case n; simpl in |- *; auto.
+generalize (prefix_correct s1 (String b s2'));
+ case (prefix s1 (String b s2')).
+intros H0 H; injection H; intros H1; rewrite <- H1; auto.
+case H0; simpl in |- *; auto.
+case m; simpl in |- *; auto.
+case (index 0 s1 s2'); intros; discriminate.
+intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto.
+intros x H H0 H1; apply H; injection H1; intros H2; injection H2; auto.
+intros; discriminate.
+intros n'; case m; simpl in |- *; auto.
+case (index n' s1 s2'); intros; discriminate.
+intros m'; generalize (Rec n' m' s1); case (index n' s1 s2'); auto.
+intros x H H1; apply H; injection H1; intros H2; injection H2; auto.
+intros; discriminate.
+Qed.
+
+(** 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 ->
+ forall p : nat, n <= p -> p < m -> substring p (length s1) s2 <> s1.
+Proof.
+intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl in |- *;
+ auto.
+intros n; case n; simpl in |- *; auto.
+intros m s1; case s1; simpl in |- *; auto.
+intros H; injection H; intros H1; rewrite <- H1.
+intros p H0 H2; inversion H2.
+intros; discriminate.
+intros; discriminate.
+intros b s2' Rec n m s1.
+case n; simpl in |- *; auto.
+generalize (prefix_correct s1 (String b s2'));
+ case (prefix s1 (String b s2')).
+intros H0 H; injection H; intros H1; rewrite <- H1; auto.
+intros p H2 H3; inversion H3.
+case m; simpl in |- *; auto.
+case (index 0 s1 s2'); intros; discriminate.
+intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto.
+intros x H H0 H1 p; try case p; simpl in |- *; auto.
+intros H2 H3; red in |- *; intros H4; case H0.
+intros H5 H6; absurd (false = true); auto with bool.
+intros n0 H2 H3; apply H; auto.
+injection H1; intros H4; injection H4; auto.
+apply Le.le_O_n.
+apply Lt.lt_S_n; auto.
+intros; discriminate.
+intros n'; case m; simpl in |- *; auto.
+case (index n' s1 s2'); intros; discriminate.
+intros m'; generalize (Rec n' m' s1); case (index n' s1 s2'); auto.
+intros x H H0 p; case p; simpl in |- *; auto.
+intros H1; inversion H1; auto.
+intros n0 H1 H2; apply H; auto.
+injection H0; intros H3; injection H3; auto.
+apply Le.le_S_n; auto.
+apply Lt.lt_S_n; auto.
+intros; discriminate.
+Qed.
+
+(** 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 ->
+ s1 <> EmptyString -> n <= m -> substring m (length s1) s2 <> s1.
+Proof.
+intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl in |- *;
+ auto.
+intros n; case n; simpl in |- *; auto.
+intros m s1; case s1; simpl in |- *; auto.
+case m; intros; red in |- *; intros; discriminate.
+intros n' m; case m; auto.
+intros s1; case s1; simpl in |- *; auto.
+intros b s2' Rec n m s1.
+case n; simpl in |- *; auto.
+generalize (prefix_correct s1 (String b s2'));
+ case (prefix s1 (String b s2')).
+intros; discriminate.
+case m; simpl in |- *; auto with bool.
+case s1; simpl in |- *; auto.
+intros a s H H0 H1 H2; red in |- *; intros H3; case H.
+intros H4 H5; absurd (false = true); auto with bool.
+case s1; simpl in |- *; auto.
+intros a s n0 H H0 H1 H2;
+ change (substring n0 (length (String a s)) s2' <> String a s) in |- *;
+ apply (Rec 0); auto.
+generalize H0; case (index 0 (String a s) s2'); simpl in |- *; auto; intros;
+ discriminate.
+apply Le.le_O_n.
+intros n'; case m; simpl in |- *; auto.
+intros H H0 H1; inversion H1.
+intros n0 H H0 H1; apply (Rec n'); auto.
+generalize H; case (index n' s1 s2'); simpl in |- *; auto; intros;
+ discriminate.
+apply Le.le_S_n; auto.
+Qed.
+
+(* Back to normal for prefix *)
+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.
+Proof.
+intros n s; generalize n; clear n; elim s; simpl in |- *; auto.
+intros n; case n; simpl in |- *; auto.
+intros; discriminate.
+intros; apply Lt.lt_O_Sn.
+intros a s' H n; case n; simpl in |- *; auto.
+intros; discriminate.
+intros n'; generalize (H n'); case (index n' EmptyString s'); simpl in |- *;
+ auto.
+intros; discriminate.
+intros H0 H1; apply Lt.lt_n_S; auto.
+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
+  | None => 0
+  end.
+
+(********************************)
+(** Examples of concrete syntax *)
+(********************************)
+
+Example HelloWorld := "	""Hello world!""
+".