proposition: Lemma IndexedBag_bupdate_Preserves_RepInv : bupdate_Preserves_RepInv IndexedBag_RepInv IndexedBag_ValidUpdate IndexedBag_bupdate.
proof: Proof. unfold bupdate_Preserves_RepInv, IndexedBag_bupdate, IndexedBag_RepInv, IndexedBag_ValidUpdate. simpl; intros [ibag pool] st ut [repi repp]; split; simpl. - clear repp; remember (ibfind ibag st) as ls; clear Heqls. eapply Common.fold_right_rect; eauto. clear repi ls; intros _ idx ls _ asmp. remember (List.fold_right (fun (idx : TIndex) (p : TPool) => match pget p idx with | Some item => pput p idx (Some (Transform ut item)) | None => p end) pool ls) as pool'; clear Heqpool'. destruct (pget pool' idx) eqn: eq; eauto. specialize (valid_update _ _ idx asmp); clear asmp ls. assert ((pget (pput pool' idx (Some (Transform ut t)))) = (fun i : TIndex => if TIndex_dec i idx then match pget pool' i with | Some item => Some (Transform ut item) | None => None end else pget pool' i)) as H; try rewrite H; eauto. extensionality idx'; destruct (TIndex_dec idx' idx); subst. + rewrite pput_eq; rewrite eq; eauto. + rewrite pput_neq; eauto. - clear valid_update; intro idx; split; intro asmp. + eapply Common.fold_right_rect; simpl; intros; try apply repp; eauto; subst. destruct (pget (List.fold_right (fun (idx : TIndex) (p : TPool) => match pget p idx with | Some item => pput p idx (Some (Transform ut item)) | None => p end) pool t) b); eauto. destruct (TIndex_dec b idx); subst; [ rewrite pput_eq; congruence | rewrite pput_neq ]; eauto. + remember (ibfind ibag st) as ls; clear Heqls. induction ls; simpl in *. apply repp; eauto. destruct (pget (List.fold_right (fun (idx : TIndex) (p : TPool) => match pget p idx with | Some item => pput p idx (Some (Transform ut item)) | None => p end) pool ls) a) eqn: eq. * destruct (TIndex_dec a idx); subst. rewrite pput_eq in asmp. apply IHls; intro; congruence. rewrite pput_neq in asmp; eauto. * apply IHls; intro; congruence. 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