proposition: Lemma evalDet_step_nil_dist_preserved : forall (A : Set)(c : Comp A), well_formed_comp c -> forall c' a, evalDet_step c nil = cs_more c' nil -> evalDist c a == evalDist c' a.
proof: Proof. induction 1; intuition; simpl in *. discriminate. case_eq (evalDet_step c1 nil); intuition; rewrite H3 in H2; try discriminate. inversion H2; clear H2; subst. erewrite evalDet_step_done_support_singleton; eauto. unfold sumList. simpl. rewrite <- ratAdd_0_l. rewrite (@evalDet_step_done_evalDist _ (comp_eq_dec c1)); eauto. destruct (comp_eq_dec c1 b b). eapply ratMult_1_l. congruence. inversion H2; clear H2; subst. simpl. rewrite sumList_permutation. 2:{ eapply evalDet_step_more_support_preserved. eauto. } eapply sumList_body_eq. intuition. eapply ratMult_eqRat_compat; intuition. destruct n. inversion H; clear H; subst. simpl. rewrite (vector_0 a). destruct (Bvector_eq_dec [] [] ). eapply eqRat_terms; intuition. congruence. discriminate. inversion H1; clear H1; subst. simpl. destruct (in_dec (comp_eq_dec c) a (getSupport c)). symmetry. eapply eqRat_trans. eapply (sumList_filter_partition P). eapply eqRat_trans. eapply ratAdd_eqRat_compat. eapply sumList_body_eq. intuition. assert (P a0 = true). eapply filter_In; eauto. rewrite H2. simpl. eapply eqRat_refl. eapply sumList_body_eq. intuition. assert (P a0 = false). assert (negb (P a0) = true). apply filter_In in H1. intuition. eapply negb_true_iff. trivial. rewrite H2. simpl. eapply eqRat_refl. case_eq (P a); intuition. unfold indicator. rewrite H1. rewrite ratMult_1_l. assert (sumList (filter P (getSupport c)) (fun a0 : A => evalDist c a0 * (if comp_eq_dec c a0 a then 1 else 0)) == evalDist c a). rewrite (@sumList_exactly_one _ a). destruct (comp_eq_dec c a a); try congruence. eapply ratMult_1_r. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_In; eauto. intuition. destruct (comp_eq_dec c b0 a); subst; intuition. eapply ratMult_0_r. rewrite H2. rewrite sumList_factor_constant_r. rewrite ratMult_1_l. assert (sumList (filter (fun a0 : A => negb (P a0)) (getSupport c)) (evalDist c) == (ratSubtract 1 (sumList (filter P (getSupport c)) (evalDist c)))). rewrite <- evalDist_lossless. rewrite (sumList_filter_partition P (getSupport c)). rewrite ratSubtract_ratAdd_inverse. intuition. trivial. rewrite H3. rewrite ratMult_ratSubtract_distrib_r. rewrite ratMult_1_l. rewrite <- (ratMult_assoc (sumList (filter P (getSupport c)) (evalDist c))). rewrite (ratMult_comm (sumList (filter P (getSupport c)) (evalDist c))). rewrite ratInverse_prod_1. rewrite ratMult_1_l. rewrite ratSubtract_ratAdd_inverse_2. intuition. eapply leRat_trans. rewrite <- ratMult_1_l. eapply leRat_refl. eapply ratMult_leRat_compat; intuition. eapply ratInverse_1_swap. intuition. eapply sumList_0 in H4. eapply getSupport_In_evalDist. eapply filter_In. eapply H0. eapply H4. trivial. eapply leRat_trans. eapply sumList_filter_le. rewrite evalDist_lossless. intuition. trivial. intuition. eapply sumList_0 in H4. eapply getSupport_In_evalDist. eapply filter_In. eapply H0. eapply H4. trivial. unfold indicator. rewrite H1. rewrite ratMult_0_l. assert (sumList (filter P (getSupport c)) (fun a0 : A => evalDist c a0 * (if comp_eq_dec c a0 a then 1 else 0)) == 0). eapply sumList_0. intuition. destruct (comp_eq_dec c a0 a); subst. assert (P a = true). eapply filter_In; eauto. congruence. eapply ratMult_0_r. rewrite H2. assert (sumList (filter (fun a0 : A => negb (P a0)) (getSupport c)) (fun a0 : A => evalDist c a0 * (0 * ratInverse (sumList (filter P (getSupport c)) (evalDist c)) * evalDist c a)) == 0). eapply sumList_0. intuition. repeat rewrite ratMult_0_l. eapply ratMult_0_r. rewrite H3. rewrite <- ratAdd_0_l. symmetry. eapply ratMult_0_l. assert (evalDist c a == 0). eapply getSupport_not_In_evalDist. trivial. rewrite H1. rewrite ratMult_0_r. symmetry. eapply sumList_0. intuition. case_eq (P a0); intuition. simpl. destruct (comp_eq_dec c a0 a); subst. intuition. eapply ratMult_0_r. simpl. rewrite H1. repeat rewrite ratMult_0_r. intuition. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat