proposition: Lemma refine_Process_Query : forall (r_o : QueryStructure DnsSchema) (r_n : UnConstrQueryStructure DnsSchema) bound, DropQSConstraints_AbsR r_o r_n -> refine (For (UnConstrQuery_In r_n Fin.F1 (fun r : RawTuple => Where (GetAttributeRaw r Fin.F1 = bound) Return r ))) (results <- For (UnConstrQuery_In r_n Fin.F1 (fun r : RawTuple => Where ((RDataTypeToRRecordType r!sRDATA) = CNAME /\ GetAttributeRaw r Fin.F1 = bound) Return r )); (Ifopt (hd_error results) as record Then (ret [record]) Else For (UnConstrQuery_In r_n Fin.F1 (fun r : RawTuple => Where ((RDataTypeToRRecordType r!sRDATA) <> CNAME /\ GetAttributeRaw r Fin.F1 = bound) Return r )))).
proof: Proof. unfold refine; intros. computes_to_inv. destruct v0; simpl in *; eauto. - unfold Query_For in *. computes_to_inv. computes_to_econstructor. eapply refine_Split_Where with (R := (GetUnConstrRelation r_n Fin.F1)) (P := fun r : resourceRecord => GetAttributeRaw r Fin.F1 = bound). auto with typeclass_instances. 2: computes_to_econstructor; try apply H0. 2: computes_to_econstructor; try apply H0'. auto with typeclass_instances. computes_to_econstructor; eauto. symmetry in H0'0; apply Permutation_nil in H0'0; subst. simpl; computes_to_econstructor; eauto. - computes_to_inv; subst. Local Transparent Query_For. Local Transparent QueryResultComp. unfold UnConstrQuery_In, Query_For, QueryResultComp in *; computes_to_inv. apply refineEquiv_bind_bind. pose proof (DropQSConstraints_AbsR_SatisfiesTupleConstraints H Fin.F1); eauto. Admitted. Lemma is_empty_app {A} : forall l1 l2 : list A, is_empty (l1 ++ l2) = is_empty l1 && is_empty l2. Proof. induction l1; simpl; 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