proposition: Theorem index_correct3 : forall (n m : nat) (s1 s2 : string), index n s1 s2 = None -> s1 <> EmptyString -> n <= m -> substring m (length s1) s2 <> s1.
proof: Proof. intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. - intros n; case n; simpl; auto. + intros m s1; case s1; simpl; auto. case m; intros; red; intros; discriminate. + intros n' m; case m; auto. intros s1; case s1; simpl; auto. - intros b s2' Rec n m s1. case n; simpl; auto. + generalize (prefix_correct s1 (String b s2')); case (prefix s1 (String b s2')). * intros; discriminate. * case m; simpl; auto with bool. -- case s1; simpl; auto. intros a s H H0 H1 H2; red; intros H3; case H. intros H4 H5; absurd (false = true); auto with bool. -- case s1; simpl; auto. intros a s n0 H H0 H1 H2; change (substring n0 (length (String a s)) s2' <> String a s); apply (Rec O); auto. ++ generalize H0; case (index 0 (String a s) s2'); simpl; auto; intros; discriminate. ++ apply Nat.le_0_l. + intros n'; case m; simpl; auto. * intros H H0 H1; inversion H1. * intros n0 H H0 H1; apply (Rec n'); auto. -- generalize H; case (index n' s1 s2'); simpl; auto; intros; discriminate. -- apply Nat.succ_le_mono; auto. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte