proposition: Theorem index_correct1 : forall (n m : nat) (s1 s2 : string), index n s1 s2 = Some 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. * intros [= <-]; auto. * 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. case H0; simpl; auto. * case m; simpl; auto. -- case (index O s1 s2'); intros; discriminate. -- intros m'; generalize (Rec O m' s1); case (index O s1 s2'); auto. ++ intros x H H0 H1; apply H; injection H1; 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 H1; apply H; injection H1; auto. -- intros; discriminate. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte