proposition: Lemma try_uFFT d : fmap (uncurry (fun a b => a == b)) (try d) = uFFT.
proof: Proof. rewrite fmapE /try bindA. under eq_bind do rewrite bindretf. rewrite /pick /monty.pick. transitivity ((Ret A <| (/ 3)%coqR%:pr |> (Ret B <| (/ 2)%coqR%:pr |> Ret C)) >>= (fun p => Ret (d == p)) : M _). congr bind; by rewrite /doors Set3.enumE 2!uniform_cons. rewrite 2!choice_bindDl 3!bindretf. rewrite /uFFT 2!uniform_cons. rewrite uniform_singl // [head _ _]/=. have : d \in doors by rewrite mem_enum. rewrite /doors Set3.enumE !inE => /or3P[] /eqP ->. - rewrite eqxx (negbTE (Set3.a_neq_b _)) (negbTE (Set3.a_neq_c _)). rewrite choiceC. erewrite choiceA_alternative. reflexivity. rewrite /= /onem; split. rewrite -RmultE -RminusE -R1E; field. rewrite -RmultE -!RminusE -R1E; field. - rewrite eq_sym (negbTE (Set3.a_neq_b _)) eqxx (negbTE (Set3.b_neq_c _)). congr (_ <| _ |> _). rewrite choiceC (@choice_ext (/ 2)%coqR%:pr) //= /onem. congr (Ret false <| _ |> Ret true). apply/val_inj => /=. by rewrite -RminusE -R1E; field. by rewrite eq_sym (negbTE (Set3.a_neq_c _)) eq_sym (negbTE (Set3.b_neq_c _)) 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