proposition: Lemma refine_filter_Tuple_Decompose_inj' : forall ns_results' : list NS_Record, refine {ns_results : list NS_Record | forall x : NS_Record, List.In x ns_results <-> List.In x (A := resourceRecord) (map (Tuple_DecomposeRawQueryStructure_inj' (qs_schema := DnsSchema) Fin.F1 (Fin.FS (Fin.FS (Fin.FS Fin.F1))) ResourceRecordTypeTypes (SumType.inj_SumType ResourceRecordTypeTypes) NS) ns_results')} (ret ns_results').
proof: Proof. intros; refine pick val _; eauto. reflexivity. induction ns_results'; simpl; split; intros; intuition eauto. subst. - left; destruct x as [? [? [? [? [ ] ] ] ] ]; reflexivity. - right; apply IHns_results'; intuition eauto. - left. unfold NS_Record2RRecord, VariantResourceRecord2RRecord, Tuple_DecomposeRawQueryStructure_inj' in H0. destruct x as [? [? [? [? [ ] ] ] ] ]; destruct a as [? [? [? [? [ ] ] ] ] ]; simpl in *. unfold GetAttribute, GetAttributeRaw in *; simpl in *. unfold icons2, ilist2_tl, ilist2_hd in H0; simpl in *. injection H0; intros; subst. reflexivity. - right; apply IHns_results'; intuition 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