proposition: Lemma ValidDomainName_app' : forall label subdomain (subdomainOK : subdomain <> EmptyString), ValidLabel label -> lt (String.length label) 64 -> ValidDomainName subdomain -> ValidDomainName (label ++ (String "." subdomain)).
proof: Proof. unfold ValidDomainName; intros. split; [ intros ? ? ? label_eq [? ?] | ]. - assert ((exists pre', pre' ++ label0 ++ post = subdomain) \/ exists post', label = (pre ++ label0 ++ post'))%string. { destruct (index 0 "." pre) eqn:pre_eq. - apply index_correct' in pre_eq; destruct pre_eq as [s [s' [ [pre_eq s_len] s_OK ] ] ]; subst. rewrite <- append_assoc in label_eq. simpl in label_eq. destruct H; eapply split_char_inj in label_eq; intuition. subst; eauto. - destruct (index 0 "." post) eqn:post_eq. apply index_correct' in post_eq; destruct post_eq as [t [t' [ [post_eq t_len] t_OK ] ] ]; subst. rewrite append_assoc in label_eq. rewrite append_assoc in label_eq. destruct H; eapply split_char_inj in label_eq; intuition; subst. rewrite <- !append_assoc; eauto. eauto using index_app. assert (index 0 "." (label ++ String "." subdomain)%string = None) by (rewrite label_eq; eauto using index_app). eapply index_correct3 with (m := String.length label) in H4; try omega; try congruence. destruct label. exfalso; destruct H; simpl in H5; omega. exfalso; apply H4; clear. induction label; simpl. + destruct subdomain; simpl; reflexivity. + apply IHlabel. } destruct H4 as [ [pre' subdomain_eq] | [post' label_eq'] ]. subst; eapply H1; unfold ValidLabel; eauto. subst. rewrite !length_append in H0; omega. - intros. assert ((label = pre) \/ exists mid, pre = label ++ String "." mid)%string. { destruct (index 0 "." pre) eqn:pre_eq. - apply index_correct' in pre_eq; destruct pre_eq as [s [s' [ [pre_eq s_len] s_OK ] ] ]; subst. rewrite <- append_assoc in H2. simpl in H2. destruct H; eapply split_char_inj in H2; intuition. subst; simpl; eauto. - destruct (index 0 "." post) eqn:post_eq. apply index_correct' in post_eq; destruct post_eq as [t [t' [ [post_eq t_len] t_OK ] ] ]; subst. destruct H; eapply split_char_inj in H2; intuition; subst. destruct H. simpl in H2; eapply split_char_inj in H2; intuition eauto. } destruct H3; subst. + apply ValidLabel_OK_split in H2; subst; repeat split; auto. * destruct pre; try congruence. destruct H; simpl in *; omega. * intro; destruct H2; subst. destruct (proj2 H1 EmptyString x eq_refl); intuition. * intros [s' pre_eq]; subst. unfold ValidLabel in H; intuition. match goal with | H : index _ _ _ = None |- _ => apply (index_correct3 _ (String.length s')) in H; try apply H; simpl end. clear; induction s'; simpl; eauto. congruence. omega. + destruct H3; subst. rewrite <- append_assoc in H2; simpl in H2. eapply (ValidLabel_OK_split label _ (x ++ String "." post)) in H2. pose proof (proj2 H1 _ _ H2); subst; eauto; repeat split; try solve [intuition]. * destruct label; simpl; congruence. * intros [s' s'_eq]. apply (proj2 (proj2 (proj2 H3))). generalize (proj1 (proj2 H3)). generalize s' x s'_eq; clear. induction label; simpl. induction s'; simpl; intros. destruct x; eauto; congruence. injection s'_eq; intros; eauto. destruct s'; simpl; intros. destruct label; discriminate. injection s'_eq; intro; eauto. 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