proposition: Lemma refine_noDup_CNAME_check : forall (rr : resourceRecord) (R : @IndexedEnsemble resourceRecord), (forall tup tup' : IndexedElement, elementIndex tup <> elementIndex tup' -> R tup -> R tup' -> (indexedElement tup)!sNAME = (indexedElement tup')!sNAME -> RDataTypeToRRecordType (indexedElement tup)!sRDATA <> CNAME) -> refine {b | decides b (forall tup', R tup' -> rr!sNAME = (indexedElement tup')!sNAME -> RDataTypeToRRecordType rr!sRDATA <> CNAME)} (If (beq_RRecordType (RDataTypeToRRecordType rr!sRDATA) CNAME) Then count <- Count For (QueryResultComp R (fun tup => Where (rr!sNAME = tup!sNAME) Return tup )%QueryImpl); ret (beq_nat count 0) Else ret true).
proof: Proof. intros. intros; setoid_rewrite refine_pick_decides at 1; [ | apply refine_is_CNAME__forall_to_exists | apply refine_not_CNAME__independent ]. setoid_rewrite refine_beq_RRecordType_dec; simplify with monad laws. apply refine_If_Then_Else; eauto. setoid_rewrite refine_constraint_check_into_QueryResultComp with (P := fun tup => rr!sNAME = tup!sNAME). rewrite refineEquiv_bind_bind. f_equiv. unfold pointwise_relation; intros; simplify with monad laws; rewrite <- negb_involutive_reverse; reflexivity. auto with typeclass_instances. intuition. reflexivity. 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