proposition: Lemma find_after_last_char_such_that_drop {Char} {HSLM : StringLikeMin Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (str : String) (P : Char -> bool) : find_after_last_char_such_that str P = let v := S (find_after_last_char_such_that (drop 1 str) P) in match get 0 str with | Some ch => match find_after_last_char_such_that (drop 1 str) P with | 0 => if P ch then 1 else 0 | _ => v end | None => 0 end.
proof: Proof. unfold find_after_last_char_such_that. destruct (length str) eqn:Hlen. { rewrite has_first_char_nonempty by assumption; simpl; reflexivity. } { rewrite find_after_last_char_such_that'_S; simpl. rewrite drop_length, Hlen; simpl. rewrite Nat.sub_0_r. 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