proposition: Lemma ProdBag_BagUpdateCorrect : BagUpdateCorrect ProdBag_RepInv ProdBag_ValidUpdate ProdBag_bfind ProdBag_bfind_matcher ProdBag_benumerate ProdBag_bupdate_transform ProdBag_bupdate.
proof: Proof. unfold ProdBag_benumerate, ProdBag_bfind_matcher, ProdBag_bupdate, ProdBag_bfind, ProdBag_bupdate_transform; hnf; intros container st ut [repA [repB repP] ] [valA [valB valP] ]. rewrite surjective_pairing with (p:=bupdate (fst container) Prod_st_A ut); rewrite surjective_pairing with (p:=bupdate (snd container) Prod_st_B ut); split. - rewrite ListFacts.partition_filter_neq; eapply perm_trans. + destruct Prod_st_choice; eapply bupdate_correct; eauto. + eapply Permutation_app. * 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. * eapply ListMorphisms.map_permutation_morphism; try reflexivity. rewrite !ListFacts.partition_filter_eq. destruct Prod_st_choice; try reflexivity. eapply ListMorphisms.filter_permutation_morphism; try reflexivity. intro; eapply Prod_st_proof. - destruct Prod_st_choice; try eapply bupdate_correct; eauto. simpl; eapply perm_trans; try eapply bupdate_correct; eauto. rewrite !ListFacts.partition_filter_eq. rewrite repP; reflexivity. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties