proposition: Lemma refine_Split_Where {heading} : forall (R : Ensemble (@IndexedRawTuple heading)) P Q (P_dec : DecideableEnsemble P) (Q_dec : DecideableEnsemble Q), refine (QueryResultComp R (fun r : RawTuple => Where (P r) Return r )) (results <- QueryResultComp R (fun r : RawTuple => Where (Q r /\ P r) Return r ); results' <- QueryResultComp R (fun r : RawTuple => Where (~Q r /\ P r) Return r ); {results'' | Permutation (results ++ results') results''}).
proof: Proof. unfold QueryResultComp; intros. autorewrite with monad laws. intros ? ?; computes_to_inv. eapply refine_flatten_CompList_filter in H'; eauto. eapply refine_flatten_CompList_filter in H'''; eauto. destruct_ex; intuition eauto; subst. apply Permutation_flatten_CompList with (l' := v2) in H2; destruct_ex; intuition. assert (exists v', Permutation v' v2 /\ FlattenCompList.flatten_CompList (map (fun r : RawTuple => Where (P r) Return r ) v') ↝ v). { generalize dependent x1. revert P_dec. generalize dependent x; clear. revert v x0. induction v2; simpl; intros; computes_to_inv; subst. - eexists nil; simpl. symmetry in H3; apply Permutation_nil in H3; subst; simpl in *. apply Permutation_nil in H''''; subst; split; eauto. - unfold Query_Where, Query_Return in H1, H2; computes_to_inv; intuition. destruct (dec (DecideableEnsemble := P_dec) a) eqn: ?. + rewrite dec_decides_P in Heqb. pose proof (H Heqb); pose proof (H1 Heqb); computes_to_inv; subst. symmetry in H3. pose proof (PermutationFacts.PermutationConsSplit _ _ _ H3); destruct_ex; intuition; subst; eauto. simpl in H''''. rewrite filter_app in H''''; simpl in H''''. destruct (dec (DecideableEnsemble := Q_dec) a) eqn: ?; simpl in H''''. * rewrite dec_decides_P in Heqb0; simpl in *. assert (exists v' v'', v = v' ++ a :: v''). { rewrite <- Permutation_middle in H''''. simpl in H''''. apply PermutationFacts.PermutationConsSplit in H''''. eauto. } destruct_ex; subst. eapply (IHv2 (x0 ++ x2)) in H2'. 2: apply H1'. 3: eassumption. destruct_ex; intuition eauto. eapply flatten_Complist_app in H6; destruct_ex. intuition. symmetry in H8; apply app_map_inv in H8; destruct_ex; intuition. subst. eexists (x6 ++ (a :: x7)); intuition. rewrite <- H2. rewrite <- Permutation_cons_app; reflexivity. rewrite map_app. eapply FlattenCompList.flatten_CompList_app; simpl; eauto. repeat computes_to_econstructor; eauto. revert P_dec; clear; induction x3; simpl; intros; intuition. unfold Query_Where, Query_Return in H1; subst; computes_to_inv; intuition. destruct (dec (DecideableEnsemble := P_dec) a) eqn: ?. rewrite dec_decides_P in Heqb; apply H1 in Heqb; computes_to_inv; subst; eauto. apply Decides_false in Heqb. pose proof (H2 Heqb); subst; eauto. eauto. apply Permutation_cons_inv with (a := a). rewrite Permutation_middle with (l1 := x0), <- H''''. rewrite <- Permutation_middle with (l1 := filter dec x); simpl. econstructor. rewrite <- filter_app. reflexivity. apply Permutation_cons_inv with (a := a); eauto. rewrite H3. apply Permutation_middle. * assert (exists v' v'', v = v' ++ a :: v''). { rewrite <- Permutation_middle in H''''. simpl in H''''. apply PermutationFacts.PermutationConsSplit in H''''. eauto. } destruct_ex; subst. eapply (IHv2 (x0 ++ x2)) in H2'. 2: apply H1'. 3: eassumption. destruct_ex; intuition eauto. eapply flatten_Complist_app in H6; destruct_ex. intuition. symmetry in H8; apply app_map_inv in H8; destruct_ex; intuition. subst. eexists (x6 ++ (a :: x7)); intuition. rewrite <- H2. rewrite <- Permutation_cons_app; reflexivity. rewrite map_app. eapply FlattenCompList.flatten_CompList_app; simpl; eauto. repeat computes_to_econstructor; eauto. revert P_dec; clear; induction x3; simpl; intros; intuition. unfold Query_Where, Query_Return in H1; subst; computes_to_inv; intuition. destruct (dec (DecideableEnsemble := P_dec) a) eqn: ?. rewrite dec_decides_P in Heqb; apply H1 in Heqb; computes_to_inv; eauto. apply Decides_false in Heqb; apply H2 in Heqb; eauto. eauto. apply Permutation_cons_inv with (a := a). rewrite Permutation_middle with (l1 := x0), <- H''''. rewrite <- Permutation_middle; simpl. econstructor. rewrite <- filter_app. reflexivity. apply Permutation_cons_inv with (a := a); eauto. rewrite H3. apply Permutation_middle. + apply Decides_false in Heqb. pose proof (H0 Heqb); pose proof (H4 Heqb); computes_to_inv; subst. simpl in *; eapply IHv2 in H2'. 2: apply H1'. destruct_ex; intuition. exists (a :: x); split; eauto. simpl. repeat computes_to_econstructor; intuition. apply H6. simpl; computes_to_econstructor. eassumption. eassumption. eassumption. } destruct_ex; intuition. computes_to_econstructor; try eassumption. computes_to_econstructor. eapply Permutation_UnIndexedEnsembleListEquivalence; try symmetry; eauto. eapply Permutation_UnIndexedEnsembleListEquivalence'; eauto. Qed.
imports: Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector Coq.Lists.List Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Examples.DnsServer.DecomposeSumField Fiat.Computation.FoldComp Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema