proposition: Lemma bdeletePlus_correct_DB_snd db_schema qs index bag_plus : forall (store: BagTypePlus bag_plus), EnsembleBagEquivalence bag_plus (GetUnConstrRelation qs index) store -> forall (DeletedRawTuples : Ensemble RawTuple) (DT_Dec : DecideableEnsemble DeletedRawTuples) search_term, ExtensionalEq (@DecideableEnsembles.dec _ _ DT_Dec) (bfind_matcher (Bag := BagPlus bag_plus) search_term) -> EnsembleBagEquivalence bag_plus (GetUnConstrRelation (@UpdateUnConstrRelation db_schema qs index (EnsembleDelete (GetUnConstrRelation qs index) DeletedRawTuples)) index) (snd (bdelete store search_term)).
proof: Proof. intros; unfold ExtensionalEq, EnsembleBagEquivalence in *. unfold EnsembleBagEquivalence. repeat rewrite get_update_unconstr_eq; simpl; intros. split; [ | eapply bdelete_RepInv; intuition ]. simpl in *; unfold EnsembleListEquivalence, EnsembleIndexedListEquivalence, UnConstrFreshIdx, EnsembleDelete, Complement in *; intuition; destruct_ex; intuition; intros. exists x; intros; eapply H; destruct H1; unfold List.In in *; eauto. unfold UnIndexedEnsembleListEquivalence, EnsembleListEquivalence in *. generalize (bdelete_correct store search_term H2); destruct_ex; intuition. rewrite partition_filter_neq in H1. unfold BagPlusProofAsBag in *; simpl in *; rewrite <- H4 in H1. clear H6 H H2 H4. remember (GetUnConstrRelation qs index) as u. generalize DeletedRawTuples DT_Dec x0 u H1 H0 H3 H7; clear. induction (benumerate (snd (bdelete store search_term))); intros. - eexists []; simpl; intuition. + destruct H; destruct H2; unfold In in *. apply H3 in H. apply Permutation_nil in H1. apply dec_decides_P; rewrite H0. revert H1 H; clear; induction x0; simpl; eauto. case_eq (bfind_matcher (Bag := BagPlus bag_plus) search_term (indexedElement a)); simpl; intros. intuition; subst; eauto. discriminate. + constructor. - assert (exists a', List.In a' x0 /\ indexedElement a' = a /\ (bfind_matcher (Bag := BagPlus bag_plus) search_term (indexedElement a') = false)). generalize (@Permutation_in _ _ _ a H1 (or_introl (refl_equal _))). rewrite ListFacts.filter_map; clear; induction x0; simpl; intuition. revert H; case_eq (bfind_matcher (Bag := BagPlus bag_plus) search_term (indexedElement a0)); simpl; intros; eauto. apply IHx0 in H0; destruct_ex; intuition eauto. subst; intuition eauto. destruct_ex; intuition eauto. destruct_ex. assert (exists x0', Permutation x0 (x :: x0') /\ ~ List.In x x0'). { intuition; subst. repeat rewrite filter_map; generalize x H2 H7; clear; induction x0; intros; simpl in *|-; intuition; subst; eauto. inversion H7; subst; exists x0; intuition. apply H1; apply in_map_iff; eexists; eauto. inversion H7; subst. destruct (IHx0 _ H H3); intuition; eexists (a :: x1). rewrite H1; intuition. constructor. simpl in H0; intuition; subst; eauto. apply H2; apply in_map_iff; eexists; eauto. } destruct_ex; intuition; subst. rewrite ListFacts.filter_map in H1; rewrite H in H1; simpl in *. rewrite H8 in *; simpl in *. destruct (IHl DeletedRawTuples DT_Dec x1 (fun tup => Ensembles.In _ u tup /\ tup <> x)); eauto; clear IHl. + rewrite ListFacts.filter_map; eapply Permutation_cons_inv; eauto. + intuition; intros. destruct H2; apply H3 in H2. eapply Permutation_in in H; eauto. simpl in *; intuition. constructor. eapply H3. symmetry in H; eapply Permutation_in; eauto. simpl; eauto. intros; subst; simpl; congruence. + assert (NoDup (map elementIndex (x :: x1))). eapply NoDup_Permutation_rewrite. eapply Permutation_map; eauto. eauto. inversion H2; subst; eauto. + eexists (x :: x2); simpl; intuition. * rewrite H5; auto. * unfold In in H9; inversion H9; subst; unfold In in *. apply H3 in H11; pose proof (Permutation_in _ H H11). simpl in H5; intuition. right; apply Permutation_cons_inv in H1. eapply H2; econstructor; unfold In; intuition. apply H3 in H11; eauto. subst; eauto. * subst; unfold In in *. constructor; unfold In. apply H3. eapply Permutation_in; eauto. rewrite <- H0 in H8; intros; apply dec_decides_P in H5; congruence. * unfold In; constructor. apply H2 in H11; inversion H11; subst; unfold In in *; intuition. unfold In in *. intros; apply dec_decides_P in H9; subst. apply Permutation_cons_inv in H1. assert (List.In (indexedElement x3) (map indexedElement x2)) as in_x2' by (rewrite in_map_iff; eauto); pose proof (Permutation_in (indexedElement x3) H1 in_x2'). rewrite in_map_iff in H5; destruct_ex; intuition. rewrite filter_In in H13; intuition; subst. rewrite <- H0, H12, H9 in H14; discriminate. * constructor; eauto. intro In_x; subst; apply Permutation_cons_inv in H1. pose proof (permutation_map_base _ H1 _ (refl_equal _)); destruct_ex; intuition. rewrite in_map_iff in *; destruct_ex; intuition. apply H2 in H13; inversion H13; subst; unfold In in *; intuition. apply H3 in H15. pose proof (Permutation_in _ H H15); simpl in *; intuition. assert (~ List.In (elementIndex x) (map elementIndex x1)). { eapply Permutation_map with (f := elementIndex) in H. pose proof (NoDup_Permutation_rewrite _ _ H H7). simpl in *; inversion H5; subst; eauto. } apply H5; rewrite in_map_iff; eexists; split; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.TreeBags Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Coq.Lists.List Coq.Program.Program Fiat.Common.ilist Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.NArith.BinNat Coq.ZArith.ZArith_dec Coq.Arith.Arith Coq.FSets.FMapAVL Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.ilist2 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements Fiat.QueryStructure.Implementation.Operations.List.ListQueryRefinements