proposition: Lemma unfoldM_isNondet S (M : nondetStateMonad S) A B (f : seq B -> M (A * seq B)%type) : (forall s, nondetState_isNondet (f s)) -> bassert_size f -> forall s, nondetState_isNondet (unfoldM (@well_founded_size B) (@nilp _) f s).
proof: Proof. move=> Hf size_f s. apply/boolp.constructive_indefinite_description. move: s; apply: (well_founded_induction (@well_founded_size _)) => s IH. have {}IH : forall x, size x < size s -> { m | nondetSem m = unfoldM (@well_founded_size B) (@nilp _) f x}. move=> x xs; exact/boolp.constructive_indefinite_description/IH. case: s IH => [|h t] IH. rewrite unfoldME //=; by exists (ndRet [::]). rewrite unfoldME //. rewrite (_ : nilp _ = false) //. case: (Hf (h :: t)) => x Hx. rewrite -Hx. set g := fun y => match Bool.bool_dec (size y < size (h :: t)) true with | left H => let: exist x _ := IH _ H in x | _ => ndRet [::] end. refine (ex_intro _ (ndBind x (fun x => ndBind (g x.2) (@ndRet _ \o cons x.1 ))) _). rewrite [in LHS]/=. rewrite Hx size_f /bassert !bindA. bind_ext => -[x1 x2]. case: assertPn; rewrite ltnS => b1b2; last by rewrite !bindfailf. rewrite !bindretf /g/=. case: Bool.bool_dec => // x2t. by case: (IH x2) => // x0 <-; rewrite fmapE. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib