proposition: Corollary refine_Count_map : forall (qs_schema : RawQueryStructureSchema) (idx : Fin.t (numRawQSschemaSchemas qs_schema)) (r_o : UnConstrQueryStructure qs_schema) (P : Ensemble RawTuple) (P_dec : DecideableEnsemble P), refine (Count For (UnConstrQuery_In r_o idx (fun r : RawTuple => Where (P r) Return r))) (Count For (UnConstrQuery_In r_o idx (fun r : RawTuple => Where (P r) Return ()))).
proof: Proof. Local Transparent Count. Local Transparent Query_For. unfold Count, Query_For; intros. rewrite !refineEquiv_bind_bind. eapply refine_under_bind_both_ambivalent; intros. apply Map_UnConstrQuery_In_Where in H. simpl in H; computes_to_inv; subst. eexists; split; eauto. eapply refine_under_bind_both_ambivalent; intros. simpl in H; computes_to_inv; subst. symmetry in H0. eexists v; split; eauto. apply Permutation_length in H0. rewrite H0. rewrite map_length; reflexivity. assumption. Local Opaque Count. Local Opaque Query_For. 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