proposition: Lemma monty_switch : play_n (switch def) = bcoin (/ 3)%coqR.~%:pr.
proof: Proof. rewrite {1}/play_n {1}/monty /switch. transitivity (hide_n >>= (fun h => pick def >>= (fun p => tease_n h p >>= (fun t => Ret (h == head def (doors \\ [:: p; t]))))) : M _). by bind_ext => d; bind_ext => d'; under eq_bind do rewrite bindretf eq_sym. transitivity (hide_n >>= (fun h => pick def >>= (fun p => tease_n h p >> if h == p then Ret false else Ret true)) : M _). bind_ext => h; bind_ext => p; rewrite /tease_n. case: ifPn => [/eqP|] hp. rewrite -{2}hp. With (rewrite (_ : _ == _ = false)) Open (X in _ >>= X). by apply/negbTE; rewrite eq_sym; apply/(Set3.head_filter card_door); rewrite inE eqxx. reflexivity. by rewrite arbitrary_inde // Set3.size_filter2. rewrite Set3.filter_another // !arbitrary1 2!bindretf. 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 //= eqxx. transitivity (hide_n >>= (fun h => pick def >>= (fun p => Ret (h != p))) : M _). bind_ext => h; bind_ext => p. by rewrite /tease_n arbitrary_inde ?Set3.size_filter2 //; case: ifPn. rewrite /hide_n /pick /monty.pick. by rewrite bcoin23E. 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