proposition: Lemma for_last_char_singleton (str : String) P ch : str ~= [ ch ] -> (P ch <-> for_last_char str P).
proof: Proof. intro H. pose proof (length_singleton _ _ H). unfold for_last_char. split; intro H'; repeat intro. { repeat match goal with | _ => intro | _ => omega | [ H : _ |- _ ] => rewrite drop_0 in H | [ H : _, H' : _ |- _ ] => rewrite (singleton_take H') in H | [ H : _ |- False ] => apply length_singleton in H | [ H : _ |- _ ] => rewrite take_length in H | [ H : _ |- _ ] => rewrite drop_length in H | [ H : ?x = 1, H' : context[?x] |- _ ] => rewrite H in H' | _ => erewrite singleton_unique; eassumption | [ H : context[min] |- _ ] => revert H; apply Nat.min_case_strong end. } { match goal with | [ H : _ |- _ ] => apply H end. repeat match goal with | [ H : ?x = 1 |- _ ] => rewrite H | _ => progress simpl end. rewrite drop_0; assumption. } 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.Common