proposition: Lemma refine_count_constraint_broken : forall (n : resourceRecord) (r : UnConstrQueryStructure DnsSchema), refine {b | decides b (forall tup' : @IndexedRawTuple (GetHeading DnsSchema sRRecords), (r!sRRecords)%QueryImpl tup' -> n!sNAME = (indexedElement tup')!sNAME -> RDataTypeToRRecordType (n!sRDATA) <> CNAME)} (If (beq_RRecordType (RDataTypeToRRecordType (n!sRDATA)) CNAME) Then count <- Count For (tup in r!sRRecords) (Where (n!sNAME = tup!sNAME) Return () )%QueryImpl; ret (beq_nat count 0) Else ret true).
proof: Proof. intros; setoid_rewrite refine_pick_decides at 1; [ | apply refine_is_CNAME__forall_to_exists | apply refine_not_CNAME__independent ]. match goal with |- context[{b | decides b (exists tup : @IndexedTuple ?heading, (@GetUnConstrRelationBnd ?qs_schema ?qs ?tbl tup /\ @?P tup))}] => let H1 := fresh in let H2 := fresh in makeEvar (Ensemble (@Tuple heading)) ltac:(fun P' => assert (Same_set (@IndexedTuple heading) (fun t => P' (indexedElement t)) P) as H1; [unfold Same_set, Included, Ensembles.In; split; [intros x H; pattern (indexedElement x); match goal with |- ?P'' (indexedElement x) => unify P' P''; simpl; eauto end | eauto] | assert (DecideableEnsemble P') as H2; [ simpl; auto with typeclass_instances | setoid_rewrite (@refine_constraint_check_into_query' qs_schema (ibound (indexb tbl)) qs P P' H2 H1); clear H2 H1 ] ]) end. remember ((n!sRDATA)); refine pick val (beq_RRecordType (RDataTypeToRRecordType d) CNAME); subst; [ | case_eq (beq_RRecordType (RDataTypeToRRecordType (n!sRDATA)) CNAME); intros; rewrite <- beq_RRecordType_dec in H; find_if_inside; unfold not; simpl in *; try congruence ]. intros; simplify with monad laws; simpl. autorewrite with monad laws. setoid_rewrite negb_involutive. apply refine_If_Then_Else; try reflexivity. intros. rewrite (@refine_Count_map DnsSchema Fin.F1). reflexivity. apply DecideableEnsemble_EqDec. eauto with typeclass_instances. 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