proposition: Lemma refine_BagADT_QSDelete_fst : forall r_o (r_n : IndexedQueryStructure qs_schema BagIndexKeys), DelegateToBag_AbsR r_o r_n -> forall (idx :Fin.t _) (DT : Ensemble RawTuple) (DT_Dec : DecideableEnsemble DT) search_pattern, ExtensionalEq (@DecideableEnsembles.dec _ _ DT_Dec) (BagMatchSearchTerm (ith3 BagIndexKeys idx) search_pattern) -> refine {x : list RawTuple | QSDeletedTuples r_o idx DT x} (l <- (CallBagDelete idx r_n search_pattern); ret (snd l)).
proof: Proof. intros; setoid_rewrite DeletedTuplesFor; auto. rewrite refine_Query_In_Enumerate by eauto. setoid_rewrite refine_List_Query_In_Where. instantiate (1 := _). simpl in *. rewrite (refineEquiv_Join_Comp_Lists_Build_single_Tuple_list r_n idx). setoid_rewrite refineEquiv_bind_bind at 1. setoid_rewrite refineEquiv_bind_bind at 1. setoid_rewrite refineEquiv_bind_unit at 1. setoid_rewrite <- refineEquiv_bind_bind at 1. rewrite (refine_Query_For_In_Find_snd' H _ H0). setoid_rewrite refine_List_Query_In_Return. setoid_rewrite refine_filter_BagFind; eauto; simplify with monad laws. unfold Build_single_Tuple_list; setoid_rewrite map_map; simpl. setoid_rewrite map_id. unfold CallBagFind, CallBagDelete, CallBagMethod; simpl; try simplify with monad laws; repeat setoid_rewrite refineEquiv_bind_bind; repeat setoid_rewrite refineEquiv_bind_unit; simpl; f_equiv; intro. refine pick val _; eauto. erewrite filter_by_equiv; eauto. 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