proposition: Lemma refine_Process_Query_Imprecise_Match : forall (r_o : QueryStructure DnsSchema) (r_n : UnConstrQueryStructure DnsSchema) bound p BStringId2 BStringId7, DropQSConstraints_AbsR r_o r_n -> refine (a4 <- MaxElements (fun r r' : resourceRecord => prefix (GetAttributeRaw r Fin.F1) (GetAttributeRaw r' Fin.F1)) For (UnConstrQuery_In r_n Fin.F1 (fun r : RawTuple => Where (prefix (GetAttributeRaw r Fin.F1) bound /\ GetAttributeRaw r Fin.F1 <> bound) Return r )); a' <- {ns_results : list NS_Record | forall x : NS_Record, List.In x ns_results <-> List.In (A := resourceRecord) x a4}; If is_empty a4 Then ret (buildempty true BStringId2 p) Else (a5 <- foldComp (fun (a6 : list RawTuple) (a7 : NS_Record) => a5 <- For (UnConstrQuery_In r_n Fin.F1 (fun rRec : RawTuple => Where (GetAttributeRaw rRec Fin.F1 = GetAttributeRaw a7 (Fin.FS (Fin.FS (Fin.FS Fin.F1)))) Return rRec )); ret (a5 ++ a6)) nil a'; ret (add_additionals a5 (add_nses (map VariantResourceRecord2RRecord a') (buildempty true BStringId7 p))))) (a4 <- MaxElements (fun r r' : resourceRecord => prefix (GetAttributeRaw r Fin.F1) (GetAttributeRaw r' Fin.F1)) For (UnConstrQuery_In r_n Fin.F1 (fun r : RawTuple => Where (RDataTypeToRRecordType r!sRDATA = NS /\ prefix (GetAttributeRaw r Fin.F1) bound) Return r )); a' <- {ns_results : list NS_Record | forall x : NS_Record, List.In x ns_results <-> List.In x (A := resourceRecord) a4}; If is_empty a' Then ret (buildempty true BStringId2 p) Else (a5 <- foldComp (fun (a6 : list RawTuple) (a7 : NS_Record) => a5 <- For (UnConstrQuery_In r_n Fin.F1 (fun rRec : RawTuple => Where (GetAttributeRaw rRec Fin.F1 = GetAttributeRaw a7 (Fin.FS (Fin.FS (Fin.FS Fin.F1)))) Return rRec )); ret (a5 ++ a6)) nil a'; ret (add_additionals a5 (add_nses (map VariantResourceRecord2RRecord a') (buildempty true BStringId7 p))))).
proof: Proof. Admitted. Lemma refine_decides_forall_and {A} : forall (P Q : A -> Prop) (P' Q' : @IndexedElement A -> Prop) (R : @IndexedEnsemble A), (forall a, P (indexedElement a) <-> P' a) -> (forall a, Q (indexedElement a) <-> Q' a) -> refine {b | decides b (forall tup' : @IndexedElement A, R tup' -> Q' tup' /\ P' tup')} (b' <- {b | decides b (forall tup' : @IndexedElement A, R tup' -> Q' tup')}; If b' Then {b | decides b (forall tup' : @IndexedElement A, R tup' -> P' tup')} Else (ret false)). Proof. unfold refine; intros; computes_to_inv; subst. computes_to_econstructor. find_if_inside; simpl in *; computes_to_inv; subst; simpl. - destruct v; simpl in *; intros. + intuition eauto. + intro; eapply H1'; intros; eapply H2; eauto. - intro; apply H1; intros; eapply H2; 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.DnsOpt Fiat.Narcissus.Examples.DNS.DNSPacket Fiat.Examples.DnsServer.DecomposeSumField Fiat.Computation.FoldComp Fiat.Examples.DnsServer.AuthoritativeDNSSchema