proposition: Lemma is_first_char_such_that__find_first_char_such_that {Char} {HSLM HSL} {HSLP : @StringLikeProperties Char HSLM HSL} str P might_be_empty (H : exists n, is_first_char_such_that might_be_empty str n (fun ch => is_true (P ch))) : is_first_char_such_that might_be_empty str (@find_first_char_such_that Char HSLM HSL str P) (fun ch => is_true (P ch)).
proof: Proof. unfold find_first_char_such_that. destruct H as [n H]. set (len := length str). setoid_replace str with (drop (length str - len) str) at 1 by (subst; rewrite Nat.sub_diag, drop_0; reflexivity). setoid_replace str with (drop (length str - len) str) in H by (subst; rewrite Nat.sub_diag, drop_0; reflexivity). assert (len <= length str) by reflexivity. clearbody len. generalize dependent str; revert n. induction len; simpl; intros n str IH Hlen. { apply first_char_such_that_0. rewrite drop_length. rewrite Nat.sub_0_r in IH |- *. rewrite Nat.sub_diag. split. { apply for_first_char_nil. rewrite drop_length; omega. } { generalize dependent str. induction n; intros str H Hlen. { apply first_char_such_that_0 in H. rewrite drop_length, Nat.sub_diag in H. destruct_head and; trivial. } { apply first_char_such_that_past_end in H; [ | rewrite drop_length; omega ]. left; assumption. } } } { pose proof (singleton_exists (take 1 (drop (length str - S len) str))) as H'. rewrite take_length, drop_length in H'. destruct H' as [ch H']; [ apply Nat.min_case_strong; intros; omega | ]. rewrite get_drop. rewrite (proj1 (get_0 _ _) H'). destruct (P ch) eqn:H''. { apply first_char_such_that_0. rewrite drop_length. split; [ | right; omega ]. apply (for_first_char__take 0). rewrite <- for_first_char_singleton by eassumption; trivial. } { apply is_first_char_such_that_drop. destruct n. { apply first_char_such_that_0 in IH. destruct IH as [IH _]. apply (for_first_char__take 0) in IH. rewrite <- for_first_char_singleton in IH by eassumption; unfold is_true in *; congruence. } { apply is_first_char_such_that_drop in IH. destruct IH as [IH _]. rewrite drop_drop in IH |- *; simpl in IH |- *. replace (S (length str - S len)) with (length str - len) in IH |- * by omega. split. { eapply IHlen; try eassumption; []. omega. } { apply (for_first_char__take 0). rewrite <- for_first_char_singleton by eassumption; congruence. } } } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Fiat.Parsers.Refinement.PreTactics Fiat.Computation.Refinements.General Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.FirstChar Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.Refinement.DisjointLemmas Fiat.Parsers.Refinement.DisjointRulesCommon Fiat.Parsers.Refinement.PossibleTerminalsSets Fiat.Parsers.ParserInterface Fiat.Parsers.StringLike.Core Fiat.Common.List.DisjointFacts