proposition: Lemma ProdBag_BagDeleteCorrect : BagDeleteCorrect ProdBag_RepInv ProdBag_bfind ProdBag_bfind_matcher ProdBag_benumerate ProdBag_bdelete.
proof: Proof. unfold ProdBag_benumerate, ProdBag_bfind_matcher, ProdBag_bdelete, ProdBag_bfind; hnf; intros container st [repA [repB repP] ]; rewrite surjective_pairing with (p:=bdelete (fst container) Prod_st_A); rewrite surjective_pairing with (p:=bdelete (snd container) Prod_st_B); split. - rewrite ListFacts.partition_filter_neq; eapply perm_trans. + destruct Prod_st_choice; eapply bdelete_correct; eauto. + eapply perm_trans; [ | eapply ListMorphisms.filter_permutation_morphism; try eapply Permutation_refl; unfold Morphisms.pointwise_relation; intro a; pose proof (ProdBag_BagMatcherEquiv st a); unfold ProdBag_bfind_matcher in H; rewrite H; reflexivity ]. rewrite <- ListFacts.partition_filter_neq; reflexivity. - destruct Prod_st_choice; try eapply bdelete_correct; eauto. simpl; eapply perm_trans; try eapply bdelete_correct; eauto. rewrite !ListFacts.partition_filter_eq. rewrite repP; reflexivity. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties