proposition: Lemma MaxElementsUnConstrQuery_In {qs_schema} : forall idx f bound (r_o : UnConstrQueryStructure qs_schema), refine (MaxElements (fun r r' : RawTuple => prefix (f r) (f r')) For (UnConstrQuery_In r_o idx (fun r : RawTuple => Where (prefix (f r) bound) Return r ))) (results' <- For (UnConstrQuery_In r_o idx (fun r : RawTuple => Where (f r = bound) Return r )); If negb (is_empty results') Then ret results' Else (MaxElements (fun r r' => prefix (f r) (f r')) For (UnConstrQuery_In r_o idx (fun r : RawTuple => Where (prefix (f r) bound /\ (f r) <> bound) Return r ))) ).
proof: Proof. intros. pose proof (fun H H' H'' H''' => @refine_MaxElements _ _ _ prefix H H' H'' H''' bound (GetUnConstrRelation r_o idx) f). Local Transparent MaxElements. Local Transparent Query_For. Local Transparent UnConstrQuery_In. Local Transparent QueryResultComp. rewrite refine_MaxElements_For. rewrite H. simplify with monad laws. unfold Query_For, UnConstrQuery_In, QueryResultComp. rewrite !refineEquiv_bind_bind. f_equiv; intro. f_equiv; intro. intros ? ?; computes_to_inv. destruct a0. - apply Permutation_nil in H0; subst; simpl in *. unfold MaxElements in *. computes_to_inv; subst. symmetry in H0''0. pose proof (Permutation_filtered_List _ H0''0 _ H0''); destruct_ex; intuition. repeat computes_to_econstructor. eassumption. eassumption. eapply refine_ListComprehension_Equiv; eauto. split; intros; eauto using UpperBound_Permutation. symmetry in H0''0; eauto using UpperBound_Permutation. rewrite H2; reflexivity. - destruct v0; simpl in *. + symmetry in H0; apply Permutation_nil in H0; discriminate. + computes_to_inv; subst; computes_to_econstructor; eauto. - apply prefix_refl . - apply prefix_trans. - intro; apply DecideableEnsemble_bool. - apply prefix_antisym. 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