proposition: Lemma IndexedBag_bdelete_Preserves_RepInv : bdelete_Preserves_RepInv IndexedBag_RepInv IndexedBag_bdelete.
proof: Proof. unfold bdelete_Preserves_RepInv, IndexedBag_bdelete, IndexedBag_RepInv. simpl; intros [ibag pool] st [repi repp]; simpl. assert (forall idx, List.In idx (ibenumerate (snd (ibdelete ibag st))) -> ~ List.In idx (fst (ibdelete ibag st))). { intros idx asmp asmp'. pose proof (ibdelete_correct _ _ st repi) as [Hsnd Hfst]. pose proof (Permutation_in _ Hsnd asmp) as asmp_ls. pose proof (Permutation_in _ Hfst asmp') as asmp'_ls. apply ListFacts.In_partition_unmatched in asmp_ls. apply ListFacts.In_partition_matched in asmp'_ls. congruence. } rewrite surjective_pairing with (p:=ibdelete ibag st); split; simpl in *. - pose proof (ibdelete_RepInv _ _ st repi) as repi'; eapply ib_RepInv; [ | eauto ]. intros idx asmp; apply H in asmp. generalize asmp; apply Common.fold_right_rect; eauto; intros; subst. destruct (TIndex_dec b idx); eauto; subst. exfalso. apply asmp0. econstructor. eauto. rewrite pput_neq; eauto. apply H0. intro. apply asmp0. econstructor 2. eauto. - intro idx; split; intro asmp. + pose proof (H _ asmp) as asmp'; generalize asmp'. eapply Common.fold_right_rect; eauto; intros; subst. apply repp. eapply (fun A f x l H => proj1 (proj1 (@List.filter_In A x f l) H)). pose proof (ibdelete_correct _ _ st repi) as [Hdel _]. rewrite ListFacts.partition_filter_neq in Hdel; eapply Permutation_in; eauto. destruct (TIndex_dec b idx); subst; [ rewrite pput_eq | rewrite pput_neq ]; eauto. exfalso; apply asmp'0; econstructor; eauto. apply H0; intro; apply asmp'0; econstructor 2; eauto. + specialize (H idx); pose proof (ibdelete_correct _ _ st repi) as [Hsnd Hfst]. rewrite ListFacts.partition_filter_neq in Hsnd; rewrite (Permutation_in' idx Hsnd) in *. rewrite ListFacts.partition_filter_eq in Hfst; symmetry in Hfst. apply PermutationFacts.permutation_filter in Hfst. destruct Hfst as [ls [Hfst1 Hfst2] ]. rewrite <- Hfst1 in *. apply List.filter_In; rewrite (Permutation_in' idx Hfst2). specialize (fun H => proj1 (Permutation_in' idx Hfst2) (proj2 (repp idx) H)); clear repp; intro repp. clear H Hfst1 Hfst2 Hsnd. induction ls; eauto; simpl in *. * exfalso; eauto. * destruct (IBagMatcher Matcher (pget pool) st a) eqn: eq; simpl in *. { destruct (TIndex_dec a idx); subst; eauto. rewrite pput_eq in asmp; congruence. rewrite pput_neq in asmp; eauto. specialize (IHls asmp); clear asmp. split; [ right | ]; apply IHls; intro; destruct (repp H); try congruence; eauto. } { destruct (TIndex_dec a idx); subst; eauto. split. tauto. rewrite eq. auto. split; [ right | ]; apply IHls; eauto. intro. destruct (repp H). congruence. auto. intro. destruct (repp H). congruence. auto. } 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.Structures.OrderedTypeEx