proposition: Theorem fact_for_ok n : crun (fact_for n) = Some (fact_rec n).
proof: Proof. rewrite /fact_for. under eq_bind do rewrite !bindA !bindretf. transitivity (crun (cnew ml_int (fact_rec n) >> Ret (fact_rec n) : M _)); last by rewrite crunret // crunnew0. congr crun. rewrite -{1}/(fact_rec 0). pose m := n. have -> : 0 = n - m by rewrite subnn. have : m <= n by []. elim: m => [|m IH] mn. rewrite subn0. under eq_bind do rewrite forloop0 ?leqnn // bindretf -cgetret. by rewrite cnewget. rewrite subnSK //. under eq_bind do (rewrite forloopS; last by apply leq_subr). under eq_bind do rewrite !bindA. rewrite cnewget. under eq_bind do rewrite bindretf. rewrite cnewput -IH; last by apply ltnW. by rewrite subnS mulnC -(@prednK (n-m)) // lt0n subn_eq0 -ltnNge. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib