proposition: Lemma for_last_char_exists (str : String) P (H : length str >= 1) : for_last_char str P <-> (exists ch, drop (pred (length str)) str ~= [ ch ] /\ P ch).
proof: Proof. rewrite (for_last_char__drop (pred (length str)) str) by omega. assert (H' : length (drop (pred (length str)) str) = 1) by (rewrite drop_length; omega). destruct (singleton_exists _ H') as [ch H'']. rewrite for_last_char_singleton_length by exact H'. split; intros. { exists ch; split; eauto. } { destruct_head ex. destruct_head and. repeat match goal with | [ H : is_true (?str ~= [ ?ch ])%string_like, H' : is_true (?str ~= [ ?ch' ])%string_like |- _ ] => assert (ch = ch') by (eapply singleton_unique; eassumption); clear H' end. subst; assumption. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.ForallChars Fiat.Common