proposition: Lemma refine_In_Where_Intersection heading : forall R P (P_dec : DecideableEnsemble P), refine (QueryResultComp (Intersection (@IndexedRawTuple heading) R (fun r => (P (indexedElement r)))) (fun r => Query_Return r)) (QueryResultComp R (fun r => Query_Where (P r) (Query_Return r))).
proof: Proof. unfold refine, In, QueryResultComp; intros * ? x H. repeat computes_to_inv. revert R x H H'. induction v; simpl in *; intros; computes_to_inv; subst. - repeat computes_to_econstructor. instantiate (1 := @nil RawTuple); simpl. inversion H; intuition; subst. econstructor; split; eauto. repeat split; intros; eauto. eapply H0; inversion H2; subst; eauto. eapply H0; eauto. eapply in_map with (f := indexedElement) in H2; rewrite H1 in H2; destruct H2. computes_to_econstructor. - inversion H; destruct x; simpl in *; intuition; try discriminate; injections. assert (UnIndexedEnsembleListEquivalence (fun t : IndexedRawTuple => elementIndex t <> elementIndex i /\ R t) (map indexedElement x)). { econstructor; intuition eauto. inversion H1; subst. apply H0 in H4; intuition. subst; intuition eauto. econstructor; intros; subst. inversion H3; subst. apply H6; eapply in_map_iff. eexists; split; eauto. eapply H0; eauto. inversion H3; subst; eauto. } pose proof (IHv _ _ H1 H''); clear IHv; computes_to_inv. inversion H'; subst. refine pick val (List.app v0 v). econstructor; intuition; eauto. rewrite map_app; eapply FlattenCompList.flatten_CompList_app; eauto. case_eq (dec (indexedElement i)); intros. apply dec_decides_P in H6; apply H4 in H6; inversion H6; subst. repeat computes_to_econstructor. eapply Decides_false in H6; apply H5 in H6; subst; simpl; computes_to_econstructor. inversion H2; subst; intuition. case_eq (dec (indexedElement i)); intros. + apply dec_decides_P in H8; pose proof (H4 H8) as H'''; inversion H'''; subst. econstructor 1. instantiate (1 := List.app [i] x0); simpl; intuition eauto. inversion H4; subst; apply H0 in H10; intuition. right; eapply H6; econstructor; unfold In; eauto. split; eauto; intros; subst. inversion H3; subst; intuition eauto. apply H15; eapply in_map_iff. eexists; eauto. eapply H0; eauto. subst. econstructor. eapply H0; eauto. unfold In; eauto. econstructor; unfold In in *; eauto. eapply H0; eauto. rewrite <- H6 in H10; inversion H10; subst; unfold In in *; intuition. eapply H0 in H13; eauto. rewrite <- H6 in H10; inversion H10; subst; unfold In in *; intuition. inversion H3; subst; econstructor; eauto. intro; rewrite in_map_iff in H4; destruct_ex; intuition eauto. apply H11; rewrite in_map_iff; destruct_ex; intuition eauto. eexists; intuition eauto. eapply H6 in H13; inversion H13; subst. unfold In in H13. inversion H13; subst. inversion H15; subst; intuition. + eapply Decides_false in H8; pose proof (H5 H8); subst; simpl. inversion H2; subst; intuition. econstructor 1. instantiate (1 := x1); intuition eauto. eapply H7. repeat econstructor; eauto. destruct H5; subst. apply H0 in H5; intuition. subst; intuition. inversion H3; subst. apply H17; apply in_map_iff; eexists; eauto. destruct H5; eauto. destruct H5; eauto. eapply H7 in H5; destruct H5; destruct H5. econstructor; eauto. Qed.
imports: Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Strings.String Coq.Lists.List Coq.Sorting.Permutation Coq.Bool.Bool Coq.Sets.Ensembles Coq.Logic.FunctionalExtensionality Fiat.ADTNotation Fiat.Common Fiat.Common.ilist2 Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure