proposition: Lemma refine_check_one_longest_prefix_s : forall (ns : list resourceRecord) (s : DomainName), (forall n' : resourceRecord, List.In n' ns -> prefix (get_name n') s) -> refine {b : bool | decides b (~ (exists x : resourceRecord, List.In x (find_UpperBound name_length ns) /\ s <> (get_name x)))} (ret match find_UpperBound name_length ns with | nil => true | n' :: _ => ?[s == (get_name n')] end).
proof: Proof. computes_to_econstructor; simpl in H; intros; computes_to_inv. subst; unfold decides; pose proof (all_longest_prefixes_same ns _ H); clear H. remember (find_UpperBound name_length ns) as l. unfold If_Then_Else. find_if_inside_eqn. - unfold not; intros; repeat destruct H; apply H1; clear H1; destruct l; [ inversion H | subst; apply H0 with (n := r) in H ]; [ find_if_inside; [ subst; auto | inversion Heqb ] | simpl; left; auto ]. - unfold not; intros; apply H; clear H; destruct l; try inversion Heqb. exists r; split; [ simpl; left; auto | intros; rewrite <- H in Heqb ]. find_if_inside; [ discriminate | unfold not in *; apply n; auto ]. 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