proposition: Lemma refine_forall_to_exists_independent {A} : forall n (P P' Q : A -> Prop) (R : @IndexedEnsemble A), (P' n -> ~ P n) -> P n -> refine {b | decides b (forall tup' : @IndexedElement A, R tup' -> Q (indexedElement tup') -> P' n)} (b <- {b | decides b (exists tup' : @IndexedElement A, R tup' /\ Q (indexedElement tup'))}; ret (negb b)).
proof: Proof. intros. rewrite (@refine_forall_to_exists _ (fun _ => P' n)). unfold refine; intros; computes_to_inv; subst. refine pick val v0. computes_to_econstructor; eauto. destruct v0; simpl in *. - destruct_ex; eexists; intuition eauto. - intro; apply H1; destruct_ex; eexists; intuition eauto. - eapply Build_DecideableEnsemble with (fun _ => false); split; intros; eauto. + discriminate. + 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