proposition: Lemma build_FilteredList_app {A} : forall l l' l'' P, (⟦element in l | P element ⟧) ↝ (l' ++ l'') -> exists k' k'' : list A , l = k' ++ k'' /\ (⟦element in k' | P element ⟧) ↝ l' /\ (⟦element in k'' | P element ⟧) ↝ l''.
proof: Proof. induction l; simpl; intros; computes_to_inv; subst. - eexists nil, nil; simpl; intuition eauto. destruct l'; destruct l''; simpl in H; try discriminate; simpl; eauto. destruct l'; destruct l''; simpl in H; try discriminate; simpl; eauto. - destruct v0; simpl in *; computes_to_inv; subst. + destruct l'; simpl in *; subst. eexists nil, _; intuition eauto; simpl. computes_to_econstructor; eauto. computes_to_econstructor; eauto. refine pick val true; simpl; eauto. apply refine_bind_unit; eauto. injections. apply IHl in H; destruct_ex; subst; intuition; computes_to_inv; subst. eexists (a0 :: x), _; intuition eauto; simpl. computes_to_econstructor; eauto. refine pick val true; simpl; eauto. apply refine_bind_unit; eauto. + apply IHl in H; destruct_ex; subst; intuition; computes_to_inv; subst. eexists (a :: x), _; intuition eauto; simpl. computes_to_econstructor; eauto. refine pick val false; simpl; eauto. apply refine_bind_unit; 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