proposition: Theorem fibo_ref_ok n : crun (cnew ml_int 1 >>= (fun a => cnew ml_int 1 >>= fun b => fibo_ref n a b >> cget a)) = Some (fibo_rec n).
proof: Proof. set x := 1. pose y := x. rewrite -{2}/y. pose i := n. rewrite -[in LHS]/i. have : (x, y) = (fibo_rec (n - i), fibo_rec (n.+1 - i)). by rewrite subnn -addn1 addKn. have : i <= n by []. elim: i x y => [|i IH] x y Hi. rewrite !subn0 => -[-> ->]. rewrite -/(fibo_rec n.+1). under eq_bind do under eq_bind do rewrite /= bindskipf. rewrite -cnewchk. under eq_bind do rewrite -cgetret cchknewget. by rewrite cnewget -bindA crunret // crunnew // crunnew0. rewrite subSS => -[] Hx Hy. rewrite -(IH y (x + y) (ltnW Hi)); last first. rewrite {}Hx {}Hy; congr pair. rewrite subSn 1?ltnW//. case: n {IH} => // n in Hi *. by rewrite [in RHS]subSn -1?ltnS// subSS subSn -1?ltnS. rewrite /=. under eq_bind do under eq_bind do rewrite !bindA. rewrite -cnewchk. under eq_bind do rewrite cchknewget. rewrite cnewget. under eq_bind do under eq_bind do rewrite !bindA. under eq_bind do rewrite cnewget. under eq_bind do under eq_bind do rewrite !bindA. rewrite -[in LHS]cnewchk. under eq_bind do rewrite cchknewput. rewrite cnewput. by under eq_bind do rewrite cnewput. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib