proposition: Lemma TrieBag_bdelete_Preserves_RepInv : bdelete_Preserves_RepInv TrieBagRepInv TrieBag_bdelete.
proof: Proof. unfold bdelete_Preserves_RepInv, TrieBagRepInv; intros trie search_term; remember []; clear Heql; revert l. unfold TrieBag_bdelete. destruct search_term as [ [l | ] s]. { eapply Trie_delete_ind; intros; subst. - econstructor; inversion containerCorrect; subst; eauto. + pose proof (bdelete_RepInv bag search_term) as e'; simpl in *; rewrite e0 in e'; eapply e'. inversion containerCorrect; eauto. + intros; eapply H1. destruct (bdelete_correct bag search_term); eauto. simpl in *; rewrite e0 in *; simpl in *. rewrite H4 in H3. rewrite In_partition; eauto. - econstructor; inversion containerCorrect; subst; eauto. + pose proof (bdelete_RepInv bag search_term) as e'; simpl in *; rewrite e0 in e'; eapply e'; eauto. + intros; eapply H2. destruct (bdelete_correct bag search_term); eauto. simpl in *; rewrite e0 in *; simpl in *. rewrite H5 in H4. rewrite In_partition; eauto. + intros; destruct (X.eq_dec k key0). * apply find_1 in H4; eauto. simpl in *. pose proof (add_1 subtries bag'' (X.eq_sym e)) as H7; apply find_1 in H7; eauto. rewrite H4 in H7; injections; intros; subst. rewrite e2 in H; eapply H. eapply H3. apply MapsTo_1 with (x := key0). symmetry; eauto. apply find_2; eauto. * apply H3. eapply add_3; eauto; intuition. - simpl; econstructor; inversion containerCorrect; subst; eauto. + pose proof (bdelete_RepInv bag search_term) as e'; simpl in *; rewrite e0 in e'; eapply e'. inversion containerCorrect; eauto. + intros; eapply H1. destruct (bdelete_correct bag search_term); eauto. simpl in *; rewrite e0 in *; simpl in *. rewrite H4 in H3. rewrite In_partition; eauto. } { intro; pattern trie, l; apply Trie_ind'; simpl; intros. intros; inversion containerCorrect; subst. case_eq (bdelete b s); simpl; intros. econstructor. + pose proof (bdelete_RepInv b s) as e'; simpl in *. rewrite H0 in e'; eapply e'; eauto. + apply XMap.is_bst. + intros; eapply H4. destruct (bdelete_correct b s); eauto. simpl in *; rewrite H0 in *; simpl in *. rewrite H5 in H1. rewrite In_partition; eauto. + intros; rewrite XMapfold_eq in H1. setoid_rewrite (fold_pair (XMap.Bst H3)) in H1; simpl in H1. assert (XMap.MapsTo k subtrie (XMap.fold (fun (k0 : XMap.key) (m0 : Trie) (b' : XMap.t Trie) => XMap.add k0 (snd (Trie_delete' m0 s)) b') {| XMap.this := m; XMap.is_bst := H3 |} (XMap.empty Trie))) by apply H1; clear H1. setoid_rewrite FMap_Insert_fold_add_map_eq in H5. rewrite map_mapsto_iff in H5; destruct_ex; intuition; subst. eapply H; 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.ZArith.ZArith Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListPrefix