proposition: Lemma is_after_last_char_such_that__find_after_last_char_such_that {Char} {HSLM HSL} {HSLP : @StringLikeProperties Char HSLM HSL} str P (H : exists n, is_after_last_char_such_that str n (fun ch => is_true (P ch))) : is_after_last_char_such_that str (@find_after_last_char_such_that Char HSLM HSL str P) (fun ch => is_true (P ch)).
proof: Proof. destruct H as [n H]. rewrite unfold_is_after_last_char_such_that in H |- *. destruct H as [H0 H1]. generalize dependent str. induction n as [|n IHn]; intros. { cut (find_after_last_char_such_that str P = 0); [ intro Heq; rewrite Heq; split; assumption | ]. rewrite drop_0 in H0. unfold find_after_last_char_such_that, find_after_last_char_such_that'. induction (length str) as [|len IHlen]; simpl; [ reflexivity | rewrite IHlen; clear IHlen ]. rewrite forall_chars_get in H0. specialize (H0 len). edestruct get; [ | reflexivity ]. specialize (H0 _ eq_refl). edestruct P; simpl in *; intuition. } { specialize (IHn (drop 1 str)). rewrite !drop_drop, !take_drop, !Nat.add_1_r in IHn. specialize_by assumption. specialize_by (apply for_last_char__add_drop; assumption). rewrite find_after_last_char_such_that_drop; simpl. destruct (get 0 str) eqn:Hg0. { destruct (find_after_last_char_such_that (drop 1 str) P) eqn:Hf. { destruct_head and. destruct (P c) eqn:Hp. { split; try assumption; []. rewrite <- for_last_char_singleton; [ | apply get_0 ]; eassumption. } { rewrite drop_0. split; [ | apply for_last_char_nil; rewrite take_length; reflexivity ]. apply (forall_chars__split _ _ 1); split; try assumption; []. rewrite <- forall_chars_singleton; [ | apply get_0; eassumption ]. congruence. } } { destruct_head and; split; try assumption; []. rewrite for_last_char__drop; [ eassumption | ]. rewrite take_length; simpl. destruct (length str) as [|[|]] eqn:Hlen; [ exfalso | exfalso | ]. { rewrite has_first_char_nonempty in Hg0 by assumption; congruence. } { move Hf at bottom. unfold find_after_last_char_such_that in Hf. rewrite drop_length, Hlen in Hf. simpl in Hf. congruence. } { simpl; omega. } } } { rewrite drop_0. apply no_first_char_empty in Hg0. split; [ apply forall_chars_nil | apply for_last_char_nil ]; rewrite ?take_length, Hg0; reflexivity. } } 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.Parsers.StringLike.LastChar Fiat.Common