proposition: Lemma refine_Singleton_Set'' : forall (r_o : QueryStructure DnsSchema) (r_n : UnConstrQueryStructure DnsSchema) q bound l a, For (UnConstrQuery_In r_n Fin.F1 (fun r : RawTuple => Where (RDataTypeToRRecordType r!sRDATA = CNAME /\ GetAttributeRaw r Fin.F1 = bound) Return r )) ↝ l -> hd_error l = Some a -> refine (SingletonSet (fun b : CNAME_Record => List.In (A := resourceRecord) b [a] /\ q <> QType_inj CNAME)) (If q == (QType_inj CNAME) Then (ret None) Else (c_record <- {c_record : CNAME_Record | a = @Tuple_DecomposeRawQueryStructure_inj' _ DnsSchema Fin.F1 (Fin.FS (Fin.FS (Fin.FS (Fin.F1)))) _ (SumType.inj_SumType ResourceRecordTypeTypes) CNAME c_record }; ret (Some c_record))).
proof: Proof. intros. destruct l as [ | ? [ | ?] ]; simpl in *; try discriminate. pose proof (@refine_Singleton_Set _ q _ _ H); eauto. - injection H0; intros; subst; simpl in H1; rewrite H1. reflexivity. - pose proof (@For_UnConstrQuery_In_Where_Prop DnsSchema Fin.F1 r_n _ _ _ H); inversion H1; subst; eauto. Admitted. Lemma refine_Singleton_Set' : forall (r_n : UnConstrQueryStructure DnsSchema) q bound l, For (UnConstrQuery_In r_n Fin.F1 (fun r : RawTuple => Where (RDataTypeToRRecordType r!sRDATA <> CNAME /\ GetAttributeRaw r Fin.F1 = bound) Return r )) ↝ l -> refine (SingletonSet (fun b : CNAME_Record => List.In (A := resourceRecord) b l /\ q <> QType_inj CNAME)) (ret None). Proof. Admitted. Lemma refine_If_Opt_Then_Else' : forall (A B : Type) (c : option A) (x y : A -> Comp B), (forall a, c = Some a -> refine (x a) (y a)) -> forall x0 y0 : Comp B, refine x0 y0 -> refine (Ifopt c as c' Then x c' Else x0) (Ifopt c as c' Then y c' Else y0). Proof. intros; destruct c; 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