proposition: Theorem bool_Comp_seq : forall (A : Set)(c1 : Comp bool)(c2 : bool -> Comp A) a, evalDist (b <-$ c1; c2 b) a == (evalDist c1 true * evalDist (c2 true) a) + (evalDist c1 false * evalDist (c2 false) a).
proof: Proof. intros. simpl. remember (getSupport c1) as ls. destruct ls. unfold sumList. simpl. assert (Pr [c1 ] == 0). eapply getSupport_not_In_evalDist. rewrite <- Heqls. simpl. intuition. rewrite H. assert (evalDist c1 false == 0). eapply getSupport_not_In_evalDist. rewrite <- Heqls. simpl. intuition. rewrite H0. repeat rewrite ratMult_0_l. eapply ratAdd_0_l. destruct b. destruct ls. unfold sumList. simpl. rewrite <- ratAdd_0_l. rewrite ratAdd_0_r at 1. eapply ratAdd_eqRat_compat. intuition. symmetry. assert (evalDist c1 false == 0). eapply getSupport_not_In_evalDist. rewrite <- Heqls. simpl. intuition. rewrite H. eapply ratMult_0_l. destruct b. exfalso. assert (NoDup (true :: true :: ls))%list. rewrite Heqls. eapply getSupport_NoDup. inversion H; clear H; subst. simpl in *. intuition. destruct ls. unfold sumList. simpl. rewrite <- ratAdd_0_l. intuition. destruct b. assert (NoDup (true :: false :: true :: ls)%list). rewrite Heqls. eapply getSupport_NoDup. inversion H; clear H; subst. simpl in *. intuition. assert (NoDup (true :: false :: false :: ls)%list). rewrite Heqls. eapply getSupport_NoDup. inversion H; clear H; subst. inversion H3; clear H3; subst. simpl in *. intuition. destruct ls. unfold sumList. simpl. eapply ratAdd_eqRat_compat; intuition. assert ( Pr [c1 ] == 0). eapply getSupport_not_In_evalDist. rewrite <- Heqls. simpl. intuition. rewrite H. rewrite ratMult_0_l. intuition. destruct b. destruct ls. unfold sumList. simpl. rewrite <- ratAdd_0_l. eapply ratAdd_comm. destruct b. assert (NoDup (false :: true :: true :: ls)%list). rewrite Heqls. eapply getSupport_NoDup. inversion H; clear H; subst. inversion H3; clear H3; subst. simpl in *. intuition. assert (NoDup (false :: true :: false :: ls)%list). rewrite Heqls. eapply getSupport_NoDup. inversion H; clear H; subst. simpl in *. intuition. assert (NoDup (false :: false :: ls)%list). rewrite Heqls. eapply getSupport_NoDup. inversion H; clear H; subst. simpl in *. intuition. Qed.
imports: FCF.FCF FCF.CompFold