proposition: Theorem RangeTreeBag_BagInsertEnumerate : BagInsertEnumerate RangeTreeBag_RepInv RangeTreeBag_benumerate RangeTreeBag_binsert.
proof: Proof. unfold BagInsertEnumerate, RangeTreeBag_benumerate, RangeTreeBag_binsert. intros; simpl in *. match goal with | [ |- context[FindWithDefault ?a ?b ?c] ] => destruct (FindWithDefault_dec a b c) as [ [ result (maps_to & _eq) ] | (find_none & _eq) ]; rewrite _eq; clear _eq end. pose proof (partition_after_KeyBasedPartition_and_add (TValue := BagType) (projection inserted) (binsert result inserted) container) as part_add. pose proof (partition_Partition_simple (BagType) (KeyBasedPartitioningFunction BagType (projection inserted)) (KeyBasedPartitioningFunction_Proper _ _) container) as part. rewrite !Values_fold_perm by (eauto using Permutation_Equivalence, Values_fold_Proper, Values_fold_transpose_neqkey). rewrite Partition_fold at 1 by (eauto using part_add, Permutation_Equivalence, Values_fold_Proper, Values_fold_transpose_neqkey). symmetry. rewrite Partition_fold at 1 by (eauto using part , Permutation_Equivalence, Values_fold_Proper, Values_fold_transpose_neqkey). symmetry. pose proof (KeyBasedPartition_fst_singleton (TValue := BagType) _ _ _ maps_to) as singleton. pose proof (add_Equal_simple singleton (projection inserted) (binsert result inserted)) as singleton'. rewrite (fold_Equal_simpl (eqA := @Permutation BagType) singleton') by (eauto using Permutation_Equivalence, Values_fold_Proper, Values_fold_transpose_neqkey). rewrite (fold_Equal_simpl (eqA := @Permutation BagType) singleton) by (eauto using Permutation_Equivalence, Values_fold_Proper, Values_fold_transpose_neqkey). rewrite (fold_Equal_simpl (multiple_adds _ _ _ _)) by (eauto using Permutation_Equivalence, Values_fold_Proper, Values_fold_transpose_neqkey). rewrite !fold_add by (eauto using Permutation_Equivalence, Values_fold_Proper, Values_fold_transpose_neqkey, empty_In). rewrite fold_empty. simpl. rewrite binsert_enumerate. rewrite <- app_comm_cons. eauto. eapply containerCorrect; eauto. rewrite <- not_find_in_iff in find_none. rewrite values_add_not_in by assumption. simpl. rewrite binsert_enumerate. rewrite benumerate_empty_eq_nil with (RepInv := RepInv) (ValidUpdate := ValidUpdate); eauto. apply bempty_RepInv. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.PeanoNat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts