Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq

Moessner’s Theorem describes a construction of the sequence of powers (1n , 2n , 3n , . . . ), 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´e’s generalizations could also be proved using (almost) the same bisimulation.

• Type: Journal
• Year: 2016
• Where: BIRTHDAY
• Authors: Robbert Krebbers, Louis Parlant, Alexandra Silva
• Keywords: Applied Computing, BIRTHDAY 2016