proposition: Theorem fact_for63_ok : crun (fact_for63 (N2int n)) = Some (N2int (fact_rec n)).
proof: Proof. rewrite /fact_for63. under eq_bind do rewrite !bindA !bindretf. set fn := N2int (fact_rec n). transitivity (crun (cnew ml_int fn >> Ret fn : M _)); last by rewrite crunret // crunnew0. congr crun. have {1}-> : (1 = N2int 1)%int63 by []. rewrite -/(fact_rec 0). have -> : (1 = Uint63.succ (N2int 0))%int63 by []. 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 forloop630 (ltsb_succ,bindretf) // -cgetret. by rewrite cnewget. rewrite -N2int_succ subnSK //. case: m IH mn => [|m] IH mn. under eq_bind do rewrite subn0 forloop631 !(ltsb_subr,bindA) //. rewrite cnewget. under eq_bind do rewrite bindretf -cgetret. rewrite cnewput -N2int_mul mulnC -{1}(prednK mn) cnewget subn1. by rewrite -/(fact_rec n.-1.+1) prednK. under eq_bind do rewrite forloop63S !(ltsb_subr,bindA) //. rewrite cnewget. under eq_bind do rewrite bindretf. rewrite cnewput -IH (ltnW,subnS) // -N2int_mul mulnC -(@prednK (n-m.+1)) //. by rewrite lt0n subn_eq0 -ltnNge. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63