proposition: Lemma IndexedBag_BagUpdateCorrect : BagUpdateCorrect IndexedBag_RepInv IndexedBag_ValidUpdate IndexedBag_bfind IndexedBag_bfind_matcher IndexedBag_benumerate bupdate_transform IndexedBag_bupdate.
proof: Proof. hnf. destruct search_term as [option_key search_term]; destruct option_key as [ key | ]; unfold IndexedBag_benumerate, IndexedBag_bfind_matcher; simpl. - case_eq (find key container); simpl; intros. destruct valid_update as [valid_update valid_update']. + rewrite partition_filter_neq. repeat rewrite <- flat_map_flatten; rewrite filter_flat_map; repeat rewrite flat_map_flatten. pose proof (bupdate_correct b search_term update_term); intuition. repeat rewrite Permutation_map_Values. destruct (bupdate b search_term update_term); simpl in *. erewrite map_add. rewrite Permutation_Partition_App by eapply partition_after_KeyBasedPartition_and_add. rewrite KeyBasedPartition_fst_singleton by (rewrite map_mapsto_iff; eexists; rewrite find_mapsto_iff; split; eauto). rewrite multiple_adds. rewrite (values_add_not_in (empty _)) by (unfold not; intros; eapply empty_in_iff; eassumption). rewrite consist''. rewrite Permutation_app_comm. rewrite Values_empty; simpl. destruct H0. eapply containerCorrect; rewrite find_mapsto_iff; eauto. intuition. repeat rewrite flatten_app; simpl; rewrite H0. rewrite app_nil_r, !app_assoc, Permutation_app; eauto. * rewrite Permutation_map_filter_negb; rewrite consist'; f_equiv. rewrite <- Permutation_map_Values, Permuation_filter_flatten, Permutation_map_Values, Permutation_map_filter, consist4, H. rewrite partition_filter_neq; reflexivity. eauto. eauto. * rewrite partition_filter_eq, partition_filter_eq. rewrite filter_and, flatten_filter, consist, H; eauto. * eapply containerCorrect; rewrite find_mapsto_iff; eauto. * destruct (bupdate b search_term update_term); simpl in *. destruct H0. eapply containerCorrect; rewrite find_mapsto_iff; eauto. intuition. rewrite H1; rewrite partition_filter_eq, partition_filter_eq. rewrite filter_and, flatten_filter, consist, H; eauto. + rewrite partition_filter_neq, flatten_filter, partition_filter_eq, filter_and, flatten_filter, consist, H; simpl; eauto; rewrite app_nil_r. pose proof (alt_IndexedBag_RepInv _ containerCorrect) as containerCorrect'. rewrite <- not_find_in_iff in H. rewrite elements_in_iff in H. unfold Values; induction (elements container); simpl; intuition. rewrite <- (fun x y => proj1 (IHl x y)); f_equiv. assert (forall item : TItem, List.In item (benumerate (snd a)) -> E.eq (projection item) (fst a)) by (intros; eapply containerCorrect'; eauto; repeat constructor; reflexivity). assert (~ E.eq key (fst a)) by (unfold not; intros; apply H; eexists; repeat econstructor; eauto). revert H0 H1. clear; induction (benumerate (snd a)); simpl; intros. constructor. case_eq (KeyFilter key a0); simpl. intros; apply KeyFilter_true in H; rewrite <- H in H1. exfalso; apply H1; apply H0; eauto. rewrite <- IHl; eauto. unfold not; intros H1; apply H; destruct H1; econstructor; constructor 2; eauto. intros; eapply containerCorrect'; eauto. - unfold IndexedBag_benumerate, IndexedBag_bfind_matcher; simpl; intros. rewrite fold_pair with (f := fun _ y => bupdate y search_term update_term). unfold Values; simpl; intuition. + rewrite !FMap_Insert_fold_add, elements_empty, app_nil_r by eauto using empty_In. rewrite !List.map_map; simpl. pose proof (alt_IndexedBag_RepInv _ containerCorrect) as containerCorrect'. induction (elements container); simpl. * constructor. * rewrite IHl, partition_app; simpl. destruct valid_update as [valid_update valid_update']. rewrite Permutation_app by (try (apply bupdate_correct; try eassumption; destruct a; eapply containerCorrect'; repeat constructor; eauto); eauto). rewrite <- !app_assoc. apply Permutation_app; [f_equiv | rewrite Permutation_app_comm, <- app_assoc]. apply Permutation_app; [f_equiv | rewrite Permutation_app_comm, map_app; f_equiv]. intros; apply containerCorrect'; constructor 2; eauto. + rewrite fold_1; rewrite fold_left_fst_partition_update with (l' := []); try reflexivity; try apply valid_update. intros; apply containerCorrect; rewrite elements_mapsto_iff; auto. Qed.
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