proposition: Lemma tease_fE (h p : door) : let d := head def (doors \\ [:: h; p]) in tease_f h p = if h == p then uniform def (doors \\ [:: h]) else fail <| (/ 2)%coqR%:pr |> Ret d : M _.
proof: Proof. move=> d. case: ifPn => [/eqP <-|hp]. rewrite /tease_f. transitivity (uniform def (doors \\ [:: h]) >>= Ret : M _). rewrite uniform_notin //. exact: Set3.filter_pred1. by move=> ?; rewrite mem_filter inE => /andP[]. by rewrite bindmret. have Hd : d = Set3.another card_door h p by rewrite {}/d Set3.filter_another. rewrite /tease_f. transitivity (uniform def [:: h; d] >>= (fun t => if t == h then fail else Ret t) : M _). have hd : h != d. rewrite Hd. apply: contra (Set3.another_notin card_door h p) => /eqP <-. by rewrite mem_head. move: (Set3.filter1_another card_door hp); rewrite -/doors -Hd => -[] -> //. by rewrite uniform2. rewrite uniform_cons (_ : _%:pr = (/ 2)%coqR%:pr)%R; last first. by apply val_inj => /=; lra. rewrite uniform_singl // [head _ _]/= choice_bindDl 2!bindretf eqxx ifF //. by apply/negbTE/(Set3.head_filter card_door); rewrite inE eqxx. 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