proposition: Lemma fold_lookahead_recr {A} (f : Char -> option Char -> A -> A) (init : A) (str : String) : fold_lookahead f init str = match get 0 str with | Some ch => f ch (get 1 str) (fold_lookahead f init (drop 1 str)) | None => init end.
proof: Proof. case_eq (get 0 str). { intros ch H'. unfold fold_lookahead. case_eq (length str). { intro H''. apply has_first_char_nonempty in H''. congruence. } { intros n H''. rewrite fold_lookahead'_cons. rewrite !H'', Nat.sub_diag, H'. replace (S n - n) with 1 by omega. rewrite drop_length, H''; simpl. rewrite Nat.sub_0_r. apply f_equal. rewrite <- fold_lookahead'_drop by omega; reflexivity. } } { intro H'. apply fold_lookahead_nil, no_first_char_empty; assumption. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.Le Fiat.Common.Tactics.SetoidSubst Fiat.Common.Tactics.IsClosed Fiat.Parsers.StringLike.Core Fiat.Common.UIP