proposition: Lemma repeat_low_tree_approx_same_tree_inv : forall (A : Set)(eqd : eq_dec A)(P : A -> bool)(t1 t2 t3 : DistApproxTree A) n a, datRepeat (eq t3) P n t1 t2 -> lowDistApproxFromTree eqd t2 a == indicator P a * ((lowDistApproxFromTree eqd t1 a) + (computeEmptySpace t1 P) * sumList (getNats 0 n) (expRat (computeEmptySpace t3 P)) * (lowDistApproxFromTree eqd t3 a)).
proof: Proof. induction 1; intuition; simpl in *. repeat rewrite ratMult_0_l. rewrite <- ratAdd_0_l. rewrite ratMult_0_r. intuition. destruct (eqd a a0); subst. unfold indicator. rewrite H. simpl. repeat rewrite ratMult_0_l. repeat rewrite ratMult_1_l. rewrite <- ratAdd_0_r. intuition. rewrite <- ratAdd_0_l. unfold indicator. rewrite H. simpl. repeat rewrite ratMult_0_l. rewrite ratMult_0_r. intuition. destruct (eqd a a0); subst. unfold indicator. rewrite H. repeat rewrite ratMult_0_l. intuition. rewrite <- ratAdd_0_l. unfold indicator. rewrite H. simpl. unfold sumList; simpl. rewrite ratMult_0_r. rewrite ratMult_0_l. rewrite ratMult_0_r. intuition. rewrite IHdatRepeat. destruct (eqd a a0); subst. unfold indicator. rewrite H0. repeat rewrite ratMult_0_l. intuition. repeat rewrite <- ratAdd_0_l. eapply ratMult_eqRat_compat; intuition. unfold indicator. rewrite H0. simpl. rewrite ratMult_1_l. rewrite <- sumList_factor_constant_l. rewrite sumList_series_incr. 2:{ intuition. assert (computeEmptySpace t P * expRat (computeEmptySpace t P) n1 == expRat (computeEmptySpace t P) (S n1)). simpl. intuition. eauto. } rewrite sumList_series_split_first. simpl. rewrite ratMult_distrib_r. rewrite ratMult_1_l. intuition. rewrite IHdatRepeat1. rewrite IHdatRepeat2. remember (sumList (getNats 0 n) (expRat (computeEmptySpace t3 P))) as v1. remember (lowDistApproxFromTree eqd t1 a) as v2. remember (computeEmptySpace t1 P) as v3. remember (indicator P a) as v4. remember (lowDistApproxFromTree eqd t3 a) as v5. remember (lowDistApproxFromTree eqd t2 a) as v6. remember (computeEmptySpace t2 P) as v7. rewrite ratMult_assoc. rewrite (ratMult_assoc v4 (v6 + v7 * v1 * v5) (1 / 2)). rewrite <- ratMult_distrib. eapply ratMult_eqRat_compat; intuition. repeat rewrite ratMult_distrib_r. repeat rewrite <- ratAdd_assoc. eapply ratAdd_eqRat_compat. repeat rewrite ratAdd_assoc. eapply ratAdd_eqRat_compat; intuition. rewrite ratAdd_comm. eapply ratAdd_eqRat_compat. intuition. rewrite ratMult_comm. repeat rewrite <- ratMult_assoc. intuition. rewrite ratMult_comm. repeat rewrite <- ratMult_assoc. intuition. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat