proposition: Theorem sumList_support_bool': forall (c : Comp bool) (f : bool -> Rat), sumList (getSupport c) (fun x => evalDist c x * f x) == Pr [c ] * (f true) + (evalDist c false * (f false)).
proof: Proof. intuition. case_eq (getSupport c); intuition. unfold sumList. simpl. assert (Pr[c] == 0). eapply getSupport_not_In_evalDist. rewrite H. simpl; intuition. rewrite H0. clear H0. assert (evalDist c false == 0). eapply getSupport_not_In_evalDist. rewrite H. simpl; intuition. rewrite H0. clear H0. repeat rewrite ratMult_0_l. rewrite <- ratAdd_0_r. reflexivity. destruct b. rewrite sumList_cons. eapply ratAdd_eqRat_compat; intuition. destruct l. unfold sumList. simpl. assert (evalDist c false == 0). eapply getSupport_not_In_evalDist. rewrite H. simpl; intuition. rewrite H0. clear H0. rewrite ratMult_0_l. intuition. destruct b. specialize (getSupport_NoDup c); intuition. rewrite H in H0. inversion H0; clear H0; subst. simpl in *; intuition. rewrite sumList_cons. symmetry. rewrite ratAdd_0_r at 1. eapply ratAdd_eqRat_compat. intuition. destruct l. unfold sumList; simpl; intuition. specialize (getSupport_NoDup c); intuition. rewrite H in H0. destruct b. inversion H0; clear H0; subst; simpl in *; intuition. inversion H0; clear H0; subst. inversion H4; clear H4; subst; simpl in *; intuition. rewrite sumList_cons. symmetry. rewrite ratAdd_comm. eapply ratAdd_eqRat_compat; intuition. destruct l. unfold sumList. simpl. assert (Pr[c] == 0). eapply getSupport_not_In_evalDist. rewrite H. simpl; intuition. rewrite H0. clear H0. eapply ratMult_0_l. destruct b. rewrite sumList_cons. rewrite ratAdd_0_r at 1. eapply ratAdd_eqRat_compat. intuition. destruct l. unfold sumList. simpl. intuition. specialize (getSupport_NoDup c); intuition. rewrite H in H0. destruct b. inversion H0; clear H0; subst. inversion H4; clear H4; subst; simpl in *; intuition. inversion H0; clear H0; subst; simpl in *; intuition. specialize (getSupport_NoDup c); intuition. rewrite H in H0. inversion H0; clear H0; subst; simpl in *; intuition. Qed.
imports: FCF.FCF Permutation