proposition: Lemma all_longest_prefixes_same : forall (ns : list resourceRecord) (s : DomainName), (forall (n' : resourceRecord), List.In n' ns -> prefix (get_name n') s) -> forall n n' : resourceRecord, List.In n (find_UpperBound name_length ns) -> List.In n' (find_UpperBound name_length ns) -> get_name n = get_name n'.
proof: Proof. unfold find_UpperBound, name_length; intros ns s H0 n n' H H1. apply filter_In in H; destruct H; apply filter_In in H1; destruct H1. pose proof (H0 _ H); pose proof (H0 _ H1). apply NPeano.leb_le in H2; apply NPeano.leb_le in H3. pose proof (fold_right_max_is_max name_length ns n H) as H2'. pose proof (fold_right_max_is_max name_length ns n' H1) as H3'. unfold name_length in *. apply (le_antisym _ _ H2') in H2; apply (le_antisym _ _ H3') in H3. rewrite <- H2 in H3. repeat unfold is_true in *. rewrite prefix_correct in H4, H5. rewrite <- H3 in H4; rewrite H4 in H5. eauto. Qed.
imports: Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector Coq.Lists.List Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Examples.DnsServer.DecomposeSumField Fiat.Computation.FoldComp Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema