proposition: Lemma theorem51 : (unfoldM p select >=> foldr op (Ret [::])) =1 @hyloM _ _ _ _ op [::] p select seed_select (@well_founded_size _).
proof: Proof. apply: (well_founded_induction (@well_founded_size _)) => y IH. rewrite hyloME; last exact: decr_size_select. case/boolP : (p y) => py. by rewrite base_case. rewrite /kleisli /= join_fmap. rewrite unfoldME; last exact: decr_size_select. rewrite (negbTE py) bindA. rewrite(@decr_size_select _ _) /bassert !bindA; bind_ext => -[b a] /=. case: assertPn => ay; last by rewrite !bindfailf. rewrite !bindretf /= -IH // bind_fmap /kleisli /= join_fmap. suff : do x <- unfoldM p select a; op b (foldr op (Ret [::]) x) = op b (do x <- unfoldM p select a; foldr op (Ret [::]) x) by []. rewrite {ay}. move: a b. apply: (well_founded_induction (@well_founded_size _)) => a IH' b. destruct a as [|u v] => //. rewrite unfoldME /=; last exact: decr_size_select. by rewrite !bindretf. rewrite unfoldME; last exact: decr_size_select. rewrite !bindA. transitivity (do x <- Ret (u, v) [~] (do y_ys <- select v; Ret (y_ys.1, u :: y_ys.2)); op b (do x0 <- fmap (cons x.1) (unfoldM p select x.2); foldr op (Ret [::]) x0)); last first. apply/esym. rewrite {1}/op /opdot_queens /opdot fmap_bind. transitivity (do st <- get; (guard (queens_ok (queens_next st b)) >> do x <- Ret (u, v) [~] (do y_ys <- select v; Ret (y_ys.1, u :: y_ys.2)); (put (queens_next st b)) >> ((cons b (o) (fun x => do x0 <- fmap (cons x.1) (unfoldM p select x.2); foldr op (Ret [::]) x0)) x))). bind_ext => st. rewrite !bindA. bind_ext; case. by rewrite -nondetState_commute. transitivity (do st <- get; (do x <- Ret (u, v) [~] (do y_ys <- select v; Ret (y_ys.1, u :: y_ys.2)) : M _; guard (queens_ok (queens_next st b)) >> put (queens_next st b) >> (cons b (o) (fun x0 => do x1 <- fmap (cons x0.1) (unfoldM p select x0.2); foldr op (Ret [::]) x1)) x)). bind_ext => st. rewrite -bindA guardsC; last exact: bindmfail. rewrite !bindA. bind_ext => x. rewrite assertE !bindA. bind_ext; case. by rewrite bindretf. rewrite -nondetState_commute//; last first. case: (@select_isNondet _ M _ v) => x <-. by exists (ndAlt (ndRet (u, v)) (ndBind x (fun y => ndRet (y.1, u :: y.2)))). by rewrite fcomp_def. bind_ext => x. rewrite {1}/op /opdot_queens /opdot. rewrite nondetState_commute; last first. rewrite fmapE. case: (unfoldM_isNondet (@select_isNondet _ M Z) (@decr_size_select M _) x.2). move=> m <-. by exists (ndBind m (fun y => ndRet (x.1 :: y))). rewrite {2}/op /opdot_queens /opdot. bind_ext => st. rewrite nondetState_commute //; last first. rewrite fmapE. case: (unfoldM_isNondet (@select_isNondet _ M Z) (@decr_size_select _ _) x.2). move=> m <-. by exists (ndBind m (fun y => ndRet (x.1 :: y))). bind_ext; case. rewrite !bind_fmap !fmap_bind. by under [RHS]eq_bind do rewrite fcomp_def. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib