proposition: Lemma is_first_char_such_that_eq_nat_iff (might_be_empty : Prop) (str : String) (n n' : nat) P (H0 : is_first_char_such_that might_be_empty str n P) (H1 : is_first_char_such_that might_be_empty str n' P) : n = n' \/ (n >= length str /\ n' >= length str /\ might_be_empty).
proof: Proof. generalize dependent n'; generalize dependent str; induction n; intros. { destruct n'; intros. { left; reflexivity. } { right. unfold is_first_char_such_that in *. repeat match goal with | _ => assumption | [ H : and _ _ |- _ ] => destruct H | [ H : ?A -> ?B, H' : ?A |- _ ] => specialize (H H') | [ H : _ |- _ ] => rewrite drop_0 in H | [ H : _ |- _ ] => apply forall_chars__impl__for_first_char in H | [ 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 | _ => omega | _ => progress destruct_head and | _ => progress destruct_head or | [ |- _ /\ _ ] => split end. } } { specialize (IHn (drop 1 str)). destruct n'; [ right; case_eq (length str) | ]; repeat match goal with | [ H : is_first_char_such_that _ _ (S _) _ |- _ ] => apply is_first_char_such_that_drop in H | _ => progress destruct_head and | [ H : ?A -> ?B, H' : ?A |- _ ] => specialize (H H') | _ => intro | [ H : _ |- _ ] => progress rewrite ?drop_length, ?Nat.le_sub_le_add_r in H | [ H : ?x = 0, H' : context[?x] |- _ ] => rewrite H in H' | _ => progress simpl in * | [ |- _ /\ _ ] => split; try omega; [] | _ => eapply first_char_such_that_past_end; [ | eassumption ]; omega | [ H : _ |- _ ] => unique pose proof (proj1 (proj1 first_char_such_that_0 H)) | [ H : for_first_char ?str ?P, H' : for_first_char ?str ?P' |- _ ] => destruct (fun H_new => for_first_char_combine (T := False) H_new H H'); cbv beta; [ tauto | clear H H' | tauto ] | _ => omega | _ => progress unfold ge in * | [ H : forall n', is_first_char_such_that ?P ?str n' ?P' -> _, H' : is_first_char_such_that ?P ?str _ ?P' |- _ ] => specialize (H _ H') | _ => progress subst | _ => left; reflexivity | _ => right; repeat split; trivial; omega | _ => progress destruct_head or 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