proposition: Theorem index_correct2 : forall (n m : nat) (s1 s2 : string), index n s1 s2 = Some m -> forall p : nat, n <= p -> p < m -> substring p (length s1) s2 <> s1.
proof: 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. * intros [= <-]. intros p H0 H2; inversion H2. * intros; discriminate. + intros; discriminate. - 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 H0 [= <-]; auto. intros p H2 H3; inversion H3. * case m; simpl; auto. -- case (index 0 s1 s2'); intros; discriminate. -- intros m'; generalize (Rec O m' s1); case (index 0 s1 s2'); auto. ++ intros x H H0 H1 p; try case p; simpl; auto. ** intros H2 H3; red; intros H4; case H0. intros H5 H6; absurd (false = true); auto with bool. ** { intros n0 H2 H3; apply H; auto. - injection H1; auto. - apply Nat.le_0_l. - apply <- Nat.succ_lt_mono; auto. } ++ intros; discriminate. + intros n'; case m; simpl; auto. * case (index n' s1 s2'); intros; discriminate. * intros m'; generalize (Rec n' m' s1); case (index n' s1 s2'); auto. -- intros x H H0 p; case p; simpl; auto. ++ intros H1; inversion H1; auto. ++ intros n0 H1 H2; apply H; auto. ** injection H0; auto. ** apply <- Nat.succ_le_mono; auto. ** apply <- Nat.succ_lt_mono; auto. -- intros; discriminate. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte