diff options
Diffstat (limited to 'theories/Strings/String.v')
| -rw-r--r-- | theories/Strings/String.v | 140 |
1 files changed, 69 insertions, 71 deletions
diff --git a/theories/Strings/String.v b/theories/Strings/String.v index c26b8818..6294d156 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -1,14 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: String.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) @@ -26,7 +24,7 @@ Inductive string : Set := Delimit Scope string_scope with string. Bind Scope string_scope with string. -Open Local Scope string_scope. +Local Open Scope string_scope. (** Equality is decidable *) @@ -74,14 +72,14 @@ Fixpoint get (n : nat) (s : string) {struct s} : option ascii := 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 s1; elim s1; simpl. +intros s2; case s2; simpl; 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 a s1' Rec s2; case s2; simpl; split; auto. intros H; generalize (H 0); intros H1; inversion H1. intros; discriminate. -intros H; generalize (H 0); simpl in |- *; intros H1; inversion H1. +intros H; generalize (H 0); simpl; intros H1; inversion H1. case (Rec s). intros H0; rewrite H0; auto. intros n; exact (H (S n)). @@ -96,9 +94,9 @@ 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 s1; elim s1; simpl; auto. intros s2 n H; inversion H. -intros a s1' Rec s2 n; case n; simpl in |- *; auto. +intros a s1' Rec s2 n; case n; simpl; auto. intros n0 H; apply Rec; auto. apply lt_S_n; auto. Qed. @@ -109,10 +107,10 @@ 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. +intros s1; elim s1; simpl; auto. +intros s2 n; rewrite plus_comm; simpl; auto. +intros a s1' Rec s2 n; case n; simpl; auto. +generalize (Rec s2 0); simpl; auto. intros. rewrite <- Plus.plus_Snm_nSm; auto. Qed. @@ -137,16 +135,16 @@ 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 s; elim s; simpl; auto. +intros n; case n; simpl; auto. +intros m; case m; simpl; auto. +intros a s' Rec; intros n; case n; simpl; auto. +intros m; case m; simpl; auto. intros p H; inversion H. -intros m' p; case p; simpl in |- *; auto. -intros n0 H; apply Rec; simpl in |- *; auto. +intros m' p; case p; simpl; auto. +intros n0 H; apply Rec; simpl; auto. apply Lt.lt_S_n; auto. -intros n' m p H; rewrite <- Plus.plus_Snm_nSm; simpl in |- *; auto. +intros n' m p H; rewrite <- Plus.plus_Snm_nSm; simpl; auto. Qed. (** The substring has at most [m] elements *) @@ -154,14 +152,14 @@ Qed. 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 s; elim s; simpl; auto. +intros n; case n; simpl; auto. +intros m; case m; simpl; auto. +intros a s' Rec; intros n; case n; simpl; auto. +intros m; case m; simpl; auto. +intros m' p; case p; simpl; auto. intros H; inversion H. -intros n0 H; apply Rec; simpl in |- *; auto. +intros n0 H; apply Rec; simpl; auto. apply Le.le_S_n; auto. Qed. @@ -190,11 +188,11 @@ 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. +intros s1; elim s1; simpl; auto. +intros s2; case s2; simpl; split; auto. +intros a s1' Rec s2; case s2; simpl; auto. split; intros; discriminate. -intros b s2'; case (ascii_dec a b); simpl in |- *; auto. +intros b s2'; case (ascii_dec a b); simpl; auto. intros e; case (Rec s2'); intros H1 H2; split; intros H3; auto. rewrite e; rewrite H1; auto. apply H2; injection H3; auto. @@ -236,28 +234,28 @@ 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 |- *; +intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. -intros n; case n; simpl in |- *; auto. -intros m s1; case s1; simpl in |- *; auto. +intros n; case n; simpl; auto. +intros m s1; case s1; simpl; 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. +case n; simpl; 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 H0; simpl; auto. +case m; simpl; 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 x H H0 H1; apply H; injection H1; auto. intros; discriminate. -intros n'; case m; simpl in |- *; auto. +intros n'; case m; simpl; 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 x H H1; apply H; injection H1; auto. intros; discriminate. Qed. @@ -269,38 +267,38 @@ Theorem index_correct2 : 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 |- *; +intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. -intros n; case n; simpl in |- *; auto. -intros m s1; case s1; simpl in |- *; auto. +intros n; case n; simpl; auto. +intros m s1; case s1; simpl; 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. +case n; simpl; 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 m; simpl; 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 x H H0 H1 p; try case p; simpl; auto. +intros H2 H3; red; 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. +injection H1; auto. apply Le.le_O_n. apply Lt.lt_S_n; auto. intros; discriminate. -intros n'; case m; simpl in |- *; auto. +intros n'; case m; simpl; 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 x H H0 p; case p; simpl; auto. intros H1; inversion H1; auto. intros n0 H1 H2; apply H; auto. -injection H0; intros H3; injection H3; auto. +injection H0; auto. apply Le.le_S_n; auto. apply Lt.lt_S_n; auto. intros; discriminate. @@ -314,33 +312,33 @@ Theorem index_correct3 : 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 |- *; +intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; 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; case n; simpl; auto. +intros m s1; case s1; simpl; auto. +case m; intros; red; intros; discriminate. intros n' m; case m; auto. -intros s1; case s1; simpl in |- *; auto. +intros s1; case s1; simpl; auto. intros b s2' Rec n m s1. -case n; simpl in |- *; auto. +case n; simpl; 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. +case m; simpl; auto with bool. +case s1; simpl; auto. +intros a s H H0 H1 H2; red; intros H3; case H. intros H4 H5; absurd (false = true); auto with bool. -case s1; simpl in |- *; auto. +case s1; simpl; auto. intros a s n0 H H0 H1 H2; - change (substring n0 (length (String a s)) s2' <> String a s) in |- *; + change (substring n0 (length (String a s)) s2' <> String a s); apply (Rec 0); auto. -generalize H0; case (index 0 (String a s) s2'); simpl in |- *; auto; intros; +generalize H0; case (index 0 (String a s) s2'); simpl; auto; intros; discriminate. apply Le.le_O_n. -intros n'; case m; simpl in |- *; auto. +intros n'; case m; simpl; 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; +generalize H; case (index n' s1 s2'); simpl; auto; intros; discriminate. apply Le.le_S_n; auto. Qed. @@ -355,13 +353,13 @@ 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 n s; generalize n; clear n; elim s; simpl; auto. +intros n; case n; simpl; auto. intros; discriminate. intros; apply Lt.lt_O_Sn. -intros a s' H n; case n; simpl in |- *; auto. +intros a s' H n; case n; simpl; auto. intros; discriminate. -intros n'; generalize (H n'); case (index n' EmptyString s'); simpl in |- *; +intros n'; generalize (H n'); case (index n' EmptyString s'); simpl; auto. intros; discriminate. intros H0 H1; apply Lt.lt_n_S; auto. |