proposition: Lemma IndexedBag_BagDeleteCorrect : BagDeleteCorrect IndexedBag_RepInv IndexedBag_bfind IndexedBag_bfind_matcher IndexedBag_benumerate IndexedBag_bdelete.
proof: Proof. hnf. destruct search_term as [option_key search_term]; destruct option_key as [ key | ]; simpl. - unfold IndexedBag_benumerate, IndexedBag_bfind_matcher, IndexedBag_bfind, IndexedBag_bdelete; simpl. case_eq (find key container); simpl; split. + rewrite partition_filter_neq. repeat rewrite <- flat_map_flatten; rewrite filter_flat_map; repeat rewrite flat_map_flatten. pose proof (bdelete_correct b search_term); intuition. repeat rewrite Permutation_map_Values. destruct (bdelete b search_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 Permutation_app_comm. rewrite Values_empty; simpl. rewrite consist''. repeat rewrite flatten_app; simpl. apply Permutation_app. * rewrite Permutation_map_filter_negb; reflexivity. * rewrite app_nil_r, <- Permutation_map_Values, Permuation_filter_flatten, Permutation_map_Values, Permutation_map_filter, consist4. destruct H0; [eapply containerCorrect; rewrite find_mapsto_iff; eauto | rewrite H0]. rewrite partition_filter_neq, H; reflexivity. eauto. * eauto. + pose proof (bdelete_correct b search_term); intuition. destruct (bdelete b search_term); simpl in *. destruct H0; [eapply containerCorrect; rewrite find_mapsto_iff; eauto | rewrite H1]. rewrite partition_filter_eq, partition_filter_eq. rewrite filter_and, flatten_filter, consist, H; eauto. + rewrite partition_filter_neq, flatten_filter. unfold Values. pose proof (alt_IndexedBag_RepInv _ containerCorrect) as containerCorrect'. rewrite <- not_find_in_iff in H. rewrite elements_in_iff in H. clear containerCorrect. induction (elements container); simpl. * constructor. * rewrite IHl. apply Permutation_app; eauto. 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. + rewrite partition_filter_eq, flatten_filter. unfold Values. pose proof (alt_IndexedBag_RepInv _ containerCorrect) as containerCorrect'. rewrite <- not_find_in_iff in H. rewrite elements_in_iff in H. induction (elements container); simpl. * constructor. * rewrite <- IHl. 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, IndexedBag_bdelete; simpl. rewrite fold_pair; 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; f_equiv ]. eapply bdelete_correct. destruct a; eapply containerCorrect'; repeat constructor; eauto. intros; eapply containerCorrect'; eauto. + rewrite fold_1, fold_left_fst_partition with (l' := []); try reflexivity. 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