proposition: Corollary refine_Query_For_In_Find_single (ResultT : Type) : forall r_o (r_n : IndexedQueryStructure qs_schema BagIndexKeys), DelegateToBag_AbsR r_o r_n -> forall (idx :Fin.t _) search_pattern (resultComp : _ -> Comp (list ResultT)) filter_rest, refine (l <- CallBagEnumerate idx r_n ; List_Query_In (filter (fun a : ilist2 (B:= @RawTuple) [_] => BagMatchSearchTerm _ search_pattern (ilist2_hd a) && filter_rest a) (Build_single_Tuple_list (snd l))) resultComp) (l <- CallBagFind idx r_n search_pattern; List_Query_In (filter filter_rest (Build_single_Tuple_list (snd l))) resultComp).
proof: Proof. simpl; intros. setoid_rewrite <- refine_BagFind_filter; eauto. unfold CallBagMethod, CallBagEnumerate, CallBagFind; simpl; intros. simplify with monad laws. repeat setoid_rewrite refineEquiv_bind_bind; repeat setoid_rewrite refineEquiv_bind_unit; simpl; f_equiv; intro. setoid_rewrite <- filter_Build_single_Tuple_list; rewrite filter_and; f_equiv. intro; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist2 Fiat.Common.i2list Fiat.Common.ilist3 Fiat.Common.i3list Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.String_as_OT Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements