proposition: Lemma refine_subcheck_to_filter {heading} : forall (R : Ensemble (@IndexedTuple heading)) (P : Ensemble Tuple) (P_dec : DecideableEnsemble P) (l : list Tuple), For (QueryResultComp R (fun tup => Where (P tup) (Return tup))) ↝ l -> forall (P' : Ensemble Tuple) (P'_dec : DecideableEnsemble P'), refine (For (QueryResultComp R (fun tup => Where (P tup /\ P' tup) (Return tup)))) (ret (filter DecideableEnsembles.dec l)).
proof: Proof. Local Transparent Query_For QueryResultComp. unfold Query_For, QueryResultComp, Query_Return; intros; computes_to_inv. refine pick val _; eauto. simplify with monad laws. unfold refine; intros; computes_to_inv; computes_to_econstructor. instantiate (1 := (filter (@dec _ _ P'_dec) v)). - clear H0 H H' v1; generalize dependent v; induction v0. + simpl; intros; computes_to_inv; subst; reflexivity. + simpl; intros; computes_to_inv; subst; apply IHv0 in H'0'; clear IHv0. destruct (@dec _ P' P'_dec a) eqn: dec_a; unfold Query_Where in *; destruct H'0. * pose proof dec_a as dec_a'; rewrite dec_decides_P in dec_a. repeat computes_to_inv; repeat computes_to_econstructor. intuition eauto. eauto. apply eq_ret_compute; destruct (@dec _ P P_dec a) eqn: dec__a. rewrite dec_decides_P in dec__a; apply H in dec__a; computes_to_inv; subst; simpl; rewrite dec_a'; reflexivity. apply Decides_false in dec__a; apply H0 in dec__a; subst; reflexivity. * pose proof dec_a as dec_a'; apply Decides_false in dec_a. repeat computes_to_inv; repeat computes_to_econstructor. intuition eauto. eauto. apply eq_ret_compute; destruct (@dec _ P P_dec a) eqn: dec__a. rewrite dec_decides_P in dec__a; apply H in dec__a; computes_to_inv; subst; simpl; rewrite dec_a'; reflexivity. apply Decides_false in dec__a; apply H0 in dec__a; subst; reflexivity. - refine pick val _; auto; subst. apply List.ListMorphisms.filter_permutation_morphism; [ reflexivity | assumption ]. 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