proposition: Lemma refine_Intersection_Where heading {ResultT} : forall R P (P_dec : DecideableEnsemble P) (bod : _ -> Comp (list ResultT)), refine (QueryResultComp (IndexedEnsemble_Intersection R P) bod) (QueryResultComp (heading := heading) R (fun r => Query_Where (P r) (bod r))).
proof: Proof. unfold refine, In, QueryResultComp; intros * ? ? v Comp_v. repeat computes_to_inv. refine pick val _; eauto using UnIndexedEnsembleListEquivalence_filter. repeat computes_to_econstructor. revert v Comp_v'; clear; induction v0; intros; simpl in *; eauto. computes_to_inv; subst. apply (refine_Where' P_dec) in Comp_v'. find_if_inside; simpl. computes_to_econstructor; eauto. computes_to_inv; subst; simpl; 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