proposition: Lemma IndexedBag_binsert_Preserves_RepInv : binsert_Preserves_RepInv IndexedBag_RepInv IndexedBag_binsert.
proof: Proof. unfold binsert_Preserves_RepInv, IndexedBag_binsert, IndexedBag_RepInv. intros [ibag pool] item [repi repp]; simpl in *; split. - eapply ibinsert_RepInv; eapply ib_RepInv; [ | eauto ]. intros idx asmp; rewrite pput_neq; eauto. intro contra; subst; apply repp in asmp; apply asmp; apply pfresh_correct. - intro idx; split; intro asmp. + eapply Permutation_in in asmp; try eapply ibinsert_enumerate; eauto. inversion asmp. subst. rewrite pput_eq. congruence. rewrite pput_neq. apply repp. assumption. intro contra. subst. apply repp in H. apply H. apply pfresh_correct. + eapply Permutation_in. symmetry. eapply ibinsert_enumerate. eauto. destruct (TIndex_dec (pfresh pool) idx); subst. * left; eauto. * right; apply repp; rewrite pput_neq in asmp; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.Structures.OrderedTypeEx