proposition: Lemma refine_count_constraint_broken' : forall (n : resourceRecord) (r : UnConstrQueryStructure DnsSchema), refine {b | decides b (forall tup' : @IndexedTuple (GetHeading DnsSchema sRRecords), (GetUnConstrRelation r bCOLLECTIONS) tup' -> (indexedElement tup')!sNAME = n!sNAME -> RDataTypeToRRecordType (indexedElement tup')!sRDATA <> CNAME)} (count <- Count For (UnConstrQuery_In r bCOLLECTIONS (fun tup : Tuple => Where (n!sNAME = tup!sNAME /\ RDataTypeToRRecordType tup!sRDATA = CNAME ) Return () )); ret (beq_nat count 0)).
proof: Proof. intros; setoid_rewrite refine_forall_to_exists'. match goal with |- context[{b | decides b (exists tup : @IndexedTuple ?heading, (@GetUnConstrRelation ?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 | setoid_rewrite (@refine_constraint_check_into_query' qs_schema tbl qs P P' H2 H1); clear H1 H2 ] ]) end. apply @DecideableEnsemble_And. apply DecideableEnsemble_EqDec. auto with typeclass_instances. apply DecideableEnsemble_EqDec. apply Query_eq_RRecordType. simplify with monad laws. setoid_rewrite negb_involutive; f_equiv. apply refine_Count_map. apply DecideableEnsemble_And. 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