proposition: Lemma bdelete_correct_DB_snd db_schema qs index (bag_plus : BagPlusProof RawTuple) : forall (store: BagTypePlus bag_plus), GetUnConstrRelation qs index ≃ store -> forall (DeletedRawTuples : Ensemble RawTuple) (DT_Dec : DecideableEnsemble DeletedRawTuples), EnsembleIndexedListEquivalence (GetUnConstrRelation (@UpdateUnConstrRelation db_schema qs index (EnsembleDelete (GetUnConstrRelation qs index) DeletedRawTuples)) index) (snd (List.partition (@DecideableEnsembles.dec _ _ DT_Dec) (benumerate store))).
proof: Proof. simpl; unfold EnsembleDelete, EnsembleBagEquivalence, Ensembles.In, Complement; simpl; unfold EnsembleIndexedListEquivalence, UnIndexedEnsembleListEquivalence, EnsembleListEquivalence; intros; intuition; destruct_ex; intuition; subst. repeat setoid_rewrite get_update_unconstr_eq; simpl; intros. exists x0. unfold UnConstrFreshIdx in *; intros; apply H; destruct H3; eauto. exists (snd (partition (@DecideableEnsembles.dec IndexedRawTuple (fun t => DeletedRawTuples (indexedElement t)) _ ) x)); intuition. - unfold BagPlusProofAsBag; rewrite <- H2. repeat rewrite partition_filter_neq. clear; induction x; simpl; eauto. unfold indexedRawTuple in *; find_if_inside; simpl; eauto; rewrite <- IHx; reflexivity. - rewrite get_update_unconstr_eq in H3. destruct H3; unfold In in *. apply H0 in H3; eapply In_partition in H3; intuition; try apply H6. apply In_partition_matched in H6; apply dec_decides_P in H6; exfalso; eauto. - rewrite get_update_unconstr_eq; constructor. eapply H0; eapply In_partition; eauto. unfold In; intros. apply In_partition_unmatched in H3. simpl in *; apply dec_decides_P in H5. unfold indexedRawTuple, GetNRelSchema in *; rewrite H3 in H5; congruence. - revert H4; clear; induction x; simpl; eauto. intros; inversion H4; subst. case_eq (partition (fun x0 => @DecideableEnsembles.dec IndexedRawTuple (fun t => DeletedRawTuples (indexedElement t)) _ x0) x); intros; simpl in *; rewrite H. rewrite H in IHx; apply IHx in H2; case_eq (@DecideableEnsembles.dec IndexedRawTuple (fun t => DeletedRawTuples (indexedElement t)) _ a); intros; simpl in *; rewrite H0; simpl; eauto. constructor; eauto. unfold not; intros; apply H1. generalize l l0 H H3; clear; induction x; simpl; intros. + injections; simpl in *; eauto. + case_eq (partition (fun x0 : IndexedRawTuple => DecideableEnsembles.dec (indexedRawTuple x0)) x). intros; rewrite H0 in H; find_if_inside; injections. eauto. simpl in H3; intuition. 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