proposition: Lemma refine_MaxElements {A B} {eqB : Query_eq B } : forall (op : B -> B -> Prop) (op_refl : forall b, op b b) (op_trans : forall b b' b'', op b b' -> op b' b'' -> op b b'') (op_dec : forall b, DecideableEnsemble (fun b' => op b' b)) (op_irrefl : forall b b', op b b' -> op b' b -> b = b') (bound : B) (As : @IndexedEnsemble A) (f : A -> B), refine (MaxElements (fun a a' => op (f a) (f a')) (As' <- {As' : list A | UnIndexedEnsembleListEquivalence As As'}; FlattenCompList.flatten_CompList (map (fun a => Where (op (f a) bound) Return a) As'))) (As' <- (As' <- {As' : list A | UnIndexedEnsembleListEquivalence As As'}; FlattenCompList.flatten_CompList (map (fun a => Where ((f a) = bound) Return a) As')); If negb (is_empty As') Then ret As' Else (MaxElements (fun a a' => op (f a) (f a')) (As' <- {As' : list A | UnIndexedEnsembleListEquivalence As As'}; FlattenCompList.flatten_CompList (map (fun a => Where (op (f a) bound /\ (f a) <> bound) Return a) As')))).
proof: Proof. unfold MaxElements; intros; simplify with monad laws. setoid_rewrite refineEquiv_bind_bind. unfold refine; intros. computes_to_inv. destruct (is_empty v1) eqn: v1_eq; simpl in *; computes_to_inv; subst. - computes_to_econstructor; eauto. computes_to_econstructor; eauto. assert (forall a', List.In a' v3 -> f a' <> bound). { intros; eapply Permutation_in in H0; eauto using (Permutation_UnIndexedEnsembleListEquivalence' H'' H). clear H. generalize dependent v1; generalize dependent v0; clear; induction v0; simpl; intros; intuition; computes_to_inv; subst. + unfold Query_Where, Query_Return in H'; computes_to_inv; subst. intuition; computes_to_inv; subst. simpl in v1_eq; discriminate. + eapply H0; eauto. rewrite is_empty_app, andb_true_iff in v1_eq. intuition. } generalize v2 H'''0 H0; clear; induction v3; simpl; intros; computes_to_inv; subst; intuition eauto. computes_to_econstructor. eapply refine_Query_Where_Cond in H'''0; eauto. intuition eauto. computes_to_econstructor. eapply IHv3; eauto. eauto. - computes_to_econstructor; eauto. assert (exists v', computes_to (FlattenCompList.flatten_CompList (map (fun a : A => Where (op (f a) bound) Return a ) v0)) v'). { revert op_dec; clear; induction v0; simpl; intros; eauto. destruct IHv0; eauto. destruct (dec (DecideableEnsemble := op_dec bound) (f a)) eqn:?. rewrite dec_decides_P in Heqb. eexists; computes_to_econstructor. computes_to_econstructor; split; intros. computes_to_econstructor. intuition. computes_to_econstructor; eauto. eexists; computes_to_econstructor. computes_to_econstructor; split; intros. apply Decides_false in Heqb. intuition. reflexivity. computes_to_econstructor; eauto. } destruct_ex; computes_to_econstructor; eauto. eapply (@refine_FindUpperBound _ _ _ op_trans bound); eauto. intros. eapply flatten_CompList_Prop in H0; eauto. refine {| dec a := dec (f a) |}. intros; rewrite dec_decides_P; reflexivity. generalize dependent v; generalize dependent x; clear H. induction v0; simpl. + intros; computes_to_inv; subst; simpl in *; discriminate. + intros; computes_to_inv; subst; simpl; eauto. unfold Query_Where, Query_Return in H0, H'; computes_to_inv; subst. intuition; computes_to_inv; subst. destruct (A_eq_dec (f a) bound); subst. * specialize (H0 (eq_refl _)); computes_to_inv; subst. specialize (H (op_refl _)); computes_to_inv; subst. eexists; simpl; intuition eauto. * apply H2 in n; subst. simpl in v1_eq. destruct (IHv0 _ H0' _ H'' v1_eq); intuition. eexists; split; eauto. apply in_or_app; right; eauto. + generalize dependent v; generalize dependent x; clear H. induction v0; simpl. * intros; computes_to_inv; subst; simpl in *; discriminate. * intros; computes_to_inv; subst; simpl; eauto. unfold Query_Where, Query_Return in H0, H'; computes_to_inv; subst. intuition; computes_to_inv; subst. destruct (dec (DecideableEnsemble := op_dec bound) (f a)) eqn:?. rewrite dec_decides_P in Heqb; pose proof (H Heqb). computes_to_inv; subst; simpl. destruct (A_eq_dec (f a) bound); subst. pose proof (H0 (eq_refl _)); computes_to_inv; subst. destruct (is_empty v2) eqn: ?. apply (@BindComputes _ _ _ _ [ ]); eauto. { revert eqB op_dec op_irrefl Heqb0 H0' H''; clear; revert v4 v2; induction v0; simpl; intros; computes_to_inv; subst; simpl. computes_to_econstructor. unfold Query_Where, Query_Return in H0', H''; computes_to_inv; subst. intuition; computes_to_inv; subst. destruct (dec (DecideableEnsemble := op_dec (f a)) (f a0)) eqn: ?. - rewrite dec_decides_P in Heqb; pose proof (H Heqb). computes_to_inv; subst. simpl. destruct (A_eq_dec (f a0) (f a)). + apply H1 in e; computes_to_inv; subst. simpl in *; discriminate. + pose proof (H2 n); subst; simpl in *. computes_to_econstructor; eauto. apply (@BindComputes _ _ _ _ false); eauto. computes_to_econstructor; simpl. intuition. - apply Decides_false in Heqb. pose proof (H0 Heqb); subst; simpl. destruct (A_eq_dec (f a0) (f a)); subst. intuition; computes_to_inv; subst. simpl in Heqb0; discriminate. apply H2 in n; subst; eauto. } apply (@BindComputes _ _ _ _ true); eauto. destruct v2; simpl in *; try discriminate. computes_to_econstructor. computes_to_econstructor. eauto. apply (@BindComputes _ _ _ _ true); eauto. pose proof (H2 n); subst; simpl. simpl in v1_eq. computes_to_econstructor; eauto. apply (@BindComputes _ _ _ _ false); eauto. computes_to_econstructor; simpl. intro; eapply n; eauto. apply Decides_false in Heqb. pose proof (H1 Heqb); subst; simpl. destruct (A_eq_dec (f a) bound); subst. intuition. apply H2 in n; subst; 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