Program calculation, a programming technique to derive efficient programs from naive ones by program transformation, is a challenging activity for program optimization. Tesson et al. have shown that Coq, a popular theorem proof assistant, provides a cheap way to implement a powerful system for verifying correctness of the transformations, but its applications are limited to the calculation of list functions in Theory of Lists. In this paper, we prove more advanced calculation rules in Coq for various recursion schemes, which capture the recursive programs on an arbitrary algebraic datatype. We construct Coq formal proof of all the lemmas and theorems about recursion schemes including histomorphism and futumorphism proposed by Uustalu and Vene. The feature of our proposal is that it is possible to obtain certified runnable programs from definitions written with recursion schemes in Coq scripts. We have succeeded in obtaining a certified runnable program to compute the n-th Fibonacci number from its histomorphic definition.