proposition: Lemma ProdBag_bupdate_Preserves_RepInv : bupdate_Preserves_RepInv ProdBag_RepInv ProdBag_ValidUpdate ProdBag_bupdate.
proof: Proof. unfold bupdate_Preserves_RepInv, ProdBag_bupdate. 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). unfold ProdBag_RepInv; intuition. - destruct Prod_st_choice; eapply bupdate_RepInv; eauto. - destruct Prod_st_choice; eapply bupdate_RepInv; eauto. - destruct Prod_st_choice; simpl; (eapply perm_trans; [ eapply bupdate_correct | ]; eauto; eapply perm_trans; [ | symmetry; eapply bupdate_correct ]; eauto; eapply Permutation_app; [ rewrite !ListFacts.partition_filter_neq | eapply ListMorphisms.map_permutation_morphism; [ unfold Morphisms.pointwise_relation; eapply valP | rewrite !ListFacts.partition_filter_eq ] ]; eapply ListMorphisms.filter_permutation_morphism; eauto; unfold Morphisms.pointwise_relation; intro; f_equal; eapply Prod_st_proof). Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties