proposition: Lemma ValidLabel_split_char : forall s label subdomain subdomain', (s ++ String "." subdomain)%string = (label ++ subdomain')%string -> ValidLabel label -> le (String.length label) (String.length s).
proof: Proof. intros. destruct (index 0 "." s) eqn:pre_eq. apply index_correct' in pre_eq; destruct pre_eq as [s' [s'' [ [s_eq s'_len] s'_OK] ] ]; subst. destruct (index 0 "." subdomain') eqn:subdomain_eq. apply index_correct' in subdomain_eq; destruct subdomain_eq as [t' [t'' [ [t_eq t'_len] t'_OK] ] ]; subst. assert (label ++ t' = s')%string. rewrite <- !append_assoc in H; simpl in H. pose proof (split_char_inj s' (s'' ++ String "." subdomain) (label ++ t') t''). rewrite <- !append_assoc in H1; simpl in H1. destruct H0. apply H1 in H; eauto using index_app. destruct H; subst; eauto. apply (f_equal String.length) in H1; rewrite !length_append in *|-*; simpl in *. omega. assert (index 0 "." ((s' ++ "." ++ s'') ++ String "." subdomain)%string = None) by (rewrite H; destruct H0; apply index_app; eauto). destruct s'. simpl in H1. destruct s''; try solve [simpl in H1; discriminate]. eapply index_correct3 with (m := S (String.length s')) in H1; try omega; try congruence. exfalso; apply H1; clear. induction s'; simpl. destruct s''; simpl; reflexivity. assumption. destruct (index 0 "." subdomain') eqn:subdomain_eq. apply index_correct' in subdomain_eq; destruct subdomain_eq as [t' [t'' [ [t_eq t'_len] t'_OK] ] ]; subst. assert (label ++ t' = s)%string. simpl in H. pose proof (split_char_inj s subdomain (label ++ t') t''). rewrite <- !append_assoc in H1; simpl in H1. destruct H0. apply H1 in H; eauto using index_app. destruct H; subst; eauto. apply (f_equal String.length) in H1; rewrite !length_append in *|-*; simpl in *. omega. assert (index 0 "." (s ++ String "." subdomain)%string = None) by (rewrite H; destruct H0; apply index_app; eauto). destruct s. simpl in H1. destruct subdomain; try solve [simpl in H1; discriminate]. eapply index_correct3 with (m := S (String.length s)) in H1; try omega; try congruence. exfalso; apply H1; clear. induction s; simpl. destruct subdomain; simpl; reflexivity. assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt