proposition: Lemma monty_f_switch : play_f (@switch def _) = Ret false <| (/ 3)%coqR%:pr |> (fail <| (/ 2)%coqR%:pr |> (Ret true : M _)).
proof: Proof. rewrite /play_f /monty hide_pickE /switch. Open (X in _ >>= X). under eq_bind do rewrite bindretf. over. under eq_bind do rewrite tease_fE fun_if if_arg. Open (X in _ >>= X). transitivity (if x.1 == x.2 then uniform def (doors \\ [:: x.1]) >> Ret false else fail <| (/ 2)%coqR%:pr |> ret _ (head def (doors \\ [:: x.1; x.2])) >>= (fun x0 => Ret (head def (doors \\ [:: x.2; x0]) == x.1)) : M _). case: x => h p; rewrite [_.1]/= [_.2]/=; case: ifPn => // /eqP <-. transitivity (uniform def (doors \\ [:: h]) >>= (fun x0 => if head def (doors \\ [:: h; x0]) == h then Ret true else Ret false) : M _). bind_ext => x; by case: ifPn. rewrite uniform_notin //. exact: Set3.filter_pred1. move=> x; rewrite mem_filter inE=> _; by rewrite Set3.head_filter // inE eqxx. reflexivity. transitivity (uniform (def, def) (cp doors doors) >>= (fun x => if x.1 == x.2 then Ret false else fail <| (/ 2)%coqR%:pr |> Ret (head def (doors \\ [:: x.2; head def (doors \\ [:: x.1; x.2])]) == x.1)) : M _). bind_ext => -[h p]; rewrite [_.1]/= [_.2]/=. case: ifPn => [?| hp]; first by rewrite uniform_inde. by rewrite choice_bindDl (@bindfailf M) bindretf. transitivity ( uniform (def, def) (cp doors doors) >>= (fun x => if x.1 == x.2 then Ret false else (fail : M _) <| (/ 2)%coqR%:pr |> (Ret true : M _))). bind_ext => -[h p]; rewrite [_.1]/= [_.2]/=. case: ifPn => // hp; congr (_ <| _ |> Ret _). apply/eqP. rewrite (_ : _ \\ _ = [:: h]) //. rewrite Set3.filter_another; last by rewrite eq_sym Set3.head_filter // !inE eqxx orbT. by rewrite Set3.filter_another //= Set3.another_another. rewrite (Set3.bcoin13E_pair _ def (fun b => if b then Ret false else fail <| (/ 2)%coqR%:pr |> Ret true)) //. by rewrite choice_bindDl 2!bindretf. 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