proposition: Theorem evalDist_bool_support : forall (c : Comp bool)(ls : list bool), well_formed_comp c -> ls = getSupport c -> sumList ls (evalDist c) == evalDist c false + evalDist c true.
proof: Proof. intuition. specialize (support_NoDup c); intuition. rewrite <- H0 in H1. destruct ls; intuition. specialize (getSupport_length_nz H); intuition. rewrite <- H0 in H2. simpl in *. lia. destruct b. destruct ls. unfold sumList; simpl. eapply ratAdd_eqRat_compat. symmetry. eapply getSupport_not_In_evalDist. intuition. rewrite <- H0 in H2. simpl in *. intuition. intuition. destruct b. inversion H1; clear H1; subst. simpl in *. intuition. destruct ls. unfold sumList. simpl. rewrite <- ratAdd_0_l. eapply ratAdd_comm. destruct b. inversion H1; clear H1; subst. simpl in *. intuition. inversion H1; clear H1; subst. simpl in *. intuition. inversion H5; clear H5; subst. simpl in *; intuition. destruct ls. unfold sumList; simpl. rewrite ratAdd_comm. eapply ratAdd_eqRat_compat. intuition. symmetry. eapply getSupport_not_In_evalDist. intuition. rewrite <- H0 in H2. simpl in *. intuition. destruct b. destruct ls. unfold sumList. simpl. rewrite <- ratAdd_0_l. intuition. destruct b. inversion H1; clear H1; subst. simpl in *. intuition. inversion H5; clear H5; subst. simpl in *; intuition. inversion H1; clear H1; subst. simpl in *; intuition. inversion H1; clear H1; subst. simpl in *; intuition. Qed.
imports: FCF.FCF FCF.Crypto FCF.Asymptotic