proposition: Lemma refine_List_Query_In_Where {QueryT ResultT} l (P : Ensemble QueryT) (resultComp : QueryT -> Comp (list ResultT)) (P_dec : DecideableEnsemble P) : refine (List_Query_In (QueryT := QueryT) l (fun b => Query_Where (P b) (resultComp b))) (List_Query_In (filter dec l) resultComp).
proof: Proof. induction l; unfold List_Query_In, Query_Where in *; simpl. - reflexivity. - caseEq (dec a); simpl; setoid_rewrite <- IHl. + f_equiv; apply dec_decides_P in H; unfold refine; intro; econstructor; intuition. + apply Decides_false in H. unfold refine; intro; econstructor; intuition. econstructor; intuition. repeat econstructor; eauto. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.Common.SetEq Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListMorphisms Fiat.Common.List.FlattenList Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.Common.List.ListFacts