proposition: Lemma lowDistApprox_low : forall (A : Set)(c : Comp A), well_formed_comp c -> forall n a r, lowDistApprox c a n r -> r <= evalDist c a.
proof: Proof. induction 1; intuition; simpl in *. rewrite lowDistApprox_Ret_inv; eauto. eapply leRat_refl. edestruct (lowDistApprox_bind_left_total); eauto. eapply leRat_trans. eapply lowDistApprox_le_bind; eauto. inversion H3; clear H3; subst. eapply sumList_rel_le. eauto. eapply sumList_rel_sumList. intuition. edestruct lowDistApprox_left_total. eapply comp_eq_dec; eauto. eauto. edestruct lowDistApprox_left_total. eapply bind_eq_dec; eauto. eauto. rewrite H5; eauto. rewrite <- H6; eauto. eapply ratMult_leRat_compat; eauto. destruct (le_dec n n0). assert (exists n1, n0 = n + n1)%nat. exists (minus n0 n). lia. destruct H0. subst. rewrite lowDistApprox_Rnd; eauto. eapply leRat_terms; intuition. rewrite lowDistApprox_Rnd_lt. eapply rat0_le_all. eauto. lia. destruct n. destruct H1. destruct H1. intuition. simpl in *. inversion H2; clear H2; subst. inversion H6; clear H6; subst. inversion H8; clear H8; subst. inversion H2; clear H2; subst. apply evalDet_steps_bind_done_inv in H8. destruct H8. destruct H2. intuition. apply filter_In in H0. intuition. assert (b = x). eapply evalDet_steps_nil_eq; eauto. subst. rewrite H6 in H5. inversion H5; clear H5; subst. simpl in *. inversion H10; clear H10; subst. inversion H1; clear H1; subst. inversion H9; clear H9; subst. inversion H7; clear H7; subst. rewrite H4. unfold indicator. rewrite H6. rewrite ratMult_1_l. erewrite evalDet_steps_done_support_singleton; eauto. unfold sumList; simpl. rewrite H6. simpl. rewrite <- ratMult_1_l. eapply ratMult_leRat_compat. rewrite <- ratInverse_1. eapply eqRat_impl_leRat. eapply ratInverse_eqRat_compat. eapply rat1_ne_rat0. rewrite <- ratAdd_0_l. rewrite (evalDet_steps_done_evalDist eqd); eauto. destruct (eqd a0 a0). intuition. congruence. eapply eqRat_impl_leRat. rewrite (evalDet_steps_done_evalDist eqd); eauto. destruct (eqd a0 a0). eapply num_dem_same_rat1. unfold natToPosnat, posnatToNat. trivial. congruence. inversion H7; clear H7; subst. rewrite H4. eapply leRat_trans. eapply eqRat_impl_leRat. eapply rat_num_0. eapply rat0_le_all. inversion H1; clear H1; subst. discriminate. inversion H6; clear H6; subst. rewrite H4. eapply leRat_trans. eapply eqRat_impl_leRat. eapply rat_num_0. eapply rat0_le_all. edestruct lowDistApprox_repeat_left_total; eauto. eapply leRat_trans. eapply lowDistApprox_le_repeat; eauto. lia. unfold lowDistApprox_repeat in *. unfold ratMult_rel, expRat_rel, indicator_rel in *. edestruct lowDistApprox_left_total. eapply comp_eq_dec; eauto. eauto. edestruct (sumList_rel_left_total (fun a1 : A => lowDistApprox c a1 (S n)) (filter (fun a1 : A => negb (P a1)) (getSupport c))). intuition. eapply lowDistApprox_left_total; eauto. edestruct (sumList_rel_left_total (fun (i : nat) (r : Rat) => forall r1' : Rat, sumList_rel (fun a : A => lowDistApprox c a (S n)) (filter (fun a : A => negb (P a)) (getSupport c)) r1' -> r == expRat r1' i) (getNats 0 (S (S n)))). intuition. econstructor. intuition. eapply expRat_eqRat_compat; eauto. eapply sumList_rel_func. eapply H4. trivial. intuition. eapply lowDistApprox_func; eauto. case_eq (P a); intuition. rewrite H2; eauto. 2:{ intuition. eapply ratMult_eqRat_compat. symmetry. eauto. eapply sumList_rel_func. eapply H5. eapply H8. intuition. rewrite H9. rewrite H11. eapply eqRat_refl. eauto. trivial. congruence. } eapply ratMult_leRat_compat. eapply ratMult_leRat_compat. unfold indicator. rewrite H6. intuition. rewrite (@sum_power_series (S (S n)) (sumList_rel (fun a : A => lowDistApprox c a (S n)) (filter (fun a : A => negb (P a)) (getSupport c)))); eauto; try lia. 2:{ intuition. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. } 3:{ unfold ratMult_rel, ratSubtract_rel, expRat_rel, ratInverse_rel. intuition. rewrite H7. rewrite H8. eapply eqRat_refl. intuition. eapply ratSubtract_eqRat_compat. eauto. eapply sumList_rel_func. eapply H4. trivial. intuition. eapply lowDistApprox_func; eauto. eapply eqRat_refl. intuition. eapply expRat_eqRat_compat. eapply sumList_rel_func. eapply H4. trivial. intuition. eapply lowDistApprox_func; eauto. } eapply leRat_trans. eapply ratMult_leRat_compat. eapply ratSubtract_le. eapply leRat_refl. eapply ratInverse_leRat. 2:{ eapply ratSubtract_leRat. eapply leRat_refl. eapply sumList_rel_le. eauto. eapply sumList_rel_sumList. intuition. rewrite <- H9. eapply IHwell_formed_comp. eauto. } intuition. eapply getSupport_In_evalDist. eapply filter_In; eauto. eapply sumList_0. rewrite <- evalDist_lossless in H7. rewrite sumList_filter_partition in H7. rewrite ratAdd_comm in H7. rewrite ratSubtract_ratAdd_inverse in H7. eapply H7. trivial. trivial. rewrite ratMult_1_l. eapply eqRat_impl_leRat. eapply ratInverse_eqRat_compat. intuition. eapply getSupport_In_evalDist. eapply filter_In; eauto. eapply sumList_0. rewrite <- evalDist_lossless in H7. rewrite sumList_filter_partition in H7. rewrite ratAdd_comm in H7. rewrite ratSubtract_ratAdd_inverse in H7. eapply H7. trivial. trivial. rewrite <- (evalDist_lossless); eauto. rewrite (sumList_filter_partition). rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_inverse. intuition. intuition. eapply ratAdd_not_leRat. erewrite <- sumList_filter_partition. eapply leRat_trans. eapply eqRat_impl_leRat. eapply evalDist_lossless. eauto. eapply leRat_trans. eapply H8. eapply sumList_rel_le. eauto. eapply sumList_rel_sumList. intuition. rewrite <- H11. eapply IHwell_formed_comp. eauto. intuition. eapply sumList_0 in H9. eapply getSupport_In_evalDist; eauto. eapply filter_In; eauto. eapply filter_In. intuition. eapply filter_In; eauto. rewrite negb_involutive. eapply filter_In; eauto. eapply IHwell_formed_comp; eauto. rewrite H2; eauto. 2:{ intuition. congruence. eapply ratMult_eqRat_compat. symmetry. eauto. eapply sumList_rel_func. eapply H5. trivial. intuition. rewrite H9; eauto. rewrite H11; eauto. intuition. } repeat rewrite ratMult_0_l. eapply rat0_le_all. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat