proposition: Lemma find_after_last_char_such_that'_S {Char} {HSLM : StringLikeMin Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (P : Char -> bool) (len : nat) (str : String) : find_after_last_char_such_that' P (S len) str = let v := S (find_after_last_char_such_that' P len (drop 1 str)) in match get 0 str with | Some ch => match find_after_last_char_such_that' P len (drop 1 str) with | 0 => if P ch then 1 else 0 | _ => v end | None => 0 end.
proof: Proof. cbv zeta. revert str; induction len as [|len IHlen]; intros. { reflexivity. } { simpl in *. rewrite IHlen; clear IHlen. repeat match goal with | [ |- context[get ?n'] ] => not constr_eq n' 0; rewrite (get_drop (n := n')) | [ H : context[get ?n'] |- _ ] => not constr_eq n' 0; setoid_rewrite (get_drop (n := n')) in H end. replace (get 0 (drop len (drop 1 str))) with (get 0 (drop (S len) str)) by (rewrite drop_drop; do 2 f_equal; omega). destruct (get 0 str) eqn:Hg0. { destruct (get 0 (drop (S len) str)) eqn:Hg1; [ | reflexivity ]. edestruct P; reflexivity. } { apply no_first_char_empty in Hg0. rewrite has_first_char_nonempty by (rewrite drop_length, Hg0; reflexivity). 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