proposition: Lemma refine_MaxElements_For {A} : forall (op : A -> A -> Prop) ens, refine (MaxElements op For ens) (l <- MaxElements op ens; {l' | Permutation l l'}).
proof: Proof. unfold MaxElements; intros. rewrite refine_For. autorewrite with monad laws. f_equiv; intro. etransitivity. apply refine_under_bind; intros. eapply refine_ListComprehension_Equiv. computes_to_inv; subst. split; intros. symmetry in H; eapply UpperBound_Permutation; eauto. simpl in H0; eapply UpperBound_Permutation; eauto. simpl. remember a. setoid_rewrite Heql at 1; rewrite Heql at 1; clear Heql. intros ? ?; computes_to_inv; subst. revert l v v0 H H'; induction a; simpl; intros; computes_to_inv; subst. - repeat computes_to_econstructor; eauto. apply Permutation_nil in H'; subst; simpl; eauto. - destruct v2; simpl in *; computes_to_inv; subst. + pose proof (PermutationFacts.PermutationConsSplit _ _ _ H'); destruct_ex; subst. eapply (IHa _ (x ++ x0)) in H. computes_to_inv. apply build_FilteredList_app in H'1; destruct_ex; intuition; subst. refine pick val (x1 ++ (a :: x2)). apply refine_bind_unit. apply app_build_FilteredList; eauto. simpl. computes_to_econstructor; eauto. refine pick val true. computes_to_econstructor; simpl; eauto. simpl; eauto. simpl; eauto. rewrite H, Permutation_middle; reflexivity. rewrite <- Permutation_middle in H'. eapply Permutation_cons_inv; eauto. + eapply IHa in H'; eauto. computes_to_inv. refine pick val (a :: v1); eauto. computes_to_econstructor. computes_to_econstructor. simpl; computes_to_econstructor; eauto. refine pick val false; simpl; eauto. repeat computes_to_econstructor. 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