proposition: Lemma monty_choice_your_choice_combine : (do h <- hide_n ; do p <- pick def : M _; Ret (h, p) = (do p <- pick def : M _; Ret (A, p)) [~] (do p <- pick def : M _ ; Ret (B, p)) [~] (do p <- pick def : M _; Ret (C, p)))%Do.
proof: Proof. pose k (h : door) : M _ := pick def >>= (fun p => Ret (h, p)). transitivity (hide_n >>= k); first by []. transitivity ((Ret A [~] Ret B [~] Ret C) >>= k). rewrite /hide_n /doors Set3.enumE /arbitrary /foldr1 [in LHS]/=. by rewrite -[in RHS]altA [in RHS]altC -[in RHS]altA. by rewrite 2!alt_bindDl 3!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