Sciweavers

Share
BIRTHDAY
2016
Springer

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

3 years 25 days ago
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.
Robbert Krebbers, Louis Parlant, Alexandra Silva
Added 30 Mar 2016
Updated 30 Mar 2016
Type Journal
Year 2016
Where BIRTHDAY
Authors Robbert Krebbers, Louis Parlant, Alexandra Silva
Comments (0)
books