proposition: Lemma refine_flatten_CompList_filter {A} : forall v l P Q (P_dec : DecideableEnsemble P) (Q_dec : DecideableEnsemble Q), FlattenCompList.flatten_CompList (map (fun r : A => Where (Q r /\ P r) Return r ) v) ↝ l -> exists l', FlattenCompList.flatten_CompList (map (fun r : A => Where (P r) Return r ) v) ↝ l' /\ l = filter (dec (DecideableEnsemble := Q_dec)) l'.
proof: Proof. induction v; simpl; intros; computes_to_inv; subst; eauto. unfold Query_Where, Query_Return in H; computes_to_inv; intuition eauto. unfold Query_Where at 1, Query_Return at 1. eapply IHv in H'; destruct_ex; intuition; subst. exists (if dec (DecideableEnsemble := P_dec) a then a :: x else x). split. - destruct (dec (DecideableEnsemble := P_dec) a) eqn: ?. + rewrite dec_decides_P in Heqb. repeat computes_to_econstructor; intuition eauto. + apply Decides_false in Heqb. repeat computes_to_econstructor; intuition eauto. - destruct (dec (DecideableEnsemble := P_dec) a) eqn: ?. + rewrite dec_decides_P in Heqb. simpl. destruct (dec (DecideableEnsemble := Q_dec) a) eqn: ?. * rewrite dec_decides_P in Heqb0. intuition eauto. computes_to_inv; subst; simpl; eauto. * apply Decides_false in Heqb0. intuition eauto. subst; simpl; eauto. + apply Decides_false in Heqb. destruct (dec (DecideableEnsemble := Q_dec) a) eqn: ?. * rewrite dec_decides_P in Heqb0. intuition eauto. computes_to_inv; subst; simpl; eauto. * apply Decides_false in Heqb0. intuition eauto. subst; simpl; eauto. 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