{"id":3912,"date":"2013-12-11T06:22:07","date_gmt":"2013-12-11T05:22:07","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3912"},"modified":"2013-12-11T06:22:29","modified_gmt":"2013-12-11T05:22:29","slug":"moessners-theorem-an-exercise-in-coinductive-reasoning-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/moessners-theorem-an-exercise-in-coinductive-reasoning-in-coq\/","title":{"rendered":"Moessner\u2019s theorem: an exercise in coinductive reasoning in Coq"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\">Coq<\/a> sobre coinduci\u00f3n titulado <a href=\"http:\/\/robbertkrebbers.nl\/research\/articles\/moessner.pdf\">Moessner\u2019s theorem: an exercise in coinductive reasoning in Coq<\/a>.<\/p>\n<p>Sus autores son <\/p>\n<ul>\n<li><a href=\"http:\/\/robbertkrebbers.nl\">Robbert Krebbers<\/a> (de la Univ. de Nimeja, Paises Bajos),\n<li><a href=\"mailto:louis.parlant@ens-lyon.fr\">Louis Parlant<\/a> (de la Escuela Normal Superior de Lyon, Francia) y\n<li><a href=\"http:\/\/www.cs.ru.nl\/staff\/Alexandra.Silva\">Alexandra Silva<\/a> (de la Univ. de Nimeja, Paises Bajos)\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\nMoessner\u2019s Theorem describes a construction of the sequence of powers (1\u207f, 2\u207f, 3\u207f,&#8230;), 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. In the process of formalizing the original proof we discovered that Long and Sali\u00e9\u2019s generalization of Moessner\u2019s Theorem could also be proved using (almost) the same bisimulation.\n<\/p><\/blockquote>\n<p>El trabajo se present\u00f3 en el <a href=\"http:\/\/homepages.cwi.nl\/~winter\/coin.html\">seminario del COIN<\/a> (<i>Coalgebra in the Netherlands<\/i>) <a href=\"http:\/\/homepages.cwi.nl\/~winter\/coin.html#Kr\"><\/a>. Las transparencias de la presentaci\u00f3n se encuentran <a href=\"http:\/\/homepages.cwi.nl\/~winter\/coin\/20131112-Kr.pdf\">aqu\u00ed<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"https:\/\/github.com\/robbertkrebbers\/moessner\">aqu\u00ed<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre coinduci\u00f3n titulado Moessner\u2019s theorem: an exercise in coinductive reasoning in Coq. Sus autores son Robbert Krebbers (de la Univ. de Nimeja, Paises Bajos), Louis Parlant (de la Escuela Normal Superior de Lyon, Francia) y Alexandra Silva (de la Univ. de Nimeja, Paises Bajos) Su&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[45,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3912"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=3912"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3912\/revisions"}],"predecessor-version":[{"id":3914,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3912\/revisions\/3914"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3912"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3912"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3912"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}