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

8 years 21 days ago

Download robbertkrebbers.nl

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.

Robbert Krebbers, Louis Parlant, Alexandra Silva

Real-time Traffic