Abstract
Moessner’s Theorem describes a construction of the sequence of powers \((1^n, 2^n, 3^n, \ldots )\), by repeatedly dropping and summing elements from the sequence of positive natural numbers. The theorem was presented by Moessner in 1951 without a proof and later proved and generalized in several directions. More recently, a coinductive proof of the original theorem was given by Niqui and Rutten. We present a formalization of their proof in the Coq proof assistant. This formalization serves as a non-trivial illustration of the use of coinduction in Coq. During the formalization, we discovered that Long and Salié’s generalizations could also be proved using (almost) the same bisimulation.
The work in this paper was developed when all authors were at the Radboud University, The Netherlands.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
We use Leibniz equality for the heads because we only deal with streams of integers. In general, for example to consider streams of streams, this is still too restrictive.
References
Bertot, Y., Castéran, P.: Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. In: Texts in TCS. Springer, Heidelberg (2004)
Bickford, M., Kozen, D., Silva, A.: Formalizing Moessner’s theorem and generalizations in Nuprl (2013). http://www.nuprl.org/documents/Moessner/
Clausen, C., Danvy, O., Masuko, M.: A characterization of Moessner’s sieve. Theor. Computut. Sci. 546, 244–256 (2014)
Conway, J.H., Guy, R.K.: Moessner’s magic. In: The Book of Numbers, pp. 63–65. Springer, New York (1996)
Coq Development Team: The Coq proof assistant reference manual. INRIA (2013)
Giménez, C.E.: Un Calcul de Constructions Infinies et son Application à la vérification de systèmes communicants. Ph.D. thesis, L’École Normale Supérieure de Lyon (1996)
Hinze, R.: Scans and convolutions— a calculational proof of Moessner’s theorem. In: Scholz, S.-B., Chitil, O. (eds.) IFL 2008. LNCS, vol. 5836, pp. 1–24. Springer, Heidelberg (2011)
Honsberger, R.: More mathematical morsels. Dolciani Mathematical Expositions. Mathematical Association of America (1991)
Kozen, D., Silva, A.: On Moessner’s theorem. Am. Math. Monthly 120(2), 131–139 (2013)
Long, C.T.: On the Moessner theorem on integral powers. Am. Math. Monthly 73(8), 846–851 (1966)
Long, C.T.: Strike it out-add it up. The Math. Gaz. 66(438), 273–277 (1982)
Moessner, A.: Eine Bemerkung über die Potenzen der natürlichen Zahlen. Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematischnaturwissenschaftliche Klasse 1952, no. 29 (1951)
Niqui, M., Rutten, J.J.M.M.: A proof of Moessner’s theorem by coinduction. High.-Ord. Symb. Comput. 24(3), 191–206 (2011)
Paasche, I.: Ein neuer Beweis des moessnerischen Satzes. Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematischnaturwissenschaftliche Klasse 1952 1, 1–5 (1953)
Paasche, I.: Ein zahlentheoretische-logarithmischer Rechenstab. Math. Naturwiss. Unterr. 6, 26–28 (1953,1954)
Paasche, I.: Eine Verallgemeinerung des moessnerschen Satzes. Compositio Mathematica 12, 263–270 (1954)
Perron, O.: Beweis des Moessnerschen Satzes. Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse 1951 4, 31–34 (1951)
Rutten, J.: A coinductive calculus of streams. Math. Struct. Comput. Sci. 15, 93–147 (2005)
Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3–80 (2000)
Salié, H.: Bemerkung zu einem Satz von Moessner. Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse 1952 2, 7–11 (1952)
Sozeau, M.: A new look at generalized rewriting in type theory. J. Form. Reason. 2(1), 41–62 (2009)
Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008)
Urbak, P.: A formal study of Moessner’s sieve, M.Sc. thesis, Aarhus University (2015)
Acknowledgments
The authors thank Dexter Kozen, Jan Rutten, Olivier Danvy, and the anonymous referees for useful comments and discussions. The last author learned from Frank many years ago that a good steak, a glass of excellent wine, and fantastic company can make the hardest of days seem distant and irrelevant in the grand scheme of things! Frank, we wish you the very best for the years to come!
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Additional information
Dedicated to Frank de Boer on the occasion of his 60 $$^{th}$$ t h birthday.
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Krebbers, R., Parlant, L., Silva, A. (2016). Moessner’s Theorem: An Exercise in Coinductive Reasoning in Coq . In: Ábrahám, E., Bonsangue, M., Johnsen, E. (eds) Theory and Practice of Formal Methods. Lecture Notes in Computer Science(), vol 9660. Springer, Cham. https://doi.org/10.1007/978-3-319-30734-3_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-30734-3_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-30733-6
Online ISBN: 978-3-319-30734-3
eBook Packages: Computer ScienceComputer Science (R0)