proposition: Lemma computeEmptySpace_correct : forall (A : Set)(eqd : eq_dec A)(t : DistApproxTree A) P, sumList (filter (fun a => negb (P a)) (getTreeSupport eqd t)) (lowDistApproxFromTree eqd t) == (computeEmptySpace t P).
proof: Proof. induction t; intuition; simpl in *. destruct o. simpl. unfold indicator. unfold sumList. case_eq (P a); intuition. simpl. intuition. simpl. destruct (eqd a a); intuition; subst. rewrite <- ratAdd_0_l. intuition. unfold sumList. simpl. intuition. rewrite sumList_sum. unfold getTreeSupport. simpl. eapply ratAdd_eqRat_compat. rewrite sumList_factor_constant_r. rewrite <- sumList_subset'. rewrite IHt1. eapply ratMult_comm. trivial. eapply filter_NoDup. eapply getUnique_NoDup. eapply filter_NoDup. eapply getUnique_NoDup. intuition. eapply filter_In; intuition. eapply in_getUnique. eapply in_or_app. left. eapply in_getUnique_if. eapply filter_In. eauto. apply filter_In in H. intuition. intuition. eapply getTreeSupport_approx_0. intuition. eapply H0. eapply filter_In. intuition. apply filter_In in H. intuition. rewrite sumList_factor_constant_r. rewrite <- sumList_subset'. rewrite IHt2. eapply ratMult_comm. trivial. eapply filter_NoDup. eapply getUnique_NoDup. eapply filter_NoDup. eapply getUnique_NoDup. intuition. eapply filter_In; intuition. eapply in_getUnique. eapply in_or_app. right. eapply in_getUnique_if. eapply filter_In. eauto. apply filter_In in H. intuition. intuition. eapply getTreeSupport_approx_0. intuition. eapply H0. eapply filter_In. intuition. apply filter_In in H. intuition. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat