proposition: Theorem lowDistApprox_Rnd: forall n2 n1 (a : Bvector n1) r, lowDistApprox (Rnd n1) a (n1 + n2) r -> r == (1 / (expnat 2 n1)).
proof: Proof. induction n2; intuition; simpl in *. rewrite Nat.add_0_r in *. unfold lowDistApprox in *. destruct H. destruct H. intuition. rewrite H2. eapply eqRat_terms. eapply pred_count_eq_1_inv; eauto. eapply comp_answer_eq_dec. unfold eq_dec. intuition. eapply Bvector_eq_dec. eapply rel_map_Rnd_NoDup. trivial. trivial. eapply rel_map_Rnd_any_in. trivial. trivial. unfold lowDistApprox in H. destruct H. destruct H. intuition. edestruct (rel_map_left_total (evalDet (Rnd n1))). intuition. eapply evalDet_left_total. eapply well_formed_Rnd. assert (pred_count (eq (ca_done a)) x1 x0). eapply pred_count_permutation. eapply rel_map_permutation. eapply getAllBlists_perm. intuition. eapply evalDet_func; eauto. 2:{ eapply H0. } intuition. eapply evalDet_left_total. eapply well_formed_Rnd. eauto. eauto. assert ((n1 + S n2) = (S (n1 + n2)))%nat. lia. rewrite H4 in H1. simpl in *. apply rel_map_app_inv in H1. intuition. rewrite map_length in H5. rewrite map_length in H6. unfold lowDistApprox in *. apply rel_map_map_inv in H5. apply rel_map_map_inv in H6. assert (rel_map (evalDet (Rnd n1)) (getAllBlists_app (n1 + n2)) (firstn (length (getAllBlists_app (n1 + n2))) x1)). eapply rel_map_eq. eapply H5. trivial. intuition. assert (length a0 = (n1 + n2)%nat). eapply getAllBlists_app_In_length. eauto. inversion H8; clear H8; subst. inversion H10; clear H10; subst. simpl in *. edestruct shiftOut_Some. assert (length a0 >= n1)%nat. lia. eapply H8. destruct x2. erewrite shiftOut_app in H14; eauto. inversion H14; clear H14; subst. simpl in *. inversion H15; clear H15; subst. econstructor. econstructor. eauto. simpl. rewrite H8. econstructor. eauto. simpl. econstructor. inversion H10; clear H10; subst. simpl in *. case_eq (shiftOut (a0 ++ true :: nil) n1); intuition. rewrite H8 in H14. destruct p. inversion H14; clear H14; subst. simpl in *. inversion H15. rewrite H8 in H14. econstructor. econstructor. eauto. simpl. erewrite shiftOut_app_None. econstructor. eauto. clear H5. assert (rel_map (evalDet (Rnd n1)) (getAllBlists_app (n1 + n2)) (skipn (length (getAllBlists_app (n1 + n2))) x1)). eapply rel_map_eq. eapply H6. trivial. intuition. assert (length a0 = (n1 + n2)%nat). eapply getAllBlists_app_In_length. eauto. inversion H8; clear H8; subst. inversion H10; clear H10; subst. simpl in *. edestruct shiftOut_Some. assert (length a0 >= n1)%nat. lia. eapply H8. destruct x2. erewrite shiftOut_app in H14; eauto. inversion H14; clear H14; subst. simpl in *. inversion H15; clear H15; subst. econstructor. econstructor. eauto. simpl. rewrite H8. econstructor. eauto. simpl. econstructor. inversion H10; clear H10; subst. simpl in *. case_eq (shiftOut (a0 ++ false :: nil) n1); intuition. rewrite H8 in H14. destruct p. inversion H14; clear H14; subst. simpl in *. inversion H15. rewrite H8 in H14. econstructor. econstructor. eauto. simpl. erewrite shiftOut_app_None. econstructor. eauto. clear H6. eapply (pred_count_first_skip) in H3. destruct H3. destruct H3. intuition. edestruct (rel_map_left_total (evalDet (Rnd n1)) (getAllBlists (n1 + n2))). intuition. eapply evalDet_left_total. eapply well_formed_Rnd. rewrite H4 in H2. simpl in *. rewrite <- H8 in H2. assert (r * (2/1) == (x2 + x3) / (expnat 2 (n1 + n2))). rewrite H2. assert (nz (expnat 2 (n1 + n2))%nat). econstructor. eapply expnat_pos. lia. assert (nz 2)%nat. econstructor. lia. eapply eqRat_trans. eapply ratMult_eqRat_compat. eapply (@eqRat_terms _ _ (x2 + x3)%nat (posnatMult (natToPosnat H10) (natToPosnat H9))). trivial. simpl. trivial. eapply eqRat_refl. rewrite <- ratMult_num_den. eapply eqRat_trans. eapply eqRat_terms. eapply Nat.mul_comm. eapply posnatMult_1_r. rewrite rat_remove_common_factor. eapply eqRat_terms; eauto. rewrite ratAdd_den_same in H9. assert (x2 / (expnat 2 (n1 + n2)) == 1 / expnat 2 n1). eapply IHn2. econstructor. econstructor. intuition. eauto. eapply pred_count_permutation. eapply Permutation_sym. eapply rel_map_permutation. eapply getAllBlists_perm. intuition. eapply evalDet_func; eauto. 2:{ eauto. } intuition. eapply evalDet_left_total. eapply well_formed_Rnd. eapply H1. eauto. eapply eqRat_terms; eauto. assert (x3 / expnat 2 (n1 + n2) == 1 / expnat 2 n1). eapply IHn2. econstructor. econstructor. intuition. eauto. eapply pred_count_permutation. eapply Permutation_sym. eapply rel_map_permutation. eapply getAllBlists_perm. intuition. eapply evalDet_func; eauto. 2:{ eapply H7. } intuition. eapply evalDet_left_total. eapply well_formed_Rnd. eapply H5. eauto. eapply eqRat_terms; eauto. rewrite H10 in H9. rewrite H11 in H9. rewrite ratMult_2 in H9. eapply ratMult_same_r_inv. eauto. discriminate. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat