proposition: Lemma evalDist_lossless : forall (A : Set)(c : Comp A), well_formed_comp c -> sumList (getSupport c) (evalDist c) == 1.
proof: Proof. induction 1; intuition; simpl in *. unfold sumList; simpl in *. destruct (pf a a); intuition. rewrite <- ratAdd_0_l. intuition. eapply eqRat_trans. apply evalDist_sum_bind_eq. eapply comp_eq_dec; eauto. eapply bind_eq_dec; eauto. eapply eqRat_trans. eapply sumList_body_eq. intuition. apply ratMult_eqRat_compat. apply eqRat_refl. apply H1. trivial. eapply eqRat_trans. eapply sumList_body_eq; intuition. apply ratMult_1_r. trivial. rewrite sumList_body_const. rewrite getAllBvectors_length. rewrite <- ratMult_num_den. rewrite Nat.mul_1_l. eapply num_dem_same_rat1. rewrite posnatMult_1_r. unfold posnatToNat, natToPosnat. trivial. eapply eqRat_trans. eapply sumList_body_eq. intuition. eapply ratMult_eqRat_compat. assert (P a = true). eapply filter_In; eauto. unfold indicator. rewrite H2. eapply ratMult_1_l. eapply eqRat_refl. eapply ratInverse_scale_sum_1. intuition. eapply getSupport_In_evalDist. eapply filter_In. eapply H1. trivial. destruct (filter P (getSupport c)); simpl in *; intuition. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec