proposition: Lemma refine_check_one_longest_prefix_CNAME : forall (ns : list resourceRecord) (n : RRecordType) (s : DomainName) (HH : forall (t t' : resourceRecord) (n n' : nat), n <> n' -> nth_error ns n = Some t -> nth_error ns n' = Some t' -> get_name t = get_name t' -> RDataTypeToRRecordType (t!sRDATA) <> CNAME), (forall n' : resourceRecord, List.In n' ns -> prefix (get_name n') s) -> refine {b' : option Tuple | forall b : Tuple, b' = Some b <-> List.In b (find_UpperBound name_length ns) /\ RDataTypeToRRecordType (b!sRDATA) = CNAME /\ n <> CNAME} (ret match (find_UpperBound name_length ns) with | nil => None | n' :: _ => if CNAME == (RDataTypeToRRecordType (n'!sRDATA)) then if n == CNAME then None else Some n' else None end).
proof: Proof. unfold refine, not; intros; pose proof (all_longest_prefixes_same ns _ H); clear H. remember (find_UpperBound name_length ns) as l. computes_to_inv; computes_to_econstructor; split; intros. - destruct l; [ subst; inversion H | ]. repeat find_if_inside_eqn; subst; try inversion H; subst. repeat split; [ simpl; left | symmetry | ]; auto. - destruct H as [? [? ?] ]; destruct l; [ inversion H | subst ]. inversion H; unfold not in *. + repeat find_if_inside; subst; auto; exfalso; auto. + assert (r = b). * pose proof (in_eq r l). pose proof H; rewrite Heql in H5; pose proof (in_list_preserve_filter _ ns b H5); clear H5. pose proof H4; rewrite Heql in H5; pose proof (in_list_preserve_filter _ ns r H5); clear H5. pose proof (in_list_exists ns b H6); pose proof (in_list_exists ns r H7); destruct_ex; pose proof (H1 r b H4 H). destruct (beq_nat x0 x) eqn: eq; [ rewrite beq_nat_true_iff in eq; subst; rewrite H8 in H5; inversion H5; auto | ]. rewrite beq_nat_false_iff in eq; symmetry in H9. pose proof (HH b r x0 x eq H5 H8 H9); exfalso; auto. * repeat find_if_inside; subst; [ exfalso; apply H3 | | exfalso; apply n0 ]; 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