proposition: Lemma Map_UnConstrQuery_In_Where {resultT}: forall (qs_schema : RawQueryStructureSchema) (idx : Fin.t (numRawQSschemaSchemas qs_schema)) (r_o : UnConstrQueryStructure qs_schema) (P : Ensemble RawTuple) (f : _ -> resultT) (P_dec : DecideableEnsemble P), refine (results <- UnConstrQuery_In r_o idx (fun r : RawTuple => Where (P r) Return r); ret (map f results)) (UnConstrQuery_In r_o idx (fun r : RawTuple => Where (P r) Return (f r))).
proof: Proof. intros; unfold UnConstrQuery_In, QueryResultComp. rewrite refineEquiv_bind_bind; f_equiv; intro. induction a; simpl; autorewrite with monad laws. - reflexivity. - setoid_rewrite <- IHa. autorewrite with monad laws. unfold Query_Where, Query_Return; f_equiv. intros ? ?. apply Bind_inv in H; destruct_ex; intuition. refine pick val (if dec a then [a] else nil). + destruct (dec a) eqn: Heq_a. * rewrite dec_decides_P in Heq_a. computes_to_inv; subst. setoid_rewrite map_app; computes_to_econstructor; intuition eauto. computes_to_econstructor; eauto. computes_to_inv; subst; computes_to_econstructor. * computes_to_inv; subst. setoid_rewrite map_app; computes_to_econstructor; intuition eauto. rewrite Decides_false in Heq_a; apply H2 in Heq_a; subst. computes_to_econstructor; eauto. + destruct (dec a) eqn: Heq_a. * rewrite dec_decides_P in Heq_a; intuition. * rewrite Decides_false in Heq_a; intuition. 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