proposition: Lemma refine_MaxElements_map {A B} : forall (f : A -> B) (c : Comp (list A)) (op : B -> B -> Prop), refine (MaxElements op (l <- c; ret (map f l))) (l <- MaxElements (fun a a' => op (f a) (f a')) c; ret (map f l)).
proof: Proof. Local Transparent MaxElements. intros; unfold MaxElements; simplify with monad laws. rewrite refineEquiv_bind_bind; f_equiv; intro. cut (forall a'', refine {b : bool | decides b (UpperBound op (map f a) (f a''))} {b : bool | decides b (UpperBound (fun a0 a' : A => op (f a0) (f a')) a a'')}). - generalize (UpperBound op (map f a)). generalize (UpperBound (fun a0 a' : A => op (f a0) (f a')) a); intros. induction a; simpl. + rewrite refineEquiv_bind_unit; reflexivity. + repeat setoid_rewrite refineEquiv_bind_bind. rewrite IHa; simplify with monad laws. f_equiv; intro. setoid_rewrite H. f_equiv; intro. find_if_inside; rewrite refineEquiv_bind_unit; reflexivity. - intros. apply refineEquiv_pick_pick; intros. apply decide_eq_iff_iff_morphism; eauto. unfold UpperBound; split; intros; induction a; simpl in *; intuition; subst; eauto. Local Opaque MaxElements. 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