proposition: Lemma bdelete_correct_DB_fst {qsSchema} : forall (qs : UnConstrQueryStructure qsSchema) (Ridx : Fin.t _) bag_plus bag (equiv_bag : EnsembleBagEquivalence bag_plus (GetUnConstrRelation qs Ridx) bag) (DT : Ensemble RawTuple) (DT_Dec : DecideableEnsemble DT) search_term, ExtensionalEq (@DecideableEnsembles.dec _ _ DT_Dec) (bfind_matcher (Bag := BagPlus bag_plus) search_term) -> refine {x | QSDeletedTuples qs Ridx DT x} (ret (fst (bdelete bag search_term))).
proof: Proof. intros; setoid_rewrite DeletedTuplesFor; auto. destruct equiv_bag as [ [ [bound ValidBound] [l [eq_bag [NoDup_l equiv_l] ] ] ] RepInv_bag]; subst. rewrite refine_List_Query_In. rewrite refine_List_Query_In_Where, refine_List_For_Query_In_Return_Permutation, (filter_by_equiv _ _ H), map_id, <- partition_filter_eq. rewrite refine_pick_val. reflexivity. destruct (bdelete_correct bag search_term RepInv_bag) as [_ Perm_bdelete]; eauto. unfold BagPlusProofAsBag, QSGetNRelSchemaHeading, GetNRelSchemaHeading, GetNRelSchema in *. rewrite Perm_bdelete; reflexivity. econstructor. eexists _; eauto. unfold UnIndexedEnsembleListEquivalence; eexists; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.TreeBags Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Coq.Lists.List Coq.Program.Program Fiat.Common.ilist Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.NArith.BinNat Coq.ZArith.ZArith_dec Coq.Arith.Arith Coq.FSets.FMapAVL Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.ilist2 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements Fiat.QueryStructure.Implementation.Operations.List.ListQueryRefinements