proposition: Theorem prefix_correct : forall s1 s2 : string, prefix s1 s2 = true <-> substring 0 (length s1) s2 = s1.
proof: Proof. intros s1; elim s1; simpl; auto. - intros s2; case s2; simpl; split; auto. - intros a s1' Rec s2; case s2; simpl; auto. + split; intros; discriminate. + intros b s2'; case (ascii_dec a b); simpl; auto. * intros e; case (Rec s2'); intros H1 H2; split; intros H3; auto. -- rewrite e; rewrite H1; auto. -- apply H2; injection H3; auto. * intros n; split; intros H; try discriminate. case n; injection H; auto. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte