proposition: Lemma DeletedTuplesFor {qsSchema} : forall qs Ridx P, DecideableEnsemble P -> refine {x | @QSDeletedTuples qsSchema qs Ridx P x} (For (UnConstrQuery_In qs Ridx (fun tup => Where (P tup) Return tup))).
proof: Proof. intros qs Ridx P P_dec v Comp_v; rewrite DeletedTuplesIntersection by auto. computes_to_constructor. unfold UnIndexedEnsembleListEquivalence. unfold Query_For in *. computes_to_inv. destruct Comp_v as [l [Perm_l_v Comp_v] ]. unfold UnConstrQuery_In, QueryResultComp in *; computes_to_inv. remember (GetUnConstrRelation qs Ridx); clear Heqi. revert P_dec i v v0 Perm_l_v Comp_v Comp_v'; clear; induction l; simpl; intros. - apply Return_inv in Comp_v; subst. eexists nil; simpl; split; eauto. rewrite Permutation_nil by eauto; reflexivity. + unfold EnsembleListEquivalence in *; intuition. * destruct H; intuition. apply Pick_inv in Perm_l_v; inversion Perm_l_v. unfold In in *; intuition; subst. apply H1 in H. eapply (@FlattenCompList.flatten_CompList_nil _ P x0); eauto. destruct x0; simpl in *; try discriminate; computes_to_econstructor. * constructor. - apply Pick_inv in Perm_l_v. unfold UnConstrRelation in i. destruct Perm_l_v as [ [ | [a' x'] ] [x_eq [equiv_u_x' NoDup_x'] ] ]. destruct l; simpl in *; try discriminate. unfold In in Comp_v; pose (Bind_inv Comp_v); destruct_ex; intuition; subst; computes_to_inv; subst. simpl in x_eq; injections. case_eq (@DecideableEnsembles.dec _ P P_dec a); intros. + apply Pick_inv in H0; intuition. apply dec_decides_P in H2. apply H3 in H2. apply Return_inv in H2; simpl in *; subst; simpl in *. pose proof (PermutationConsSplit _ _ _ Comp_v'); destruct_ex; subst. unfold UnIndexedEnsembleListEquivalence in *. destruct (H (fun x => i x /\ x <> {|indexedElement := a; elementIndex := a' |}) (app x x0) v1); intuition eauto. apply PickComputes. computes_to_inv; injections. eexists _; intuition eauto. unfold In in *; intuition. rewrite equiv_u_x' in H2; destruct H2; subst; eauto; congruence. unfold In; intuition. apply equiv_u_x'; simpl; intuition. inversion NoDup_x'; subst; eauto. apply H7; apply in_map_iff; eexists; split; eauto; simpl; eauto. inversion NoDup_x'; subst; eauto. eapply Permutation_cons_inv; rewrite Permutation_middle; eassumption. * symmetry in H2; pose proof (app_map_inv _ _ _ _ H2); destruct_ex; intuition; subst. eexists (app x2 ({|indexedElement := a; elementIndex := a' |} :: x3)); simpl; rewrite map_app. { simpl; intuition; computes_to_inv; injections. - destruct H5; unfold In in *; apply equiv_u_x' in H5; simpl in *; intuition. apply in_or_app; simpl; eauto. assert (i x) as u_x by (apply equiv_u_x'; eauto). assert (List.In x (x2 ++ x3)) as In_x by (apply H0; constructor; unfold In; intuition; subst; inversion NoDup_x'; subst; eapply H10; apply in_map_iff; eexists; split; cbv beta; simpl; eauto; reflexivity). apply in_or_app; simpl; apply in_app_or in In_x; intuition. - unfold In. assert (List.In x (x2 ++ x3) \/ x = {|indexedElement := a; elementIndex := a' |}) as In_x0 by (apply in_app_or in H5; simpl in H5; intuition). intuition. + apply H0 in H7; destruct H7; unfold In in *; intuition. constructor; eauto. + subst; constructor; eauto. apply equiv_u_x'; simpl; eauto. case_eq (@DecideableEnsembles.dec _ P P_dec a); intros. apply dec_decides_P; eauto. assert (~ P a) as H'' by (unfold not; intros H'; apply dec_decides_P in H'; congruence); apply H4 in H''; discriminate. - rewrite map_app; apply NoDup_app_swap; simpl; constructor; eauto. inversion NoDup_x'; subst; unfold not; intros; apply H8. rewrite <- map_app in H5; apply in_map_iff in H5; destruct_ex; intuition. assert (List.In x (x2 ++ x3)) as In_a by (apply in_or_app; apply in_app_or in H10; intuition). apply H0 in In_a; destruct In_a; unfold In in *; intuition. apply equiv_u_x' in H12; simpl in *; intuition. destruct x; simpl in *; subst. apply in_map_iff; eexists; split; eauto; simpl; eauto. apply NoDup_app_swap; rewrite <- map_app; eauto. } + unfold Query_Where, Query_Return in H0; computes_to_inv; intuition. assert (~ P a) as H'' by (unfold not; intros H'; apply dec_decides_P in H'; congruence ). apply H4 in H''; subst; simpl in *; subst. destruct (H (fun x => i x /\ x <> {|indexedElement := a; elementIndex := a' |}) v v1); intuition eauto. * computes_to_econstructor. eexists; intuition; eauto. unfold In in *; intuition. apply equiv_u_x' in H5; destruct H5; subst; eauto. congruence. unfold In; intuition. unfold In; intuition. subst. apply equiv_u_x'; simpl; intuition. inversion NoDup_x'; subst; eauto. apply H8; apply in_map_iff; eexists; split; eauto; simpl; eauto. inversion NoDup_x'; subst; eauto. * unfold In. eexists; split; eauto. unfold UnIndexedEnsembleListEquivalence in *; intuition. destruct H6; intuition. eapply H0; constructor; unfold In in *; subst; intuition. subst; apply_in_hyp dec_decides_P; simpl in *; congruence. constructor; apply H0 in H6; destruct H6; unfold In in *; intuition. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.List.ListFacts Fiat.Computation Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.Schema Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Specification.Operations.Mutate Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements Fiat.Common.IterateBoundedIndex Fiat.Common.DecideableEnsembles Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.MutateRefinements Fiat.Common.Ensembles.EnsembleListEquivalence