String.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team

Require Import Arith.
Require Import Ascii.
Require Import Bool.
Require Import Coq.Strings.Byte.

Definition of strings

Implementation of string as list of ascii characters

Inductive string : Set :=
  | EmptyString : string
  | String : ascii -> string -> string.

Declare Scope string_scope.
Delimit Scope string_scope with string.
Bind Scope string_scope with string.
Local Open Scope string_scope.

Register EmptyString as plugins.syntax.EmptyString.
Register String as plugins.syntax.String.

Equality is decidable

Definition string_dec : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}.forall s1 s2 : string, {s1 = s2} + {s1 <> s2}
Proof.forall s1 s2 : string, {s1 = s2} + {s1 <> s2}
 decide equality; apply ascii_dec.
Defined.

Local Open Scope lazy_bool_scope.

Fixpoint eqb s1 s2 : bool :=
 match s1, s2 with
 | EmptyString, EmptyString => true
 | String c1 s1', String c2 s2' => Ascii.eqb c1 c2 &&& eqb s1' s2'
 | _,_ => false
 end.

Infix "=?" := eqb : string_scope.

Lemma eqb_spec s1 s2 : Bool.reflect (s1 = s2) (s1 =? s2)%string.s1, s2:string
reflect (s1 = s2) (s1 =? s2)
Proof.s1, s2:string
reflect (s1 = s2) (s1 =? s2)
 revert s2.s1:string
forall s2 : string, reflect (s1 = s2) (s1 =? s2) induction s1; destruct s2; try (constructor; easy); simpl.a:ascii
s1:string
IHs1:forall s0 : string,
reflect (s1 = s0) (s1 =? s0)
a0:ascii
s2:string
reflect (String a s1 = String a0 s2)
  ((a =? a0)%char &&& (s1 =? s2))
 case Ascii.eqb_spec; simpl; [intros -> | constructor; now intros [= ]].s1:string
IHs1:forall s0 : string,
reflect (s1 = s0) (s1 =? s0)
a0:ascii
s2:string
reflect (String a0 s1 = String a0 s2) (s1 =? s2)
 case IHs1; [intros ->; now constructor | constructor; now intros [= ]].
Qed.

Ltac t_eqb :=
  repeat first [ congruence
               | progress subst
               | apply conj
               | match goal with
                 | [ |- context[eqb ?x ?y] ] => destruct (eqb_spec x y)
                 end
               | intro ].
Lemma eqb_refl x : (x =? x)%string = true.x:string
(x =? x) = true Proof.x:string
(x =? x) = true t_eqb. Qed.
Lemma eqb_sym x y : (x =? y)%string = (y =? x)%string.x, y:string
(x =? y) = (y =? x) Proof.x, y:string
(x =? y) = (y =? x) t_eqb. Qed.
Lemma eqb_eq n m : (n =? m)%string = true <-> n = m.n, m:string
(n =? m) = true <-> n = m Proof.n, m:string
(n =? m) = true <-> n = m t_eqb. Qed.
Lemma eqb_neq x y : (x =? y)%string = false <-> x <> y.x, y:string
(x =? y) = false <-> x <> y Proof.x, y:string
(x =? y) = false <-> x <> y t_eqb. Qed.
Lemma eqb_compat: Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) eqb.Morphisms.Proper
  (Morphisms.respectful eq
     (Morphisms.respectful eq eq)) eqb
Proof.Morphisms.Proper
  (Morphisms.respectful eq
     (Morphisms.respectful eq eq)) eqb t_eqb. Qed.

Concatenation of strings

Reserved Notation "x ++ y" (right associativity, at level 60).

Fixpoint append (s1 s2 : string) : 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.forall s1 s2 : string,
(forall n : nat, get n s1 = get n s2) <-> s1 = s2
Proof.forall s1 s2 : string,
(forall n : nat, get n s1 = get n s2) <-> s1 = s2
intros s1; elim s1; simpl.s1:string
forall s2 : string,
(forall n : nat, None = get n s2) <-> EmptyString = s2
s1:string
forall (a : ascii) (s : string),
(forall s2 : string,
 (forall n : nat, get n s = get n s2) <-> s = s2) ->
forall s2 : string,
(forall n : nat,
 match n with
 | 0 => Some a
 | S n' => get n' s
 end = get n s2) <-> String a s = s2
intros s2; case s2; simpl; split; auto.s1, s2:string
a:ascii
s:string
(forall n : nat,
 None =
 match n with
 | 0 => Some a
 | S n' => get n' s
 end) -> EmptyString = String a s
s1, s2:string
a:ascii
s:string
EmptyString = String a s ->
forall n : nat,
None =
match n with
| 0 => Some a
| S n' => get n' s
end
s1:string
forall (a : ascii) (s : string),
(forall s2 : string,
 (forall n : nat, get n s = get n s2) <-> s = s2) ->
forall s2 : string,
(forall n : nat,
 match n with
 | 0 => Some a
 | S n' => get n' s
 end = get n s2) <-> String a s = s2
intros H; generalize (H O); intros H1; inversion H1.s1, s2:string
a:ascii
s:string
EmptyString = String a s ->
forall n : nat,
None =
match n with
| 0 => Some a
| S n' => get n' s
end
s1:string
forall (a : ascii) (s : string),
(forall s2 : string,
 (forall n : nat, get n s = get n s2) <-> s = s2) ->
forall s2 : string,
(forall n : nat,
 match n with
 | 0 => Some a
 | S n' => get n' s
 end = get n s2) <-> String a s = s2
intros; discriminate.s1:string
forall (a : ascii) (s : string),
(forall s2 : string,
 (forall n : nat, get n s = get n s2) <-> s = s2) ->
forall s2 : string,
(forall n : nat,
 match n with
 | 0 => Some a
 | S n' => get n' s
 end = get n s2) <-> String a s = s2
intros a s1' Rec s2; case s2; simpl; split; auto.s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
(forall n : nat,
 match n with
 | 0 => Some a
 | S n' => get n' s1'
 end = None) -> String a s1' = EmptyString
s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
String a s1' = EmptyString ->
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end = None
s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
(forall n : nat,
 match n with
 | 0 => Some a
 | S n' => get n' s1'
 end =
 match n with
 | 0 => Some a0
 | S n' => get n' s
 end) -> String a s1' = String a0 s
s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
String a s1' = String a0 s ->
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
intros H; generalize (H O); intros H1; inversion H1.s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
String a s1' = EmptyString ->
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end = None
s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
(forall n : nat,
 match n with
 | 0 => Some a
 | S n' => get n' s1'
 end =
 match n with
 | 0 => Some a0
 | S n' => get n' s
 end) -> String a s1' = String a0 s
s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
String a s1' = String a0 s ->
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
intros; discriminate.s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
(forall n : nat,
 match n with
 | 0 => Some a
 | S n' => get n' s1'
 end =
 match n with
 | 0 => Some a0
 | S n' => get n' s
 end) -> String a s1' = String a0 s
s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
String a s1' = String a0 s ->
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
intros H; generalize (H O); simpl; intros H1; inversion H1.s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
H:forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
H1:Some a = Some a0
H2:a = a0
String a0 s1' = String a0 s
s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
String a s1' = String a0 s ->
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
case (Rec s).s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
H:forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
H1:Some a = Some a0
H2:a = a0
((forall n : nat, get n s1' = get n s) -> s1' = s) ->
(s1' = s -> forall n : nat, get n s1' = get n s) ->
String a0 s1' = String a0 s
s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
String a s1' = String a0 s ->
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
intros H0; rewrite H0; auto.s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
H:forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
H1:Some a = Some a0
H2:a = a0
H0:(forall n : nat, get n s1' = get n s) -> s1' = s
forall n : nat, get n s1' = get n s
s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
String a s1' = String a0 s ->
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
intros n; exact (H (S n)).s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
String a s1' = String a0 s ->
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
intros H; injection H as H1 H2.s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
H1:a = a0
H2:s1' = s
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s1'
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
rewrite H2; trivial.s1:string
a:ascii
s1':string
Rec:forall s0 : string, (forall n : nat, get n s1' = get n s0) <-> s1' = s0
s2:string
a0:ascii
s:string
H1:a = a0
H2:s1' = s
forall n : nat,
match n with
| 0 => Some a
| S n' => get n' s
end =
match n with
| 0 => Some a0
| S n' => get n' s
end
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).forall (s1 s2 : string) (n : nat),
n < length s1 -> get n s1 = get n (s1 ++ s2)
Proof.forall (s1 s2 : string) (n : nat),
n < length s1 -> get n s1 = get n (s1 ++ s2)
intros s1; elim s1; simpl; auto.s1:string
forall (s2 : string) (n : nat),
n < 0 -> None = get n s2
s1:string
forall (a : ascii) (s : string),
(forall (s2 : string) (n : nat),
 n < length s -> get n s = get n (s ++ s2)) ->
forall (s2 : string) (n : nat),
n < S (length s) ->
match n with
| 0 => Some a
| S n' => get n' s
end =
match n with
| 0 => Some a
| S n' => get n' (s ++ s2)
end
intros s2 n H; inversion H.s1:string
forall (a : ascii) (s : string),
(forall (s2 : string) (n : nat),
 n < length s -> get n s = get n (s ++ s2)) ->
forall (s2 : string) (n : nat),
n < S (length s) ->
match n with
| 0 => Some a
| S n' => get n' s
end =
match n with
| 0 => Some a
| S n' => get n' (s ++ s2)
end
intros a s1' Rec s2 n; case n; simpl; auto.s1:string
a:ascii
s1':string
Rec:forall (s0 : string) (n0 : nat),
n0 < length s1' -> get n0 s1' = get n0 (s1' ++ s0)
s2:string
n:nat
forall n0 : nat,
S n0 < S (length s1') ->
get n0 s1' = get n0 (s1' ++ s2)
intros n0 H; apply Rec; auto.s1:string
a:ascii
s1':string
Rec:forall (s0 : string) (n1 : nat),
n1 < length s1' -> get n1 s1' = get n1 (s1' ++ s0)
s2:string
n, n0:nat
H:S n0 < S (length s1')
n0 < length s1'
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).forall (s1 s2 : string) (n : nat),
get n s2 = get (n + length s1) (s1 ++ s2)
Proof.forall (s1 s2 : string) (n : nat),
get n s2 = get (n + length s1) (s1 ++ s2)
intros s1; elim s1; simpl; auto.s1:string
forall (s2 : string) (n : nat),
get n s2 = get (n + 0) s2
s1:string
forall (a : ascii) (s : string),
(forall (s2 : string) (n : nat),
 get n s2 = get (n + length s) (s ++ s2)) ->
forall (s2 : string) (n : nat),
get n s2 =
match n + S (length s) with
| 0 => Some a
| S n' => get n' (s ++ s2)
end
intros s2 n; rewrite plus_comm; simpl; auto.s1:string
forall (a : ascii) (s : string),
(forall (s2 : string) (n : nat),
 get n s2 = get (n + length s) (s ++ s2)) ->
forall (s2 : string) (n : nat),
get n s2 =
match n + S (length s) with
| 0 => Some a
| S n' => get n' (s ++ s2)
end
intros a s1' Rec s2 n; case n; simpl; auto.s1:string
a:ascii
s1':string
Rec:forall (s0 : string) (n0 : nat),
get n0 s0 = get (n0 + length s1') (s1' ++ s0)
s2:string
n:nat
get 0 s2 = get (length s1') (s1' ++ s2)
s1:string
a:ascii
s1':string
Rec:forall (s0 : string) (n0 : nat),
get n0 s0 = get (n0 + length s1') (s1' ++ s0)
s2:string
n:nat
forall n0 : nat,
get (S n0) s2 = get (n0 + S (length s1')) (s1' ++ s2)
generalize (Rec s2 O); simpl; auto.s1:string
a:ascii
s1':string
Rec:forall (s0 : string) (n0 : nat),
get n0 s0 = get (n0 + length s1') (s1' ++ s0)
s2:string
n:nat
forall n0 : nat,
get (S n0) s2 = get (n0 + S (length s1')) (s1' ++ s2) intros.s1:string
a:ascii
s1':string
Rec:forall (s0 : string) (n1 : nat),
get n1 s0 = get (n1 + length s1') (s1' ++ s0)
s2:string
n, n0:nat
get (S n0) s2 = get (n0 + S (length s1')) (s1' ++ s2)
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) : string :=
  match n, m, s with
  | O, O, _ => EmptyString
  | O, S m', EmptyString => s
  | O, 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.forall (s : string) (n m p : nat),
p < m -> get p (substring n m s) = get (p + n) s
Proof.forall (s : string) (n m p : nat),
p < m -> get p (substring n m s) = get (p + n) s
intros s; elim s; simpl; auto.s:string
forall n m p : nat,
p < m ->
get p
  match n with
  | 0 => match m with
         | 0 | _ => EmptyString
         end
  | S _ => EmptyString
  end = None
s:string
forall (a : ascii) (s0 : string),
(forall n m p : nat,
 p < m -> get p (substring n m s0) = get (p + n) s0) ->
forall n m p : nat,
p < m ->
get p
  match n with
  | 0 =>
      match m with
      | 0 => EmptyString
      | S m' => String a (substring 0 m' s0)
      end
  | S n' => substring n' m s0
  end =
match p + n with
| 0 => Some a
| S n' => get n' s0
end
intros n; case n; simpl; auto.s:string
n:nat
forall m p : nat,
p < m ->
get p match m with
      | 0 | _ => EmptyString
      end = None
s:string
forall (a : ascii) (s0 : string),
(forall n m p : nat,
 p < m -> get p (substring n m s0) = get (p + n) s0) ->
forall n m p : nat,
p < m ->
get p
  match n with
  | 0 =>
      match m with
      | 0 => EmptyString
      | S m' => String a (substring 0 m' s0)
      end
  | S n' => substring n' m s0
  end =
match p + n with
| 0 => Some a
| S n' => get n' s0
end
intros m; case m; simpl; auto.s:string
forall (a : ascii) (s0 : string),
(forall n m p : nat,
 p < m -> get p (substring n m s0) = get (p + n) s0) ->
forall n m p : nat,
p < m ->
get p
  match n with
  | 0 =>
      match m with
      | 0 => EmptyString
      | S m' => String a (substring 0 m' s0)
      end
  | S n' => substring n' m s0
  end =
match p + n with
| 0 => Some a
| S n' => get n' s0
end
intros a s' Rec; intros n; case n; simpl; auto.s:string
a:ascii
s':string
Rec:forall n0 m p : nat, p < m -> get p (substring n0 m s') = get (p + n0) s'
n:nat
forall m p : nat,
p < m ->
get p
  match m with
  | 0 => EmptyString
  | S m' => String a (substring 0 m' s')
  end =
match p + 0 with
| 0 => Some a
| S n' => get n' s'
end
s:string
a:ascii
s':string
Rec:forall n0 m p : nat, p < m -> get p (substring n0 m s') = get (p + n0) s'
n:nat
forall n0 m p : nat,
p < m ->
get p (substring n0 m s') =
match p + S n0 with
| 0 => Some a
| S n' => get n' s'
end
intros m; case m; simpl; auto.s:string
a:ascii
s':string
Rec:forall n0 m0 p : nat, p < m0 -> get p (substring n0 m0 s') = get (p + n0) s'
n, m:nat
forall p : nat,
p < 0 ->
None =
match p + 0 with
| 0 => Some a
| S n' => get n' s'
end
s:string
a:ascii
s':string
Rec:forall n0 m0 p : nat, p < m0 -> get p (substring n0 m0 s') = get (p + n0) s'
n, m:nat
forall n0 p : nat,
p < S n0 ->
match p with
| 0 => Some a
| S n' => get n' (substring 0 n0 s')
end =
match p + 0 with
| 0 => Some a
| S n' => get n' s'
end
s:string
a:ascii
s':string
Rec:forall n0 m p : nat, p < m -> get p (substring n0 m s') = get (p + n0) s'
n:nat
forall n0 m p : nat,
p < m ->
get p (substring n0 m s') =
match p + S n0 with
| 0 => Some a
| S n' => get n' s'
end
intros p H; inversion H.s:string
a:ascii
s':string
Rec:forall n0 m0 p : nat, p < m0 -> get p (substring n0 m0 s') = get (p + n0) s'
n, m:nat
forall n0 p : nat,
p < S n0 ->
match p with
| 0 => Some a
| S n' => get n' (substring 0 n0 s')
end =
match p + 0 with
| 0 => Some a
| S n' => get n' s'
end
s:string
a:ascii
s':string
Rec:forall n0 m p : nat, p < m -> get p (substring n0 m s') = get (p + n0) s'
n:nat
forall n0 m p : nat,
p < m ->
get p (substring n0 m s') =
match p + S n0 with
| 0 => Some a
| S n' => get n' s'
end
intros m' p; case p; simpl; auto.s:string
a:ascii
s':string
Rec:forall n0 m0 p0 : nat,
p0 < m0 -> get p0 (substring n0 m0 s') = get (p0 + n0) s'
n, m, m', p:nat
forall n0 : nat,
S n0 < S m' ->
get n0 (substring 0 m' s') = get (n0 + 0) s'
s:string
a:ascii
s':string
Rec:forall n0 m p : nat, p < m -> get p (substring n0 m s') = get (p + n0) s'
n:nat
forall n0 m p : nat,
p < m ->
get p (substring n0 m s') =
match p + S n0 with
| 0 => Some a
| S n' => get n' s'
end
intros n0 H; apply Rec; simpl; auto.s:string
a:ascii
s':string
Rec:forall n1 m0 p0 : nat,
p0 < m0 -> get p0 (substring n1 m0 s') = get (p0 + n1) s'
n, m, m', p, n0:nat
H:S n0 < S m'
n0 < m'
s:string
a:ascii
s':string
Rec:forall n0 m p : nat, p < m -> get p (substring n0 m s') = get (p + n0) s'
n:nat
forall n0 m p : nat,
p < m ->
get p (substring n0 m s') =
match p + S n0 with
| 0 => Some a
| S n' => get n' s'
end
apply Lt.lt_S_n; auto.s:string
a:ascii
s':string
Rec:forall n0 m p : nat, p < m -> get p (substring n0 m s') = get (p + n0) s'
n:nat
forall n0 m p : nat,
p < m ->
get p (substring n0 m s') =
match p + S n0 with
| 0 => Some a
| S n' => get n' s'
end
intros n' m p H; rewrite <- Plus.plus_Snm_nSm; simpl; 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.forall (s : string) (n m p : nat),
m <= p -> get p (substring n m s) = None
Proof.forall (s : string) (n m p : nat),
m <= p -> get p (substring n m s) = None
intros s; elim s; simpl; auto.s:string
forall n m p : nat,
m <= p ->
get p
  match n with
  | 0 => match m with
         | 0 | _ => EmptyString
         end
  | S _ => EmptyString
  end = None
s:string
forall (a : ascii) (s0 : string),
(forall n m p : nat,
 m <= p -> get p (substring n m s0) = None) ->
forall n m p : nat,
m <= p ->
get p
  match n with
  | 0 =>
      match m with
      | 0 => EmptyString
      | S m' => String a (substring 0 m' s0)
      end
  | S n' => substring n' m s0
  end = None
intros n; case n; simpl; auto.s:string
n:nat
forall m p : nat,
m <= p ->
get p match m with
      | 0 | _ => EmptyString
      end = None
s:string
forall (a : ascii) (s0 : string),
(forall n m p : nat,
 m <= p -> get p (substring n m s0) = None) ->
forall n m p : nat,
m <= p ->
get p
  match n with
  | 0 =>
      match m with
      | 0 => EmptyString
      | S m' => String a (substring 0 m' s0)
      end
  | S n' => substring n' m s0
  end = None
intros m; case m; simpl; auto.s:string
forall (a : ascii) (s0 : string),
(forall n m p : nat,
 m <= p -> get p (substring n m s0) = None) ->
forall n m p : nat,
m <= p ->
get p
  match n with
  | 0 =>
      match m with
      | 0 => EmptyString
      | S m' => String a (substring 0 m' s0)
      end
  | S n' => substring n' m s0
  end = None
intros a s' Rec; intros n; case n; simpl; auto.s:string
a:ascii
s':string
Rec:forall n0 m p : nat, m <= p -> get p (substring n0 m s') = None
n:nat
forall m p : nat,
m <= p ->
get p
  match m with
  | 0 => EmptyString
  | S m' => String a (substring 0 m' s')
  end = None
intros m; case m; simpl; auto.s:string
a:ascii
s':string
Rec:forall n0 m0 p : nat, m0 <= p -> get p (substring n0 m0 s') = None
n, m:nat
forall n0 p : nat,
S n0 <= p ->
match p with
| 0 => Some a
| S n' => get n' (substring 0 n0 s')
end = None
intros m' p; case p; simpl; auto.s:string
a:ascii
s':string
Rec:forall n0 m0 p0 : nat, m0 <= p0 -> get p0 (substring n0 m0 s') = None
n, m, m', p:nat
S m' <= 0 -> Some a = None
s:string
a:ascii
s':string
Rec:forall n0 m0 p0 : nat, m0 <= p0 -> get p0 (substring n0 m0 s') = None
n, m, m', p:nat
forall n0 : nat,
S m' <= S n0 -> get n0 (substring 0 m' s') = None
intros H; inversion H.s:string
a:ascii
s':string
Rec:forall n0 m0 p0 : nat, m0 <= p0 -> get p0 (substring n0 m0 s') = None
n, m, m', p:nat
forall n0 : nat,
S m' <= S n0 -> get n0 (substring 0 m' s') = None
intros n0 H; apply Rec; simpl; auto.s:string
a:ascii
s':string
Rec:forall n1 m0 p0 : nat, m0 <= p0 -> get p0 (substring n1 m0 s') = None
n, m, m', p, n0:nat
H:S m' <= S n0
m' <= n0
apply Le.le_S_n; auto.
Qed.

Concatenating lists of strings

concat sep sl concatenates the list of strings sl, inserting the separator string sep between each.

Fixpoint concat (sep : string) (ls : list string) :=
  match ls with
  | nil => EmptyString
  | cons x nil => x
  | cons x xs => x ++ sep ++ concat sep xs
  end.

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.forall s1 s2 : string,
prefix s1 s2 = true <->
substring 0 (length s1) s2 = s1
Proof.forall s1 s2 : string,
prefix s1 s2 = true <->
substring 0 (length s1) s2 = s1
intros s1; elim s1; simpl; auto.s1:string
forall s2 : string,
prefix EmptyString s2 = true <->
substring 0 0 s2 = EmptyString
s1:string
forall (a : ascii) (s : string),
(forall s2 : string,
 prefix s s2 = true <-> substring 0 (length s) s2 = s) ->
forall s2 : string,
prefix (String a s) s2 = true <->
substring 0 (S (length s)) s2 = String a s
intros s2; case s2; simpl; split; auto.s1:string
forall (a : ascii) (s : string),
(forall s2 : string,
 prefix s s2 = true <-> substring 0 (length s) s2 = s) ->
forall s2 : string,
prefix (String a s) s2 = true <->
substring 0 (S (length s)) s2 = String a s
intros a s1' Rec s2; case s2; simpl; auto.s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
false = true <-> EmptyString = String a s1'
s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
forall (a0 : ascii) (s : string),
ascii_dec a a0 &&& prefix s1' s = true <->
String a0 (substring 0 (length s1') s) = String a s1'
split; intros; discriminate.s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
forall (a0 : ascii) (s : string),
ascii_dec a a0 &&& prefix s1' s = true <->
String a0 (substring 0 (length s1') s) = String a s1'
intros b s2'; case (ascii_dec a b); simpl; auto.s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
b:ascii
s2':string
a = b ->
prefix s1' s2' = true <->
String b (substring 0 (length s1') s2') = String a s1'
s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
b:ascii
s2':string
a <> b ->
false = true <->
String b (substring 0 (length s1') s2') = String a s1'
intros e; case (Rec s2'); intros H1 H2; split; intros H3; auto.s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
b:ascii
s2':string
e:a = b
H1:prefix s1' s2' = true ->
substring 0 (length s1') s2' = s1'
H2:substring 0 (length s1') s2' = s1' ->
prefix s1' s2' = true
H3:prefix s1' s2' = true
String b (substring 0 (length s1') s2') = String a s1'
s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
b:ascii
s2':string
e:a = b
H1:prefix s1' s2' = true ->
substring 0 (length s1') s2' = s1'
H2:substring 0 (length s1') s2' = s1' ->
prefix s1' s2' = true
H3:String b (substring 0 (length s1') s2') =
String a s1'
prefix s1' s2' = true
s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
b:ascii
s2':string
a <> b ->
false = true <->
String b (substring 0 (length s1') s2') = String a s1'
rewrite e; rewrite H1; auto.s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
b:ascii
s2':string
e:a = b
H1:prefix s1' s2' = true ->
substring 0 (length s1') s2' = s1'
H2:substring 0 (length s1') s2' = s1' ->
prefix s1' s2' = true
H3:String b (substring 0 (length s1') s2') =
String a s1'
prefix s1' s2' = true
s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
b:ascii
s2':string
a <> b ->
false = true <->
String b (substring 0 (length s1') s2') = String a s1'
apply H2; injection H3; auto.s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
b:ascii
s2':string
a <> b ->
false = true <->
String b (substring 0 (length s1') s2') = String a s1'
intros n; split; intros; try discriminate.s1:string
a:ascii
s1':string
Rec:forall s0 : string,
prefix s1' s0 = true <-> substring 0 (length s1') s0 = s1'
s2:string
b:ascii
s2':string
n:a <> b
H:String b (substring 0 (length s1') s2') =
String a s1'
false = true
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) : option nat :=
  match s2, n with
  | EmptyString, O =>
      match s1 with
      | EmptyString => Some O
      | String a s1' => None
      end
  | EmptyString, S n' => None
  | String b s2', O =>
      if prefix s1 s2 then Some O
      else
        match index O 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 avoid 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.forall (n m : nat) (s1 s2 : string),
index n s1 s2 = Some m ->
substring m (length s1) s2 = s1
Proof.forall (n m : nat) (s1 s2 : string),
index n s1 s2 = Some m ->
substring m (length s1) s2 = s1
intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl;
 auto.s2:string
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    match s1 with
    | EmptyString => Some 0
    | String _ _ => None
    end
| S _ => None
end = Some m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end = s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 substring m (length s1) s = s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end = s1
intros n; case n; simpl; auto.s2:string
n:nat
forall (m : nat) (s1 : string),
match s1 with
| EmptyString => Some 0
| String _ _ => None
end = Some m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end = s1
s2:string
n:nat
nat ->
forall (m : nat) (s1 : string),
None = Some m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end = s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 substring m (length s1) s = s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end = s1
intros m s1; case s1; simpl; auto.s2:string
n, m:nat
s1:string
Some 0 = Some m ->
match m with
| 0 | _ => EmptyString
end = EmptyString
s2:string
n, m:nat
s1:string
forall (a : ascii) (s : string),
None = Some m ->
match m with
| 0 | _ => EmptyString
end = String a s
s2:string
n:nat
nat ->
forall (m : nat) (s1 : string),
None = Some m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end = s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 substring m (length s1) s = s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end = s1
intros H; injection H as <-; auto.s2:string
n, m:nat
s1:string
forall (a : ascii) (s : string),
None = Some m ->
match m with
| 0 | _ => EmptyString
end = String a s
s2:string
n:nat
nat ->
forall (m : nat) (s1 : string),
None = Some m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end = s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 substring m (length s1) s = s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end = s1
intros; discriminate.s2:string
n:nat
nat ->
forall (m : nat) (s1 : string),
None = Some m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end = s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 substring m (length s1) s = s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end = s1
intros; discriminate.s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 substring m (length s1) s = s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end = s1
intros b s2' Rec n m s1.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
match n with
| 0 =>
    if prefix s1 (String b s2')
    then Some 0
    else
     match index 0 s1 s2' with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s2' with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
case n; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
(if prefix s1 (String b s2')
 then Some 0
 else
  match index 0 s1 s2' with
  | Some n0 => Some (S n0)
  | None => None
  end) = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
generalize (prefix_correct s1 (String b s2'));
 case (prefix s1 (String b s2')).s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
true = true <->
substring 0 (length s1) (String b s2') = s1 ->
Some 0 = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
false = true <->
substring 0 (length s1) (String b s2') = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
intros H0 H; injection H as <-; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m : nat) (s0 : string),
index n0 s0 s2' = Some m -> substring m (length s0) s2' = s0
n:nat
s1:string
H0:true = true <->
substring 0 (length s1) (String b s2') = s1
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
false = true <->
substring 0 (length s1) (String b s2') = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
case H0; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
false = true <->
substring 0 (length s1) (String b s2') = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
case m; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = Some 0 ->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some (S n0) -> substring n0 (length s1) s2' = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
case (index O s1 s2'); intros; discriminate.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some (S n0) -> substring n0 (length s1) s2' = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
intros m'; generalize (Rec O m' s1); case (index O s1 s2'); auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
m':nat
forall n0 : nat,
(Some n0 = Some m' ->
 substring m' (length s1) s2' = s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
Some (S n0) = Some (S m') ->
substring m' (length s1) s2' = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
m':nat
(None = Some m' -> substring m' (length s1) s2' = s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
None = Some (S m') ->
substring m' (length s1) s2' = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
intros x H H0 H1; apply H; injection H1; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
m':nat
(None = Some m' -> substring m' (length s1) s2' = s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
None = Some (S m') ->
substring m' (length s1) s2' = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
intros; discriminate.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end = s1
intros n'; case m; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
n':nat
match index n' s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = Some 0 ->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
n':nat
forall n0 : nat,
match index n' s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some (S n0) -> substring n0 (length s1) s2' = s1
case (index n' s1 s2'); intros; discriminate.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
n':nat
forall n0 : nat,
match index n' s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some (S n0) -> substring n0 (length s1) s2' = s1
intros m'; generalize (Rec n' m' s1); case (index n' s1 s2'); auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
n', m':nat
forall n0 : nat,
(Some n0 = Some m' ->
 substring m' (length s1) s2' = s1) ->
Some (S n0) = Some (S m') ->
substring m' (length s1) s2' = s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
n', m':nat
(None = Some m' -> substring m' (length s1) s2' = s1) ->
None = Some (S m') ->
substring m' (length s1) s2' = s1
intros x H H1; apply H; injection H1; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 -> substring m0 (length s0) s2' = s0
n, m:nat
s1:string
n', m':nat
(None = Some m' -> substring m' (length s1) s2' = s1) ->
None = Some (S m') ->
substring m' (length s1) s2' = s1
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.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.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
intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl;
 auto.s2:string
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    match s1 with
    | EmptyString => Some 0
    | String _ _ => None
    end
| S _ => None
end = Some m ->
forall p : nat,
n <= p ->
p < m ->
match p with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 forall p : nat,
 n <= p -> p < m -> substring p (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
forall p : nat,
n <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros n; case n; simpl; auto.s2:string
n:nat
forall (m : nat) (s1 : string),
match s1 with
| EmptyString => Some 0
| String _ _ => None
end = Some m ->
forall p : nat,
0 <= p ->
p < m ->
match p with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
n:nat
forall (n0 m : nat) (s1 : string),
None = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 forall p : nat,
 n <= p -> p < m -> substring p (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
forall p : nat,
n <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros m s1; case s1; simpl; auto.s2:string
n, m:nat
s1:string
Some 0 = Some m ->
forall p : nat,
0 <= p ->
p < m ->
match p with
| 0 | _ => EmptyString
end <> EmptyString
s2:string
n, m:nat
s1:string
forall (a : ascii) (s : string),
None = Some m ->
forall p : nat,
0 <= p ->
p < m ->
match p with
| 0 | _ => EmptyString
end <> String a s
s2:string
n:nat
forall (n0 m : nat) (s1 : string),
None = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 forall p : nat,
 n <= p -> p < m -> substring p (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
forall p : nat,
n <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros H; injection H as <-.s2:string
n:nat
s1:string
forall p : nat,
0 <= p ->
p < 0 ->
match p with
| 0 | _ => EmptyString
end <> EmptyString
s2:string
n, m:nat
s1:string
forall (a : ascii) (s : string),
None = Some m ->
forall p : nat,
0 <= p ->
p < m ->
match p with
| 0 | _ => EmptyString
end <> String a s
s2:string
n:nat
forall (n0 m : nat) (s1 : string),
None = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 forall p : nat,
 n <= p -> p < m -> substring p (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
forall p : nat,
n <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros p H0 H2; inversion H2.s2:string
n, m:nat
s1:string
forall (a : ascii) (s : string),
None = Some m ->
forall p : nat,
0 <= p ->
p < m ->
match p with
| 0 | _ => EmptyString
end <> String a s
s2:string
n:nat
forall (n0 m : nat) (s1 : string),
None = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 forall p : nat,
 n <= p -> p < m -> substring p (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
forall p : nat,
n <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros; discriminate.s2:string
n:nat
forall (n0 m : nat) (s1 : string),
None = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 forall p : nat,
 n <= p -> p < m -> substring p (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
forall p : nat,
n <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros; discriminate.s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = Some m ->
 forall p : nat,
 n <= p -> p < m -> substring p (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
forall p : nat,
n <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros b s2' Rec n m s1.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
match n with
| 0 =>
    if prefix s1 (String b s2')
    then Some 0
    else
     match index 0 s1 s2' with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s2' with
    | Some n0 => Some (S n0)
    | None => None
    end
end = Some m ->
forall p : nat,
n <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
case n; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
(if prefix s1 (String b s2')
 then Some 0
 else
  match index 0 s1 s2' with
  | Some n0 => Some (S n0)
  | None => None
  end) = Some m ->
forall p : nat,
0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
generalize (prefix_correct s1 (String b s2'));
 case (prefix s1 (String b s2')).s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
true = true <->
substring 0 (length s1) (String b s2') = s1 ->
Some 0 = Some m ->
forall p : nat,
0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
false = true <->
substring 0 (length s1) (String b s2') = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = Some m ->
forall p : nat,
0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros H0 H; injection H as <-; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m : nat) (s0 : string),
index n0 s0 s2' = Some m ->
forall p : nat, n0 <= p -> p < m -> substring p (length s0) s2' <> s0
n:nat
s1:string
H0:true = true <->
substring 0 (length s1) (String b s2') = s1
forall p : nat,
0 <= p ->
p < 0 ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
false = true <->
substring 0 (length s1) (String b s2') = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = Some m ->
forall p : nat,
0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros p H2 H3; inversion H3.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
false = true <->
substring 0 (length s1) (String b s2') = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = Some m ->
forall p : nat,
0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
case m; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = Some 0 ->
forall p : nat,
0 <= p ->
p < 0 ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some (S n0) ->
forall p : nat,
0 <= p ->
p < S n0 ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
case (index 0 s1 s2'); intros; discriminate.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some (S n0) ->
forall p : nat,
0 <= p ->
p < S n0 ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros m'; generalize (Rec O m' s1); case (index 0 s1 s2'); auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
m':nat
forall n0 : nat,
(Some n0 = Some m' ->
 forall p : nat,
 0 <= p -> p < m' -> substring p (length s1) s2' <> s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
Some (S n0) = Some (S m') ->
forall p : nat,
0 <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
m':nat
(None = Some m' ->
 forall p : nat,
 0 <= p -> p < m' -> substring p (length s1) s2' <> s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
None = Some (S m') ->
forall p : nat,
0 <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros x H H0 H1 p; try case p; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p0 : nat, n0 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p:nat
0 <= 0 ->
0 < S m' ->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p0 : nat, n0 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p:nat
forall n0 : nat,
0 <= S n0 ->
S n0 < S m' -> substring n0 (length s1) s2' <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
m':nat
(None = Some m' ->
 forall p : nat,
 0 <= p -> p < m' -> substring p (length s1) s2' <> s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
None = Some (S m') ->
forall p : nat,
0 <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros H2 H3; red; intros H4; case H0.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p0 : nat, n0 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p:nat
H2:0 <= 0
H3:0 < S m'
H4:match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
(false = true ->
 match length s1 with
 | 0 => EmptyString
 | S m'0 => String b (substring 0 m'0 s2')
 end = s1) ->
(match length s1 with
 | 0 => EmptyString
 | S m'0 => String b (substring 0 m'0 s2')
 end = s1 -> false = true) -> False
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p0 : nat, n0 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p:nat
forall n0 : nat,
0 <= S n0 ->
S n0 < S m' -> substring n0 (length s1) s2' <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
m':nat
(None = Some m' ->
 forall p : nat,
 0 <= p -> p < m' -> substring p (length s1) s2' <> s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
None = Some (S m') ->
forall p : nat,
0 <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros H5 H6; absurd (false = true); auto with bool.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p0 : nat, n0 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p:nat
forall n0 : nat,
0 <= S n0 ->
S n0 < S m' -> substring n0 (length s1) s2' <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
m':nat
(None = Some m' ->
 forall p : nat,
 0 <= p -> p < m' -> substring p (length s1) s2' <> s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
None = Some (S m') ->
forall p : nat,
0 <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros n0 H2 H3; apply H; auto.s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p, n0:nat
H2:0 <= S n0
H3:S n0 < S m'
Some x = Some m'
s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p, n0:nat
H2:0 <= S n0
H3:S n0 < S m'
0 <= n0
s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p, n0:nat
H2:0 <= S n0
H3:S n0 < S m'
n0 < m'
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
m':nat
(None = Some m' ->
 forall p : nat,
 0 <= p -> p < m' -> substring p (length s1) s2' <> s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
None = Some (S m') ->
forall p : nat,
0 <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
injection H1; auto.s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p, n0:nat
H2:0 <= S n0
H3:S n0 < S m'
0 <= n0
s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p, n0:nat
H2:0 <= S n0
H3:S n0 < S m'
n0 < m'
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
m':nat
(None = Some m' ->
 forall p : nat,
 0 <= p -> p < m' -> substring p (length s1) s2' <> s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
None = Some (S m') ->
forall p : nat,
0 <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
apply Le.le_O_n.s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
0 <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1
H1:Some (S x) = Some (S m')
p, n0:nat
H2:0 <= S n0
H3:S n0 < S m'
n0 < m'
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
m':nat
(None = Some m' ->
 forall p : nat,
 0 <= p -> p < m' -> substring p (length s1) s2' <> s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
None = Some (S m') ->
forall p : nat,
0 <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
apply Lt.lt_S_n; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
m':nat
(None = Some m' ->
 forall p : nat,
 0 <= p -> p < m' -> substring p (length s1) s2' <> s1) ->
false = true <->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end = s1 ->
None = Some (S m') ->
forall p : nat,
0 <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros; discriminate.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some m ->
forall p : nat,
S n0 <= p ->
p < m ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros n'; case m; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n':nat
match index n' s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = Some 0 ->
forall p : nat,
S n' <= p ->
p < 0 ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n':nat
forall n0 : nat,
match index n' s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some (S n0) ->
forall p : nat,
S n' <= p ->
p < S n0 ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
case (index n' s1 s2'); intros; discriminate.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n':nat
forall n0 : nat,
match index n' s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = Some (S n0) ->
forall p : nat,
S n' <= p ->
p < S n0 ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
intros m'; generalize (Rec n' m' s1); case (index n' s1 s2'); auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n', m':nat
forall n0 : nat,
(Some n0 = Some m' ->
 forall p : nat,
 n' <= p ->
 p < m' -> substring p (length s1) s2' <> s1) ->
Some (S n0) = Some (S m') ->
forall p : nat,
S n' <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n', m':nat
(None = Some m' ->
 forall p : nat,
 n' <= p ->
 p < m' -> substring p (length s1) s2' <> s1) ->
None = Some (S m') ->
forall p : nat,
S n' <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
intros x H H0 p; case p; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p0 : nat, n0 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
n', m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
n' <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:Some (S x) = Some (S m')
p:nat
S n' <= 0 ->
0 < S m' ->
match length s1 with
| 0 => EmptyString
| S m'0 => String b (substring 0 m'0 s2')
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p0 : nat, n0 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
n', m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
n' <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:Some (S x) = Some (S m')
p:nat
forall n0 : nat,
S n' <= S n0 ->
S n0 < S m' -> substring n0 (length s1) s2' <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n', m':nat
(None = Some m' ->
 forall p : nat,
 n' <= p ->
 p < m' -> substring p (length s1) s2' <> s1) ->
None = Some (S m') ->
forall p : nat,
S n' <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
intros H1; inversion H1; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p0 : nat, n0 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
n', m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
n' <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:Some (S x) = Some (S m')
p:nat
forall n0 : nat,
S n' <= S n0 ->
S n0 < S m' -> substring n0 (length s1) s2' <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n', m':nat
(None = Some m' ->
 forall p : nat,
 n' <= p ->
 p < m' -> substring p (length s1) s2' <> s1) ->
None = Some (S m') ->
forall p : nat,
S n' <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
intros n0 H1 H2; apply H; auto.s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
n', m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
n' <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:Some (S x) = Some (S m')
p, n0:nat
H1:S n' <= S n0
H2:S n0 < S m'
Some x = Some m'
s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
n', m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
n' <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:Some (S x) = Some (S m')
p, n0:nat
H1:S n' <= S n0
H2:S n0 < S m'
n' <= n0
s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
n', m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
n' <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:Some (S x) = Some (S m')
p, n0:nat
H1:S n' <= S n0
H2:S n0 < S m'
n0 < m'
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n', m':nat
(None = Some m' ->
 forall p : nat,
 n' <= p ->
 p < m' -> substring p (length s1) s2' <> s1) ->
None = Some (S m') ->
forall p : nat,
S n' <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
injection H0; auto.s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
n', m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
n' <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:Some (S x) = Some (S m')
p, n0:nat
H1:S n' <= S n0
H2:S n0 < S m'
n' <= n0
s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
n', m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
n' <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:Some (S x) = Some (S m')
p, n0:nat
H1:S n' <= S n0
H2:S n0 < S m'
n0 < m'
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n', m':nat
(None = Some m' ->
 forall p : nat,
 n' <= p ->
 p < m' -> substring p (length s1) s2' <> s1) ->
None = Some (S m') ->
forall p : nat,
S n' <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
apply Le.le_S_n; auto.s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = Some m0 ->
forall p0 : nat, n1 <= p0 -> p0 < m0 -> substring p0 (length s0) s2' <> s0
n, m:nat
s1:string
n', m', x:nat
H:Some x = Some m' ->
forall p0 : nat,
n' <= p0 ->
p0 < m' -> substring p0 (length s1) s2' <> s1
H0:Some (S x) = Some (S m')
p, n0:nat
H1:S n' <= S n0
H2:S n0 < S m'
n0 < m'
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n', m':nat
(None = Some m' ->
 forall p : nat,
 n' <= p ->
 p < m' -> substring p (length s1) s2' <> s1) ->
None = Some (S m') ->
forall p : nat,
S n' <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
apply Lt.lt_S_n; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = Some m0 ->
forall p : nat, n0 <= p -> p < m0 -> substring p (length s0) s2' <> s0
n, m:nat
s1:string
n', m':nat
(None = Some m' ->
 forall p : nat,
 n' <= p ->
 p < m' -> substring p (length s1) s2' <> s1) ->
None = Some (S m') ->
forall p : nat,
S n' <= p ->
p < S m' ->
match p with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m'0 => String b (substring 0 m'0 s2')
    end
| S n'0 => substring n'0 (length s1) s2'
end <> s1
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.forall (n m : nat) (s1 s2 : string),
index n s1 s2 = None ->
s1 <> EmptyString ->
n <= m -> substring m (length s1) s2 <> s1
Proof.forall (n m : nat) (s1 s2 : string),
index n s1 s2 = None ->
s1 <> EmptyString ->
n <= m -> substring m (length s1) s2 <> s1
intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl;
 auto.s2:string
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    match s1 with
    | EmptyString => Some 0
    | String _ _ => None
    end
| S _ => None
end = None ->
s1 <> EmptyString ->
n <= m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = None ->
 s1 <> EmptyString ->
 n <= m -> substring m (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None ->
s1 <> EmptyString ->
n <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros n; case n; simpl; auto.s2:string
n:nat
forall (m : nat) (s1 : string),
match s1 with
| EmptyString => Some 0
| String _ _ => None
end = None ->
s1 <> EmptyString ->
0 <= m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
n:nat
forall (n0 m : nat) (s1 : string),
None = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = None ->
 s1 <> EmptyString ->
 n <= m -> substring m (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None ->
s1 <> EmptyString ->
n <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros m s1; case s1; simpl; auto.s2:string
n, m:nat
s1:string
forall (a : ascii) (s : string),
None = None ->
String a s <> EmptyString ->
0 <= m ->
match m with
| 0 | _ => EmptyString
end <> String a s
s2:string
n:nat
forall (n0 m : nat) (s1 : string),
None = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = None ->
 s1 <> EmptyString ->
 n <= m -> substring m (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None ->
s1 <> EmptyString ->
n <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
case m; intros; red; intros; discriminate.s2:string
n:nat
forall (n0 m : nat) (s1 : string),
None = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 => match length s1 with
       | 0 | _ => EmptyString
       end
| S _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = None ->
 s1 <> EmptyString ->
 n <= m -> substring m (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None ->
s1 <> EmptyString ->
n <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros n' m; case m; auto.s2:string
n, n', m:nat
forall s1 : string,
None = None ->
s1 <> EmptyString ->
S n' <= 0 ->
match length s1 with
| 0 | _ => EmptyString
end <> s1
s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = None ->
 s1 <> EmptyString ->
 n <= m -> substring m (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None ->
s1 <> EmptyString ->
n <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros s1; case s1; simpl; auto.s2:string
forall (a : ascii) (s : string),
(forall (n m : nat) (s1 : string),
 index n s1 s = None ->
 s1 <> EmptyString ->
 n <= m -> substring m (length s1) s <> s1) ->
forall (n m : nat) (s1 : string),
match n with
| 0 =>
    if prefix s1 (String a s)
    then Some 0
    else
     match index 0 s1 s with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None ->
s1 <> EmptyString ->
n <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String a (substring 0 m' s)
    end
| S n' => substring n' (length s1) s
end <> s1
intros b s2' Rec n m s1.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
match n with
| 0 =>
    if prefix s1 (String b s2')
    then Some 0
    else
     match index 0 s1 s2' with
     | Some n0 => Some (S n0)
     | None => None
     end
| S n' =>
    match index n' s1 s2' with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None ->
s1 <> EmptyString ->
n <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
case n; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
(if prefix s1 (String b s2')
 then Some 0
 else
  match index 0 s1 s2' with
  | Some n0 => Some (S n0)
  | None => None
  end) = None ->
s1 <> EmptyString ->
0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
generalize (prefix_correct s1 (String b s2'));
 case (prefix s1 (String b s2')).s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
true = true <->
substring 0 (length s1) (String b s2') = s1 ->
Some 0 = None ->
s1 <> EmptyString ->
0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
false = true <->
substring 0 (length s1) (String b s2') = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = None ->
s1 <> EmptyString ->
0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros; discriminate.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
false = true <->
substring 0 (length s1) (String b s2') = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = None ->
s1 <> EmptyString ->
0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
case m; simpl; auto with bool.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = None ->
s1 <> EmptyString ->
0 <= 0 ->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
0 <= S n0 -> substring n0 (length s1) s2' <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
case s1; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall (a : ascii) (s : string),
false = true <->
String b (substring 0 (length s) s2') = String a s ->
match index 0 (String a s) s2' with
| Some n0 => Some (S n0)
| None => None
end = None ->
String a s <> EmptyString ->
0 <= 0 ->
String b (substring 0 (length s) s2') <> String a s
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
0 <= S n0 -> substring n0 (length s1) s2' <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros a s H H0 H1 H2; red; intros H3; case H.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
a:ascii
s:string
H:false = true <->
String b (substring 0 (length s) s2') = String a s
H0:match index 0 (String a s) s2' with
| Some n0 => Some (S n0)
| None => None
end = None
H1:String a s <> EmptyString
H2:0 <= 0
H3:String b (substring 0 (length s) s2') =
String a s
(false = true ->
 String b (substring 0 (length s) s2') = String a s) ->
(String b (substring 0 (length s) s2') = String a s ->
 false = true) -> False
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
0 <= S n0 -> substring n0 (length s1) s2' <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros H4 H5; absurd (false = true); auto with bool.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
false = true <->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end = s1 ->
match index 0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
0 <= S n0 -> substring n0 (length s1) s2' <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
case s1; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall (a : ascii) (s : string) (n0 : nat),
false = true <->
String b (substring 0 (length s) s2') = String a s ->
match index 0 (String a s) s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
String a s <> EmptyString ->
0 <= S n0 ->
substring n0 (S (length s)) s2' <> String a s
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros a s n0 H H0 H1 H2;
 change (substring n0 (length (String a s)) s2' <> String a s);
 apply (Rec O); auto.s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = None ->
s0 <> EmptyString -> n1 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
a:ascii
s:string
n0:nat
H:false = true <->
String b (substring 0 (length s) s2') = String a s
H0:match index 0 (String a s) s2' with
| Some n1 => Some (S n1)
| None => None
end = None
H1:String a s <> EmptyString
H2:0 <= S n0
index 0 (String a s) s2' = None
s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = None ->
s0 <> EmptyString -> n1 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
a:ascii
s:string
n0:nat
H:false = true <->
String b (substring 0 (length s) s2') = String a s
H0:match index 0 (String a s) s2' with
| Some n1 => Some (S n1)
| None => None
end = None
H1:String a s <> EmptyString
H2:0 <= S n0
0 <= n0
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
generalize H0; case (index 0 (String a s) s2'); simpl; auto; intros;
 discriminate.s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = None ->
s0 <> EmptyString -> n1 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
a:ascii
s:string
n0:nat
H:false = true <->
String b (substring 0 (length s) s2') = String a s
H0:match index 0 (String a s) s2' with
| Some n1 => Some (S n1)
| None => None
end = None
H1:String a s <> EmptyString
H2:0 <= S n0
0 <= n0
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
apply Le.le_O_n.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
forall n0 : nat,
match index n0 s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n0 <= m ->
match m with
| 0 =>
    match length s1 with
    | 0 => EmptyString
    | S m' => String b (substring 0 m' s2')
    end
| S n' => substring n' (length s1) s2'
end <> s1
intros n'; case m; simpl; auto.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
n':nat
match index n' s1 s2' with
| Some n0 => Some (S n0)
| None => None
end = None ->
s1 <> EmptyString ->
S n' <= 0 ->
match length s1 with
| 0 => EmptyString
| S m' => String b (substring 0 m' s2')
end <> s1
s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
n':nat
forall n0 : nat,
match index n' s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n' <= S n0 -> substring n0 (length s1) s2' <> s1
intros H H0 H1; inversion H1.s2:string
b:ascii
s2':string
Rec:forall (n0 m0 : nat) (s0 : string),
index n0 s0 s2' = None ->
s0 <> EmptyString -> n0 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
n':nat
forall n0 : nat,
match index n' s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None ->
s1 <> EmptyString ->
S n' <= S n0 -> substring n0 (length s1) s2' <> s1
intros n0 H H0 H1; apply (Rec n'); auto.s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = None ->
s0 <> EmptyString -> n1 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
n', n0:nat
H:match index n' s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None
H0:s1 <> EmptyString
H1:S n' <= S n0
index n' s1 s2' = None
s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = None ->
s0 <> EmptyString -> n1 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
n', n0:nat
H:match index n' s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None
H0:s1 <> EmptyString
H1:S n' <= S n0
n' <= n0
generalize H; case (index n' s1 s2'); simpl; auto; intros;
 discriminate.s2:string
b:ascii
s2':string
Rec:forall (n1 m0 : nat) (s0 : string),
index n1 s0 s2' = None ->
s0 <> EmptyString -> n1 <= m0 -> substring m0 (length s0) s2' <> s0
n, m:nat
s1:string
n', n0:nat
H:match index n' s1 s2' with
| Some n1 => Some (S n1)
| None => None
end = None
H0:s1 <> EmptyString
H1:S n' <= S n0
n' <= n0
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.forall (n : nat) (s : string),
index n EmptyString s = None -> length s < n
Proof.forall (n : nat) (s : string),
index n EmptyString s = None -> length s < n
intros n s; generalize n; clear n; elim s; simpl; auto.s:string
forall n : nat,
match n with
| 0 => Some 0
| S _ => None
end = None -> 0 < n
s:string
ascii ->
forall s0 : string,
(forall n : nat,
 index n EmptyString s0 = None -> length s0 < n) ->
forall n : nat,
match n with
| 0 => Some 0
| S n' =>
    match index n' EmptyString s0 with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None -> S (length s0) < n
intros n; case n; simpl; auto.s:string
n:nat
Some 0 = None -> 0 < 0
s:string
n:nat
forall n0 : nat, None = None -> 0 < S n0
s:string
ascii ->
forall s0 : string,
(forall n : nat,
 index n EmptyString s0 = None -> length s0 < n) ->
forall n : nat,
match n with
| 0 => Some 0
| S n' =>
    match index n' EmptyString s0 with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None -> S (length s0) < n
intros; discriminate.s:string
n:nat
forall n0 : nat, None = None -> 0 < S n0
s:string
ascii ->
forall s0 : string,
(forall n : nat,
 index n EmptyString s0 = None -> length s0 < n) ->
forall n : nat,
match n with
| 0 => Some 0
| S n' =>
    match index n' EmptyString s0 with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None -> S (length s0) < n
intros; apply Lt.lt_O_Sn.s:string
ascii ->
forall s0 : string,
(forall n : nat,
 index n EmptyString s0 = None -> length s0 < n) ->
forall n : nat,
match n with
| 0 => Some 0
| S n' =>
    match index n' EmptyString s0 with
    | Some n0 => Some (S n0)
    | None => None
    end
end = None -> S (length s0) < n
intros a s' H n; case n; simpl; auto.s:string
a:ascii
s':string
H:forall n0 : nat,
index n0 EmptyString s' = None -> length s' < n0
n:nat
Some 0 = None -> S (length s') < 0
s:string
a:ascii
s':string
H:forall n0 : nat,
index n0 EmptyString s' = None -> length s' < n0
n:nat
forall n0 : nat,
match index n0 EmptyString s' with
| Some n1 => Some (S n1)
| None => None
end = None -> S (length s') < S n0
intros; discriminate.s:string
a:ascii
s':string
H:forall n0 : nat,
index n0 EmptyString s' = None -> length s' < n0
n:nat
forall n0 : nat,
match index n0 EmptyString s' with
| Some n1 => Some (S n1)
| None => None
end = None -> S (length s') < S n0
intros n'; generalize (H n'); case (index n' EmptyString s'); simpl;
 auto.s:string
a:ascii
s':string
H:forall n0 : nat,
index n0 EmptyString s' = None -> length s' < n0
n, n':nat
forall n0 : nat,
(Some n0 = None -> length s' < n') ->
Some (S n0) = None -> S (length s') < S n'
s:string
a:ascii
s':string
H:forall n0 : nat,
index n0 EmptyString s' = None -> length s' < n0
n, n':nat
(None = None -> length s' < n') ->
None = None -> S (length s') < S n'
intros; discriminate.s:string
a:ascii
s':string
H:forall n0 : nat,
index n0 EmptyString s' = None -> length s' < n0
n, n':nat
(None = None -> length s' < n') ->
None = None -> S (length s') < S n'
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 => O
  end.

Conversion to/from list ascii and list byte

Fixpoint string_of_list_ascii (s : list ascii) : string
  := match s with
     | nil => EmptyString
     | cons ch s => String ch (string_of_list_ascii s)
     end.

Fixpoint list_ascii_of_string (s : string) : list ascii
  := match s with
     | EmptyString => nil
     | String ch s => cons ch (list_ascii_of_string s)
     end.

Lemma string_of_list_ascii_of_string s : string_of_list_ascii (list_ascii_of_string s) = s.s:string
string_of_list_ascii (list_ascii_of_string s) = s
Proof.s:string
string_of_list_ascii (list_ascii_of_string s) = s
  induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ].
Defined.

Lemma list_ascii_of_string_of_list_ascii s : list_ascii_of_string (string_of_list_ascii s) = s.s:list ascii
list_ascii_of_string (string_of_list_ascii s) = s
Proof.s:list ascii
list_ascii_of_string (string_of_list_ascii s) = s
  induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ].
Defined.

Definition string_of_list_byte (s : list byte) : string
  := string_of_list_ascii (List.map ascii_of_byte s).

Definition list_byte_of_string (s : string) : list byte
  := List.map byte_of_ascii (list_ascii_of_string s).

Lemma string_of_list_byte_of_string s : string_of_list_byte (list_byte_of_string s) = s.s:string
string_of_list_byte (list_byte_of_string s) = s
Proof.s:string
string_of_list_byte (list_byte_of_string s) = s
  cbv [string_of_list_byte list_byte_of_string].s:string
string_of_list_ascii
  (List.map ascii_of_byte
     (List.map byte_of_ascii (list_ascii_of_string s))) =
s
  erewrite List.map_map, List.map_ext, List.map_id, string_of_list_ascii_of_string; [ reflexivity | intro ].s:string
a:ascii
ascii_of_byte (byte_of_ascii a) =
(fun x : ascii => x) a
  apply ascii_of_byte_of_ascii.
Qed.

Lemma list_byte_of_string_of_list_byte s : list_byte_of_string (string_of_list_byte s) = s.s:list byte
list_byte_of_string (string_of_list_byte s) = s
Proof.s:list byte
list_byte_of_string (string_of_list_byte s) = s
  cbv [string_of_list_byte list_byte_of_string].s:list byte
List.map byte_of_ascii
  (list_ascii_of_string
     (string_of_list_ascii (List.map ascii_of_byte s))) =
s
  erewrite list_ascii_of_string_of_list_ascii, List.map_map, List.map_ext, List.map_id; [ reflexivity | intro ].s:list byte
a:byte
byte_of_ascii (ascii_of_byte a) =
(fun x : byte => x) a
  apply byte_of_ascii_of_byte.
Qed.

Concrete syntax

The concrete syntax for strings in scope string_scope follows the Coq convention for strings: all ascii characters of code less than 128 are literals to the exception of the character `double quote' which must be doubled.

Strings that involve ascii characters of code >= 128 which are not part of a valid utf8 sequence of characters are not representable using the Coq string notation (use explicitly the String constructor with the ascii codes of the characters).

Module Export StringSyntax.
  String Notation string string_of_list_byte list_byte_of_string : string_scope.
End StringSyntax.

Example HelloWorld := "	""Hello world!""
".