proposition: Lemma repeat_low_tree_approx_same_inv : forall (A : Set) (eqd : eq_dec A)(c : Comp A)(P : A -> bool) (n : nat) (a : A) (t : DistApproxTree A) (r : Rat), well_formed_comp c -> (exists a, In a (filter P (getSupport c))) -> lowDistApprox_repeat c P a n r -> dat_correct_repeat2 c P n t -> n > 0 -> r == lowDistApproxFromTree eqd t a.
proof: Proof. intuition. destruct H2. intuition. unfold lowDistApprox_repeat, ratMult_rel, expRat_rel, indicator_rel in *. unfold dat_correct in *. symmetry. edestruct (sumList_rel_left_total (fun (i : nat) (r : Rat) => forall r1'1 : Rat, sumList_rel (fun a : A => lowDistApprox c a n) (filter (fun a : A => negb (P a)) (getSupport c)) r1'1 -> r == expRat r1'1 i) (getNats O (S n))). intuition. edestruct (sumList_rel_left_total (fun a : A => lowDistApprox c a n) (filter (fun a : A => negb (P a)) (getSupport c))). intuition. eapply lowDistApprox_left_total. trivial. trivial. exists (expRat x0 a0). intuition. eapply expRat_eqRat_compat. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. edestruct lowDistApprox_left_total; eauto. rewrite (H1 (indicator P a * x0) x1); eauto. edestruct (sumList_rel_left_total (fun a : A => lowDistApprox c a n) (filter (fun a : A => negb (P a)) (getSupport c))). intuition. eapply lowDistApprox_left_total; eauto. assert (sumList_rel (fun a : A => lowDistApprox c a n) (filter (fun a : A => negb (P a)) (getTreeSupport eqd x)) x2). eapply sumList_rel_ls_intersect. eauto. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_NoDup. eapply getUnique_NoDup. trivial. intuition. eapply lowDistApprox_func; eauto. intuition. eapply lowDistApprox_val_eq. eapply low_tree_approx_same. trivial. eapply H4. eapply lowDistApproxFromTree_eq_0. intuition. eapply H9. eapply filter_In; intuition; eauto. apply filter_In in H8. intuition. intuition. exfalso. eapply H9. eapply filter_In; intuition. eapply getTreeSupport_in. eauto. eapply filter_In. eauto. apply filter_In in H8. intuition. assert (sumList_rel (fun i => expRat_rel (eqRat x2) i) (getNats O (S n)) x0). eapply sumList_rel_body_eq. eapply H2. intuition. unfold expRat_rel in *. intuition. rewrite H9. eapply expRat_eqRat_compat. eapply H10. trivial. intuition. trivial. clear H2. clear H7. assert (sumList (getNats O (S n)) (expRat x2) == x0). rewrite sumList_rel_func. eapply eqRat_refl. eapply sumList_rel_sumList_eqRat. eapply sumList_rel_body_eq. eapply H9. intuition. unfold expRat_rel in *. rewrite H2. eapply eqRat_refl. intuition. intuition. intuition. intuition. rewrite <- H2. rewrite H7. intuition. rewrite <- H2. clear H9. clear H2. assert (x1 == (lowDistApproxFromTree eqd x a)). eapply lowDistApprox_func. eauto. eauto. eapply low_tree_approx_same; eauto. rewrite H2. assert (x2 == (computeEmptySpace x P)). assert (sumList (filter (fun a : A => negb (P a)) (getTreeSupport eqd x)) (fun a : A => lowDistApproxFromTree eqd x a) == x2). eapply sumList_rel_func. eapply sumList_rel_sumList_eqRat. eapply sumList_rel_body_eq. eapply H8. intuition. eapply lowDistApprox_func. eauto. eapply low_tree_approx_same. trivial. eauto. trivial. intuition. trivial. intuition. rewrite <- H7. rewrite H9. intuition. rewrite <- H7. eauto. eapply computeEmptySpace_correct; eauto. eapply eqRat_trans. 2:{ eapply ratMult_eqRat_compat. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply sumList_body_eq. intuition. eapply expRat_eqRat_compat. symmetry. eapply H7. eapply eqRat_refl. } eapply eqRat_trans. eapply repeat_low_tree_approx_same_tree_inv; eauto. eapply datRepeat_func_eq. eauto. intuition. eapply dat_correct_func; eauto. rewrite (ratMult_assoc (indicator P a) (sumList (getNats 0 (S n)) (fun a0 : nat => expRat (computeEmptySpace x P) a0))). eapply ratMult_eqRat_compat. intuition. rewrite <- sumList_factor_constant_l. rewrite sumList_series_incr. 2:{ intuition. assert (computeEmptySpace x P * expRat (computeEmptySpace x P) n0 == expRat (computeEmptySpace x P) (S n0)). simpl. intuition. eapply H9. } remember (lowDistApproxFromTree eqd x a) as v. rewrite <- (ratMult_1_l v) at 1. rewrite <- ratMult_distrib_r. assert ((expRat (computeEmptySpace x P)) O = 1). simpl. intuition. rewrite <- H9 at 1. rewrite <- sumList_series_split_first. simpl. eapply eqRat_refl. unfold indicator. intuition. rewrite H7. rewrite H10. repeat rewrite ratMult_1_l. eapply sumList_rel_func; eauto. intuition. edestruct (sumList_rel_left_total (fun a : A => lowDistApprox c a n) (filter (fun a : A => negb (P a)) (getSupport c))). intuition. eapply lowDistApprox_left_total; eauto. rewrite H9; eauto. rewrite H11; eauto. intuition. rewrite H7. rewrite H10. repeat rewrite ratMult_0_l. intuition. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat