proposition: Lemma refine_filter_BagFind : forall r_o (r_n : IndexedQueryStructure qs_schema BagIndexKeys), DelegateToBag_AbsR r_o r_n -> forall (idx : Fin.t _) filter_dec search_pattern, ExtensionalEq filter_dec (BagMatchSearchTerm (ith3 BagIndexKeys idx) search_pattern) -> refine (CallBagFind idx r_n search_pattern) (l <- {l | EnsembleIndexedListEquivalence (GetIndexedRelation r_n idx) l}; ret (r_n, filter filter_dec l)).
proof: Proof. unfold UnConstrQuery_In, QueryResultComp, CallBagEnumerate, CallBagFind, CallBagMethod, Query_For; intros; simpl. repeat setoid_rewrite refineEquiv_bind_bind; repeat setoid_rewrite refineEquiv_bind_unit; simpl. setoid_rewrite (filter_by_equiv _ _ H0). intros v Comp_v. computes_to_inv. subst. destruct Comp_v as [? ?]. pose proof (UnIndexedEnsembleListEquivalence_filter (DecideableEnsemble_bool (BagMatchSearchTerm (ith3 BagIndexKeys idx) search_pattern)) H2). repeat computes_to_econstructor. eexists; eauto. destruct H1 as [? H1]; eexists; intros ? ?; try eapply H1. apply H4. unfold UpdateIndexedRelation, GetIndexedRelation. rewrite replace3_Index3_eq. computes_to_econstructor. 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