proposition: Lemma consist'' : forall (container: IndexedBag) key search_term (containerCorrect : IndexedBag_RepInv container), Permutation (Values (map (fun x : BagType => List.filter (fun a : TItem => negb (KeyFilter key a && bfind_matcher search_term a)) (benumerate x)) container)) (Values (map benumerate (snd (partition (KeyBasedPartitioningFunction _ key) container))) ++ (Values (map (fun x : BagType => List.filter (fun a : TItem => negb (bfind_matcher (Bag := TBag) search_term a)) (benumerate x)) (fst (partition (KeyBasedPartitioningFunction _ key) container))))).
proof: Proof. unfold Values; intros; rewrite <- List.map_app. eapply Permutation_InA_cons; eauto using elements_3w. - eapply NoDupA_app; eauto using elements_3w, equiv_eq_key; intros. unfold eq_key in H. destruct x. apply elements_in_if' in H. apply elements_in_if' in H0. rewrite map_in_iff in H, H0. apply In_KeyBasedPartition_snd in H. apply In_KeyBasedPartition_fst in H0. congruence. - intros; rewrite InA_app_iff by eauto using equiv_eq_key_elt. repeat rewrite <- elements_mapsto_iff; repeat rewrite map_mapsto_iff. intuition. destruct H as [a [? In_k] ]; subst. destruct (E.eq_dec key0 k); [ right | left ]. + eexists a. rewrite <- e in *. rewrite KeyBasedPartition_fst_singleton; eauto; split. simpl; unfold IndexedBag_bfind_matcher; simpl. * generalize (proj2 (containerCorrect _ _ In_k)); induction (benumerate a); simpl; intros; eauto. case_eq (KeyFilter key0 a0); intros; simpl. case_eq (bfind_matcher search_term a0); intros; simpl. rewrite IHl; eauto. rewrite IHl; eauto. apply KeyFilter_false in H0; exfalso; eauto. * generalize (proj2 (containerCorrect _ _ In_k)); induction (benumerate a); simpl; intros; eauto. eapply add_1; reflexivity. + eexists a; split. generalize (proj2 (containerCorrect _ _ In_k)); induction (benumerate a); intros; simpl; eauto. case_eq (KeyFilter key0 a0); simpl; try rewrite IHl; eauto. intros Filter_key0; apply KeyFilter_true in Filter_key0. exfalso; apply n; rewrite <- Filter_key0, H; eauto. simpl in *; constructor; eauto. intros; apply H; constructor 2; eauto. intros; apply H; constructor 2; eauto. rewrite partition_iff_2 with (f := KeyBasedPartitioningFunction _ key0); eauto using KeyBasedPartitioningFunction_Proper. intuition; eapply KeyBasedPartitioningFunction_eq_false; eassumption. + destruct H0 as [a [? MapsTo_k] ]; subst. pose proof (MapsTo_KeyBasedPartition_snd _ _ _ _ MapsTo_k). rewrite partition_iff_2 with (f := KeyBasedPartitioningFunction _ key0) in MapsTo_k; eauto using KeyBasedPartitioningFunction_Proper. exists a; intuition. generalize (proj2 (containerCorrect _ _ H0)). induction (benumerate a); simpl; intros; eauto. case_eq (KeyFilter key0 a0); simpl; try rewrite <- IHl; eauto. intros Filter_key0; apply KeyFilter_true in Filter_key0. exfalso; apply H; rewrite <- Filter_key0; eapply H2; eauto. + destruct H0 as [a [? MapsTo_k] ]; subst. pose proof (MapsTo_KeyBasedPartition_fst _ _ _ _ MapsTo_k). rewrite partition_iff_1 with (f := KeyBasedPartitioningFunction _ key0) in MapsTo_k; eauto using KeyBasedPartitioningFunction_Proper. simpl; unfold IndexedBag_bfind_matcher; simpl. exists a; intuition. generalize (proj2 (containerCorrect _ _ H0)). induction (benumerate a); simpl; intros; eauto. case_eq (KeyFilter key0 a0); simpl; eauto. intros Filter_key0; apply KeyFilter_true in Filter_key0. rewrite IHl; eauto. intros Filter_key0; apply KeyFilter_false in Filter_key0. exfalso; apply Filter_key0; rewrite H, H2; eauto. 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