proposition: Lemma bcoin23E : arbitrary def doors >>= (fun h => uniform def doors >>= (fun p => Ret (h != p))) = bcoin (/ 3)%coqR.~%:pr :> M _.
proof: Proof. transitivity (arbitrary def doors >>= (fun h => uniform def doors >>= (fun p => Ret (h, p) >>= (fun x => Ret (x.1 != x.2) : M _)))). by bind_ext => h; under [RHS]eq_bind do rewrite bindretf. transitivity ((arbitrary def doors >>= (fun h => uniform def doors >>= (fun p => Ret (h, p) : M _))) >>= (fun x => Ret (x.1 != x.2))). by rewrite bindA; under [RHS]eq_bind do rewrite bindA. rewrite monty_choice_your_choice_combine /pick /monty.pick 2!alt_bindDl. have K : forall D, (uniform def doors >>= (fun p : door => Ret (D, p))) >>= (fun x : door * door => Ret (x.1 != x.2)) = uniform def doors >>= (fun p : door => Ret (D != p)) :> M _. move=> D; rewrite bindA. by under eq_bind do rewrite bindretf. rewrite 3!K !(@Set3.uniform_unfold _ _ _ (fun a b => a != b)) !eqxx /=. rewrite Set3.a_neq_b Set3.b_neq_c Set3.a_neq_c eq_sym Set3.a_neq_b eq_sym. rewrite Set3.a_neq_c eq_sym Set3.b_neq_c choicemm. rewrite (@choiceC _ _ _ (/2)%coqR%:pr). rewrite (@choiceA_alternative _ _ _ _ _ (/ 2)%coqR%:pr (/ 3)%coqR.~%:pr); last first. rewrite /onem /=; split. rewrite -RmultE -RminusE -R1E; field. rewrite -RmultE -!RminusE -R1E; field. rewrite choicemm. rewrite (@choiceA_alternative _ _ _ _ _ (/ 2)%coqR%:pr (/ 3)%coqR.~%:pr); last first. rewrite /onem /=; split. rewrite -RmultE -RminusE -R1E; field. rewrite -RmultE -!RminusE -R1E; field. by rewrite choicemm choiceC /= 2!altmm. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra reals Rstruct) infotheo(ssrR realType_ext Reals_ext proba) monae_lib hierarchy monad_lib fail_lib proba_lib