proposition: Lemma IndexedBag_bupdate_Preserves_RepInv : bupdate_Preserves_RepInv IndexedBag_RepInv IndexedBag_ValidUpdate IndexedBag_bupdate.
proof: Proof. unfold bupdate_Preserves_RepInv, IndexedBag_RepInv. intros; destruct search_term; destruct o; simpl in *. destruct valid_update as [valid_update valid_update']. - case_eq (find t0 container); intros; rewrite H0 in *. rewrite <- find_mapsto_iff in H0. assert (RepInv b) as WF_b by (eapply containerCorrect; eauto). case_eq (bupdate b s update_term); intros; rewrite H1 in *; simpl in *. pose proof (bupdate_RepInv b s update_term WF_b valid_update) as RepInv_H1. rewrite H1 in RepInv_H1. intuition. + rewrite add_mapsto_iff in H; intuition. unfold IndexedBag_ValidUpdate in *. rewrite <- H3; intuition. eapply containerCorrect; eauto. + rewrite add_mapsto_iff in H; intuition. pose proof (bupdate_correct b s update_term WF_b valid_update); simpl in *; intuition. rewrite <- H4 in H2. rewrite <- H; rewrite H1 in H5; simpl in *. pose proof (Permutation_in _ H5 H2); apply in_app_or in H3; destruct H3. * pose proof ((proj2 (In_partition _ _ _)) (or_intror H3)); eapply containerCorrect; eauto. * apply in_map_iff in H3; destruct H3 as [item' [item'_eq In_item'] ]. rewrite <- item'_eq in *. eapply valid_update'. eapply containerCorrect; eauto; eapply In_partition; eauto. * eapply containerCorrect; eauto. + eapply containerCorrect; eauto. - rewrite fold_pair in H; simpl in H. rewrite FMap_Insert_fold_add_map_eq in H. rewrite map_mapsto_iff in H; destruct H as [bag' [bag'_eq MapsTo_key0] ]; subst. assert (RepInv bag') as WF_bag' by (eapply containerCorrect; eauto). destruct valid_update as [valid_update valid_update']. pose proof (bupdate_correct bag' s update_term WF_bag' valid_update); intuition. apply bupdate_RepInv; eauto. pose proof (Permutation_in _ H0 H) as H4; apply in_app_or in H4; destruct H4. + pose proof ((proj2 (In_partition _ _ _)) (or_intror H2)); eapply containerCorrect; eauto. + rewrite in_map_iff in H2; destruct H2 as [item' [item'_eq In_item'] ]. rewrite <- item'_eq in *. eapply valid_update'. eapply containerCorrect; eauto; eapply In_partition; eauto. Defined.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Arith.PeanoNat Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts