proposition: Lemma InvertedIndex_binsert_Preserves_RepInv : binsert_Preserves_RepInv InvertedIndex_RepInv InvertedIndex_binsert.
proof: Proof. unfold binsert_Preserves_RepInv, InvertedIndex_binsert, UpdateKeyMap; intros; repeat split; intros; simpl in *. rewrite MKeysProperties.update_mapsto_iff in H; intuition. - rewrite FMap_fold_add_MapsTo_In in H1. simpl in *; intuition; subst. simpl in *; intuition; subst. exists item; intuition eauto using MValues.add_1. eapply filter_InA; eauto with typeclass_instances. unfold Proper, respectful; intros. repeat case_InA; eauto. rewrite H0 in i; intuition. rewrite <- H0 in i; intuition. intro. apply MKeys_elements_in_iff in H; destruct H. eapply MKeys.empty_1; eauto. - rewrite MKeysProperties.update_mapsto_iff in H; intuition. + rewrite MoreMKeysFacts.BasicFacts.map_mapsto_iff in H1; destruct H1; intuition; subst; destruct H0; subst. exists item; intuition eauto using MValues.add_1. rewrite MKeysProperties.filter_iff in H3; intuition; eauto. case_InA; try discriminate; eauto. unfold Proper, respectful; intros. repeat case_InA; subst; eauto. rewrite H in i; intuition. rewrite <- H in i; intuition. destruct (eq_nat_dec idx (NumValues container)); subst. exists item; intuition eauto using MValues.add_1. rewrite MKeysProperties.filter_iff in H3; intuition; eauto. case_InA; try discriminate; eauto. unfold Proper, respectful; intros. repeat case_InA; subst; eauto. rewrite H0 in i; intuition. rewrite <- H0 in i; intuition. rewrite MKeysProperties.filter_iff in H3; intuition; eauto. case_InA; try discriminate; eauto. unfold InvertedIndex_RepInv in containerCorrect; intuition. destruct (H3 _ _ H0 _ H); intuition. eexists; split; eauto using MValues.add_2. unfold Proper, respectful; intros. repeat case_InA; subst; eauto. rewrite H0 in i; intuition. rewrite <- H0 in i; intuition. + rewrite MKeysProperties.filter_iff in H; intuition; eauto. case_InA; simpl in *; try discriminate. unfold InvertedIndex_RepInv in containerCorrect; intuition. destruct (H _ _ H1 _ H0); intuition. eexists; split; eauto. eapply MValues.add_2; eauto. intro; subst; eapply H7. reflexivity. eexists; eauto. unfold Proper, respectful; intros. repeat case_InA; subst; eauto. rewrite H1 in i; intuition. rewrite <- H1 in i; intuition. - rewrite MValuesFacts.add_mapsto_iff in H; intuition; subst. destruct (InA_dec E.eq_dec key (let (includedKeys, notIncludedKeys) := MKeysProperties.partition (fun key _ => if (InA_dec E.eq_dec key (projection item0)) then true else false) (KeyMap container) in let oldKeys := map fst (MKeys.elements includedKeys) in List.filter (fun key : E.t => if InA_dec E.eq_dec key oldKeys then false else true) (projection item0))); simpl in *. + apply filter_InA in i; intuition. case_InA; try discriminate. eexists [NumValues container]. rewrite MKeysProperties.update_mapsto_iff. split; simpl; eauto. left. eapply FMap_fold_add_MapsTo_In; intuition; eauto. apply MKeys_elements_in_iff in H2; destruct H2; eapply MKeys.empty_1; eauto. eapply filter_InA. eauto with typeclass_instances. unfold Proper, respectful; intros. repeat case_InA; subst; eauto. rewrite H2 in i; intuition. rewrite <- H2 in i; intuition. intuition; eauto. case_InA; eauto. unfold Proper, respectful; intros. repeat case_InA; subst; eauto. let H := match goal with H : E.eq _ _ |- _ => constr:(H) end in rewrite H in i0; intuition. let H := match goal with H : E.eq _ _ |- _ => constr:(H) end in rewrite <- H in i0; intuition. + assert (MKeys.In key (KeyMap container)). induction (projection item0); simpl in *. * inversion H0. * inversion H0; subst; eauto. case_InA. rewrite <- MKeys_elements_in_iff in i0. destruct i0. rewrite MKeysProperties.filter_iff in H; intuition; eauto. eexists x; rewrite H1; eauto. unfold Proper, respectful; intros. destruct (MoreMKeysFacts.BasicProperties.F.eq_dec x0 a); destruct (MoreMKeysFacts.BasicProperties.F.eq_dec y a); eauto. subst. rewrite H2 in e; intuition. repeat case_InA; eauto. rewrite H2 in i0; intuition. rewrite <- H2 in i0; intuition. exfalso; apply n; econstructor; eauto. apply IHi; eauto. repeat case_InA. intro. apply filter_InA in H; intuition eauto with typeclass_instances. case_InA; try discriminate. apply n0. rewrite <- MKeys_elements_in_iff. rewrite <- MKeys_elements_in_iff in i0. destruct i0. rewrite MKeysProperties.filter_iff in H4; intuition; eauto. destruct (E.eq_dec key a). rewrite e; eauto. rewrite filter_InA in n; eauto with typeclass_instances. intuition. case_InA. apply MKeys_elements_in_iff in i0. destruct i0. rewrite MKeysProperties.filter_iff in H4; intuition. destruct (MoreMKeysFacts.BasicProperties.F.eq_dec key a). eexists. rewrite MKeysProperties.filter_iff; intuition; eauto. case_InA; eauto. rewrite e0 in H2; intuition. unfold Proper, respectful; intros. subst. repeat find_if_inside; try reflexivity. rewrite H4 in i0; intuition. rewrite H4 in i0; intuition. rewrite <- H4 in i0; intuition. rewrite <- H4 in i0; intuition. case_InA. eexists. rewrite MKeysProperties.filter_iff; intuition; eauto. discriminate. unfold Proper, respectful; intros. destruct (MoreMKeysFacts.BasicProperties.F.eq_dec x1 a); destruct (MoreMKeysFacts.BasicProperties.F.eq_dec y a); try reflexivity. rewrite H8 in e0; intuition. rewrite <- H8 in e0; intuition. repeat case_InA; try reflexivity. rewrite H8 in i1; intuition. rewrite <- H8 in i1; intuition. rewrite H8 in i0; intuition. rewrite <- H8 in i0; intuition. intuition. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. rewrite H4 in i1; intuition. rewrite <- H4 in i1; intuition. rewrite H4 in i0; intuition. rewrite <- H4 in i0; intuition. rewrite filter_InA in n; eauto with typeclass_instances. intuition. case_InA. apply MKeys_elements_in_iff in i0. destruct i0. rewrite MKeysProperties.filter_iff in H4; intuition. destruct (MoreMKeysFacts.BasicProperties.F.eq_dec key a). intuition. case_InA. eexists. rewrite MKeysProperties.filter_iff; intuition; eauto. find_if_inside; eauto. unfold Proper, respectful; intros. subst. repeat find_if_inside; try reflexivity. rewrite H4 in i1; intuition. rewrite H4 in i1; intuition. rewrite <- H4 in i1; intuition. rewrite <- H4 in i1; intuition. discriminate. unfold Proper, respectful; intros. destruct (MoreMKeysFacts.BasicProperties.F.eq_dec x1 a); destruct (MoreMKeysFacts.BasicProperties.F.eq_dec y a); try reflexivity. rewrite H8 in e; intuition. rewrite <- H8 in e; intuition. repeat case_InA; try reflexivity. rewrite H8 in i1; intuition. rewrite <- H8 in i1; intuition. rewrite H8 in i0; intuition. rewrite <- H8 in i0; intuition. intuition. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. rewrite H4 in i1; intuition. rewrite <- H4 in i1; intuition. rewrite H4 in i0; intuition. rewrite <- H4 in i0; intuition. unfold Proper, respectful; intros. destruct (MoreMKeysFacts.BasicProperties.F.eq_dec x0 a); destruct (MoreMKeysFacts.BasicProperties.F.eq_dec y a); try reflexivity. rewrite H5 in e; intuition. rewrite <- H5 in e; intuition. repeat case_InA; try reflexivity. rewrite H5 in i0; intuition. rewrite <- H5 in i0; intuition. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite H3 in i1; intuition. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite <- H3 in i1; intuition. intro; eapply n. destruct (E.eq_dec key a). rewrite e; eauto. econstructor 2; eauto. apply filter_InA in H; intuition eauto with typeclass_instances. apply filter_InA. eauto with typeclass_instances. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. rewrite H4 in i1; intuition. rewrite <- H4 in i1; intuition. rewrite H4 in i0; intuition. rewrite <- H4 in i0; intuition. intuition. repeat case_InA. discriminate. discriminate. rewrite <- MKeys_elements_in_iff in i0; destruct i0. rewrite MKeysProperties.filter_iff in H4. destruct H4. destruct (MoreMKeysFacts.BasicProperties.F.eq_dec key a). intuition. case_InA. destruct n2. rewrite <- MKeys_elements_in_iff. eexists; rewrite MKeysProperties.filter_iff. split; eauto. case_InA; eauto. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. rewrite H6 in i1; intuition. rewrite <- H6 in i1; intuition. discriminate. unfold Proper, respectful; intros. destruct (MoreMKeysFacts.BasicProperties.F.eq_dec x0 a); destruct (MoreMKeysFacts.BasicProperties.F.eq_dec y a); try reflexivity. rewrite H5 in e; intuition. rewrite <- H5 in e; intuition. repeat case_InA; try reflexivity. rewrite H5 in i0; intuition. rewrite <- H5 in i0; intuition. reflexivity. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite H3 in i0; intuition. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite <- H3 in i0; intuition. * unfold InvertedIndex_RepInv in containerCorrect; intuition. destruct H. eexists (NumValues container :: x); split; simpl; eauto. rewrite MKeysProperties.update_mapsto_iff; right. rewrite MKeysProperties.update_mapsto_iff; split. left. rewrite MoreMKeysFacts.BasicFacts.map_mapsto_iff; eexists; split; eauto. rewrite MKeysProperties.filter_iff. split; eauto. case_InA; eauto. unfold Proper, respectful; intros. repeat case_InA; eauto. rewrite H2 in i; intuition. rewrite <- H2 in i; intuition. unfold not; intros. apply n. eapply filter_InA; eauto with typeclass_instances. unfold Proper, respectful; intros. repeat case_InA; eauto. rewrite H5 in i; intuition. rewrite <- H5 in i; intuition. split; eauto. find_if_inside; try reflexivity. destruct H2; rewrite FMap_fold_add_MapsTo_In in H2. intuition. intro H'; apply MKeys_elements_in_iff in H'; destruct H'; eapply MKeys.empty_1; eauto. + unfold InvertedIndex_RepInv in containerCorrect; intuition. destruct (H4 _ _ H2 _ H0); intuition. destruct (InA_dec E.eq_dec key (projection item)). * eexists (NumValues container :: x); split; simpl; eauto. rewrite MKeysProperties.update_mapsto_iff; right. rewrite MKeysProperties.update_mapsto_iff; split. left. rewrite MoreMKeysFacts.BasicFacts.map_mapsto_iff; eexists; split; eauto. rewrite MKeysProperties.filter_iff. split; eauto. case_InA; eauto. unfold Proper, respectful; intros. repeat case_InA; eauto. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite H3 in i0; intuition. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite <- H3 in i0; intuition. unfold not; intros. destruct H3; rewrite FMap_fold_add_MapsTo_In in H3. intuition. apply filter_InA in H8; intuition. case_InA; try discriminate. apply n. apply MKeys_elements_in_iff. eexists; apply MKeysProperties.filter_iff. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. rewrite H8 in i0; intuition. rewrite <- H8 in i0; intuition. split; eauto. case_InA; eauto. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite H3 in i0; intuition. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite <- H3 in i0; intuition. intro H'; apply MKeys_elements_in_iff in H'; destruct H'; eapply MKeys.empty_1; eauto. * eexists x; split; simpl; eauto. rewrite MKeysProperties.update_mapsto_iff; right. rewrite MKeysProperties.update_mapsto_iff; split. right; split. apply MKeysProperties.filter_iff. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite H3 in i; intuition. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite <- H3 in i; intuition. split; eauto. case_InA; intuition. intro H3; destruct H3; rewrite MoreMKeysFacts.BasicFacts.map_mapsto_iff in H3. destruct H3; intuition; subst. rewrite MKeysProperties.filter_iff in H9; intuition. case_InA; intuition. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite H3 in i; intuition. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite <- H3 in i; intuition. intro; apply n. destruct H3; apply FMap_fold_add_MapsTo_In in H3; intuition. apply filter_InA in H8; intuition. unfold Proper, respectful; intros. repeat case_InA; try reflexivity. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite H3 in i; intuition. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite <- H3 in i; intuition. let H8 := match goal with H8 : InA _ _ _ |- _ => constr:(H8) end in apply MKeys_elements_in_iff in H8; destruct H8; eapply MKeys.empty_1; eauto. - inversion H; subst. unfold InvertedIndex_RepInv in *; intro H'; destruct H' as [x H']; rewrite add_mapsto_iff in H'; intuition. eapply (H3 (S (NumValues container))); eauto. eexists; eauto. unfold InvertedIndex_RepInv in *; intro H'; destruct H' as [x H']; rewrite add_mapsto_iff in H'; intuition. eapply (H4 (S m)); unfold MValues.In in *; eauto. omega. Unshelve. exact x0. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.Peano_dec Coq.Structures.OrdersEx Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListInclusion