proposition: Lemma is_first_char_such_that_drop (might_be_empty : Prop) (str : String) (n : nat) P : is_first_char_such_that might_be_empty str (S n) P <-> (is_first_char_such_that might_be_empty (drop 1 str) n P /\ for_first_char str (fun ch => ~P ch)).
proof: Proof. generalize dependent str; induction n; intros; unfold is_first_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 : _ |- _ ] => apply forall_chars__impl__for_first_char, for_first_char__take in H; assumption | [ H : for_first_char (take (S _) _) _ |- _ ] => apply for_first_char__take in H | [ H : for_first_char ?str ?P, H' : for_first_char ?str ?P' |- _ ] => destruct (fun H0 => for_first_char_combine (T := False) H0 H H'); cbv beta; [ tauto | clear H H' | tauto ] | [ 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, ?drop_take, ?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, ?drop_take, ?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 | _ => apply for_first_char__for_first_char__iff_short; [ rewrite take_length; destruct (length str); simpl in *; omega | apply -> (for_first_char__take 0); assumption ] end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Arith.PeanoNat Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.ForallChars Fiat.Parsers.StringLike.FirstChar Fiat.Common Fiat.Common.NatFacts