proposition: Lemma play_switch : play switch = bcoin (/ 3)%coqR.~%:pr.
proof: Proof. rewrite {1}/play {1}/monty hide_pickE. transitivity (do hp <- uniform (def, def) (cp doors doors); do t <- tease hp.1 hp.2; Ret ((head def (doors \\ [:: hp.2; t])) == hp.1) : M _)%Do. bind_ext => -[h p]. by rewrite [_.1]/= [_.2]/=; under eq_bind do rewrite bindretf. transitivity (uniform (def, def) (cp doors doors) >>= (fun hp => if hp.1 == hp.2 then Ret false else Ret true : M _)). bind_ext => -[h p]. rewrite [_.1]/= [_.2]/=. case: ifPn => [/eqP|] hp. rewrite -{2}hp. With (rewrite (_ : _ == _ = false)) Open (X in _ >>= X). by apply/negbTE/(Set3.head_filter card_door); rewrite inE eqxx. reflexivity. by rewrite /tease uniform_inde. rewrite /tease. rewrite Set3.filter_another //. rewrite uniform_singl // -/(head _) bindretf. rewrite (_ : head _ _ = h) ?eqxx //. rewrite Set3.filter_another /=; last first. move: (Set3.another_notin card_door h p). rewrite !inE negb_or => /andP[_]; by rewrite eq_sym. by rewrite Set3.another_another. transitivity (uniform (def, def) (cp doors doors) >>= (fun hp => Ret (hp.1 != hp.2)) : M _). bind_ext => -[h p]; by case: ifPn. exact: Set3.bcoin23E_pair. 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