proposition: Lemma refine_Singleton_Set : forall (r_n : UnConstrQueryStructure DnsSchema) q bound a, For (UnConstrQuery_In r_n Fin.F1 (fun r : RawTuple => Where (RDataTypeToRRecordType r!sRDATA = CNAME /\ GetAttributeRaw r Fin.F1 = bound) Return r )) ↝ [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. unfold refine; intros. destruct (q == CNAME); simpl in *; computes_to_inv; subst. - computes_to_econstructor; split; intros. discriminate. intuition. - unfold SingletonSet. computes_to_econstructor; split; intros. + pose proof (@For_UnConstrQuery_In_Where_Prop DnsSchema Fin.F1 r_n _ _ _ H); inversion H1; subst; eauto. injection H0; intro; subst. intuition. left. destruct b as [? [? [? [? ?] ] ] ]; simpl in *. unfold Tuple_DecomposeRawQueryStructure_inj'; simpl. unfold icons2, ilist2_hd, ilist2_tl; simpl; repeat f_equal. unfold SumType.inj_SumType; simpl. unfold CNAME_Record2RRecord; simpl. unfold VariantResourceRecord2RRecord; simpl. unfold icons2; simpl. destruct prim_snd; destruct (@inil2 Type); reflexivity. + f_equal. intuition. destruct b as [? [? [? [? ?] ] ] ]; simpl in *. unfold Tuple_DecomposeRawQueryStructure_inj' in *; simpl in *. unfold icons2, ilist2_hd, ilist2_tl in *; simpl in *; unfold SumType.inj_SumType in *; simpl in *. unfold CNAME_Record2RRecord in *; simpl in *. unfold VariantResourceRecord2RRecord in *; simpl in *. unfold icons2 in *; simpl in *. destruct v0 as [? [? [? [? ?] ] ] ]; simpl in *. injections; simpl. destruct prim_snd; destruct (@inil2 Type); reflexivity. 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