proposition: Lemma refine_Where_Intersection heading {ResultT} : forall R P (P_dec : DecideableEnsemble P) (bod : _ -> Comp (list ResultT)), FiniteEnsemble R -> refine (QueryResultComp (heading := heading) R (fun r => Query_Where (P r) (bod r))) (QueryResultComp (IndexedEnsemble_Intersection R P) bod) .
proof: Proof. unfold refine, In, QueryResultComp; intros * ? ? Fin_R v Comp_v. repeat computes_to_inv. destruct Fin_R as [? Fin_R]. pose proof (UnIndexedEnsembleListEquivalence_filter P_dec Fin_R). pose proof (Permutation_UnIndexedEnsembleListEquivalence' H Comp_v). eapply PermutationFacts.permutation_filter in H0; destruct_ex; intuition subst. refine pick val x0; eauto using Permutation_UnIndexedEnsembleListEquivalence. repeat computes_to_econstructor; eauto. revert v Comp_v'; clear; induction x0; simpl; intros; eauto. case_eq (dec a); simpl in *; intro H; rewrite H in *; simpl in Comp_v'; computes_to_inv. - computes_to_inv; subst; repeat computes_to_econstructor. apply dec_decides_P in H; split; intros; intuition. eapply IHx0; eauto. - computes_to_inv; subst; repeat computes_to_econstructor. apply Decides_false in H; split; intros; intuition. eauto. simpl; computes_to_econstructor. 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