proposition: Lemma Permutation_filtered_List {A} : forall l l' P, Permutation (A := A) l l' -> forall l'', computes_to (⟦x in l | P x ⟧) l'' -> exists l''', computes_to (⟦x in l' | P x ⟧) l''' /\ Permutation l'' l'''.
proof: Proof. intros ? ? ? H; induction H; simpl; intros; computes_to_inv. - subst; eauto. - apply IHPermutation in H0; destruct_ex; intuition. eexists (if v0 then x :: x0 else x0); split. repeat computes_to_econstructor; eauto. destruct v0; computes_to_inv; subst; eauto. destruct v0; computes_to_inv; subst; eauto. - eexists (if v0 && v2 then _ :: _ :: _ else if v0 then _ :: _ else if v2 then _ :: _ else _ ); split. repeat setoid_rewrite refine_bind_bind. computes_to_econstructor; eauto. computes_to_econstructor; eauto. destruct v0; destruct v2; simpl; repeat computes_to_econstructor; simpl; eauto. simpl; eauto. simpl; eauto. simpl; eauto. destruct v0; destruct v2; simpl in *; computes_to_inv; subst; eauto. constructor 3; subst. subst; eauto. - apply IHPermutation1 in H1; destruct_ex; intuition. apply IHPermutation2 in H2; destruct_ex; intuition. eexists; split; eauto. rewrite H3; assumption. 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