proposition: Lemma refine_Where_Intersection' heading {ResultT} : forall R, FiniteEnsemble R -> forall P (bod : _ -> Comp (list ResultT)), (P \/ ~ P) -> refine (QueryResultComp (heading := heading) R (fun r => Query_Where P (bod r))) (Query_Where P (QueryResultComp R bod)) .
proof: Proof. unfold refine, In, Query_Where, QueryResultComp; intros ? Fin_R ? ? ? v Comp_v. intuition; computes_to_inv; intuition. - computes_to_inv; refine pick val _; eauto. repeat computes_to_econstructor. eapply refine_flatten_CompList_func; eauto. intros * ? ? ?; computes_to_econstructor. computes_to_inv; intuition. - subst. destruct Fin_R as [? Fin_R]. computes_to_econstructor; eauto. eapply refine_flatten_CompList_func. intros * ? ? ?; computes_to_econstructor ; intuition. revert H1. instantiate (1 := fun _ => ret nil); simpl; intros; computes_to_inv; subst; eauto. clear; induction x; simpl; repeat computes_to_econstructor; eauto. Qed.
imports: Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Strings.String Coq.Lists.List Coq.Sorting.Permutation Coq.Bool.Bool Coq.Sets.Ensembles Coq.Logic.FunctionalExtensionality Fiat.ADTNotation Fiat.Common Fiat.Common.ilist2 Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure