proposition: Lemma is_after_last_char_such_that_drop (str : String) (n : nat) P : is_after_last_char_such_that str (S n) P -> is_after_last_char_such_that (drop 1 str) n P .
proof: Proof. revert dependent str; induction n as [|n IHn]; intros; unfold is_after_last_char_such_that in *; [ | specialize (IHn (drop 1 str)); rewrite (forall_chars__split _ _ 1) ]; repeat match goal with | _ => assumption | _ => intro | _ => progress destruct_head and | _ => progress destruct_head iff | [ H : ?A -> ?B, H' : ?A |- _ ] => specialize (H H') | _ => progress simpl in * | [ H : ?x < ?y |- _ \/ (_ /\ ?y <= ?x) ] => left | [ H : ?x = 0 |- context[?x] ] => rewrite H | _ => apply forall_chars_nil; rewrite ?take_length, ?drop_length; reflexivity | _ => omega | [ H : ?A /\ ?B -> ?C |- _ ] => specialize (fun x y => H (conj x y)) | [ H : _ -> ?A /\ ?B -> ?C |- _ ] => specialize (fun a x y => H a (conj x y)) | [ H : _ |- _ ] => progress rewrite ?drop_0, ?drop_drop, ?take_take, ?drop_length, ?take_length, ?take_drop, ?Nat.add_1_r, ?Nat.le_sub_le_add_r, <- ?(Nat.add_comm 2), <- ?Nat.lt_add_lt_sub_r in H | _ => progress rewrite ?drop_0, ?drop_drop, ?take_take, ?drop_length, ?take_length, ?take_drop, ?Nat.add_1_r, ?Nat.le_sub_le_add_r, <- ?(Nat.add_comm 2), <- ?Nat.lt_add_lt_sub_r | _ => progress destruct_head or | [ |- _ /\ _ ] => split | [ |- _ <-> _ ] => split | _ => left; repeat split; trivial; omega | _ => right; repeat split; trivial; omega | [ H : for_last_char ?str ?P |- for_last_char (drop ?n ?str) ?P ] => eapply for_last_char__add_drop; eexact H | [ H : for_last_char (drop _ _) _ |- _ ] => rewrite <- for_last_char__drop in H by (rewrite ?take_length; apply Nat.min_case_strong; omega) | [ |- forall_chars (drop _ (take _ _)) _ ] => rewrite drop_take, Nat.sub_succ_l, Nat.sub_diag by omega; simpl; apply (proj1 (forall_chars_take _ _)) | [ H : forall_chars (drop ?n ?str) ?P |- forall_chars (drop (S ?n) ?str) ?P ] => rewrite <- (drop_drop str 1 n); apply (proj1 (forall_chars_drop _ _)); assumption end. 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